
Accession Number : ADA323441
Title : RealTime Logics: Complexity and Expressiveness,
Corporate Author : STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Personal Author(s) : Alur, Rajeev ; Henzinger, Thomas A.
PDF Url : ADA323441
Report Date : 15 MAR 1990
Pagination or Media Count : 40
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 omegaregular 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 tableaubased decision procedures. Consequently, these two formalisms are wellsuited for the specification and verification of real time systems.
Descriptors : *MEASUREMENT, *REAL TIME, *MATHEMATICAL LOGIC, *TIME STUDIES, VERIFICATION, THEORY, SEQUENCES, VARIATIONS, INFINITE SERIES, FRAGMENTS.
Subject Categories : Theoretical Mathematics
Computer Programming and Software
Distribution Statement : APPROVED FOR PUBLIC RELEASE