
Timed
Automata
Title: 
Timed Automata 
Author:

Simon Wimmer

Submission date: 
20160308 
Abstract: 
Timed automata are a widely used formalism for modeling realtime
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 diagonalfree timed
automata, which is sufficient to model many interesting problems. We
first define the basic concepts and semantics of diagonalfree 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 socalled `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 FloydWarshall algorithm for the allpairs 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
DBMbased 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. 
BibTeX: 
@article{Timed_AutomataAFP,
author = {Simon Wimmer},
title = {Timed Automata},
journal = {Archive of Formal Proofs},
month = mar,
year = 2016,
note = {\url{http://isaafp.org/entries/Timed_Automata.shtml},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

