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

Simon Wimmer; Johannes Hölzl

doi:10.1007/978-3-319-94821-8_35

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 proceeding › Conference contribution › Academic › peer-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 language	English
Title of host publication	Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
Publisher	Springer/Verlag
Pages	597-603
Number of pages	7
ISBN (Electronic)	9783319948218
ISBN (Print)	9783319948201
DOIs	https://doi.org/10.1007/978-3-319-94821-8_35
Publication status	Published - 2018
Event	9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom Duration: 9 Jul 2018 → 12 Jul 2018

Publication series

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

Conference

Conference	9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/Territory	United Kingdom
City	Oxford
Period	9/07/18 → 12/07/18

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/978-3-319-94821-8_35

Persistent URL (handle)

Copy link address

Cite this

Wimmer, S., & Hölzl, J. (2018). MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 597-603). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10895 LNCS). Springer/Verlag. https://doi.org/10.1007/978-3-319-94821-8_35

Wimmer, Simon ; Hölzl, Johannes. / MDP + TA = PTA : Probabilistic Timed Automata, Formalized (Short Paper). Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, 2018. pp. 597-603 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4fdbd89785194156bf788ac2e9ac94ed,

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

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

author = "Simon Wimmer and Johannes H{\"o}lzl",

year = "2018",

doi = "10.1007/978-3-319-94821-8_35",

language = "English",

isbn = "9783319948201",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer/Verlag",

pages = "597--603",

booktitle = "Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",

note = "9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 09-07-2018 Through 12-07-2018",

}

Wimmer, S & Hölzl, J 2018, MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). in Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10895 LNCS, Springer/Verlag, pp. 597-603, 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 9/07/18. https://doi.org/10.1007/978-3-319-94821-8_35

MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). / Wimmer, Simon; Hölzl, Johannes.
Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag, 2018. p. 597-603 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10895 LNCS).

Research output: Chapter in Book / Report / Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - MDP + TA = PTA

T2 - 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018

AU - Wimmer, Simon

AU - Hölzl, Johannes

PY - 2018

Y1 - 2018

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

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

UR - http://www.scopus.com/inward/record.url?scp=85049886241&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85049886241&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-94821-8_35

DO - 10.1007/978-3-319-94821-8_35

M3 - Conference contribution

AN - SCOPUS:85049886241

SN - 9783319948201

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 597

EP - 603

BT - Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings

PB - Springer/Verlag

Y2 - 9 July 2018 through 12 July 2018

ER -

Wimmer S, Hölzl J. MDP + TA = PTA: Probabilistic Timed Automata, Formalized (Short Paper). In Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer/Verlag. 2018. p. 597-603. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2018 Jul 4. doi: 10.1007/978-3-319-94821-8_35

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

Abstract

Publication series

Conference

UN SDGs

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this