A theory of timed automata. (English) Zbl 0803.68071

Alur, Rajeev; Dill, David L.

Theor. Comput. Sci. 126, No. 2, 183-235 (1994).

Summary: 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 with timing constraints using finitely many real-valued clocks. A timed automaton accepts timed words – infinite sequences in which a real-valued time for 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^ 1_ 1\)-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.

MSC:

68Q45	Formal languages and automata
68Q60	Specification and verification (program logics, model checking, etc.)
68Q55	Semantics in the theory of computing

Keywords:

timed language; undecidability; Büchi automata; modeling of time; behavior of real-time systems; timed automata; nondeterministic timed automata; deterministic timed Muller automata; PSPACE-complete; verification

References:

[1]	Alur, R.; Courcoubetis, C.; Dill, D., Model-checking for real-time systems, Proc. 5th IEEE Symp. on Logic in Computer Science, 414-425 (1990)
[2]	Alur, R.; Courcoubetis, C.; Dill, D., Model-checking for probabilistic real-time systems, (Automata, Languages and Programming: Proc. 18th ICALP, Vol. 510 (1991), Springer: Springer Berlin), 115-136, Lecture Notes in Computer Science · Zbl 0769.68088
[3]	Alur, R.; Courcoubetis, C.; Dill, D., Verifying automata specifications of probabilistic real-time systems, (Proc. REX Workshop “Real-Time: Theory in Practice”, Vol. 600 (1991), Springer: Springer Berlin), 28-44, Lecture Notes in Computer Science
[4]	Alur, R.; Feder, T.; Henzinger, T., The benefits of relaxing punctuality, Proc. 10th ACM Symp. on Principles of Distributed Computing, 139-152 (1991) · Zbl 1314.68195
[5]	Alur, R.; Henzinger, T., A really temporal logic, Proc. 30th IEEE Symp. on Foundations of Computer Science, 164-169 (1989)
[6]	Bernstein, A.; Harter, P., Proving real-time properties of programs with temporal logic, Proc. 8th ACM Symp. on Operating System Principles, 164-176 (1981)
[7]	Büchi, R., On a decision method in restricted second-order arithmetic, (Proc. Internat. Cong. on Logic, Methodology, and Philosophy of Science 1960 (1962), Stanford University Press: Stanford University Press Stanford), 1-12
[8]	Burch, J.; Clarke, E.; Dill, D.; Hwang, L.; McMillan, K. L., Symbolic model checking: \(10^{20}\) states and beyond, Inform. and Comput., 98, 2, 142-170 (1992) · Zbl 0753.68066
[10]	Choueka, Y., Theories of automata on ω-tapes: a simplified approach, J. Comput. System Sci., 8, 117-141 (1974) · Zbl 0292.02033
[11]	Clarke, E.; Draghicescu, I.; Kurshan, R., A unified approach for showing language containment and equivalence between various types of ω-automata, Tech. Report (1989), Carnegie Mellon University · Zbl 0925.68274
[12]	Clarke, E.; Emerson, E. A.; Sistla, A. P., Automatic verification of finite-state concurrent systems using temporal-logic specifications, ACM Trans. Programming Languages and Systems, 8, 2, 244-263 (1986) · Zbl 0591.68027
[13]	Courcoubetis, C.; Yannakakis, M., Minimum and maximum delay problems in real-time systems, (Proc. 3rd Workshop on Computer-Aided Verification, Vol. 575 (1991), Springer: Springer Berlin), 399-409, Lecture Notes in Computer Science
[14]	Dill, D., Timing assumptions and verification of finite-state concurrent systems, (Sifakis, J., Automatic Verification Methods for Finite State Systems, Vol. 407 (1989), Springer: Springer Berlin), 197-212, Lecture Notes in Computer Science
[15]	Dill, D., Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits (1989), MIT Press: MIT Press Cambridge, MA
[16]	Dill, D.; Wong-Toi, H., Synthesizing processes and schedulers from temporal specifications, (Proc. 2nd Workshop on Computer-Aided Verification, Vol. 531 (1990), Springer: Springer Berlin), 272-281, Lecture Notes in Computer Science · Zbl 0765.68148
[17]	Emerson, E. A.; Clarke, E. M., Using branching-time temporal logic to synthesize synchronization skeletons, Sci. Comput. Programming, 2, 241-266 (1982) · Zbl 0514.68032
[18]	Emerson, E. A.; Mok, A.; Sistla, A. P.; Srinivasan, J., Quantitative temporal reasoning, (Proc. 2nd Workshop on Computer-Aided Verification, Vol. 531 (1990), Springer: Springer Berlin), 136-145, Lecture Notes in Computer Science · Zbl 0765.68121
[19]	Godefroid, P.; Wolper, P., A partial approach to model-checking, Proc. 6th IEEE Symp. on Logic in Computer Science, 406-415 (1991)
[20]	Harel, E.; Lichtenstein, O.; Pnueli, A., Explicit-clock temporal logic, Proc. 5th IEEE Symp. on Logic in Computer Science, 402-413 (1990)
[21]	Harel, D.; Pnueli, A.; Stavi, J., Propositional dynamic logic of regular programs, J. Comput. System Sci., 26, 222-243 (1983) · Zbl 0536.68041
[22]	Henzinger, T.; Manna, Z.; Pnueli, A., Temporal proof methodologies for real-time systems, Proc. 18th ACM Symp. on Principles of Programming Languages, 353-366 (1991)
[23]	Hoare, C., Communicating sequential processes, Comm. ACM, 21, 666-677 (1978) · Zbl 0383.68028
[24]	Hopcroft, J.; Ullman, J., Introduction to Automata Theory, Languages, and Computation (1979), Addison-Wesley: Addison-Wesley Reading, MA · Zbl 0426.68001
[25]	Jahanian, F.; Mok, A., Safety analysis of timing properties in real-time systems, IEEE Trans. Software Engrg., SE-12, 890-904 (1986)
[26]	Jahanian, F.; Mok, A., A graph-theoretic approach for timing analysis and its implementation, IEEE Trans. Comput., C-36, 961-975 (1987) · Zbl 0618.68008
[27]	Koymans, R., Specifying real-time properties with metric temporal logic, J. Real-time Systems, 2, 255-299 (1990)
[28]	Kurshan, R., Complementing deterministic Büchi automata in polynomial time, J. Comput. System Sci., 35, 59-71 (1987) · Zbl 0666.68058
[29]	Lamport, L., What good is temporal logic?, (Mason, R., Information Processing 83: Proc. 9th IFIP World Computer Cong. (1983), Elsevier: Elsevier Amsterdam), 657-668
[30]	Leveson, N.; Stolzy, J., Analyzing safety and fault tolerance using timed Petri nets, (Proc. Internat. Joint Conf. on Theory and Practice of Software Development, Vol. 186 (1985), Springer: Springer Berlin), 339-355, Lecture Notes in Computer Science
[31]	Lewis, H., Finite-state analysis of asynchronous circuits with bounded temporal uncertainty, Tech. Report TR-15-89 (1989), Harvard University
[32]	Lynch, N.; Attiya, H., Using mappings to prove timing properties, Proc. 9th ACM Symp. on Principles of Distributed Computing, 265-280 (1990)
[33]	Manna, Z.; Pnueli, A., The temporal framework for concurrent programs, (Boyer, R.; Moore, J., The Correctness Problem in Computer Science (1981), Academic Press: Academic Press New York), 215-274
[34]	McNaughton, R., Testing and generating infinite sequences by a finite automaton, Inform. and Control, 9, 521-530 (1966) · Zbl 0212.33902
[35]	Nicollin, X.; Sifakis, J.; Yovine, S., From ATP to timed graphs and hybrid systems, (Proc. REX workshop “Real-time: Theory in Practice”, Vol. 600 (1991), Springer: Springer Berlin), 549-572, Lecture Notes in Computer Science
[36]	Ostroff, J., Temporal Logic of Real-Time Systems (1990), Research Studies Press
[37]	Pnueli, A., The temporal logic of programs, Proc. 18th IEEE Symp. on Foundations of Computer Science, 46-77 (1977)
[38]	Pnueli, A., Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, (Current Trends in Concurrency, Vol. 224 (1986), Springer: Springer Berlin), 510-584, Lecture Notes in Computer Science · Zbl 0607.68022
[39]	Ramchandani, C., Analysis of asynchronous concurrent systems by Petri nets, Tech. Report MACTR-120 (1974), Massachusetts Institute of Technology
[40]	Rogers, H., Theory of Recursive Functions and Effective Computability (1967), McGraw-Hill: McGraw-Hill New York · Zbl 0183.01401
[41]	Safra, S., On the complexity of ω-automata, Proc. 29th IEEE Symp. on Foundations of Computer Science, 319-327 (1988)
[42]	Sistla, A. P.; Vardi, M.; Wolper, P., The complementation problem for Büchi automata with applications to temporal logic, Theoret. Comput. Sci., 49, 217-237 (1987) · Zbl 0613.03015
[43]	Thomas, W., Automata on infinite objects, (van Leeuwen, J., Handbook of Theoretical Computer Science, Vol. B (1990), Elsevier: Elsevier Amsterdam), 133-191 · Zbl 0900.68316
[44]	Vardi, M., Verification of concurrent programs-the automata-theoretic framework, Proc. 2nd IEEE Symp. on Logic in Computer Science, 167-176 (1987)
[45]	Vardi, M.; Wolper, P., An automata-theoretic approach to automatic program verification, Proc. 1st IEEE Symp. on Logic in Computer Science, 332-344 (1986)
[46]	Wolper, P., Temporal logic can be more expressive, Inform. and Control, 56, 72-99 (1983) · Zbl 0534.03009
[47]	Wong-Toi, H.; Hoffmann, G., The control of dense real-time discrete event systems, Proc. 30th IEEE Conf. on Decision and Control, 1527-1528 (1991)
[48]	Wolper, P.; Vardi, M.; Sistla, A. P., Reasoning about infinite computation paths, Proc. 24th IEEE Symp. on Foundations of Computer Science, 185-194 (1983)