A Complete Axiomatisation for Divergence Preserving Branching Congruence of Finite-State Behaviours

TL;DR

This paper introduces a complete set of axioms for divergence preserving branching congruence in finite-state behaviors, resolving a long-standing open problem since 1993.

Contribution

It provides a sound and complete equational inference system specifically tailored for divergence sensitive semantics, refining previous axiomatizations.

Findings

The inference system is proven sound and complete.

It refines Rob van Glabbeek's axiomatization by removing an unsound axiom.

The system addresses divergence preserving branching congruence.

Abstract

We present an equational inference system for finite-state expressions, and prove that the system is sound and complete with respect to divergence preserving branching congruence, closing a problem that has been open since 1993. The inference system refines Rob van Glabbeek's simple and elegant complete axiomatisation for branching bisimulation congruence of finite-state behaviours by joining four simple axioms after dropping one axiom which is unsound under the more refined divergence sensitive semantics.