Confluence Reduction for Probabilistic Systems

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

    13 Citations (Scopus)
    83 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

    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

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

    Cite this