Partial Order Reduction for Probabilistic Branching Time

Christel Baier, Pedro d' Argenio, Marcus Größer

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

    31 Citations (Scopus)

    Abstract

    In the past, partial order reduction has been used successfully to combat the state explosion problem in the context of model checking for non-probabilistic systems. For both linear time and branching time specifications, methods have been developed to apply partial order reduction in the context of model checking. Only recently, results were published that give criteria on applying partial order reduction for verifying quantitative linear time properties for probabilistic systems. This paper presents partial order reduction criteria for Markov decision processes and branching time properties, such as formulas of probabilistic computation tree logic. Moreover, we provide a comparison of the results established so far about reduction conditions for Markov decision processes.
    Original languageEnglish
    Title of host publicationProceedings of the Third Workshop on Quantitative Aspects of Programming Languages (QAPL 2005)
    EditorsA. Cerone, H. Wiklicky
    Place of PublicationAmsterdam
    PublisherElsevier
    Pages97-116
    Number of pages20
    DOIs
    Publication statusPublished - 23 May 2005
    Event3rd Workshop on Quantitative Aspects of Programming Languages, QAPL 2005 - Edinburgh, Scotland, United Kingdom
    Duration: 2 Apr 20053 Apr 2005
    Conference number: 3

    Publication series

    NameElectronic Notes in Theoretical Computer Science
    PublisherElsevier
    Number2
    Volume153
    ISSN (Print)1571-0661
    ISSN (Electronic)1571-0661

    Workshop

    Workshop3rd Workshop on Quantitative Aspects of Programming Languages, QAPL 2005
    Abbreviated titleQAPL
    CountryUnited Kingdom
    CityEdinburgh, Scotland
    Period2/04/053/04/05

    Fingerprint Dive into the research topics of 'Partial Order Reduction for Probabilistic Branching Time'. Together they form a unique fingerprint.

    Cite this