Document Open Access Logo

On the Axiomatisability of Parallel Composition: A Journey in the Spectrum

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

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2020.18.pdf
  • Filesize: 0.61 MB
  • 22 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
Mathias Ruggaard Pedersen
  • Reykjavik University, Iceland

Funding

This work has been supported by the project "Open Problems in the Equational Logic of Processes" (OPEL) of the Icelandic Research Fund (grant No. 196050-051).

Acknowledgements

We thank the anonymous reviewers for their valuable comments, and Rob van Glabbeek for a fruitful discussion on the axiomatisability of failures equivalence.

Cite AsGet BibTex

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 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 18:1-18:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CONCUR.2020.18

Abstract

This paper studies the existence of finite equational axiomatisations of the interleaving parallel composition operator modulo the behavioural equivalences in van Glabbeek’s linear time-branching time spectrum. In the setting of the process algebra BCCSP over a finite set of actions, we provide finite, ground-complete axiomatisations for various simulation and (decorated) trace semantics. On the other hand, we show that no congruence over that language that includes bisimilarity and is included in possible futures equivalence has a finite, ground-complete axiomatisation. This negative result applies to all the nested trace and nested simulation semantics.

Subject Classification

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

Metrics

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

References

  1. Luca Aceto, Wan Fokkink, Rob J. van Glabbeek, and Anna Ingólfsdóttir. Nested semantics over finite trees are equationally hard. Inf. Comput., 191(2):203-232, 2004. URL: https://doi.org/10.1016/j.ic.2004.02.001.
  2. 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.
  3. Luca Aceto, Wan Fokkink, Anna Ingólfsdóttir, and Mohammad Reza Mousavi. Lifting non-finite axiomatizability results to extensions of process algebras. Acta Inf., 47(3):147-177, 2010. URL: https://doi.org/10.1007/s00236-010-0114-7.
  4. Jos C.M. Baeten, T. Basten, and M.A. Reniers. Process algebra: Equational Theories of Communicating Processes. Cambridge tracts in theoretical computer science. Cambridge University Press, United Kingdom, 2010. URL: https://doi.org/10.1017/CBO9781139195003.
  5. 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.
  6. Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors. Handbook of Process Algebra. North-Holland / Elsevier, 2001. URL: https://doi.org/10.1016/b978-0-444-82830-9.x5017-6.
  7. Stefan Blom, Wan Fokkink, and Sumit Nain. On the axiomatizability of ready traces, ready simulation, and failure traces. In Proceedings of ICALP 2003, volume 2719 of Lecture Notes in Computer Science, pages 109-118, 2003. URL: https://doi.org/10.1007/3-540-45061-0_10.
  8. Taolue Chen and Wan 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.
  9. Taolue Chen, Wan Fokkink, Bas Luttik, and Sumit Nain. On finite alphabets and infinite bases. Inf. Comput., 206(5):492-519, 2008. URL: https://doi.org/10.1016/j.ic.2007.09.003.
  10. David de Frutos-Escrig and Carlos Gregorio-Rodríguez. Universal coinductive characterisations of process semantics. In IFIP International Conference On Theoretical Computer Science 2008, volume 273 of IFIP, pages 397-412, 2008. URL: https://doi.org/10.1007/978-0-387-09680-3_27.
  11. David de Frutos-Escrig, Carlos Gregorio-Rodríguez, Miguel Palomino, and David Romero-Hernández. Unifying the linear time-branching time spectrum of process semantics. Logical Methods in Computer Science, 9(2), 2013. URL: https://doi.org/10.2168/LMCS-9(2:11)2013.
  12. 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.
  13. Wan Fokkink and Bas Luttik. An omega-complete equational specification of interleaving. In Proceedings of ICALP 2000, volume 1853 of Lecture Notes in Computer Science, pages 729-743, 2000. URL: https://doi.org/10.1007/3-540-45022-X_61.
  14. Rob J. van Glabbeek. Full abstraction in structural operational semantics (extended abstract). In Proceedings of AMAST '93, Workshops in Computing, pages 75-82, 1993. Google Scholar
  15. 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.
  16. Rob J. van Glabbeek. The linear time - branching time spectrum I. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 3-99. North-Holland / Elsevier, 2001. URL: https://doi.org/10.1016/b978-044482830-9/50019-9.
  17. Jan Friso Groote and Frits W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Inf. Comput., 100(2):202-260, 1992. URL: https://doi.org/10.1016/0890-5401(92)90013-6.
  18. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. Assoc. Comput. Mach., 32:137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
  19. Charles A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. Google Scholar
  20. Robert M. Keller. Formal verification of parallel programs. Commun. ACM, 19(7):371-384, 1976. URL: https://doi.org/10.1145/360248.360251.
  21. Robin Milner. Communication and Concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  22. Faron Moller. Axioms for Concurrency. PhD thesis, Department of Computer Science, University of Edinburgh, 1989. Report CST-59-89. Also published as ECS-LFCS-89-84. Google Scholar
  23. 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.
  24. Faron Moller. The nonexistence of finite axiomatisations for CCS congruences. In Proceedings of LICS '90, pages 142-153. IEEE Computer Society, 1990. URL: https://doi.org/10.1109/LICS.1990.113741.
  25. David M.R. Park. Concurrency and automata of infinite sequences. In 5^th GI Conference, volume 104 of LNCS, pages 167-183. Springer, 1981. Google Scholar
  26. Gordon D. Plotkin. A structural approach to operational semantics. Report DAIMI FN-19, Aarhus University, 1981. Google Scholar
  27. William C. Rounds and Stephen D. Brookes. Possible futures, acceptances, refusals, and communicating processes. In Proceedings of Annual Symposium on Foundations of Computer Science, pages 140-149, 1981. URL: https://doi.org/10.1109/SFCS.1981.36.
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