Deterministic automata have been traditionally studied through the point of view of language equivalence, but another perspective is given by the canonical notion of shortest-distinguishing-word distance quantifying the of states. Intuitively, the longer the word needed to observe a difference between two states, then the closer their behaviour is. In this paper, we give a sound and complete axiomatisation of shortest-distinguishing-word distance between regular languages. Our axiomatisation relies on a recently developed quantitative analogue of equational logic, allowing to manipulate rational-indexed judgements of the form $e \equiv_\varepsilon f$ meaning term $e$ is approximately equivalent to term $f$ within the error margin of $\varepsilon$. The technical core of the paper is dedicated to the completeness argument that draws techniques from order theory and Banach spaces to simplify the calculation of the behavioural distance to the point it can be then mimicked by axiomatic reasoning.

翻译：确定性自动机传统上通过语言等价的视角进行研究，但另一种视角由最短区分词距离的规范概念给出，该距离用于量化状态之间的接近程度。直观上，观测两个状态差异所需的词越长，它们的行为就越接近。本文给出了正则语言之间最短区分词距离的可靠且完全的公理化。我们的公理化依赖于最近发展的等式逻辑的量化类比，允许处理形如$e \equiv_\varepsilon f$的理性指标判断，其含义是项$e$在误差范围$\varepsilon$内近似等价于项$f$。本文的技术核心在于完全性论证，该论证借助序理论和巴拿赫空间技术，将行为距离的计算简化至可通过公理推理模拟的程度。