Modal logics for communicating systems

AbstractSimple modal logics for Milner's SCCS and CCS are presented. We offer sound and complete axiomatizations of validity relative to these calculi as models. Also we present compositional proof systems for when a program satisfies a formula. These involve proof rules which are like Gentzen introduction rules except that there are also introduction rules for the program combinators of SCCS and CCS. The compositional rules for restriction (or hiding) and parallel combinators arise out of a simple semantic strategy