Abstract

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 languageUndefined
Pages364-379
Number of pages16
DOIs
StatePublished - Sep 2012
Event23rd International Conference on Concurrency Theory, CONCUR 2012 - Newcastle upon Tyne, United Kingdom

Conference

Conference23rd International Conference on Concurrency Theory, CONCUR 2012
Abbreviated titleCONCUR
CountryUnited Kingdom
CityNewcastle upon Tyne
Period4/09/127/09/12

Fingerprint

Specifications
Syntactics
Linearization
Chemical analysis

Keywords

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

Cite this

Koutny, M. (Ed.), Timmer, M., Ulidowski, I. (Ed.), Katoen, J. P., van de Pol, J. C., & Stoelinga, M. I. A. (2012). Efficient Modelling and Generation of Markov Automata. 364-379. Paper presented at 23rd International Conference on Concurrency Theory, CONCUR 2012, Newcastle upon Tyne, United Kingdom.DOI: 10.1007/978-3-642-32940-1_26

Koutny, M. (Editor); Timmer, Mark; Ulidowski, I. (Editor); Katoen, Joost P.; van de Pol, Jan Cornelis; Stoelinga, Mariëlle Ida Antoinette / Efficient Modelling and Generation of Markov Automata.

2012. 364-379 Paper presented at 23rd International Conference on Concurrency Theory, CONCUR 2012, Newcastle upon Tyne, United Kingdom.

Research output: Scientific - peer-reviewPaper

@misc{735d6d1ff2764ec9b4328ea82b13ba21,
title = "Efficient Modelling and Generation of Markov Automata",
abstract = "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.",
keywords = "Efficient state space generation, EWI-22202, Symbolic transformations, Process Algebra, IR-81400, Markov Automata",
author = "M. Koutny and Mark Timmer and I. Ulidowski and Katoen, {Joost P.} and {van de Pol}, {Jan Cornelis} and Stoelinga, {Mariëlle Ida Antoinette}",
year = "2012",
month = "9",
doi = "10.1007/978-3-642-32940-1_26",
pages = "364--379",

}

Koutny, M (ed.), Timmer, M, Ulidowski, I (ed.), Katoen, JP, van de Pol, JC & Stoelinga, MIA 2012, 'Efficient Modelling and Generation of Markov Automata' Paper presented at 23rd International Conference on Concurrency Theory, CONCUR 2012, Newcastle upon Tyne, United Kingdom, 4/09/12 - 7/09/12, pp. 364-379. DOI: 10.1007/978-3-642-32940-1_26

Efficient Modelling and Generation of Markov Automata. / Koutny, M. (Editor); Timmer, Mark; Ulidowski, I. (Editor); Katoen, Joost P.; van de Pol, Jan Cornelis; Stoelinga, Mariëlle Ida Antoinette.

2012. 364-379 Paper presented at 23rd International Conference on Concurrency Theory, CONCUR 2012, Newcastle upon Tyne, United Kingdom.

Research output: Scientific - peer-reviewPaper

TY - CONF

T1 - Efficient Modelling and Generation of Markov Automata

AU - Timmer,Mark

AU - Katoen,Joost P.

AU - van de Pol,Jan Cornelis

AU - Stoelinga,Mariëlle Ida Antoinette

A2 - Koutny,M.

A2 - Ulidowski,I.

PY - 2012/9

Y1 - 2012/9

N2 - 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.

AB - 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.

KW - Efficient state space generation

KW - EWI-22202

KW - Symbolic transformations

KW - Process Algebra

KW - IR-81400

KW - Markov Automata

U2 - 10.1007/978-3-642-32940-1_26

DO - 10.1007/978-3-642-32940-1_26

M3 - Paper

SP - 364

EP - 379

ER -

Koutny M, (ed.), Timmer M, Ulidowski I, (ed.), Katoen JP, van de Pol JC, Stoelinga MIA. Efficient Modelling and Generation of Markov Automata. 2012. Paper presented at 23rd International Conference on Concurrency Theory, CONCUR 2012, Newcastle upon Tyne, United Kingdom. Available from, DOI: 10.1007/978-3-642-32940-1_26