A master thesis from Aalborg University
Efficient Model Checking for Probabilistic Timed Automata
Term
2. term
Education
Publication year
2008
Submitted on
2008-06-12
Pages
0 pages
Abstract
In this thesis, we focus on the modeling formalism networks of probabilistic timed automata. Networks of probabilistic timed automata may be used to model systems where time, i.e. delays and timeouts, concurrency and synchronisation as well as probabilistic behaviour, either from the system or its environment, are all important properties in the model. We introduce a forward state space exploration and reduction algorithm to partition the state space of probabilistic and normal timed automata according to time-abstract equivalences. We demonstrate how this partitioning can be used to compute probabilistic reachabilities. A prototype tool, Uppaal Prob, has been implemented as an extension to the Uppaal Prob tool. This includes the state space exploration and reduction algorithm, refinement according to probabilistic reachability formulae and computation of maximal reachability probabilities.
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.