The Timestamp of Timed Automata

Abstract

Let (Formula Presented) be the class of non-deterministic timed automata with silent transitions. Given (Formula Presented), we effectively compute its timestamp: the set of all pairs (time value, action) of all observable timed traces of A. We show that the timestamp is eventually periodic and that one can compute a simple deterministic timed automaton with the same timestamp as that of A. As a consequence, we have a partial method, not bounded by time or number of steps, for the general language non-inclusion problem for (Formula Presented). We also show that the language of A is periodic with respect to suffixes.