A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes

TL;DR

This paper develops a sound and complete diagrammatic axiomatisation for behavioural distances in nondeterministic processes, using string diagrams to facilitate compositional reasoning.

Contribution

It introduces a novel diagrammatic formalism for behavioural distances, extending automata theory with a rigorous, variable-free graphical syntax.

Findings

Provides a formal, compositional framework for behavioural distances

Uses string diagrams to model charts and automata-like structures

Lays groundwork for quantitative analysis of weighted transition systems

Abstract

Behavioural distances provide a quantitative approach to comparing the states of transition systems, moving beyond traditional Boolean notions of equivalence. In this paper, we develop a sound and complete axiomatisation of behavioural distance for nondeterministic processes using Milner's charts, a model that generalises finite-state automata by incorporating variable outputs. Charts provide a compelling setting for studying behavioural distances because they shift the focus from language equivalence to bisimilarity. Their axiomatic study lays the groundwork for quantitative analysis of more expressive models, such as weighted transition systems. To formalise this approach, we adopt string diagrams as our syntax of choice. String diagrams closely mirror the graphical structure of charts, while providing a rigorous formalism that supports inductive reasoning and compositional semantics. Unlike traditional algebraic syntaxes, which require additional mechanisms such as binders and substitution, string diagrams offer a variable-free representation where recursion naturally decomposes into simpler components. This makes them well-suited for reasoning about behavioural distances and aligns with broader efforts to axiomatise automata-theoretic equivalences through a unified diagrammatic framework.