Abstract
In this paper, we present an algorithm for checking weak context bisimulation over a finite higher order π-calculus, called linear higher order π-calculus. To achieve this aim, we propose a new bisimulation, called linear normal bisimulation, and furthermore prove the equivalence between context bisimulation and linear normal bisimulation for such linear higher order π-calculus. The correctness of this algorithm is also demonstrated. At last, we give a complete inference system for linear higher order π-calculus.
This work was supported by the National Natural Science Foundation of China under Grant 60473036.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Hennessy, M., Lin, H.: Symbolic bisimulations. Theoretical Computer Science 138, 353–389 (1995)
Hennessy, M., Lin, H.: Proof systems for message-passing process algebras. Formal Aspects of Computing 8, 379–407 (1996)
Jeffrey, A., Rathke, J.: Contextual equivalence for higher-order π-calculus revisited. In: Proceedings of Mathematical Foundations of Programming Semantics, Elsevier, Amsterdam (2003)
Jonsson, B., Parrow, J.: Deciding bisimulation equivalences for a class of non-finite-state program. Information and Computation 107, 272–302 (1993)
Larsen, K.G.: Efficient local correctness checking (extended abstract). In: Probst, D.K., von Bochmann, G. (eds.) CAV 1992. LNCS, vol. 663, pp. 30–43. Springer, Heidelberg (1993)
Li, Z., Chen, H.: Checking strong/weak bisimulation equivalences and observation congruence for the π-calculus. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 707–718. Springer, Heidelberg (1998)
Lin, H.: Complete proof systems for observation congruence in finite-control π-calculus. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 443–454. Springer, Heidelberg (1998)
Lin, H.: Computing bisimulations for finite-control π -calculus. Journal of Computer Science and Technology 15(1), 1–9 (2000)
Lin, H.: Complete inference systems for weak bisimulation equivalences in the π-calculus. Information and Computation 180(1), 1–29 (2003)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Parrow, J.: An introduction to the π-calculus. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, North-Holland, Amsterdam (2001)
Parrow, J., Sangiorgi, D.: Algebraic theories for name-passing calculi. Information and Computation 120(2), 174–197 (1995)
Sangiorgi, D.: Expressing mobility in process algebras: first-order and higher-order paradigms. Ph.D thesis, Department of Computer Science, University of Einburgh (1992)
Sangiorgi, D.: Bisimulation in higher-order calculi. Information and Computation 131(2) (1996)
Thomsen, B.: Calculus for higher order communicating systems. Ph.D thesis, Department of Computer, Imperial College (1990)
Thomsen, B.: Plain CHOCS: A second generation calculus for higher order processes. Acta Informatica 30, 1–59 (1993)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cao, Z. (2008). Equivalence Checking for a Finite Higher Order π-Calculus. In: Beckert, B., Hähnle, R. (eds) Tests and Proofs. TAP 2008. Lecture Notes in Computer Science, vol 4966. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79124-9_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-79124-9_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79123-2
Online ISBN: 978-3-540-79124-9
eBook Packages: Computer ScienceComputer Science (R0)