# [isabelle] New AFP article: Timed Automata

*To*: Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] New AFP article: Timed Automata
*From*: Tobias Nipkow <nipkow at in.tum.de>
*Date*: Fri, 11 Mar 2016 18:43:47 +0100
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

Timed Automata
Simon Wimmer

`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.
`
http://afp.sourceforge.net/entries/Timed_Automata.shtml
Enjoy!

**Attachment:
**`smime.p7s`

*Description:* S/MIME Cryptographic Signature

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*