REAL-TIME LOGICS - COMPLEXITY AND EXPRESSIVENESS

被引：213

作者：

ALUR, R ^{[1
]}

HENZINGER, TA ^{[1
]}

机构：

[1] STANFORD UNIV,DEPT COMP SCI,STANFORD,CA 94305

来源：

INFORMATION AND COMPUTATION | 1993年 / 104卷 / 01期

关键词：

D O I：

10.1006/inco.1993.1025

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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. © 1993 Academic Press, Inc.

引用

页码：35 / 77

页数：43