A Complete Quantitative Axiomatisation of Behavioural Distance of Regular Expressions

TL;DR

This paper provides a comprehensive axiomatic framework for quantifying behavioural distances between regular expressions, using a novel quantitative logic approach to measure how similar automata states are.

Contribution

It introduces a complete axiomatisation for behavioural distance of regular languages based on a new quantitative equational logic, bridging automata theory and metric reasoning.

Findings

Established a sound and complete axiomatization for behavioural distance

Utilized order theory and Banach spaces to simplify distance calculations

Demonstrated the applicability of quantitative logic to automata behavioural analysis

Abstract

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.