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. © 2012 Elsevier Inc. All rights reserved.
Deng, Y., & Hennessy, M. (2013). On the semantics of Markov automata. In Information and Computation (Vol. 222, pp. 139–168). https://doi.org/10.1016/j.ic.2012.10.010