Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A General Completeness Theorem for Skip-free Star Algebras

Tobias Kappé, Todd Schmid

TL;DR

The paper tackles complete axiomatizations for bisimilarity in skip-free process algebras parametrized by an equational theory $\mathsf{T}$ that is both supported and malleable, via a free-algebra construction $(M,\eta,\rho)$. It develops a coalgebraic, subsystem-based framework with $M$-systems and well-layered charts, enabling a theory-parameterized generalization of Grabmayer–Fokkink's completeness approach to $\mathsf{T}^*$ and unifying existing results for $\mathsf{SL}^*$, $\mathsf{GA}^*$, $\mathsf{CA}^*$, and $\mathsf{GC}^*$, including new completeness theorems for skip-free probabilistic expressions. Central contributions include the notions of a supported malleable theory, a canonical solution to well-layered $M$-systems, and a modular proof strategy that yields completeness w.r.t. bisimilarity under broad but precise conditions, while clarifying the scope via negative results (e.g., $\mathsf{CS}$ is not malleable). The framework provides a path toward resolving open completeness questions for full GKAT and highlights the role of distributive laws and monad interactions in skip-free settings. Overall, the work offers a coherent, theory-parameterized methodology for proving completeness results across diverse skip-free process algebras with probabilistic and nondeterministic branching.

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.

A General Completeness Theorem for Skip-free Star Algebras

TL;DR

The paper tackles complete axiomatizations for bisimilarity in skip-free process algebras parametrized by an equational theory that is both supported and malleable, via a free-algebra construction . It develops a coalgebraic, subsystem-based framework with -systems and well-layered charts, enabling a theory-parameterized generalization of Grabmayer–Fokkink's completeness approach to and unifying existing results for , , , and , including new completeness theorems for skip-free probabilistic expressions. Central contributions include the notions of a supported malleable theory, a canonical solution to well-layered -systems, and a modular proof strategy that yields completeness w.r.t. bisimilarity under broad but precise conditions, while clarifying the scope via negative results (e.g., is not malleable). The framework provides a path toward resolving open completeness questions for full GKAT and highlights the role of distributive laws and monad interactions in skip-free settings. Overall, the work offers a coherent, theory-parameterized methodology for proving completeness results across diverse skip-free process algebras with probabilistic and nondeterministic branching.

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.
Paper Structure (2 sections, 2 theorems, 3 equations, 2 figures)

This paper contains 2 sections, 2 theorems, 3 equations, 2 figures.

Table of Contents

  1. Introduction
  2. 1-free Star Expressions

Key Result

lemma thmcounterlemma

Given states $x \in X$ and $y \in Y$ of charts $(X, \delta_X)$ and $(Y, \delta_Y)$, $x \mathrel{\raisebox{1pt}{$\underline{\leftrightarrow}$}} y$ if and only if there is a third chart $(Z, \delta_Z)$ and chart homomorphisms $h \colon (X, \delta_X) \to (Z, \delta_Z)$ and $k \colon (X, \delta_X) \to (

Figures (2)

  • Figure 1: Rules defining the transition structure of the syntactic chart $(\mathit{StExp}, \delta)$. In the above, $a \in \mathit{Act}$, $r_1,r_2,s \in \mathit{StExp}$, and $\xi \in \checkmark + \mathit{StExp}$.
  • Figure 2: The axioms proposed by Grabmayer and Fokkink in grabmayer-fokkink-2020. The theory $\mathsf{SL}^*$ consists of the axioms above and equational logic (not pictured above).

Theorems & Definitions (7)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • lemma thmcounterlemma
  • definition thmcounterdefinition
  • theorem thmcountertheorem: Soundness and completeness of $\mathsf{SL}^*$
  • definition thmcounterdefinition