You are here
Tanszékcsoporti szeminárium
Félév:
2015/16 I. félév
Helyszín:
Árpád tér 2. II. em. 220. sz.
Dátum:
2015-11-03
Időpont:
14:00-15:00
Előadó:
Karin Quaas (Universitat Leipzig, Germany)
Cím:
The Language Inclusion Problem for Timed Automata extended with Pushdown Stack and Counters
Absztrakt:
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.