Real-time logics: Complexity and expressiveness

R. Alur, T.A. Henzinger, Information and Computation 104 (1993) 35–77.

Download
No fulltext has been uploaded. References only!

Journal Article | Published
Author
Abstract
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.
Publishing Year
Date Published
1993-05-01
Journal Title
Information and Computation
Volume
104
Issue
1
Page
35 - 77
IST-REx-ID

Cite this

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, 104(1), 35–77. https://doi.org/10.1006/inco.1993.1025
Alur, Rajeev, and Thomas A Henzinger. “Real-Time Logics: Complexity and Expressiveness.” Information and Computation 104, no. 1 (1993): 35–77. 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, 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.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar