A Complete Axiom System for 1-Free Kleene Star Expressions under Bisimilarity: An Elementary Proof

TL;DR

This paper presents a simplified, elementary proof of a complete axiom system for 1-free Kleene star expressions under bisimilarity, along with a formal verification in Coq, making the proof more accessible and implementable.

Contribution

It offers a simpler, inductive proof of the axiom system's completeness and provides a formal Coq verification, improving understandability and potential automation.

Findings

Simpler proof relying on induction and normal forms

Complete verification of results in Coq

Closer to rewriting algorithms for process terms

Abstract

Grabmayer and Fokkink recently presented a finite and complete axiomatization for 1-free process terms over the binary Kleene star under bismilarity equivalence (proceedings of LICS 2020, preprint available). A different and considerably simpler proof is detailed in this paper. This result, albeit still somewhat technical, only relies on induction and normal forms and is therefore also much closer to a potential rewriting algorithm. In addition, a complete verification in the Coq proof assistant of all results in this work is provided, but correctness does not depend upon any computer-assisted methodology.