01whole.pdf (1.15 MB)
Download file

Algebraic verification of probabilistic and concurrent systems

Download (1.15 MB)
thesis
posted on 28.03.2022, 09:16 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.

History

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.

Notes

Theoretical thesis. Bibliography: pages 167-175

Awarding Institution

Macquarie University

Degree Type

Thesis PhD

Degree

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

Department, Centre or School

Department of Computing

Year of Award

2014

Principal Supervisor

Annabelle McIver

Additional Supervisor 1

Georg Struth

Rights

Copyright Mananjanahary Tahiry Rabehaja 2014 Copyright disclaimer: http://www.copyright.mq.edu.au

Language

English

Extent

1 online resource (ii, 175 pages)

Former Identifiers

mq:42926 http://hdl.handle.net/1959.14/1057067