Bisimulation and cocongruence for probabilistic systems

We introduce a new notion of bisimulation, called event bisimulation on labelled Markov processes (LMPs) and compare it with the, now standard, notion of probabilistic bisimulation, originally due to Larsen and Skou. Event bisimulation uses a sub -algebra as the basic carrier of information rather than an equivalence relation. The resulting notion is thus based on measurable subsets rather than on points: hence the name. Event bisimulation applies smoothly for general measure spaces; bisimulation, on the other hand, is known only to work satisfactorily for analytic spaces. We prove the logical characterization theorem for event bisimulation without having to invoke any of the subtle aspects of analytic spaces that feature prominently in the corresponding proof for ordinary bisimulation. These complexities only arise when we show that on analytic spaces the two concepts co-incide. We show that the concept of event bisimulation arises naturally from taking the co-congruence point of vie...

• Type: Journal
• Year: 2006
• Where: IANDC
• Authors: Vincent Danos, Josee Desharnais, François Laviolette, Prakash Panangaden
• Keywords: Bisimulation, Event Bisimulation, IANDC 2006, Probabilistic Bisimulation