A master thesis from Aalborg University
Compositionality & Abstraction in verification of Probabilistic Transition
Author(s)
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
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.