A MODEL PARAMETRIC REAL-TIME LOGIC

TRIO is a formal notation for the logic-based specification of real-ti me systems. In this paper the language and its straightforward model-t heoretic semantics are briefly summarized. Then the need for assigning a consistent meaning to TRIO specifications is discussed, with refere nce to a variety of underlying time structures such as infinite-time s tructures (both dense and discrete) and finite-time structures. The ma in motivation is the ability to validate formal specifications. A solu tion 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 characteri zed.