Efficient Modelling and Generation of Markov Automata

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

135 Downloads (Pure)


This paper introduces a framework for the efficient modelling and generation of Markov automata. It consists of (1) the data-rich process-algebraic language MAPA, allowing concise modelling of systems with nondeterminism, probability and Markovian timing; (2) a restricted form of the language, the MLPPE, enabling easy state space generation and parallel composition; and (3) several syntactic reduction techniques on the MLPPE format, for generating equivalent but smaller models. Technically, the framework relies on an encoding of MAPA into the existing prCRL language for probabilistic automata. First, we identify a class of transformations on prCRL that can be lifted to the Markovian realm using our encoding. Then, we employ this result to reuse prCRL's linearisation procedure to transform any MAPA specification to an equivalent MLPPE, and to lift three prCRL reduction techniques to MAPA. Additionally, we define two novel reduction techniques for MLPPEs. All our techniques treat data as well as Markovian and interactive behaviour in a fully symbolic manner, working on specifications instead of models and thus reducing state spaces prior to their construction. The framework has been implemented in our tool SCOOP, and a case study on polling systems and mutual exclusion protocols shows its practical applicability.
Original languageEnglish
Title of host publicationCONCUR 2012 - Concurrency Theory
Subtitle of host publication23rd International Conference
EditorsMaciej Koutny, Irek Ulidowski
Place of PublicationBerlin, Heidelberg
Number of pages16
ISBN (Electronic)978-3-642-32940-1
ISBN (Print)978-3-642-32939-5
Publication statusPublished - Sept 2012
Event23rd International Conference on Concurrency Theory, CONCUR 2012 - Newcastle upon Tyne, United Kingdom
Duration: 4 Sept 20127 Sept 2012
Conference number: 23

Publication series

NameLectures Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference23rd International Conference on Concurrency Theory, CONCUR 2012
Abbreviated titleCONCUR
Country/TerritoryUnited Kingdom
CityNewcastle upon Tyne


  • Efficient state space generation
  • EWI-22202
  • Symbolic transformations
  • Process Algebra
  • IR-81400
  • Markov Automata


Dive into the research topics of 'Efficient Modelling and Generation of Markov Automata'. Together they form a unique fingerprint.

Cite this