### Abstract

Timed automata are a widely used formalism for modeling real-time systems, which is employed in a class of successful model checkers such as UPPAAL [LPY97], HyTech [HHWt97] or Kronos [Yov97]. This work formalizes the theory for the subclass of diagonal-free timed automata, which is sufficient to model many interesting problems. We first define the basic concepts and semantics of diagonal-free timed automata. Based on this, we prove two types of decidability results for the language emptiness problem. The first is the classic result of Alur and Dill [AD90, AD94], which uses a finite partitioning of the state space into so-called `regions`. Our second result focuses on an approach based on `Difference Bound Matrices (DBMs)`, which is practically used by model checkers. We prove the correctness of the basic forward analysis operations on DBMs. One of these operations is the Floyd-Warshall algorithm for the all-pairs shortest paths problem. To obtain a finite search space, a widening operation has to be used for this kind of analysis. We use Patricia Bouyer's [Bou04] approach to prove that this widening operation is correct in the sense that DBM-based forward analysis in combination with the widening operation also decides language emptiness. The interesting property of this proof is that the first decidability result is reused to obtain the second one.

### License

BSD License

### Topics

- Computer science/Automata and formal languages

### Session Timed_Automata

- Floyd_Warshall
- Timed_Automata
- DBM
- Paths_Cycles
- DBM_Basics
- DBM_Operations
- DBM_Zone_Semantics
- Misc
- DBM_Normalization
- Regions_Beta
- Regions
- Closure
- Approx_Beta
- Normalized_Zone_Semantics

### Used by

- Probabilistic Timed Automata

## Cite

×

Timed_Automata-AFP

    @article{Timed_Automata-AFP,
      author  = {Simon Wimmer},
      title   = {Timed Automata},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/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
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Mar 11, 2016 : Isabelle2016