University of Twente Student Theses

Login

Representing PCTL counterexamples

Damman, B. (2008) Representing PCTL counterexamples.

[img] PDF
2MB
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:https://purl.utwente.nl/essays/58611
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page