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.

翻译：行为距离提供了一种定量方法，用于比较转移系统的状态，超越了传统布尔等价概念。本文利用米尔纳图（一种通过纳入可变输出而推广有限状态自动机的模型），为非确定性过程建立了一个完备且一致的行为距离公理化。米尔纳图为研究行为距离提供了引人注目的框架，因为它将焦点从语言等价转向了互模拟等价。其公理化研究为更富表达力模型（如加权转移系统）的定量分析奠定了基础。为形式化该方法，我们选择串图作为语法载体。串图不仅紧密映射了米尔纳图的图结构，还提供了支持归纳推理与组合语义的严谨形式体系。有别于需要绑定器与替换机制等附加手段的传统代数语法，串图提供了无变量表示，其中递归可自然分解为更简单的组件。这使其非常适于行为距离推理，并与通过统一图式框架公理化自动机理论等价的更广泛努力相一致。