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.
|Title of host publication||Proceedings 1st South-East European Workshop on Formal Methods (SEEFM 2003, Thessaloniki, Greece, November 20, 2003), included in Proceedings 1st Balkan Conference in Informatics|
|Publication status||Published - 2003|