Confluence versus Ample Sets in Probabilistic Branching Time

Henri Hansen, Mark Timmer

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

    62 Downloads (Pure)

    Abstract

    To improve the efficiency of model checking in general, and probabilistic model checking in particular, several reduction techniques have been introduced. Two of these, confluence reduction and partial-order reduction by means of ample sets, are based on similar principles, and both preserve branching-time properties for probabilistic models. Confluence reduction has been introduced for probabilistic automata, whereas ample set reduction has been introduced for Markov decision processes. In this presentation we will explore the relationship between confluence and ample sets. To this end, we redefine confluence reduction to handle MDPs. We show that all non-trivial ample sets consist of confluent transitions, but that the converse is not true. We also show that the two notions coincide if the definition of confluence is restricted, and point out the relevant parts where the two theories differ. The results we present also hold for non-probabilistic models, as our theorems can just as well be applied in a context where all transitions are non-probabilistic. To show a practical application of our results, we adapt a state space generation technique based on representative states, already known in combination with confluence reduction, so that it can also be applied with partial-order reduction.
    Original languageUndefined
    Title of host publicationProceedings of the 3rd Young Researchers Workshop on Concurrency Theory
    EditorsB. Bollig
    Place of PublicationCachan, France
    PublisherEcole normale superieure de Cachan
    Pages-
    Number of pages4
    ISBN (Print)not assigned
    Publication statusPublished - Sept 2011
    Event3rd Young Researchers Workshop on Concurrency Theory - Aachen, Germany
    Duration: 10 Sept 201110 Sept 2011

    Publication series

    Name
    PublisherÉcole normale supérieure de Cachan

    Workshop

    Workshop3rd Young Researchers Workshop on Concurrency Theory
    Period10/09/1110/09/11
    Other10 September 2011

    Keywords

    • METIS-278793
    • IR-78024
    • Markov Decision Processes
    • Ample sets Probabilistic branching time
    • EWI-20500
    • Partial order reduction
    • EC Grant Agreement nr.: FP7/214755
    • EC Grant Agreement nr.: FP7-ICT-2007-1
    • Confluence reduction

    Cite this