Astrid Belder: Decidability of bisimilarity and axiomatisation for sequential processes in the presence of intermediate termination

Event Details

An alternative semantics for sequential composition in a setting with intermediate termination was proposed in a recent article by Baeten, Luttik and Yang. We consider two open questions regarding sequential processes with intermediate termination that use the revised semantics for sequential composition (TSP;). First, a ground-complete axiomatisation is proposed for TSP;, extended with an auxiliary operator that is used to remove intermediate termination from terms. Additionally, it is shown that TSP; does not afford a ground-complete axiomatisation with respect to bisimilarity without an auxiliary operator. Second, we prove that bisimilarity is decidable for processes definable by finite guarded recursive specification over TSP;. This is done by showing that every guarded recursive TSP;-specification can be transformed to a normal form, which allows us to eliminate redundant intermediate termination from processes. Using this normal form, the existing decidability proofs for context-free processes without intermediate termination, can be adapted for TSP;.