Confluence Reduction for Probabilistic Systems

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

    13 Citations (Scopus)
    83 Downloads (Pure)


    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
    Number of pages15
    ISBN (Print)978-3-642-19834-2
    Publication statusPublished - Mar 2011

    Publication series

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


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

    Fingerprint Dive into the research topics of 'Confluence Reduction for Probabilistic Systems'. Together they form a unique fingerprint.

    Cite this