A number of extensions to classical temporal logic have been proposed in recent years for the specification of real-time systems. The authors of this paper have developed one such extension, called TRIO, which is a first-order logic that includes the temporal operators Futr(A,t) and Past(A,t). The authors’ primary goal was to develop a logic that would allow the execution of the formal specification of a real-time system. In this paper, they extend their previous work with TRIO to provide a model parametric semantics for the language, which is the basis for proving the satisfiability of a TRIO specification constructively.

The paper includes a summary of the syntax and semantics of TRIO. The model parametric semantics is motivated with examples that illustrate the problems of interpreting temporal formulas on infinite time domains by restricting the domain to a finite approximation. The model parametric semantics is presented with restriction theorems that give conditions under which the truth value of a formula is preserved when the domain is restricted. The authors also describe a pair of algorithms for constructively verifying the satisfiability of a formula on a restricted domain.

The paper is self-contained and clearly written. The authors compare and contrast their work with other approaches to the problem of finite time domains and with other extensions to temporal logic. Although the focus of the paper is a set of theoretical results, the results are clearly identified and illustrated with examples. Moreover, a TRIO specification of a small example system is developed in an appendix.