On the expressiveness and decidability of higher-order process calculi (Q627133)

The authors present a core calculus of higher-order concurrency, abbreviated as HOcore. Other examples of higher-order process calculi include CHOCS, Plain CHOCS, and the higher-order \(\pi\)-calculus. HOcore includes only the operators necessary to express higher-order communications, i.e., communications that allow for passing of processes. These operators are input prefix, process output, and parallel composition. HOcore itself does not include the restriction operator, but it is explored how adding it to the calculus affects the decidability of bisimilarity. HOcore is shown to be Turing complete via a deterministic encoding of Minsky machines. Thus, the termination problem for HOcore is undecidable. While several definitions of bisimilarity for higher-order process calculi have been proposed by various authors, including higher-order bisimilarity, context bisimilarity, normal bisimilarity, and barbed congruence, all of these turn out to coincide for HOcore. In fact, the result is even stronger: the authors define three conditions on output transitions and three conditions on input transitions and demonstrate that a combination of any two conditions, one from the former three and one from the latter three, yields the same notion of bisimilarity for HOcore. The proposed definitions of bisimilarity above, except for barbed congruence, are all instances of such combinations. The authors proceed to show that both asynchronous and synchronous barbed congruence also coincide with the common notion of HOcore bisimilarity. They also briefly mention that the proofs can be adapted to show that the asynchronous versions of the above-mentioned combinations still produce the same notion of HOcore bisimilarity. This unique HOcore bisimilarity is shown to be a congruence, to be preserved under substitutions, and to be decidable, using a form of open bisimilarity that is a particularly simple combination of conditions that does not include conditions on \(\tau\)-transitions. Further, the HOcore bisimilarity is axiomatized by adapting Moller and Milner's unique decomposition of processes and Hirschkoff and Pous's axiomatization of a fragment of CCS to a higher-order setting. This axiomatization is then used to construct an algorithm, presented as a pseudocode, for checking whether two HOcore processes are bisimilar in time polynomial in the size of these processes. Adding the restriction operator to HOcore enables to encode recursion, effectively falsifying most of the results mentioned above. Even a very weak form of restriction, static restriction that does not appear inside output messages, causes the undecidability of any bisimilarity produced from one of the above mentioned combinations that includes a condition on \(\tau\)-transitions. Using a reduction from the Post correspondence problem, the authors show that in fact four such static restriction operators are sufficient to break decidability.