On the Semantics of Markov Automata

Markov automata describe systems in terms of events which may be nondeterministic, may occur probabilistically, or may be subject to time delays. We define a novel notion of weak bisimulation for such systems and prove that this provides both a sound and complete proof methodology for a natural extensional behavioural equivalence between such systems, a generalisation of reduction barbed congruence, the well-known touchstone equivalence for a large variety of process description languages.

• Type: Journal
• Year: 2011
• Where: ICALP
• Authors: Yuxin Deng, Matthew Hennessy
• Keywords: Description Languages, ICALP 2011, Process Description, Programming Languages, Time Delays