Confluence Reduction for Markov Automata

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

21 Citations (Scopus)
34 Downloads (Pure)

Abstract

Markov automata are a novel formalism for specifying systems exhibiting nondeterminism, probabilistic choices and Markovian rates. Recently, the process algebra MAPA was introduced to efficiently model such systems. As always, the state space explosion threatens the analysability of the models generated by such specifications. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep these models small. We define the notion of confluence directly on Markov automata, and discuss how to syntactically detect confluence on the MAPA language as well. That way, Markov automata generated by MAPA specifications can be reduced on-the-fly while preserving divergence-sensitive branching bisimulation. Three case studies demonstrate the significance of our approach, with reductions in analysis time up to an order of magnitude.
Original languageUndefined
Title of host publicationProceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)
EditorsVictor Braberman, Laurent Fribourg
Place of PublicationBerlin
PublisherSpringer
Pages243-257
Number of pages15
ISBN (Print)978-3-642-40228-9
DOIs
Publication statusPublished - Aug 2013
Event11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013 - Universidad de Buenos Aires, Buenos Aires, Argentina
Duration: 29 Aug 201331 Aug 2013
Conference number: 11

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume8053
ISSN (Print)0302-9743

Conference

Conference11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013
Abbreviated titleFORMATS
CountryArgentina
CityBuenos Aires
Period29/08/1331/08/13

Keywords

  • Confluence
  • METIS-318706
  • EC Grant Agreement nr.: FP7/318003
  • Markov Automata
  • State space reduction
  • EWI-23541
  • Divergence-sensitive branching bisimulation
  • EC Grant Agreement nr.: FP7/318490
  • EC Grant Agreement nr.: FP7/2007-2013
  • IR-87074
  • Process Algebra

Cite this

Timmer, M., van de Pol, J. C., & Stoelinga, M. I. A. (2013). Confluence Reduction for Markov Automata. In V. Braberman, & L. Fribourg (Eds.), Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS) (pp. 243-257). (Lecture Notes in Computer Science; Vol. 8053). Berlin: Springer. https://doi.org/10.1007/978-3-642-40229-6_17
Timmer, Mark ; van de Pol, Jan Cornelis ; Stoelinga, Mariëlle Ida Antoinette. / Confluence Reduction for Markov Automata. Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). editor / Victor Braberman ; Laurent Fribourg. Berlin : Springer, 2013. pp. 243-257 (Lecture Notes in Computer Science).
@inproceedings{bd2b98b6794a4611b8d9776a6fda7b22,
title = "Confluence Reduction for Markov Automata",
abstract = "Markov automata are a novel formalism for specifying systems exhibiting nondeterminism, probabilistic choices and Markovian rates. Recently, the process algebra MAPA was introduced to efficiently model such systems. As always, the state space explosion threatens the analysability of the models generated by such specifications. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep these models small. We define the notion of confluence directly on Markov automata, and discuss how to syntactically detect confluence on the MAPA language as well. That way, Markov automata generated by MAPA specifications can be reduced on-the-fly while preserving divergence-sensitive branching bisimulation. Three case studies demonstrate the significance of our approach, with reductions in analysis time up to an order of magnitude.",
keywords = "Confluence, METIS-318706, EC Grant Agreement nr.: FP7/318003, Markov Automata, State space reduction, EWI-23541, Divergence-sensitive branching bisimulation, EC Grant Agreement nr.: FP7/318490, EC Grant Agreement nr.: FP7/2007-2013, IR-87074, Process Algebra",
author = "Mark Timmer and {van de Pol}, {Jan Cornelis} and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
note = "Foreground = 15{\%};Type of activity = conference;Main leader = UT;Type of audience = scientific community;Size of audience = 40;Countries addressed = international;",
year = "2013",
month = "8",
doi = "10.1007/978-3-642-40229-6_17",
language = "Undefined",
isbn = "978-3-642-40228-9",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "243--257",
editor = "Victor Braberman and Laurent Fribourg",
booktitle = "Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)",

}

Timmer, M, van de Pol, JC & Stoelinga, MIA 2013, Confluence Reduction for Markov Automata. in V Braberman & L Fribourg (eds), Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). Lecture Notes in Computer Science, vol. 8053, Springer, Berlin, pp. 243-257, 11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013, Buenos Aires, Argentina, 29/08/13. https://doi.org/10.1007/978-3-642-40229-6_17

Confluence Reduction for Markov Automata. / Timmer, Mark; van de Pol, Jan Cornelis; Stoelinga, Mariëlle Ida Antoinette.

Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). ed. / Victor Braberman; Laurent Fribourg. Berlin : Springer, 2013. p. 243-257 (Lecture Notes in Computer Science; Vol. 8053).

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

TY - GEN

T1 - Confluence Reduction for Markov Automata

AU - Timmer, Mark

AU - van de Pol, Jan Cornelis

AU - Stoelinga, Mariëlle Ida Antoinette

N1 - Foreground = 15%;Type of activity = conference;Main leader = UT;Type of audience = scientific community;Size of audience = 40;Countries addressed = international;

PY - 2013/8

Y1 - 2013/8

N2 - Markov automata are a novel formalism for specifying systems exhibiting nondeterminism, probabilistic choices and Markovian rates. Recently, the process algebra MAPA was introduced to efficiently model such systems. As always, the state space explosion threatens the analysability of the models generated by such specifications. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep these models small. We define the notion of confluence directly on Markov automata, and discuss how to syntactically detect confluence on the MAPA language as well. That way, Markov automata generated by MAPA specifications can be reduced on-the-fly while preserving divergence-sensitive branching bisimulation. Three case studies demonstrate the significance of our approach, with reductions in analysis time up to an order of magnitude.

AB - Markov automata are a novel formalism for specifying systems exhibiting nondeterminism, probabilistic choices and Markovian rates. Recently, the process algebra MAPA was introduced to efficiently model such systems. As always, the state space explosion threatens the analysability of the models generated by such specifications. We therefore introduce confluence reduction for Markov automata, a powerful reduction technique to keep these models small. We define the notion of confluence directly on Markov automata, and discuss how to syntactically detect confluence on the MAPA language as well. That way, Markov automata generated by MAPA specifications can be reduced on-the-fly while preserving divergence-sensitive branching bisimulation. Three case studies demonstrate the significance of our approach, with reductions in analysis time up to an order of magnitude.

KW - Confluence

KW - METIS-318706

KW - EC Grant Agreement nr.: FP7/318003

KW - Markov Automata

KW - State space reduction

KW - EWI-23541

KW - Divergence-sensitive branching bisimulation

KW - EC Grant Agreement nr.: FP7/318490

KW - EC Grant Agreement nr.: FP7/2007-2013

KW - IR-87074

KW - Process Algebra

U2 - 10.1007/978-3-642-40229-6_17

DO - 10.1007/978-3-642-40229-6_17

M3 - Conference contribution

SN - 978-3-642-40228-9

T3 - Lecture Notes in Computer Science

SP - 243

EP - 257

BT - Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)

A2 - Braberman, Victor

A2 - Fribourg, Laurent

PB - Springer

CY - Berlin

ER -

Timmer M, van de Pol JC, Stoelinga MIA. Confluence Reduction for Markov Automata. In Braberman V, Fribourg L, editors, Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). Berlin: Springer. 2013. p. 243-257. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-40229-6_17