Report Number: CS-TR-90-1307
Institution: Stanford University, Department of Computer Science
Title: Real-time logics: complexity and expressiveness
Author: Alur, Rajeev
Author: Henzinger, Thomas A.
Date: March 1990
Abstract: The theory of the natural numbers with linear order and monadic predicates underlies propositional linear temporal logic. To study temporal logics for real-time systems, we combine this classical theory of infinite state sequences with a theory of 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 omega-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. In fact, 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 give tableau-based decision procedures. Consequently, these two formalisms are well-suited for the specification and verification of real-time systems.
http://i.stanford.edu/pub/cstr/reports/cs/tr/90/1307/CS-TR-90-1307.pdf