Sequencing and intermediate acceptance: axiomatisation and decidability of bisimilarity

Astrid Belder, Bas Luttik, Jos Baeten

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Downloads (Pure)

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.

Original languageEnglish
Title of host publication8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019
EditorsMarkus Roggenbach, Ana Sokolova
PublisherSchloss Dagstuhl - Leibniz-Zentrum für Informatik
Number of pages22
ISBN (Electronic)978-3-95977-120-7
DOIs
Publication statusPublished - Nov 2019
Event8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019 - London, United Kingdom
Duration: 3 Jun 20196 Jun 2019

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume139
ISSN (Print)1868-8969

Conference

Conference8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019
CountryUnited Kingdom
CityLondon
Period3/06/196/06/19

Keywords

  • Axiomatisation
  • Bisimilarity
  • Decidability
  • Sequencing
  • Sequential composition

Fingerprint Dive into the research topics of 'Sequencing and intermediate acceptance: axiomatisation and decidability of bisimilarity'. Together they form a unique fingerprint.

  • Cite this

    Belder, A., Luttik, B., & Baeten, J. (2019). Sequencing and intermediate acceptance: axiomatisation and decidability of bisimilarity. In M. Roggenbach, & A. Sokolova (Eds.), 8th Conference on Algebra and Coalgebra in Computer Science, CALCO 2019 [11] (Leibniz International Proceedings in Informatics, LIPIcs; Vol. 139). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.CALCO.2019.11