Regular Expressions for PCTL Counterexamples


Damman, B. and Han, T. and Katoen, J.P. (2008) Regular Expressions for PCTL Counterexamples. In: Proceedings of the 5th International Conference on the Quantitative Evaluaiton of Systems (QEST 2008), 14-17 Sept 2008, Saint Malo, France (pp. pp. 179-188).

[img] PDF
Restricted to UT campus only
: Request a copy
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.
Item Type:Conference or Workshop Item
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page

Metis ID: 255050