Timed Automata with Counters
Karin Quaas ( Universität Leipzig )
- 11:00 27th February 2014 ( week 6, Hilary Term 2014 )Lecture Theatre A
Timed automata are a prominent model used in the verification of real-time
systems. In this talk, I will give a short overview over recent extensions
of timed automata with unbounded data structures, such as counters and
stacks. I will then present some results on one of these extensions,
called timed one-counter nets. A timed one-counter net is a timed
automaton extended with a counter ranging over the natural numbers. A
timed one-counter system can also be regarded as an extension of a
one-dimensional vector addition system with states extended with finitely
many clocks. By an easy generalization of the classical region graph
construction for timed automata, one can prove that the emptiness problem
for timed one-counter nets is decidable. We will prove that the
universality problem for timed one-counter nets is decidable if the net
uses at most one clock, whereas the language inclusion problem and the
MTL-model checking problem are undecidable. This also answers an open
question originated in a work by Emmi and Majumdar, 2006. Finally, we can
use similar proof methods to show that MTL-model checking of an extension
of timed automata with parameters is undecidable even if the timed
automaton only uses at most one parametric clock.