Real-Time Logics: Complexity and Expressiveness,
Abstract
The theory of the natural numbers with linear order and monadic predicates underlies propositional linear temporal 10 logic. To study temporal logics for real time systems, the authors 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 one 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. The authors 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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 15, 1990
- Accession Number
- ADA323441
Entities
People
- Rajeev Alur
- Thomas Henzinger
Organizations
- Stanford University