Confluence versus Ample Sets in Probabilistic Branching Time

Henri Hansen, Mark Timmer

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

    25 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 - Sep 2011

    Publication series

    Name
    PublisherÉcole normale supérieure de Cachan

    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

    Hansen, H., & Timmer, M. (2011). Confluence versus Ample Sets in Probabilistic Branching Time. In B. Bollig (Ed.), Proceedings of the 3rd Young Researchers Workshop on Concurrency Theory (pp. -). Cachan, France: Ecole normale superieure de Cachan.