Constructing witnesses for lower bounds on behavioural distances

Tools

Turkenburg, Ruben and Beohar, Harsh and van Breugel, Franck and Kupke, Clemens and Rot, Jurriaan; Guerrini, Stefano and Konig, Barbara, eds. (2026) Constructing witnesses for lower bounds on behavioural distances. In: 34th EACSL Annual Conference on Computer Science Logic, CSL 2026. Leibniz International Proceedings in Informatics, LIPIcs, 363 . Schloss Dagstuhl - Leibniz-Zentrum für Informatik. ISBN 9783959774116 (https://doi.org/10.4230/LIPIcs.CSL.2026.25)

[thumbnail of Turkenburg-etal-2026-Constructing-witnesses-for-lower-bounds-on-behavioural-distances]
Preview
 Text. Filename: Turkenburg-etal-2026-Constructing-witnesses-for-lower-bounds-on-behavioural-distances.pdf
Final Published Version
License: Creative Commons Attribution 4.0 logo
Download (1MB)| Preview

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.

ORCID iDs

Turkenburg, Ruben, Beohar, Harsh, van Breugel, Franck, Kupke, Clemens ORCID logoORCID: https://orcid.org/0000-0002-0502-391X and Rot, Jurriaan; Guerrini, Stefano and Konig, Barbara
CORE (COnnecting REpositories)