Constructing Witnesses for Lower Bounds on Behavioural Distances
Ruben Turkenburg, Harsh Beohar, Franck van Breugel, Clemens Kupke, Jurriaan Rot
TL;DR
This work tackles lower bounds on behavioural distances for labelled Markov chains by introducing an inductive derivation system that yields finite witnessing proofs. It establishes soundness and approximate completeness with respect to the least fixed point distance defined via non-expansive liftings, and builds a constructive bridge between proofs and a modal logic with quantitative semantics that can produce witnessing formulas. The framework handles infinite-state systems by focusing on finite supports and rational-valued maps, and demonstrates practical improvements in witness size over prior approaches through examples like random walks. By integrating proof systems, linear programming witnesses, and logic, it provides a practical methodology for evidencing behavioural distinctions between states and lays groundwork for broader coalgebraic extensions.
Abstract
Behavioural distances provide a robust alternative to notions of equivalence such as bisimilarity in the context of probabilistic transition systems. They can be defined as least fixed points, whose universal property allows us to exhibit upper bounds on the distance between states, showing them to be at most some distance apart. In this paper, we instead consider the problem of bounding distances from below, showing states to be at least some distance apart. Contrary to upper bounds, it is possible to reason about lower bounds inductively. We exploit this by giving an inductive derivation system for lower bounds on an existing definition of behavioural distance for labelled Markov chains. This is inspired by recent work on apartness as an inductive counterpart to bisimilarity. Proofs in our system will be shown to closely match the behavioural distance by soundness and (approximate) completeness results. We further provide a constructive correspondence between our derivation system and formulas in a modal logic with quantitative semantics. This logic was used in recent work of Rady and van Breugel to construct evidence for lower bounds on behavioural distances. Our constructions provide smaller witnessing formulas in many examples.