Annabelle McIver and Tjark Weber. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, volume 3835 of Lecture Notes in Computer Science, pages 534-548. Springer, December 2005.
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.
@inproceedings{mciver05towards,
author = {Annabelle McIver and Tjark Weber},
title = {Towards Automated Proof Support for Probabilistic Distributed Systems},
editor = {Geoff Sutcliffe and Andrei Voronkov},
booktitle = {Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings},
volume = {3835},
series = {Lecture Notes in Computer Science},
pages = {534--548},
publisher = {Springer},
month = dec,
year = {2005},
isbn = {3-540-30553-X},
url = {http://dx.doi.org/10.1007/11591191_37}
}