Functional Temporal Calculus Versus Temporal Logic: An Engineering Approach

摘要

It is demonstrated that functional temporal calculus directly merges with the formalisms used in system theory, communication theory, stochastic processes, and concurrent programming. Functions, predicates, and logical operators are defined by natural extension from mappings between value domains to mappings between so-called temporal domains. The modal operators of temporal logic are replaced by temporal combinators (second-order functions) defined directly as mappings between temporal domains. With this semantic formulation, the usual model-theoretic arguments and the distinction between validity and provability are replaced by arguments in standard (nonmodal) logic, while retaining all advantages of temporal logic, particularly the possibility of dealing with time implicity. The demonstration of this correspondence leads to redefinitions of concepts from temporal logic, constituting a nontrivial generalization of their syntactic counterparts. The flexibility of the semantic formulation leads to extensions such as continuous-time temporal calculus.