TY - GEN
T1 - Sampled universality of timed automata
AU - Abdulla, Parosh Aziz
AU - Krcal, Pavel
AU - Yi, Wang
PY - 2007
Y1 - 2007
N2 - 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 e 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.
AB - 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 e 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.
UR - https://www.scopus.com/pages/publications/37149022609
U2 - 10.1007/978-3-540-71389-0_2
DO - 10.1007/978-3-540-71389-0_2
M3 - 会议稿件
AN - SCOPUS:37149022609
SN - 3540713883
SN - 9783540713883
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 2
EP - 16
BT - Foundations of Software Science and Computational Structures - 10th International Conference, FOSSACS 2007. Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007
PB - Springer Verlag
T2 - 10th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2007
Y2 - 24 March 2007 through 1 April 2007
ER -