Timed Automata with Counters
Karin Quaas ( Universität Leipzig )
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.