Regular Expressions for PCTL Counterexamples


Share/Save/Bookmark

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.

[img]PDF
Restricted to UT campus only
: Request a copy
239Kb
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
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/62644
Official URL:http://dx.doi.org/10.1109/QEST.2008.11
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 255050