Undecidability and completeness results for process algebras with alternative with alternative quantification over data

We define a class of process algebras with a generalised operation $sum$ that allows explicit treatment of emph{alternative quantification over data, and investigate the specific subclass formed by the algebras of finite processes modulo strong bisimulation. We prove that, in such algebras, equality between process terms is definable by means of a first-order data formula, and that, if the data is computable and has a built-in equality predicate, any $Pi^0_4$ data formula is definable as an equation between ground process terms. From these results we work to the conclusion that equality in strong bisimulation algebras with a computable data part is $Pi^0_4$-hard. We also investigate a restricted version of alternative quantification: the input prefix mechanism of Parrow and Sangiorgi (1995) and Hennessy and Lin (1996). We show that this restriction yields a less expressive formalism if the data is computable and has a built-in equality predicate: equality between input prefix processes coincides with the universal fragment of first-order logic for the data. That is, the input prefix mechanism gives rise to strong bisimulation algebras for which equality is complete in $Pi^0_1$. Finally, we give a ground complete axiomatisation for those strong bisimulation algebras of which the data part has built-in equality and Skolem functions