We present a formalization of probabilistic timed automata (PTA) in which we try to follow the formula “MDP + TA = PTA” as far as possible: our work starts from 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.
CITATION STYLE
Wimmer, S., & Hölzl, J. (2018). MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10895 LNCS, pp. 597–603). Springer Verlag. https://doi.org/10.1007/978-3-319-94821-8_35
Mendeley helps you to discover research relevant for your work.