Branching versus linear logics yet again

Abstract

A brief overview is given of the temporal logics used in concurrent program verification and in database and systems specification. The properties of the underlying modal frame structures are analysed. The relative advantages of the linear and branching approaches are discussed. The state versus path formulas controversy is revisited. A meta-linear operator L is proposed and compared with the "in all trajectories" operator considered in the language CTL*. The usefulness of the new operator within the context of a layered methodology for database and information systems specification and verification is illustrated. The operator is seen as a "frame change operator" and other interesting operators of this class are referred. Finitary and infinitary axiomatisations are given for the operator L. The proof of the completeness of the infinitary axiomatisation is briefly outlined. This proof requires an appropriate extension of the usual Henkin methods. © 1990 BCS.