Confluence reduction for Markov automata

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

32 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 Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013)
Place of PublicationTrieste
PublisherUniversity of Trieste
Pages18
Number of pages4
ISBN (Print)not assigned
Publication statusPublished - Mar 2013
Event11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013 - Rome, Italy
Duration: 23 Mar 201324 Mar 2013
Conference number: 11
http://eptcs.web.cse.unsw.edu.au/content.cgi?QAPL2013

Publication series

Name
PublisherUniversity of Trieste

Workshop

Workshop11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013
Abbreviated titleQAPL 2013
CountryItaly
CityRome
Period23/03/1324/03/13
Internet address

Keywords

  • EWI-23224
  • EC Grant Agreement nr.: FP7/318003
  • METIS-296379
  • EC Grant Agreement nr.: FP7/2007-2013
  • IR-85419
  • EC Grant Agreement nr.: FP7/318490

Cite this

Timmer, M., van de Pol, J. C., & Stoelinga, M. I. A. (2013). Confluence reduction for Markov automata. In Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013) (pp. 18). Trieste: University of Trieste.
Timmer, Mark ; van de Pol, Jan Cornelis ; Stoelinga, Mariëlle Ida Antoinette. / Confluence reduction for Markov automata. Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013). Trieste : University of Trieste, 2013. pp. 18
@inproceedings{fdcaa19a65d84e39820bc3accb583035,
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 = "EWI-23224, EC Grant Agreement nr.: FP7/318003, METIS-296379, EC Grant Agreement nr.: FP7/2007-2013, IR-85419, EC Grant Agreement nr.: FP7/318490",
author = "Mark Timmer and {van de Pol}, {Jan Cornelis} and Stoelinga, {Mari{\"e}lle Ida Antoinette}",
note = "eemcs-eprint-23224",
year = "2013",
month = "3",
language = "Undefined",
isbn = "not assigned",
publisher = "University of Trieste",
pages = "18",
booktitle = "Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013)",

}

Timmer, M, van de Pol, JC & Stoelinga, MIA 2013, Confluence reduction for Markov automata. in Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013). University of Trieste, Trieste, pp. 18, 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, QAPL 2013, Rome, Italy, 23/03/13.

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

Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013). Trieste : University of Trieste, 2013. p. 18.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

TY - GEN

T1 - Confluence reduction for Markov automata

AU - Timmer, Mark

AU - van de Pol, Jan Cornelis

AU - Stoelinga, Mariëlle Ida Antoinette

N1 - eemcs-eprint-23224

PY - 2013/3

Y1 - 2013/3

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 - EWI-23224

KW - EC Grant Agreement nr.: FP7/318003

KW - METIS-296379

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

KW - IR-85419

KW - EC Grant Agreement nr.: FP7/318490

M3 - Conference contribution

SN - not assigned

SP - 18

BT - Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013)

PB - University of Trieste

CY - Trieste

ER -

Timmer M, van de Pol JC, Stoelinga MIA. Confluence reduction for Markov automata. In Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013). Trieste: University of Trieste. 2013. p. 18