Confluence Reduction for Probabilistic Systems (extended version)

    Research output: Working paper

    37 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 languageUndefined
    Place of PublicationIthaca, NY, USA
    Number of pages28
    Publication statusPublished - 10 Nov 2010

    Publication series



    • 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

    Cite this