We present a survey of proof systems for deriving properties of message-passing process calculi. This includes systems for proving · that two process specifications are semantically equivalent with respect to variations on bismulation equivalence · a process satisfies a behavioural property expressed in a first order modal logic. The key question to be discussed is the extent to which such proof systems can be complete, given that both processes and properties can be parameterised recursively on data domains.
展开▼
