A theory of timed automata.

*(English)*Zbl 0803.68071Summary: 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
PDF
BibTeX
XML
Cite

\textit{R. Alur} and \textit{D. L. Dill}, Theor. Comput. Sci. 126, No. 2, 183--235 (1994; Zbl 0803.68071)

Full Text:
DOI

##### 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, (), 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, (), 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, (), 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 |

[9] | K. Čerāns, Decidability of bisimulation equivalence for parallel timer processes, in Proc. 4th Workshop on Computer-aided Verification, Lecture Notes in Computer Science (to appear). |

[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, (), 399-409, Lecture Notes in Computer Science |

[14] | Dill, D., Timing assumptions and verification of finite-state concurrent systems, (), 197-212, Lecture Notes in Computer Science |

[15] | Dill, D., Trace theory for automatic hierarchical verification of speed-independent circuits, (1989), MIT Press Cambridge, MA |

[16] | Dill, D.; Wong-Toi, H., Synthesizing processes and schedulers from temporal specifications, (), 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, (), 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 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?, (), 657-668 |

[30] | Leveson, N.; Stolzy, J., Analyzing safety and fault tolerance using timed Petri nets, (), 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, (), 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, (), 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, (), 510-584, Lecture Notes in Computer Science |

[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 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, (), 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) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.