Cylindric process algebras with conditionals give substitutionless $ p $ CRL

Theories that are designed to reason about processes and the information they exchange usually also include a construction to quantify over this information. We mention the input prefix mechanism of, e.g., the $pi$-calculus and the operation $gsum{$ for alternative quantification over data of mcrl. These constructions are implemented as binders, and hence imply a relatively complicated notion of substitution that takes the binding of these operations into account. As a consequence, the defining axioms of such constructions are not suitable for purely equational reasoning, or, to put it differently, proof systems for process theories that contain binders are not algebraic. In this paper, we shall define the variety of cylindric process algebras with conditionals, and we prove that, for data with built-in equality and built-in Skolem functions, it is an algebraic semantics of a subsystem of mcrl{. Thus we obtain a proof system for a class of process algebras with data and alternative quantification from which the complicated notion of substitution is eliminated.