Alur, Rajeev; Henzinger, Thomas AIST Austria
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
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.