Let eNTA be the class of non-deterministic timed automata with silent transitions. Given A∈eNTA , 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 eNTA . We also show that the language of A is periodic with respect to suffixes.
|Name||Lecture Notes in Computer Science|
|Conference||17th International Conference on Formal Modeling and Analysis of Timed Systems|
|Abbreviated title||FORMATS 2019|
|Period||27/08/19 → 29/08/19|