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

TL;DR

This paper revises the operational semantics of sequential composition to eliminate transparency issues, enabling better correspondence between process classes and establishing the reactive Turing power of TCP with iteration.

Contribution

It introduces a new operational semantics for sequential composition that removes transparency, improving process expressiveness and theoretical properties.

Findings

Eliminates transparency in sequential composition

Establishes correspondence between context-free and pushdown processes

Proves reactive Turing powerfulness of TCP with iteration

Abstract

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.