Branching versus linear logics yet again

Publisher Website
Google Scholar
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 operatorLis 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 operatorL. The proof of the completeness of the infinitary axiomatisation is briefly outlined. This proof requires an appropriate extension of the usual Henkin methods.

This publication has 39 references indexed in Scilit: