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

### License

BSD License

### Topics

- Mathematics/Probability theory
- Computer science/Automata and formal languages

### Session Probabilistic_Timed_Automata

- MDP_Aux
- Finiteness
- Basic
- Sequence
- Sequence_LTL
- Instantiate_Existentials
- More_List
- Stream_More
- Graphs
- Lib
- PTA
- PTA_Reachability

### Depends on

- Markov Models
- Timed Automata

### Auto-related entries

- Markov Decision Processes with Rewards

## Cite

×

Probabilistic_Timed_Automata-AFP

    @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},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- May 25, 2018 : Isabelle2017