White Rose University Consortium logo
University of Leeds logo University of Sheffield logo York University logo

Algebraic Verification of Probabilistic and Concurrent Systems

Rabehaja, Mananjanahary Tahiry (2014) Algebraic Verification of Probabilistic and Concurrent Systems. PhD thesis, University of Sheffield.

Available under License Creative Commons Attribution-Noncommercial-No Derivative Works 2.0 UK: England & Wales.

Download (1175Kb) | Preview


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 complete with 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 the new 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 probabilities are constructed to provide a state based model for the soundness of the probabilistic rely/guarantee rules.

Item Type: Thesis (PhD)
Academic Units: The University of Sheffield > Faculty of Engineering (Sheffield) > Computer Science (Sheffield)
The University of Sheffield > Faculty of Science (Sheffield) > Computer Science (Sheffield)
Identification Number/EthosID: uk.bl.ethos.631452
Depositing User: Mr. Mananjanahary Tahiry Rabehaja
Date Deposited: 11 Dec 2014 16:00
Last Modified: 03 Oct 2016 11:18
URI: http://etheses.whiterose.ac.uk/id/eprint/7456

You do not need to contact us to get a copy of this thesis. Please use the 'Download' link(s) above to get a copy.
You can contact us about this thesis. If you need to make a general enquiry, please see the Contact us page.

Actions (repository staff only: login required)