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. © 2011 Springer-Verlag.
CITATION STYLE
Deng, Y., & Hennessy, M. (2011). On the semantics of Markov automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6756 LNCS, pp. 307–318). https://doi.org/10.1007/978-3-642-22012-8_24
Mendeley helps you to discover research relevant for your work.