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

Xian Xu
(East China University of Science and Technology)
Wenbo Zhang
(Shanghai Ocean University, Shanghai Key Laboratory of Trustworthy Computing)

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.

In Ornela Dardha and Valentina Castiglioni: Proceedings Combined 28th International Workshop on Expressiveness in Concurrency and 18th Workshop on Structural Operational Semantics (EXPRESS/SOS 2021), Paris, France (online event), 23rd August 2021, Electronic Proceedings in Theoretical Computer Science 339, pp. 76–92.
Published: 23rd August 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.339.8 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org