
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
