A logic for the description of behaviours and properties of concurrent systems

Abstract

We present two logic LSP (Logic of Sequential Processes) and LP (Logic of Processes) which are propositional μ-calculi with both logical operators and standard operators of process algebras such as prefixing, non-deterministic choice, parallel composition and restriction. The process algebra operators are extended on unions of bisimulation classes. LSP is an extension of an algebra of sequential processes with strong bisimulation. A deductive system is proposed for this logic and a comparison with the propositional μ-calculus of Kozen is carried out. LP is an extension of an algebra of communicating processes with strong bisimulation. A deductive system is proposed for this logic and its use is illustrated by an example.