Notes on several methods for 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 lan-guages, the inference systems and the semantics of two one-dimensional temporal logic systems, generating families of two-dimensional temporal languages with varying ex-pressivity 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 consid-erably more expressive language but fails to transfer completeness and decidability in several cases. So a weaker method of restricted interlacing is proposed and shown to transfer all three basic logical properties. The connections of our work with more generic works on combininbg (any) logic systems are unfortunately absent from the current version of this paper but will be present in its nal version.