Quantitative temporal reasoning

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.The work of E.A. Emerson was supported in part by NSF grant DCR-8511354, ONR URI contract N00014-86-K-0763, and Netherlands NWO grant nf-3/nfb 62-500. The work of A.K.Mok was supported in part by ONR Grant number N00014-89-J-1472 and Texas Advanced Technology Program Grant 003658-250. A summary of these results was presented at the Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, France, June 12–14, 1989.