On the expressiveness of choice quantification Original Research Article

We define process algebras with a generalised operation ∑ for choice. For every infinite cardinal κ, we prove that the algebra of transition trees with branching degree <κ is free in the class of process algebras in which ∑ is defined for all subsets with a cardinality <κ. We explain how the expressions of a fragment of the specification language μCRL may be used to denote elements of our process algebras. In particular, we explain how choice quantifiers may be used to denote infinite sums. We show that choice quantifiers can simulate both the existential and the universal quantifiers of first-order logic, while the input prefix mechanism can only simulate the universal quantifier.