A Model Parametric Real-Time Logic

Abstract

TRIO is a formal notation for the logic-based specification of real-time systems. In this paper the language and its straightforward model-theoretic semantics are briefly summarized. Then the need for assigning a consistent meaning to TRIO specifications is discussed, with reference to a variety of underlying time structures such as infinite-time structures (both dense and discrete) and finite-time structures. The main motivation is the ability to validate formal specifications. A solution to this problem is presented, which gives a new, model-parametric semantics to the language. An algorithm for constructively verifying the satisfiability of formulas in the decidable cases is defined, and several important temporal properties of specifications are characterized.