Combining Temporal Logic Systems

This paper is a continuation of the work started in [FG92] on combining temporal logics. In this work, four combination methods are described and studied with respect to the transference of logical properties from the component one-dimensional temporal logics to the resulting two-dimensional temporal logic. Three basic logical properties are analysed, namely soundness, completeness and decidability. Each combination method is composed of three submethods that combine the languages, the inference systems and the semantics of two one-dimensional temporal logic systems, generating families of two-dimensional temporal languages with varying expressivity and varying degree of transference of logical properties. The temporalisation method and the independent combination method are shown to transfer all three basic logical properties. The method of full interlacing of logic systems generates a considerably more expressive language but fails to transfer completeness and decidability in several..