A General Completeness Theorem for Skip-free Star Algebras

TL;DR

This paper establishes a comprehensive completeness theorem for skip-free star algebras, extending axiomatization of bisimilarity to probabilistic and guarded branching processes, unifying and generalizing previous results.

Contribution

It introduces a new completeness theorem for skip-free process algebras with probabilistic branching, generalizing prior axiomatizations of bisimilarity.

Findings

Proves a general completeness theorem for skip-free star algebras.

Extends axiomatization of bisimilarity to probabilistic guarded branching.

Unifies existing completeness results under a broader framework.

Abstract

We consider process algebras with branching parametrized by an equational theory T, and show that it is possible to axiomatize bisimilarity under certain conditions on T. Our proof abstracts an earlier argument due to Grabmayer and Fokkink (LICS'20), and yields new completeness theorems for skip-free process algebras with probabilistic (guarded) branching, while also covering existing completeness results.