On the Semantics of Markov Automata  

                       Yuxin Deng and Matthew Hennessy

  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.