Efficient Modelling and Generation of Markov Automata

This presentation introduces a process-algebraic framework with data for modelling and generating Markov automata. We show how an existing linearisation procedure for process-algebraic representations of probabilistic automata can be reused to transform systems in our new framework to a special format. This format enables easy state space generation and facilitates the definition of syntactic reduction techniques. We introduce several such techniques, which treat data as well as Markovian and interactive behaviour in a fully symbolic manner. In this way, reductions are obtained on the specification level instead of the model level, reducing state spaces prior to their construction.