Confluence Reduction for Probabilistic Systems

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

    13 Citations (Scopus)
    89 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
    Event17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011 - Saarbrücken, Germany
    Duration: 26 Mar 20113 Apr 2011

    Publication series

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

    Conference

    Conference17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2011
    Period26/03/113/04/11
    Other26 March - 3 April 2011

    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