Tanszékcsoporti szeminárium

We study decidability of verification problems for timed automata
extended with a pushdown stack and 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.