Document Open Access Logo

Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity

Authors Astrid Belder, Bas Luttik, Jos Baeten

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2019.11.pdf
  • Filesize: 0.56 MB
  • 22 pages

Document Identifiers

Author Details

Astrid Belder
  • Eindhoven University of Technology, Eindhoven, The Netherlands
Bas Luttik
  • Eindhoven University of Technology, Eindhoven, The Netherlands
Jos Baeten
  • CWI, Amsterdam, The Netherlands
  • University of Amsterdam, Amsterdam, The Netherlands

Acknowledgements

We thank the anonymous reviewers for their elaborate reviews.

Cite AsGet BibTex

Astrid Belder, Bas Luttik, and Jos Baeten. Sequencing and Intermediate Acceptance: Axiomatisation and Decidability of Bisimilarity. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CALCO.2019.11

Abstract

The Theory of Sequential Processes includes deadlock, successful termination, action prefixing, alternative and sequential composition. Intermediate acceptance, which is important for the integration of classical automata theory, can be expressed through a combination of alternative composition and successful termination. Recently, it was argued that complications arising from the interplay between intermediate acceptance and sequential composition can be eliminated by replacing sequential composition by sequencing. In this paper we study the equational theory of the recursion-free fragment of the resulting process theory modulo bisimilarity, proving that it is not finitely based, but does afford a ground-complete axiomatisation if a unary auxiliary operator is added. Furthermore, we prove that bisimilarity is decidable for processes definable by means of a finite guarded recursive specification over the process theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
Keywords
  • Sequencing
  • Sequential composition
  • Bisimilarity
  • Axiomatisation
  • Decidability

Metrics

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

References

  1. Luca Aceto and Matthew Hennessy. Termination, Deadlock, and Divergence. J. ACM, 39(1):147-187, 1992. URL: https://doi.org/10.1145/147508.147527.
  2. Jos C. M. Baeten, Twan Basten, and Michel Reniers. Process algebra: equational theories of communicating processes, volume 50. Cambridge University Press, 2010. Google Scholar
  3. Jos C. M. Baeten, Pieter J. L. Cuijpers, Bas Luttik, and P. J. A. van Tilburg. A Process-Theoretic Look at Automata. In Farhad Arbab and Marjan Sirjani, editors, Proceedings of FSEN 2009, volume 5961 of LNCS, pages 1-33. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-11623-0_1.
  4. Jos C. M. Baeten, Pieter J. L. Cuijpers, and P. J. A. van Tilburg. A Context-Free Process as a Pushdown Automaton. In Franck van Breugel and Marsha Chechik, editors, Proceedings of CONCUR 2008, volume 5201 of LNCS, pages 98-113. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85361-9_11.
  5. Jos C. M. Baeten, Bas Luttik, Tim Muller, and Paul van Tilburg. Expressiveness modulo bisimilarity of regular expressions with parallel composition. Mathematical Structures in Computer Science, 26(6):933-968, 2016. URL: https://doi.org/10.1017/S0960129514000309.
  6. Jos C. M. Baeten, Bas Luttik, and Paul van Tilburg. Reactive Turing machines. Inf. Comput., 231:143-166, 2013. URL: https://doi.org/10.1016/j.ic.2013.08.010.
  7. Jos C. M. Baeten, Bas Luttik, and Fei Yang. Sequential Composition in the Presence of Intermediate Termination (Extended Abstract). In Kirstin Peters and Simone Tini, editors, Proceedings of EXPRESS/SOS 2017, volume 255 of EPTCS, pages 1-17, 2017. URL: https://doi.org/10.4204/EPTCS.255.1.
  8. Astrid Belder. Decidability of bisimilarity and axiomatisation for sequential processes in the presence of intermediate termination. Master’s thesis, Eindhoven University of Technology, 2018. Available from URL: https://research.tue.nl/en/studentTheses/decidability-of-bisimilarity-and-axiomatisation-for-sequential-pr.
  9. 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.
  10. Bard Bloom. When is Partial Trace Equivalence Adequate? Formal Asp. Comput., 6(3):317-338, 1994. URL: https://doi.org/10.1007/BF01215409.
  11. Roland N. Bol and Jan Friso Groote. The Meaning of Negative Premises in Transition System Specifications. J. ACM, 43(5):863-914, 1996. URL: https://doi.org/10.1145/234752.234756.
  12. Olaf Burkart, Didier Caucal, Faron Moller, and Bernhard Steffen. Verification on Infinite Structures. In J.A. Bergstra, A.J. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, pages 545-623. Elsevier, 2001. Google Scholar
  13. Søren Christensen, Hans Hüttel, and Colin Stirling. Bisimulation Equivalence is Decidable for All Context-Free Processes. Inf. Comput., 121(2):143-148, 1995. URL: https://doi.org/10.1006/inco.1995.1129.
  14. Rob J. van Glabbeek. The meaning of negative premises in transition system specifications II. J. Log. Algebr. Program., 60-61:229-258, 2004. URL: https://doi.org/10.1016/j.jlap.2004.03.007.
  15. Jan Friso Groote. Transition System Specifications with Negative Premises. Theor. Comput. Sci., 118(2):263-299, 1993. URL: https://doi.org/10.1016/0304-3975(93)90111-6.
  16. Stephen C. Kleene. Representation of Events in Nerve Nets and Finite Automata. Automata Studies, pages 3-41, 1956. Google Scholar
  17. Hans Leiß. Towards Kleene Algebra with Recursion. In Egon Börger, Gerhard Jäger, Hans Kleine Büning, and Michael M. Richter, editors, Proceedings of CSL '91, volume 626 of LNCS, pages 242-256. Springer, 1991. URL: https://doi.org/10.1007/BFb0023771.
  18. R. Milner. Communication and Concurrency. Prentice Hall, Englewood Cliffs, 1989. Google Scholar
  19. Faron Moller. Infinite Results. In Ugo Montanari and Vladimiro Sassone, editors, Proceedings of CONCUR '96, volume 1119 of Lecture Notes in Computer Science, pages 195-216. Springer, 1996. URL: https://doi.org/10.1007/3-540-61604-7_56.
  20. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction, number 52 in Cambridge Tracts in Theoretical Computer Science, pages 233–-289. Cambridge University Press, 2012. Google Scholar
  21. Peter Thiemann. Partial Derivatives for Context-Free Languages - From μ-Regular Expressions to Pushdown Automata. In Javier Esparza and Andrzej S. Murawski, editors, Proceedings of FOSSACS 2017, volume 10203 of LNCS, pages 248-264, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_15.
  22. Chris Verhoef. A General Conservative Extension Theorem in Process Algebra. In Ernst-Rüdiger Olderog, editor, Proceedings of PROCOMET'94, volume A-56 of IFIP Transactions, pages 149-168. North-Holland, 1994. Google Scholar
  23. Chris Verhoef. A Congruence Theorem for Structured Operational Semantics with Predicates and Negative Premises. Nord. J. Comput., 2(2):274-302, 1995. Google Scholar
  24. Jos L. M. Vrancken. The Algebra of Communicating Processes With Empty Process. Theor. Comput. Sci., 177(2):287-328, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00250-2.
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