FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)

Authors: Simon Wimmer and Johannes Hölzl

Paper Information

Title:MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)
Authors:Simon Wimmer and Johannes Hölzl
Proceedings:ITP Papers
Editors: Jeremy Avigad and Assia Mahboubi
Keywords:Isabelle/HOL, Probabilistic Timed Automata, Timed Automata, Markov Decision Processes
Abstract:

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 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.

Pages:7
Talk:Jul 11 16:20 (Session 67C)
Paper: