Probabilistic Timed Automata

Simon Wimmer 🌐 and Johannes Hölzl 🌐

May 24, 2018

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


We present a formalization of probabilistic timed automata (PTA) for which we try to follow the formula MDP + TA = PTA as far as possible: our work starts from our existing formalizations of Markov decision processes (MDP) and timed automata (TA) and combines them modularly. We prove the fundamental result for probabilistic timed automata: the region construction that is known from timed automata carries over to the probabilistic setting. In particular, this allows us to prove that minimum and maximum reachability probabilities can be computed via a reduction to MDP model checking, including the case where one wants to disregard unrealizable behavior. Further information can be found in our ITP paper [2].


BSD License


Session Probabilistic_Timed_Automata