Confluence Reduction for Probabilistic Systems (extended version)

Mark Timmer; Mariëlle Ida Antoinette Stoelinga; Jan Cornelis van de Pol

Confluence Reduction for Probabilistic Systems (extended version)

Mark Timmer, Mariëlle Ida Antoinette Stoelinga, Jan Cornelis van de Pol

Research output: Working paper

44 Downloads (Pure)

Abstract

This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic process algebra with data, facilitated by an earlier defined linear format. A case study demonstrates that significant reductions can be obtained.

Original language	Undefined
Place of Publication	Ithaca, NY, USA
Publisher	ArXiv.org
Number of pages	28
Publication status	Published - 10 Nov 2010

Publication series

Name
Publisher	arXiv.org
No.	1011.2314

Keywords

State space reduction
Probabilistic automata
EWI-19088
EC Grant Agreement nr.: FP7/214755
IR-75221
Branching probabilistic bisimulation
Probabilistic process algebra
METIS-276225
EC Grant Agreement nr.: FP7-ICT-2007-1
Confluence

Access to Document

paperFinal published version, 322 KB

http://arxiv.org/abs/1011.2314v1

1 Conference contribution

Confluence Reduction for Probabilistic Systems
Timmer, M., Stoelinga, M. & van de Pol, J., Mar 2011, Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011. Abdulla, P. A. & Leino, K. R. M. (eds.). Berlin: Springer, p. 311-325 15 p. (Lecture Notes in Computer Science; vol. 6605).
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

Open Access
File
13 Citations (Scopus)

137 Downloads (Pure)

Cite this

@techreport{d1ed29a34ea34f4e99345bcd1152e09e,

title = "Confluence Reduction for Probabilistic Systems (extended version)",

abstract = "This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic process algebra with data, facilitated by an earlier defined linear format. A case study demonstrates that significant reductions can be obtained.",

keywords = "State space reduction, Probabilistic automata, EWI-19088, EC Grant Agreement nr.: FP7/214755, IR-75221, Branching probabilistic bisimulation, Probabilistic process algebra, METIS-276225, EC Grant Agreement nr.: FP7-ICT-2007-1, Confluence",

author = "Mark Timmer and Stoelinga, {Mari{\"e}lle Ida Antoinette} and {van de Pol}, {Jan Cornelis}",

note = "eemcs-eprint-19088eemcs-eprint-19088 ",

year = "2010",

month = nov,

day = "10",

language = "Undefined",

publisher = "ArXiv.org",

number = "1011.2314",

type = "WorkingPaper",

institution = "ArXiv.org",

}

TY - UNPB

T1 - Confluence Reduction for Probabilistic Systems (extended version)

AU - Timmer, Mark

AU - Stoelinga, Mariëlle Ida Antoinette

AU - van de Pol, Jan Cornelis

N1 - eemcs-eprint-19088eemcs-eprint-19088

PY - 2010/11/10

Y1 - 2010/11/10

N2 - This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic process algebra with data, facilitated by an earlier defined linear format. A case study demonstrates that significant reductions can be obtained.

AB - This paper presents a novel technique for state space reduction of probabilistic specifications, based on a newly developed notion of confluence for probabilistic automata. We prove that this reduction preserves branching probabilistic bisimulation and can be applied on-the-fly. To support the technique, we introduce a method for detecting confluent transitions in the context of a probabilistic process algebra with data, facilitated by an earlier defined linear format. A case study demonstrates that significant reductions can be obtained.

KW - State space reduction

KW - Probabilistic automata

KW - EWI-19088

KW - EC Grant Agreement nr.: FP7/214755

KW - IR-75221

KW - Branching probabilistic bisimulation

KW - Probabilistic process algebra

KW - METIS-276225

KW - EC Grant Agreement nr.: FP7-ICT-2007-1

KW - Confluence

M3 - Working paper

BT - Confluence Reduction for Probabilistic Systems (extended version)

PB - ArXiv.org

CY - Ithaca, NY, USA

ER -