A theory of timed automata Export

@article{citeulike:2764420, abstract = {We propose timed (finite) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words-infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both B\"{u}chi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable ([Pi]11-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems.}, author = {Alur, Rajeev and Dill, David L.}, citeulike-article-id = {2764420}, citeulike-linkout-0 = {http://portal.acm.org/citation.cfm?id=180782.180519}, citeulike-linkout-1 = {http://dx.doi.org/10.1016/0304-3975(94)90010-8}, citeulike-linkout-2 = {http://www.sciencedirect.com/science/article/B6V1G-45D9T5J-X/1/a623311730b429ee9da8b0f30882d2bb}, doi = {10.1016/0304-3975(94)90010-8}, journal = {Theoretical Computer Science}, keywords = {automata, formal, formalism, temporal-logic, time}, month = {April}, number = {2}, pages = {183--235}, posted-at = {2009-03-01 15:45:49}, priority = {2}, title = {A theory of timed automata}, url = {http://dx.doi.org/10.1016/0304-3975(94)90010-8}, volume = {126}, year = {1994} }

TY - JOUR ID - citeulike:2764420 L3 - citeulike-article-id:2764420 N2 - We propose timed (finite) automata to model the behavior of real-time systems over time. Our definition provides a simple, and yet powerful, way to annotate state-transition graphs with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words-infinite sequences in which a real-valued time of occurrence is associated with each symbol. We study timed automata from the perspective of formal language theory: we consider closure properties, decision problems, and subclasses. We consider both nondeterministic and deterministic transition structures, and both Büchi and Muller acceptance conditions. We show that nondeterministic timed automata are closed under union and intersection, but not under complementation, whereas deterministic timed Muller automata are closed under all Boolean operations. The main construction of the paper is an (PSPACE) algorithm for checking the emptiness of the language of a (nondeterministic) timed automaton. We also prove that the universality problem and the language inclusion problem are solvable only for the deterministic automata: both problems are undecidable ([Pi]11-hard) in the nondeterministic case and PSPACE-complete in the deterministic case. Finally, we discuss the application of this theory to automatic verification of real-time requirements of finite-state systems. IS - 2 JF - Theoretical Computer Science EP - 235 TI - A theory of timed automata VL - 126 SP - 183 KW - automata KW - formal KW - formalism KW - temporal-logic KW - time AU - Alur, Rajeev AU - Dill, David PY - 1994/04/25/ UR - http://dx.doi.org/10.1016/0304-3975(94)90010-8 ER -