Combining temporal logic systems (Q1815427)

Modular combinations of temporal logic systems are investigated. Four methods for combining two temporal logics are described and studied. 1. The temporalization method, i.e. the external application of a temporal logic to another temporal system (adding a temporal dimension to a logic system). 2. The independent combination of two temporal systems. 3. The full join of two temporal systems, where flows of time are considered over a two-dimensional plane. 4. The restriction join of two temporal systems. Three basic logical properties (soundness, completeness, and decidability) are analyzed. Each combination method comprises three submethods that combine the languages, the interface systems, and the semantics of two one-dimensional temporal logic systems, generating families of two-dimensional temporal languages with varying expressivity and varying degrees of transfer of logical properties. The first, second, and fourth method are shown to transfer all three basic logical properties. The third method generates a considerably more expressive language but fails to transfer completeness and decidability in several cases.