Almost Periodicity and the Timestamp of Timed Automata.
Amnon Rosenmann · arXiv (Cornell University) · 2014
Given a non-deterministic timed automaton with silent transitions (eNTA), we show that after an initial stage it becomes time-periodic. After computing the periodic parameters, we construct a finite almost periodic augmented region automaton, which includes a clock measuring the global time. In the next step we construct the timestamp of the automaton: the union of all its observable timed traces, which contains all the dates on which events occur - a generalization of the reachability problem. The timestamp of each event is an almost periodic subset of the non-negative reals. We also construct a simple deterministic timed automaton with the same timestamp as the given timed automaton, in contrast to the fact that the timed automaton itself may be non-determinizable. One application is the decidability of the $1$-bounded language inclusion problem for eNTA. Another is a partial method, which is not bounded by time or number of steps, for showing the non-inclusion of languages of timed automata.