Confluence Reduction for Probabilistic Systems

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

13 Citations (Scopus)
54 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 languageEnglish
Title of host publicationProceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011
EditorsP.A. Abdulla, K.R.M. Leino
Place of PublicationBerlin
PublisherSpringer
Pages311-325
Number of pages15
ISBN (Print)978-3-642-19834-2
DOIs
Publication statusPublished - Mar 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume6605
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Algebra
Specifications

Keywords

  • METIS-277817
  • Branching probabilistic bisimulation
  • Confluence
  • IR-75536
  • EC Grant Agreement nr.: FP7/214755
  • State space reduction
  • Probabilistic process algebra
  • EWI-19229
  • Probabilistic automata

Cite this

Timmer, M., Stoelinga, M. I. A., & van de Pol, J. C. (2011). Confluence Reduction for Probabilistic Systems. In P. A. Abdulla, & K. R. M. Leino (Eds.), Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011 (pp. 311-325). (Lecture Notes in Computer Science; Vol. 6605). Berlin: Springer. https://doi.org/10.1007/978-3-642-19835-9_29
Timmer, Mark ; Stoelinga, Mariëlle Ida Antoinette ; van de Pol, Jan Cornelis. / Confluence Reduction for Probabilistic Systems. Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011. editor / P.A. Abdulla ; K.R.M. Leino. Berlin : Springer, 2011. pp. 311-325 (Lecture Notes in Computer Science).
@inproceedings{bb424a198e4f43409639d3797a9cd9dc,
title = "Confluence Reduction for Probabilistic Systems",
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 = "METIS-277817, Branching probabilistic bisimulation, Confluence, IR-75536, EC Grant Agreement nr.: FP7/214755, State space reduction, Probabilistic process algebra, EWI-19229, Probabilistic automata",
author = "Mark Timmer and Stoelinga, {Mari{\"e}lle Ida Antoinette} and {van de Pol}, {Jan Cornelis}",
year = "2011",
month = "3",
doi = "10.1007/978-3-642-19835-9_29",
language = "English",
isbn = "978-3-642-19834-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "311--325",
editor = "P.A. Abdulla and K.R.M. Leino",
booktitle = "Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011",

}

Timmer, M, Stoelinga, MIA & van de Pol, JC 2011, Confluence Reduction for Probabilistic Systems. in PA Abdulla & KRM Leino (eds), Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011. Lecture Notes in Computer Science, vol. 6605, Springer, Berlin, pp. 311-325. https://doi.org/10.1007/978-3-642-19835-9_29

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

Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011. ed. / P.A. Abdulla; K.R.M. Leino. Berlin : Springer, 2011. p. 311-325 (Lecture Notes in Computer Science; Vol. 6605).

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

TY - GEN

T1 - Confluence Reduction for Probabilistic Systems

AU - Timmer, Mark

AU - Stoelinga, Mariëlle Ida Antoinette

AU - van de Pol, Jan Cornelis

PY - 2011/3

Y1 - 2011/3

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 - METIS-277817

KW - Branching probabilistic bisimulation

KW - Confluence

KW - IR-75536

KW - EC Grant Agreement nr.: FP7/214755

KW - State space reduction

KW - Probabilistic process algebra

KW - EWI-19229

KW - Probabilistic automata

U2 - 10.1007/978-3-642-19835-9_29

DO - 10.1007/978-3-642-19835-9_29

M3 - Conference contribution

SN - 978-3-642-19834-2

T3 - Lecture Notes in Computer Science

SP - 311

EP - 325

BT - Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011

A2 - Abdulla, P.A.

A2 - Leino, K.R.M.

PB - Springer

CY - Berlin

ER -

Timmer M, Stoelinga MIA, van de Pol JC. Confluence Reduction for Probabilistic Systems. In Abdulla PA, Leino KRM, editors, Proceedings of the 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011. Berlin: Springer. 2011. p. 311-325. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-642-19835-9_29