Mar 20, 2012: Mark Timmer: Efficient Modelling and Generation of Markov Automata

March 20, 2012Efficient Modelling and Generation of Markov Automata
Room: Zi 5126Mark Timmer

In this talk we present 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. In this way, reductions are obtained on the specification level instead of the model level, reducing state spaces prior to their construction. We introduce several such techniques, which treat data as well as Markovian and interactive behaviour in a fully symbolic manner. We show how many of the techniques that were already available for models of probabilistic automata can directly be applied to models of Markov automata, by means of a novel notion of bisimulation.