Abstract

We discuss counterexamples for Probabilistic Computational Tree Logic (PCTL), and an algorithm based on the k shortest path algorithm to find these counterexamples. Also discussed are the hop-constrained variants of the algorithms, and way to reduce hop-constrained problems to unconstrained problems. The discussed algorithms are implemented and this implementation is used to analyse several case studies. The experiments and mathematical analysis show that in practice the number of paths needed for a counterexample may grow exponentially. In order to combat this size explosion we propose to use the existing technique of bisimulation minimisation on the one hand, and on the other hand we introduce regular expressions to represent sets of paths compactly. Experiments of these compactifications are also included, which show that very short expressive, and above all, intelligble, expressions can be obtained.

Additional Resources

1. The paper