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
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.