The language inclusion problem for timed automata with counters

Karin Quaas

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