Date and Time: Thursday, 22 January 2009, 15:30 - 16:30

Location: HG 6.96

Speaker: Sonja Georgievska (FM)

Title: On compositionality, efficiency and applicability of abstraction in probabilistic systems

Abstract:

A branching bisimulation for probabilistic systems that is preserved under parallel composition has been defined recently for the alternating model of Hansson. In this paper we show that, besides being compositional, it possesses other desirable properties. We present a polynomial algorithm which decides whether two systems are equivalent. We show that the branching bisimulation preserves the properties expressible in the probabilistic Computation Tree Logic (pCTL). The ground-complete axiomatization shows that the equivalence can be characterized with a single axiom in addition to the set of axioms for the strong bisimulation. Finally, we investigate the verification power of the new process algebra enriched with a set of sound recursive verification rules, by verifying the Concurrent Alternating Bit protocol with lossy channels.

(joint work with Suzana Andova)