arxiv: 2604.27268 · v1 · submitted 2026-04-29 · 💻 cs.LO · cs.FL· cs.PL

Recognition: unknown

A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes

Wojciech R\'o\.zowski , Robin Piedeleu , Alexandra Silva , Fabio Zanasi

Authors on Pith no claims yet

Pith reviewed 2026-05-07 09:34 UTC · model grok-4.3

classification 💻 cs.LO cs.FLcs.PL

keywords behavioural distancenondeterministic processesstring diagramsMilner's chartsaxiomatisationbisimilarityquantitative semantics

0 comments

The pith

String diagrams supply a sound and complete axiomatisation of behavioural distance for nondeterministic processes using Milner's charts.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out to replace yes-or-no equivalence checks with a quantitative measure of how far apart the behaviours of two nondeterministic processes are. It encodes the processes as Milner's charts, which extend automata with outputs, and then writes the distance axioms in string-diagram syntax. The diagrams give a variable-free way to decompose recursive definitions into smaller pieces while preserving compositionality. A reader would care because the result moves quantitative reasoning about approximate equivalence into a clean graphical calculus that avoids binders and substitution. This supplies the first complete axiomatic treatment of behavioural distance in this setting and prepares the ground for similar treatments of richer models.

Core claim

We develop a sound and complete axiomatisation of behavioural distance for nondeterministic processes by representing them as Milner's charts and equipping the charts with string-diagram syntax, in which recursion decomposes directly into simpler components without the need for binders or substitution.

What carries the argument

Milner's charts equipped with string-diagram syntax, which gives a graphical, variable-free representation of processes and their behavioural distances.

If this is right

Behavioural distances between nondeterministic processes become derivable by purely diagrammatic manipulations.
The same syntax and axiomatisation extend, at least in principle, to quantitative analysis of weighted transition systems.
Recursion in process definitions is handled by local decomposition rather than global substitution.
Compositional reasoning about distances follows directly from the diagrammatic semantics.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The diagrammatic style could be lifted to probabilistic or continuous-state systems by replacing the underlying algebra of charts.
A similar axiomatisation might unify several automata equivalences under one graphical framework.
Tool builders could implement the axioms as rewrite rules inside existing diagram editors for approximate equivalence checking.

Load-bearing premise

The chosen string-diagram syntax together with the model of charts admits a sound and complete axiomatisation of behavioural distance without extra mechanisms such as binders.

What would settle it

A pair of charts whose behavioural distance, computed directly from the transition structure, cannot be derived from or is contradicted by the proposed axioms.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives a string-diagram axiomatisation for behavioural distances on Milner's charts and claims soundness plus completeness, but the quantitative fixed-point details are the part that needs the closest look.

read the letter

This paper gives a string-diagram axiomatisation for behavioural distances on Milner's charts and claims soundness plus completeness, but the quantitative fixed-point details are the part that needs the closest look. The authors move from the usual Boolean bisimilarity to a metric version and do it without the binders and substitution that algebraic syntax normally requires. That variable-free handling of recursion is the concrete advance here, and it fits the graphical shape of charts in a way that feels natural for compositional reasoning. The choice of charts as the model also makes sense because it keeps the focus on bisimilarity while opening the door to weighted systems later. Those are the parts that land cleanly. The rest of the contribution is mostly groundwork rather than a fully worked-out theory for distances yet. On the soft spots, the central claim rests on the diagrammatic rules capturing the least-fixed-point definition of the distance, including the suprema over nondeterministic choices and infima over matching transitions. The abstract says recursion decomposes into simpler components, but it is not obvious from the summary whether the axioms preserve the metric structure for values strictly between zero and one. If the rules only work cleanly for the zero-one case or if some matching step loses the quantitative information, completeness would fail. The full text presumably contains the proofs and the explicit axioms, so the gap may be filled there, but the stress-test concern about faithful encoding of the fixed-point operator is worth checking directly. This work is for readers already comfortable with coalgebra, string diagrams, and process algebra. Someone who knows the standard coalgebraic definition of behavioural distance will see the value in the new syntax and the extension to charts. It is not a paper that stands alone for a general audience. It deserves a serious referee because the idea is a clear step in making quantitative equivalences axiomatic in a diagrammatic setting, and the authors have stated the scope and the intended follow-on work without overclaiming. I would send it to peer review.

Referee Report

2 major / 1 minor

Summary. The paper claims to develop a sound and complete axiomatisation of behavioural distance for nondeterministic processes, modeled via Milner's charts, by adopting string diagrams as a variable-free syntax in which recursion decomposes naturally into simpler components, thereby extending qualitative bisimilarity to a quantitative setting and laying groundwork for more expressive models such as weighted transition systems.

Significance. If the soundness and completeness claims hold, the work would offer a compositional, diagrammatic framework for quantitative process semantics that unifies qualitative and metric-based reasoning without binders or substitution, potentially enabling inductive proofs for distances in chart-like models and facilitating extensions to weighted automata.

major comments (2)

[Abstract] The abstract asserts soundness and completeness of the axiomatisation but supplies no proof sketch, definitions of the behavioural distance (as the least fixed point of a monotone operator), or verification steps; without these the central claim cannot be assessed and major derivation gaps remain.
[The manuscript] The central claim requires that the chosen string-diagram syntax and chart semantics admit a sound and complete axiomatisation for the least-fixed-point behavioural distance (suprema over nondeterministic choices, infima over matching transitions). No section or equation supplies an explicit fixed-point axiom or proves that the diagrammatic semantics coincides with the standard metric on the final coalgebra, which is load-bearing for distances strictly between 0 and 1.

minor comments (1)

The abstract states that charts generalise finite-state automata by incorporating variable outputs and shift focus to bisimilarity; a brief inline definition or reference to the precise coalgebraic semantics of charts would improve accessibility for readers unfamiliar with Milner's model.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and valuable comments. We have carefully considered each point and made revisions to improve the clarity of our presentation regarding the soundness and completeness of the axiomatisation.

read point-by-point responses

Referee: [Abstract] The abstract asserts soundness and completeness of the axiomatisation but supplies no proof sketch, definitions of the behavioural distance (as the least fixed point of a monotone operator), or verification steps; without these the central claim cannot be assessed and major derivation gaps remain.

Authors: We agree that the abstract, being concise, does not include these details. To address this, we have revised the abstract to briefly define the behavioural distance as the least fixed point of the monotone operator and provide a high-level sketch of the soundness and completeness proofs. The detailed definitions, axioms, and proofs are contained in the body of the paper, specifically in Sections 3 (syntax and semantics) and 4 (axiomatisation and proofs). revision: yes
Referee: [The manuscript] The central claim requires that the chosen string-diagram syntax and chart semantics admit a sound and complete axiomatisation for the least-fixed-point behavioural distance (suprema over nondeterministic choices, infima over matching transitions). No section or equation supplies an explicit fixed-point axiom or proves that the diagrammatic semantics coincides with the standard metric on the final coalgebra, which is load-bearing for distances strictly between 0 and 1.

Authors: While the string diagram syntax encodes the recursive structure that corresponds to the least fixed point of the behavioural distance operator, we acknowledge that an explicit fixed-point axiom and a direct proof of coincidence with the final coalgebra metric were not sufficiently highlighted. We have added an explicit axiom capturing the fixed-point property in the diagrammatic calculus and strengthened the proof in the relevant theorem to explicitly verify the match with the standard metric, including for distances in (0,1). revision: yes

Circularity Check

0 steps flagged

No circularity: axiomatisation developed from string-diagram syntax and chart semantics

full rationale

The paper claims to develop a sound and complete axiomatisation of behavioural distance for nondeterministic processes via Milner's charts and string diagrams. The abstract describes string diagrams as providing a variable-free representation where recursion decomposes naturally, but this is presented as a syntactic choice enabling inductive reasoning rather than a reduction of the target distance to its own inputs by definition or fit. No equations, self-citations, or uniqueness theorems are quoted that would force the completeness result to be equivalent to the semantics by construction. The approach is self-contained against external coalgebraic notions of behavioural distance, with no load-bearing self-referential steps visible.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the assumption that string diagrams provide compositional semantics and inductive reasoning for behavioural distance; no free parameters or invented entities are introduced in the abstract.

axioms (2)

domain assumption String diagrams closely mirror the graphical structure of charts and support inductive reasoning and compositional semantics.
Invoked to justify the choice of syntax over traditional algebraic representations.
standard math Charts generalise finite-state automata by incorporating variable outputs and shift focus from language equivalence to bisimilarity.
Stated as the model providing a compelling setting for behavioural distances.

pith-pipeline@v0.9.0 · 5494 in / 1204 out tokens · 46899 ms · 2026-05-07T09:34:56.398012+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

3 extracted references · 3 canonical work pages

[1]

29 Dexter Kozen

URL:https://arxiv.org/abs/1704.08668,arXiv:1704.08668. 29 Dexter Kozen. A completeness theorem for kleene algebras and the algebra of regular events. Inf. Comput., 110(2):366–390, 1994. URL:https://doi.org/10.1006/inco.1994.1037, doi: 10.1006/INCO.1994.1037. 30 Kim G. Larsen, Uli Fahrenberg, and Claus R. Thrane. Metrics for weighted transition systems: Ax...

work page doi:10.1006/inco.1994.1037 1994
[2]

48550/ARXIV.2408.14701

URL: https://doi.org/10.48550/arXiv.2408.14701, arXiv:2408.14701, doi:10. 48550/ARXIV.2408.14701. 39 Robin Piedeleu and Fabio Zanasi. A finite axiomatisation of finite-state automata using string diagrams.Log. Methods Comput. Sci., 19(1), 2023. URL: https://doi.org/10.46298/ lmcs-19(1:13)2023,doi:10.46298/LMCS-19(1:13)2023. 40 Robin Piedeleu and Fabio Zan...

work page doi:10.48550/arxiv.2408.14701 2023
[3]

A Appendix A.1 Algebra of Regular Behaviours In the appendix, we rely on a slightly different, but equivalent [34], characterisation of the setΩof all regular behaviours

URL: https://www.sciencedirect.com/science/article/pii/S0890540198927468, doi:10.1006/inco.1998.2746. A Appendix A.1 Algebra of Regular Behaviours In the appendix, we rely on a slightly different, but equivalent [34], characterisation of the setΩof all regular behaviours. In this section, we elaborate on this characterisation and related conventions. In p...

work page doi:10.1006/inco.1998.2746 1998