On the semantics of Markov automata (Q1951578)

Markov automata (MA) are labeled transition systems with two types of transitions: action transitions yield a probability distribution over states while timed transitions are parameterised by a rate of a negative exponential distribution determining the random delay. MA thus extend Segala's probabilistic automata with exponential delays. This paper presents a novel notion of weak bisimulation and shows that this notion is compositional (e.g., for parallel composition), preserves simple testing experiments (so-called barbs), and is reduction-closed. The paper introduces an extension of the process algebra CCS to describe Markov automata.