Regular Expressions for PCTL Counterexamples

B. Damman, Tingting Han, Joost P. Katoen

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

    14 Citations (Scopus)

    Abstract

    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
    Pages179-188
    Number of pages10
    ISBN (Print)978-0-7695-3360-5
    DOIs
    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
    http://www.qest.org/qest2008/

    Conference

    Conference5th International Conference on the Quantitative Evaluation of Systems, QEST 2008
    Abbreviated titleQEST
    CountryFrance
    CitySt Malo
    Period14/09/0817/09/08
    Internet address

      Fingerprint

    Keywords

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

    Cite this

    Damman, B., Han, T., & Katoen, J. P. (2008). Regular Expressions for PCTL Counterexamples. In Proceedings of the 5th International Conference on the Quantitative Evaluaiton of Systems (QEST 2008) (pp. 179-188). [10.1109/QEST.2008.11] Los Alamitos: IEEE Computer Society Press. https://doi.org/10.1109/QEST.2008.11