Relevance logic and concurrent composition

• Main Author: Dam, Mads F.
• Other Authors: Stirling, Colin
• Published: University of Edinburgh 1990
• Subjects: 510
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.561615

Compositionality, i.e. that properties of composite systems are deduced in terms of those of their immediate constituents, is crucial to the tractability and practical usefulness of program logics. A general technique for obtaining this for parallel composition appeals to a relativisation of properties with respect to properties of parallel environments. This induces a notion of consequence on properties which will in general be a relevant one. Based on this observation we suggest using modal or temporal extensions of relevance logics to build compositional logics for processes. We investigate the general model theory of propositional relevance logic and introduce a notion of model based on semilattices with an inf-preserving binary operation. We present a number of correspondence and completeness results, investigate the relationship to Sylvan and Meyer's ternary model, and present concrete models based on Milner's SCCS. To account for dynamic behaviour a modal extension of linear logic is introduced, interpreted over models extended by prefixing in the style of CCS/SCCS. We show a variety of characterisation results, relating models to processes under testing preorders, and obtain completeness results, first for the general algebraically based interpretations and next for the process-based ones giving, for the latter, procedures for deciding validity and satisfiability of formulas. From a computational point of view the processes considered are unacceptably weak in that they lack a suitable notion of external, or controllable, choice. To remedy this we consider indexed modal models under weak preorders, generalising notions of process equivalence such as testing and failures equivalence. We give characterisations of these in terms of modal logic and axiomatise the logics obtained. Relevant extensions of these logics are introduced, interpreted over model classes on which a parallel composition is defined. We axiomatise the logics obtained, giving decision procedures as before, and conclude by specialising the results to testing equivalence and synchronous parallel composition.