The Language Inclusion Problem for Timed Automata extended with Pushdown Stack and Counters

We study decidability of verication problems for timed automata extended with a pushdown stack or discrete counters. In this way, we obtain a strong model that may for instance be used to model real-time programs with procedure calls. It is long known that the reachability problem for this model is decidable. The goal of this work is to investigate the language inclusion problem and related problems for this class of automata and over finite timed words. On the negative side, we prove that the language inclusion problem is undecidable for the case that A is a pushdown timed automaton and B is a one-clock timed automaton. This is even the case if A is a deterministic instance of a very restricted subclass of timed pushdown automata called timed visibly one-counter nets. On the positive side, we prove that the language inclusion problem is decidable if A is a timed automaton and B is a timed automaton extended with a finite set of counters that can be incremented and decremented, and which we call timed counter nets. As a special case, we obtain the decidability of the universality problem for timed counter nets: given a timed automaton A with input alphabet $\Sigma$, does L(A) accept the set of all timed words over $\Sigma$? Finally, we give the precise decidability border for the universality problem by proving that the universality problem is undecidable for the class of timed visibly one-counter automata.

Authors

• Karin Quaas

Keywords

No keywords are indexed for this paper.