Verification of random behaviours

S. Andova, T.A.C. Willemse

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

56 Downloads (Pure)


We introduce abstraction in a probabilistic process algebra. The process algebra can be employed for specifying processes that exhibit both probabilistic and non-deterministic choices in their behaviours. Several rules and axioms are identified, allowing us to rewrite processes to less complex processes by removing redundant internal activity. Using these rules, we have successfully conducted a verification of the Concurrent Alternating Bit Protocol. The verification shows that after abstraction of internal activity, the protocol behaves as a buffer.
Original languageEnglish
Title of host publicationProceedings 1st South-East European Workshop on Formal Methods (SEEFM 2003, Thessaloniki, Greece, November 20, 2003), included in Proceedings 1st Balkan Conference in Informatics
Publication statusPublished - 2003


Dive into the research topics of 'Verification of random behaviours'. Together they form a unique fingerprint.

Cite this