Sequential Composition in the Presence of Intermediate Termination (Extended Abstract)

Jos Baeten
(CWI and University of Amsterdam)
Bas Luttik
(Eindhoven University of Technology)
Fei Yang
(Eindhoven University of Technology)

The standard operational semantics of the sequential composition operator gives rise to unbounded branching and forgetfulness when transparent process expressions are put in sequence. Due to transparency, the correspondence between context-free and pushdown processes fails modulo bisimilarity, and it is not clear how to specify an always terminating half counter. We propose a revised operational semantics for the sequential composition operator in the context of intermediate termination. With the revised operational semantics, we eliminate transparency, allowing us to establish a close correspondence between context-free processes and pushdown processes. Moreover, we prove the reactive Turing powerfulness of TCP with iteration and nesting with the revised operational semantics for sequential composition.

In Kirstin Peters and Simone Tini: Proceedings Combined 24th International Workshop on Expressiveness in Concurrency and 14th Workshop on Structural Operational Semantics (EXPRESS/SOS 2017), Berlin, Germany, 4th September 2017, Electronic Proceedings in Theoretical Computer Science 255, pp. 1–17.
Published: 31st August 2017.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: