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

Regular Expressions
Counterexample
Likelihood
Combinatorial argument
Leader Election
Reachability
Markov chain
Exceed
Path
Experiment

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
Damman, B. ; Han, Tingting ; Katoen, Joost P. / Regular Expressions for PCTL Counterexamples. Proceedings of the 5th International Conference on the Quantitative Evaluaiton of Systems (QEST 2008). Los Alamitos : IEEE Computer Society Press, 2008. pp. 179-188
@inproceedings{14518a6795e04050815d1c8d674f2bc4,
title = "Regular Expressions for PCTL Counterexamples",
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.",
keywords = "EWI-14720, METIS-255050, IR-62644",
author = "B. Damman and Tingting Han and Katoen, {Joost P.}",
note = "10.1109/QEST.2008.11",
year = "2008",
month = "9",
doi = "10.1109/QEST.2008.11",
language = "English",
isbn = "978-0-7695-3360-5",
pages = "179--188",
booktitle = "Proceedings of the 5th International Conference on the Quantitative Evaluaiton of Systems (QEST 2008)",
publisher = "IEEE Computer Society Press",

}

Damman, B, Han, T & Katoen, JP 2008, Regular Expressions for PCTL Counterexamples. in Proceedings of the 5th International Conference on the Quantitative Evaluaiton of Systems (QEST 2008)., 10.1109/QEST.2008.11, IEEE Computer Society Press, Los Alamitos, pp. 179-188, 5th International Conference on the Quantitative Evaluation of Systems, QEST 2008, St Malo, France, 14/09/08. https://doi.org/10.1109/QEST.2008.11

Regular Expressions for PCTL Counterexamples. / Damman, B.; Han, Tingting; Katoen, Joost P.

Proceedings of the 5th International Conference on the Quantitative Evaluaiton of Systems (QEST 2008). Los Alamitos : IEEE Computer Society Press, 2008. p. 179-188 10.1109/QEST.2008.11.

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

TY - GEN

T1 - Regular Expressions for PCTL Counterexamples

AU - Damman, B.

AU - Han, Tingting

AU - Katoen, Joost P.

N1 - 10.1109/QEST.2008.11

PY - 2008/9

Y1 - 2008/9

N2 - 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.

AB - 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.

KW - EWI-14720

KW - METIS-255050

KW - IR-62644

U2 - 10.1109/QEST.2008.11

DO - 10.1109/QEST.2008.11

M3 - Conference contribution

SN - 978-0-7695-3360-5

SP - 179

EP - 188

BT - Proceedings of the 5th International Conference on the Quantitative Evaluaiton of Systems (QEST 2008)

PB - IEEE Computer Society Press

CY - Los Alamitos

ER -

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