Efficient Model Checking for Probabilistic Timed Automata

Student thesis: Master Thesis and HD Thesis

  • Robert Jørgensgaard Engdahl
  • Arild Martin Møller Haugstad
2. term, Computer Science, Master (Master Programme)
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.
Publication date2008
Publishing institutionInstitut for Datalogi
ID: 14466601