Alur, Rajeev; Henzinger, Thomas AISTA
The theory of the natural numbers with linear order and monadic predicates underlies propositional linear temporal logic. To study temporal logics that are suitable for reasoning about real-time systems, we combine this classical theory of infinite state sequences with a theory of discrete time, via a monotonic function that maps every state to its time. The resulting theory of timed state sequences is shown to be decidable, albeit nonelementary, and its expressive power is characterized by ω-regular sets. Several more expressive variants are proved to be highly undecidable. This framework allows us to classify a wide variety of real-time logics according to their complexity and expressiveness. Indeed, it follows that most formalisms proposed in the literature cannot be decided. We are, however, able to identify two elementary real-time temporal logics as expressively complete fragments of the theory of timed state sequences, and we present tableau-based decision procedures for checking validity. Consequently, these two formalisms are well-suited for the specification and verification of real-time systems. Copyright © 1993 Academic Press. All rights reserved.
Information and Computation
We thank David Dill, Zohar Manna, and Amir Pnueli for helpful discussion.
35 - 77
Alur R, Henzinger TA. Real-time logics: Complexity and expressiveness. Information and Computation. 1993;104(1):35-77. doi:10.1006/inco.1993.1025
Alur, R., & Henzinger, T. A. (1993). Real-time logics: Complexity and expressiveness. Information and Computation. Elsevier. https://doi.org/10.1006/inco.1993.1025
Alur, Rajeev, and Thomas A Henzinger. “Real-Time Logics: Complexity and Expressiveness.” Information and Computation. Elsevier, 1993. https://doi.org/10.1006/inco.1993.1025.
R. Alur and T. A. Henzinger, “Real-time logics: Complexity and expressiveness,” Information and Computation, vol. 104, no. 1. Elsevier, pp. 35–77, 1993.
Alur R, Henzinger TA. 1993. Real-time logics: Complexity and expressiveness. Information and Computation. 104(1), 35–77.
Alur, Rajeev, and Thomas A. Henzinger. “Real-Time Logics: Complexity and Expressiveness.” Information and Computation, vol. 104, no. 1, Elsevier, 1993, pp. 35–77, doi:10.1006/inco.1993.1025.
All files available under the following license(s):
This Item is protected by copyright and/or related rights. [...]
Link(s) to Main File(s)