Undecidability and completeness results for process algebras with alternative quantification over data
Jan Friso Groote, S.P. Luttik · 1998
We define a class of process algebras with a generalised operation P that allows explicit treatment of 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 proc...