Document Open Access Logo

From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases

Authors Rowin Versteeg , Valentina Castiglioni , Bas Luttik

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2025.35.pdf
  • Filesize: 0.79 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Equational logic and rewriting
Keywords
  • Equational basis
  • Parallel composition
  • Preorders
  • Equivalences
  • Linear time - branching time spectrum

Metrics

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

Abstract

We consider process algebras with inaction, action prefix, non-deterministic choice and interleaving parallel composition modulo the behavioural equivalences in van Glabbeek’s linear time-branching time spectrum, and study the existence of finite bases (i.e., finite sound and complete axiomatisations) for these algebras. We prove that if the alphabet of actions is infinite and the behavioural equivalence is either simulation equivalence or trace equivalence, then a finite basis exists and is obtained by extending the known ground-complete axiomatisations for these behavioural equivalences. We prove that if the alphabet of actions is finite, then a finite basis does not exist for these equivalences. We also prove for all behavioural equivalences between ready simulation and completed traces there cannot exist a finite basis irrespective of the cardinality of the alphabet of actions (provided that it is non-empty). Finally, we prove that these results are maintained if the process algebra is extended with a constant for successful termination.

Cite As Get BibTex

Rowin Versteeg, Valentina Castiglioni, and Bas Luttik. From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases. In 36th International Conference on Concurrency Theory (CONCUR 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 348, pp. 35:1-35:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CONCUR.2025.35

Author Details

Rowin Versteeg
  • Eindhoven University of Technology, The Netherlands
Valentina Castiglioni
  • Eindhoven University of Technology, The Netherlands
Bas Luttik
  • Eindhoven University of Technology, The Netherlands

References

  1. Luca Aceto, Elli Anastasiadi, Valentina Castiglioni, and Anna Ingólfsdóttir. Non-finite axiomatisability results via reductions: CSP parallel composition and CCS restriction. In A Journey from Process Algebra via Timed Automata to Model Learning, volume 13560 of Lecture Notes in Computer Science, pages 1-26. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-15629-8_1.
  2. Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard 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. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2020.18.
  3. Luca Aceto, Valentina Castiglioni, Anna Ingólfsdóttir, Bas Luttik, and Mathias Ruggaard Pedersen. On the axiomatisability of parallel composition. Log. Methods Comput. Sci., 18(1), 2022. URL: https://doi.org/10.46298/LMCS-18(1:15)2022.
  4. Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. On the two-variable fragment of the equational theory of the max-sum algebra of the natural numbers. Technical report, Aarhus University, 1999. URL: https://doi.org/10.7146/brics.v6i22.20079.
  5. Luca Aceto, Zoltán Ésik, and Anna Ingólfsdóttir. The max-plus algebra of the natural numbers has no finite equational basis. Theoretical Computer Science, 293(1):169-188, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00236-0.
  6. Luca Aceto, Wan Fokkink, and Anna Ingólfsdóttir. Ready to preorder: Get your BCCSP axiomatization for free! In Algebra and Coalgebra in Computer Science, pages 65-79. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73859-6_5.
  7. Luca Aceto, Wan Fokkink, Rob van Glabbeek, and Anna Ingólfsdóttir. Nested semantics over finite trees are equationally hard. Information and Computation, 191(2):203-232, 2004. URL: https://doi.org/10.1016/j.ic.2004.02.001.
  8. Luca Aceto, Wan Fokkink, and Chris Verhoef. Structural operational semantics. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 197-292. North-Holland / Elsevier, 2001. URL: https://doi.org/10.1016/B978-044482830-9/50021-7.
  9. Luca Aceto, Wan J. 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.
  10. Josephus C.M. Baeten, Twan Basten, and Michel A. Reniers. Process algebra: equational theories of communicating processes, volume 50. Cambridge university press, 2010. URL: https://doi.org/10.1017/CBO9781139195003.
  11. Stefan Blom, Wan Fokkink, and Sumit Nain. On the axiomatizability of ready traces, ready simulation, and failure traces. In Automata, Languages and Programming, pages 109-118. Springer Berlin Heidelberg, 2003. URL: https://doi.org/10.1007/3-540-45061-0_10.
  12. Taolue Chen and Wan Fokkink. On finite alphabets and infinite bases III: Simulation. In Proceedings of CONCUR 2006, pages 421-434. Springer, 2006. URL: https://doi.org/10.1007/11817949_28.
  13. Taolue Chen, Wan Fokkink, Bas Luttik, and Sumit Nain. On finite alphabets and infinite bases. Information and Computation, 206(5):492-519, 2008. URL: https://doi.org/10.1016/j.ic.2007.09.003.
  14. Taolue Chen and Wan J. Fokkink. On the axiomatizability of impossible futures: Preorder versus equivalence. In Proceedings of LICS 2008, pages 156-165. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/LICS.2008.13.
  15. Taolue Chen, Wan J. Fokkink, and Sumit Nain. On finite alphabets and infinite bases II: completed and ready simulation. In Proceedings of FOSSACS 2006, volume 3921 of Lecture Notes in Computer Science, pages 1-15. Springer, 2006. URL: https://doi.org/10.1007/11690634_1.
  16. Taolue Chen, Wan J. Fokkink, and Rob J. van Glabbeek. On the axiomatizability of impossible futures. Log. Methods Comput. Sci., 11(3), 2015. URL: https://doi.org/10.2168/LMCS-11(3:17)2015.
  17. Robert de Simone. Higher-level synchronising devices in Meije-SCCS. Theor. Comput. Sci., 37:245-267, 1985. URL: https://doi.org/10.1016/0304-3975(85)90093-3.
  18. Wan J. Fokkink and Sumit Nain. On finite alphabets and infinite bases: From ready pairs to possible worlds. In Proceedings of FOSSACS 2004, volume 2987 of Lecture Notes in Computer Science, pages 182-194. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24727-2_14.
  19. Wan J. Fokkink and Sumit Nain. A finite basis for failure semantics. In Proceedings of ICALP 2005, volume 3580 of Lecture Notes in Computer Science, pages 755-765. Springer, 2005. URL: https://doi.org/10.1007/11523468_61.
  20. Rob J. van Glabbeek. The Linear Time - Branching Time Spectrum I. In Handbook of Process Algebra, pages 3-99. Elsevier Science, 2001. URL: https://doi.org/10.1016/B978-044482830-9/50019-9.
  21. Jan Friso Groote. A new strategy for proving ω-completeness applied to process algebra. In Proceedings of CONCUR 1990, pages 314-331. Springer, 1990. URL: https://doi.org/10.1007/BFb0039068.
  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. Charles A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666-677, 1978. URL: https://doi.org/10.1145/359576.359585.
  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. Robin Milner. A Calculus of Communicating Systems. LNCS 92, Springer-Verlag, Berlin, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  27. 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
  28. Faron Moller. The nonexistence of finite axiomatisations for CCS congruences. In Proceedings of LICS 1990, pages 142-153. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/LICS.1990.113741.
  29. Gordon D. Plotkin. A structural approach to operational semantics. Technical report, Aarhus University, 1981. Google Scholar
  30. Rowin Versteeg. From Bisimulation to Traces: The Impact of Parallel Composition on Finite Bases. Master’s thesis, Eindhoven University of Technology, 2021. URL: https://research.tue.nl/en/studentTheses/from-bisimulation-to-traces.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact