A modal logic for message passing processes

A first-order modal logic is given for describing properties of processes which may send and receive values or messages along communication ports. We give two methods for proving that a process enjoys such a property. The first is the construction, for each processP and formulaF, of acharacteristic formula P satF such thatP enjoys the propertyF if and only if the formulaP satF is logically equivalent to tt. The second is a sound and complete proof system whose judgements take the formB P: F, meaning: under the assumptionB the processP enjoys the propertyF.The notion ofsymbolic operational semantics plays a crucial role in the design of both the characteristic formulae and the proof system.This work was been supported by the SERC grant GR/H16537 and the ESPRIT BRA CONCUR II