Macquarie University
01whole.pdf (1.15 MB)

Algebraic verification of probabilistic and concurrent systems

Download (1.15 MB)
posted on 2022-03-28, 09:16 authored by Mananjanahary Tahiry Rabehaja
This thesis provides an algebraic modelling and verification of probabilistic concurrent systems in the style of Kleene algebra. Without concurrency, it is shown that the equational theory of continuous probabilistic Kleene algebra is completewith respect to an automata model under standard simulation equivalence. This yields a minimisation-based decision procedure for the algebra. Without probability, an event structure model of Hoare et al.'s concurrent Kleene algebra is constructed. These two algebras are then \merged" to provide probabilistic concurrent Kleene algebra which is used to discover and prove development rules for probabilistic concurrent systems (e.g. rely/guarantee calculus). Soundness of thenew algebra is ensured by models based on probabilistic automata (interleaving) and probabilistic bundle event structures (true concurrency) quotiented with the respective simulation equivalences. Lastly, event structures with implicit probabilitiesare constructed to provide a state based model for the soundness of the probabilistic rely/guarantee rules.


Table of Contents

1. Introduction -- 2. Continuity in probabilistic Kleene algebra -- 3. Event structures and concurrent Kleene algebra -- 4. Probabilistic concurrent Kleene algebra -- 5. True concurrency in probabilistic concurrent Kleene algebra -- 6. Bundle event structure with implicit probability -- 7. Probabilistic rely/guarantee calculus -- 8. Conclusion.


Theoretical thesis. Bibliography: pages 167-175

Awarding Institution

Macquarie University

Degree Type

Thesis PhD


PhD, Macquarie University, Faculty of Science and Engineering, Department of Computing

Department, Centre or School

Department of Computing

Year of Award


Principal Supervisor

Annabelle McIver

Additional Supervisor 1

Georg Struth


Copyright Mananjanahary Tahiry Rabehaja 2014 Copyright disclaimer:




1 online resource (ii, 175 pages)

Former Identifiers