Regular Expressions for PCTL Counterexamples

B. Damman, Tingting Han, Joost P. Katoen

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

    15 Citations (Scopus)


    Counterexamples for probabilistic reachability in Markov chains are sets of paths that all reach a goal state and whose cumulative likelihood exceeds a threshold. This paper is concerned with the issue of how to conveniently represent these sets. Experiments, partially substantiated with combinatorial arguments, show that the cardinality of such sets may be excessive. To obtain compact representations of counterexamples we suggest to use regular expressions. We present a simple algorithm to generate minimal regular expressions and adopt a recursive scheme to determine their likelihood. Markov chain reduction prior to counterexample generation may yield even shorter regular expressions. The feasibility of the approach is illustrated by means two protocols: leader election and the Crowds protocol.
    Original languageEnglish
    Title of host publicationProceedings of the 5th International Conference on the Quantitative Evaluaiton of Systems (QEST 2008)
    Place of PublicationLos Alamitos
    PublisherIEEE Computer Society Press
    Number of pages10
    ISBN (Print)978-0-7695-3360-5
    Publication statusPublished - Sep 2008
    Event5th International Conference on the Quantitative Evaluation of Systems, QEST 2008 - Palais du Grand Large, St Malo, France
    Duration: 14 Sep 200817 Sep 2008
    Conference number: 5


    Conference5th International Conference on the Quantitative Evaluation of Systems, QEST 2008
    Abbreviated titleQEST
    CitySt Malo
    Internet address


    • EWI-14720
    • METIS-255050
    • IR-62644


    Dive into the research topics of 'Regular Expressions for PCTL Counterexamples'. Together they form a unique fingerprint.

    Cite this