A substantially large class of programs operate in distributed and real-time environments, and an integral part of their correctness specification requires the expression of time-critical properties that relate the occurrence of events of the system. We focus on the formal specification and reasoning about the correctness of such programs. We propose a system of temporal logic, RTCTL (Real-Time Computation Tree Logic), that allows the melding of qualitative temporal assertions together with real-time constraints to permit specification and reasoning at the twin levels of abstraction: qualitative and quantitative. We argue that many practically useful correctness properties of temporal systems, which need to express timing as an essential part of their functionality requirements, can be expressed in RTCTL. We develop a model-checking algorithm for RTCTL whose complexity is linear in the size of the RTCTL specification formula and in the size of the structure. We also present an essentially optimal, exponential time tableau-based decision procedure for the satisfiability of RTCTL formulae. Finally, we consider several variants and extensions of RTCTL for real-time reasoning.
展开▼
