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.

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:	Formal Methods and Tools (FMT)
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

Show download statistics for this publication

Repository Staff Only: item control page

Metis ID: 255050