Advertisement
Published in:
2007 | OriginalPaper | Chapter
Sampled Universality of Timed Automata
Authors : Parosh Aziz Abdulla, Pavel Krcal, Wang Yi
Published in: Foundations of Software Science and Computational Structures
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
Timed automata can be studied in not only a dense-time setting but also a discrete-time setting. The most common example of discrete-time semantics is the so called
sampled
semantics (i.e., discrete semantics with a fixed time granularity
ε
). In the real-time setting, the universality problem is known to be undecidable for timed automata. In this work, we study the universality question for the languages accepted by timed automata with sampled semantics. On the negative side, we show that deciding whether for all sampling periods
ε
a timed automaton accepts all timed words in
ε
-sampled semantics is as hard as in the real-time case, i.e., undecidable. On the positive side, we show that checking whether there is a sampling period such that a timed automaton accepts all untimed words in
ε
-sampled semantics is decidable. Our proof uses clock difference relations, developed to characterize the reachability relation for timed automata in connection with sampled semantics.