MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)

Simon Wimmer*, Johannes Hölzl

*Corresponding author for this work

Research output: Chapter in Book / Report / Conference proceedingConference contributionAcademicpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationInteractive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
PublisherSpringer/Verlag
Pages597-603
Number of pages7
ISBN (Electronic)9783319948218
ISBN (Print)9783319948201
DOIs
Publication statusPublished - 2018
Event9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom
Duration: 9 Jul 201812 Jul 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10895 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018
CountryUnited Kingdom
CityOxford
Period9/07/1812/07/18

Fingerprint Dive into the research topics of 'MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper)'. Together they form a unique fingerprint.

Cite this