Relevance logic and concurrent composition

The operation of relativizing properties with respect to parallel environments often used in obtaining compositionality in theories for concurrency corresponds to a notion of (contraction-free) relevant deduction. The author considers program logics in which this notion of deduction is internalized by the corresponding implication. The idea is carried through for safety properties of a simple system of SCCS-type synchronous processes with an internal choice operator. They present two completeness results: first for a modal extension of positive propositional linear logic with respect to the equational class of algebras containing the safety testing quotient of the author´s process system as its free member, and second for the free algebra itself.<>