Document Open Access Logo

On the Axiomatisation of Branching Bisimulation Congruence over CCS

Authors Luca Aceto , Valentina Castiglioni , Anna Ingólfsdóttir , Bas Luttik

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2022.6.pdf
  • Filesize: 0.81 MB
  • 18 pages

Document Identifiers

Author Details

Luca Aceto
  • Reykjavik University, Iceland
  • Gran Sasso Science Institute, L'Aquila, Italy
Valentina Castiglioni
  • Reykjavik University, Iceland
Anna Ingólfsdóttir
  • Reykjavik University, Iceland
Bas Luttik
  • Eindhoven University of Technology, The Netherlands

Funding

This work has been partially supported by the project "Open Problems in the Equational Logic of Processes" (OPEL) of the Icelandic Research Fund (grant No. 196050-051). V. Castiglioni has been supported by the project "Programs in the wild: Uncertainties, adaptabiLiTy and veRificatiON" (ULTRON) of the Icelandic Research Fund (grant No. 228376-051).

Acknowledgements

We thank the reviewers for their valuable comments that helped us to improve our contribution.

Cite AsGet BibTex

Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, and Bas Luttik. On the Axiomatisation of Branching Bisimulation Congruence over CCS. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 6:1-6:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.CONCUR.2022.6

Abstract

In this paper we investigate the equational theory of (the restriction, relabelling, and recursion free fragment of) CCS modulo rooted branching bisimilarity, which is a classic, bisimulation-based notion of equivalence that abstracts from internal computational steps in process behaviour. Firstly, we show that CCS is not finitely based modulo the considered congruence. As a key step of independent interest in the proof of that negative result, we prove that each CCS process has a unique parallel decomposition into indecomposable processes modulo branching bisimilarity. As a second main contribution, we show that, when the set of actions is finite, rooted branching bisimilarity has a finite equational basis over CCS enriched with the left merge and communication merge operators from ACP.

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Equational basis
  • Weak semantics
  • CCS
  • Parallel composition

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Luca Aceto. On "Axiomatising Finite Concurrent Processes". SIAM J. Comput., 23(4):852-863, 1994. URL: https://doi.org/10.1137/S0097539793243600.
  2. Luca Aceto, Elli Anastasiadi, Valentina Castiglioni, Anna Ingólfsdóttir, and Bas Luttik. In search of lost time: Axiomatising parallel composition in process algebras. In Proceedings of LICS 2021, pages 1-14. IEEE, 2021. URL: https://doi.org/10.1109/LICS52264.2021.9470526.
  3. Luca Aceto, Valentina Castiglioni, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. Are two binary operators necessary to finitely axiomatise parallel composition? In Proceedings of CSL 2021, volume 183 of LIPIcs, pages 8:1-8:17, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.8.
  4. Luca Aceto, Valentina Castiglioni, Anna Ingolfsdottir, and Bas Luttik. On the axiomatisation of branching bisimulation congruence over ccs, 2022. URL: https://doi.org/10.48550/ARXIV.2206.13927.
  5. Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias R. Pedersen. On the axiomatisability of parallel composition: A journey in the spectrum. In Proceedings of CONCUR 2020, volume 171 of LIPIcs, pages 18:1-18:22, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.18.
  6. Luca Aceto, David de Frutos-Escrig, Carlos Gregorio-Rodríguez, and Anna Ingólfsdóttir. Axiomatizing weak simulation semantics over BCCSP. Theor. Comput. Sci., 537:42-71, 2014. URL: https://doi.org/10.1016/j.tcs.2013.03.013.
  7. Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir, and Bas Luttik. A finite equational base for CCS with left merge and communication merge. ACM Trans. Comput. Log., 10(1):6:1-6:26, 2009. URL: https://doi.org/10.1145/1459010.1459016.
  8. Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir, and Sumit Nain. Bisimilarity is not finitely based over BPA with interrupt. Theor. Comput. Sci., 366(1-2):60-81, 2006. URL: https://doi.org/10.1016/j.tcs.2006.07.003.
  9. Luca Aceto, Anna Ingólfsdóttir, Bas Luttik, and Paul van Tilburg. Finite equational bases for fragments of CCS with restriction and relabelling. In Proceedings of IFIP TCS 2008, volume 273 of IFIP, pages 317-332, 2008. URL: https://doi.org/10.1007/978-0-387-09680-3_22.
  10. Luca Aceto, Rob J. van Glabbeek, Wan Fokkink, and Anna Ingólfsdóttir. Axiomatizing prefix iteration with silent steps. Inf. Comput., 127(1):26-40, 1996. URL: https://doi.org/10.1006/inco.1996.0047.
  11. Twan Basten. Branching bisimilarity is an equivalence indeed! Inf. Process. Lett., 58(3):141-147, 1996. URL: https://doi.org/10.1016/0020-0190(96)00034-8.
  12. Jan A. Bergstra and Jan Willem Klop. Process algebra for synchronous communication. Information and Control, 60(1-3):109-137, 1984. URL: https://doi.org/10.1016/S0019-9958(84)80025-X.
  13. Jan A. Bergstra and Jan Willem Klop. Algebra of communicating processes with abstraction. Theor. Comput. Sci., 37:77-121, 1985. URL: https://doi.org/10.1016/0304-3975(85)90088-X.
  14. Taolue Chen, Wan Fokkink, and Rob J. van Glabbeek. Ready to preorder: The case of weak process semantics. Inf. Process. Lett., 109(2):104-111, 2008. URL: https://doi.org/10.1016/j.ipl.2008.09.003.
  15. Rob J. van Glabbeek. The linear time-branching time spectrum (extended abstract). In Proceedings of CONCUR '90, volume 458 of Lecture Notes in Computer Science, pages 278-297, 1990. URL: https://doi.org/10.1007/BFb0039066.
  16. Rob J. van Glabbeek. A complete axiomatization for branching bisimulation congruence of finite-state behaviours. In Proceedings of MFCS'93, volume 711 of Lecture Notes in Computer Science, pages 473-484, 1993. URL: https://doi.org/10.1007/3-540-57182-5_39.
  17. Rob J. van Glabbeek. The linear time - branching time spectrum II. In Proceedings of CONCUR'93, volume 715 of Lecture Notes in Computer Science, pages 66-81, 1993. URL: https://doi.org/10.1007/3-540-57208-2_6.
  18. Rob J. van Glabbeek. On cool congruence formats for weak bisimulations. Theor. Comput. Sci., 412(28):3283-3302, 2011. URL: https://doi.org/10.1016/j.tcs.2011.02.036.
  19. Rob J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). In IFIP Congress, pages 613-618, 1989. Google Scholar
  20. Rob J. van Glabbeek and W. P. Weijland. Branching time and abstraction in bisimulation semantics. J. ACM, 43(3):555-600, 1996. URL: https://doi.org/10.1145/233551.233556.
  21. Matthew Hennessy. Axiomatising finite concurrent processes. SIAM J. Comput., 17(5):997-1017, 1988. URL: https://doi.org/10.1137/0217063.
  22. Matthew Hennessy and Robin Milner. On observing nondeterminism and concurrency. In Proceedings of ICALP 1980, volume 85 of Lecture Notes in Computer Science, pages 299-309, 1980. URL: https://doi.org/10.1007/3-540-10003-2_79.
  23. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
  24. Tony Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. Google Scholar
  25. Robert M. Keller. Formal verification of parallel programs. Commun. ACM, 19(7):371-384, 1976. URL: https://doi.org/10.1145/360248.360251.
  26. Bas Luttik. Unique parallel decomposition in branching and weak bisimulation semantics. Theor. Comput. Sci., 612:29-44, 2016. URL: https://doi.org/10.1016/j.tcs.2015.10.013.
  27. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  28. Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  29. Robin Milner. A complete axiomatisation for observational congruence of finite-state behaviors. Inf. Comput., 81(2):227-247, 1989. URL: https://doi.org/10.1016/0890-5401(89)90070-9.
  30. Faron Moller. Axioms for Concurrency. PhD thesis, Department of Computer Science, University of Edinburgh, July 1989. Report CST-59-89. Also published as ECS-LFCS-89-84. Google Scholar
  31. Faron Moller. The importance of the left merge operator in process algebras. In Proceedings of ICALP `90, volume 443 of Lecture Notes in Computer Science, pages 752-764, 1990. URL: https://doi.org/10.1007/BFb0032072.
  32. Faron Moller. The nonexistence of finite axiomatisations for CCS congruences. In Proceedings of LICS '90, pages 142-153, 1990. URL: https://doi.org/10.1109/LICS.1990.113741.
  33. Rocco De Nicola and Matthew Hennessy. Testing equivalence for processes. In Proceedings of ICALP 1983, volume 154 of Lecture Notes in Computer Science, pages 548-560, 1983. URL: https://doi.org/10.1007/BFb0036936.
  34. David M. R. Park. Concurrency and automata on infinite sequences. In Proceedings of GI-Conference, volume 104 of Lecture Notes in Computer Science, pages 167-183, 1981. URL: https://doi.org/10.1007/BFb0017309.
  35. Gordon D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Computer Science Department, Aarhus University, 1981. Google Scholar
  36. Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebraic Methods Program., 60-61:17-139, 2004. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact