Compositionality & Abstraction in verification of Probabilistic Transition
Translated title
Authors
Term
4. term
Education
Publication year
2003
Submitted on
2012-02-14
Abstract
In this thesis, we present techniques adapted to probabilistic transition systems in order to avoid or reduce the state space explored in verification. By using compositional abstraction, abstracts of components of a concurrent system can be used for model checking. We use probabilistic simulation preorder to establish a good abstract. We further present a minimization algorithm for probabilistic transition systems, which generates a minimized structure, with respect to simulation equivalence. Finally, we introduce the Quotient technique for our PTS model with the concept of using the minimization algorithm to minimize the size of the transformed specifications. However, it is realized that this situation never arises, as the transformed specification is the minimal structure possible given our constraints and assumptions. We propose at the end, the application of the simplification heuristic on components of the system, before applying the Quotienting technique rather than afterwards. We implement the quotient technique as part of our tool, CAPS and demonstrate the algorithms proposed in this thesis.
Documents