Towards automated proof support for probabilistic distributed systems

Annabelle K. McIver*, Tjark Weber

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

17 Citations (Scopus)


The mechanisation of proofs for probabilistic systems is particularly challenging due to the verification of real-valued properties that probability entails: experience indicates [12, 4, 11] that there are many difficulties in automating real-number arithmetic in the context of other program features. In this paper we propose a framework for verification of probabilistic distributed systems based on the generalisation of Kleene algebra with tests that has been used as a basis for development of concurrency control in standard programming [7]. We show that verification of real-valued properties in these systems can be considerably simplified, and moreover that there is an interpretation which is susceptible to counterexample search via state exploration, despite the underlying real-number domain.

Original languageEnglish
Pages (from-to)534-548
Number of pages15
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3835 LNAI
Publication statusPublished - 2005


Dive into the research topics of 'Towards automated proof support for probabilistic distributed systems'. Together they form a unique fingerprint.

Cite this