# Probabilistic Timed Automata

 Title: Probabilistic Timed Automata Authors: Simon Wimmer and Johannes Hölzl Submission date: 2018-05-24 Abstract: 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]. BibTeX: @article{Probabilistic_Timed_Automata-AFP, author = {Simon Wimmer and Johannes Hölzl}, title = {Probabilistic Timed Automata}, journal = {Archive of Formal Proofs}, month = may, year = 2018, note = {\url{https://isa-afp.org/entries/Probabilistic_Timed_Automata.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Markov_Models, Timed_Automata