The Timestamp of Timed Automata

TL;DR

This paper introduces a method to compute the timestamp of non-deterministic timed automata with silent transitions, revealing its periodic nature and enabling partial solutions to language non-inclusion problems.

Contribution

It presents an effective way to compute the timestamp of eNTA and shows its eventual periodicity, facilitating analysis of timed automata behaviors.

Findings

Timestamp of eNTA is eventually periodic.

A deterministic automaton with the same timestamp can be constructed.

Partial method for language non-inclusion problem is introduced.

Abstract

Given a member A of the class of non-deterministic timed automata with silent transitions (eNTA), we effectively compute its timestamp: the set of all pairs (time value, action) of all observable timed traces of A, a generalization of the reachability problem. 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.