Invariants in Process Algebra with Data

Abstract

We provide rules for calculating with invariants in process algebra with data, and illustrate these with examples. The new rules turn out to be equivalent to the well known Recursive Specification Principle which states that guarded recursive equations have at most one solution. In the setting with data this is reformulated as 'every convergent linear process operator has at most one fixed point' (CL-RSP). As a consequence, one can carry out verifications in well-known process algebras satisfying CL-RSP using invariants.