On Decidability of the Bisimilarity on Higher-order Processes with Parameterization

TL;DR

This paper investigates the decidability of strong bisimilarity in higher-order processes with parameterization, establishing that it remains decidable and providing decision procedures and axioms for verification.

Contribution

It proves the decidability of strong bisimilarity for parameterized higher-order processes and develops an algorithm and axioms for bisimilarity checking.

Findings

Strong bisimilarity is decidable with name and process parameterization.

An algorithm for bisimilarity checking is proposed.

An axiomatic system for bisimilarity is constructed.

Abstract

Higher-order processes with parameterization are capable of abstraction and application (migrated from the lambda-calculus), and thus are computationally more expressive. For the minimal higher-order concurrency, it is well-known that the strong bisimilarity (i.e., the strong bisimulation equality) is decidable in absence of parameterization. By contrast, whether the strong bisimilarity is still decidable for parameterized higher-order processes remains unclear. In this paper, we focus on this issue. There are basically two kinds of parameterization: one on names and the other on processes. We show that the strong bisimilarity is indeed decidable for higher-order processes equipped with both kinds of parameterization. Then we demonstrate how to adapt the decision approach to build an axiom system for the strong bisimilarity. On top of these results, we provide an algorithm for the bisimilarity checking.