A complete axiomatisation of branching bisimulation for probabilistic systems, with an application in protocol verification

S. Andova, J.C.M. Baeten, T.A.C. Willemse

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

6 Citations (Scopus)
1 Downloads (Pure)

Abstract

We consider abstraction in probabilistic process algebra. The process algebra can be employed for specifying processes that exhibit both probabilistic and non-deterministic choices in their behaviour. We give a set of axioms that completely axiomatises the branching bisimulation for the strictly alternating probabilistic graph model. In addition, several recursive verification rules are identified, allowing us to remove redundant internal activity. Using the axioms and the verification rules, we have successfully conducted a verification of the Concurrent Alternating Bit Protocol. This is a simple communication protocol, slightly more ‘sophisticated’ than the well-known Alternating Bit Protocol. As channels are lossy, sending continuous streams of data through the channels is a method to overcome this possible loss of data. This instigates a considerable level of parallelism (parallel activities) and as such requires more complex techniques for proving the protocol correct. Using our process algebra we show that after abstraction of internal activity, the protocol behaves as a buffer.
Original languageEnglish
Title of host publicationCONCUR 2006 - Concurrency Theory (Proceedings 17th International Conference, Bonn, Germany, August 27-30, 2006)
EditorsC. Baier, H. Hermanns
Place of PublicationBerlin
PublisherSpringer
Pages327-342
ISBN (Print)3-540-27276-4
DOIs
Publication statusPublished - 2006

Publication series

NameLecture Notes in Computer Science
Volume4137
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'A complete axiomatisation of branching bisimulation for probabilistic systems, with an application in protocol verification'. Together they form a unique fingerprint.

Cite this