Abstract
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 language | English |
---|---|
Title of host publication | SEEFM 200: First south-east europian workshop on formal methods |
Editors | Y. Manolopoulos, P. Spirakis |
Place of Publication | Thessaloniki, Greece |
Publisher | Aristotle University of Thessaloniki |
Pages | 84-99 |
Number of pages | 16 |
Publication status | Published - 20 Nov 2003 |
Event | 1st South-East Europian Workshop on Formal Methods, SEEFM 2003 - Thessaloniki, Greece Duration: 20 Nov 2003 → 20 Nov 2003 Conference number: 1 |
Conference
Conference | 1st South-East Europian Workshop on Formal Methods, SEEFM 2003 |
---|---|
Country/Territory | Greece |
City | Thessaloniki |
Period | 20/11/03 → 20/11/03 |