University of Twente Student Theses


Representing PCTL counterexamples

Damman, B. (2008) Representing PCTL counterexamples.

[img] PDF
Abstract:We discuss counterexamples for Probabilistic Computational Tree Logic, 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.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page