Confluence Reduction for Markov Automata

Mark Timmer; Jaco van de Pol; Mariëlle I.A. Stoelinga

doi:10.1007/978-3-642-40229-6_17

Confluence Reduction for Markov Automata

Mark Timmer, Jaco van de Pol, Mariëlle I.A. Stoelinga

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

21 Citations (Scopus)

113 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 language	English
Title of host publication	Proceedings of the 11th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS)
Editors	Victor Braberman, Laurent Fribourg
Place of Publication	Berlin
Publisher	Springer
Pages	243-257
Number of pages	15
ISBN (Electronic)	978-3-642-40229-6
ISBN (Print)	978-3-642-40228-9
DOIs	https://doi.org/10.1007/978-3-642-40229-6_17
Publication status	Published - Aug 2013
Event	11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013 - Universidad de Buenos Aires, Buenos Aires, Argentina Duration: 29 Aug 2013 → 31 Aug 2013 Conference number: 11

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	8053
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013
Abbreviated title	FORMATS
Country/Territory	Argentina
City	Buenos Aires
Period	29/08/13 → 31/08/13

Keywords

Confluence
Process algebra
Markov automata
State space reduction
Divergence-sensitive branching bisimulation
EC Grant Agreement nr.: FP7/318490
EC Grant Agreement nr.: FP7/2007-2013
EC Grant Agreement nr.: FP7/318003
2024 OA procedure

Access to Document

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

ArticleFinal published version, 280 KBLicence: Taverne

21 Citations
1 Report
1 Conference contribution
1 Article

Confluence reduction for Markov automata
Timmer, M., Katoen, J.-P., van de Pol, J. & Stoelinga, M., 6 Dec 2016, In: Theoretical computer science. 655, B, p. 193-219 27 p.
Research output: Contribution to journal › Article › Academic › peer-review

Open Access
File
8 Citations (Scopus)

207 Downloads (Pure)
Confluence reduction for Markov automata
Timmer, M., van de Pol, J. & Stoelinga, M., Mar 2013, Proceedings of the 11th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2013). Trieste: University of Trieste, p. 18 4 p.
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic

Open Access
File
Confluence reduction for Markov automata (extended version)
Timmer, M., van de Pol, J. & Stoelinga, M. I. A., Jun 2013, Enschede: Centre for Telematics and Information Technology (CTIT). 26 p. (CTIT Technical Report Series; no. TR-CTIT-13-14)
Research output: Book/Report › Report › Professional

Open Access
File

Cite this

@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, Process algebra, Markov automata, State space reduction, Divergence-sensitive branching bisimulation, EC Grant Agreement nr.: FP7/318490, EC Grant Agreement nr.: FP7/2007-2013, EC Grant Agreement nr.: FP7/318003, 2024 OA procedure",

author = "Mark Timmer and {van de Pol}, Jaco and Stoelinga, {Mari{\"e}lle I.A.}",

note = "Foreground = 15%;Type of activity = conference;Main leader = UT;Type of audience = scientific community;Size of audience = 40;Countries addressed = international;; 11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013, FORMATS ; Conference date: 29-08-2013 Through 31-08-2013",

year = "2013",

month = aug,

doi = "10.1007/978-3-642-40229-6_17",

language = "English",

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)",

address = "Germany",

}

Timmer, M , van de Pol, J & 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, Jaco ; Stoelinga, Mariëlle I.A.
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 proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Confluence Reduction for Markov Automata

AU - Timmer, Mark

AU - van de Pol, Jaco

AU - Stoelinga, Mariëlle I.A.

N1 - Conference code: 11

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 - Process algebra

KW - Markov automata

KW - State space reduction

KW - Divergence-sensitive branching bisimulation

KW - EC Grant Agreement nr.: FP7/318490

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

KW - EC Grant Agreement nr.: FP7/318003

KW - 2024 OA procedure

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

T2 - 11th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2013

Y2 - 29 August 2013 through 31 August 2013

ER -

Confluence Reduction for Markov Automata

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Research output

Confluence reduction for Markov automata

Confluence reduction for Markov automata

Confluence reduction for Markov automata (extended version)

Cite this