A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions

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.