Reference. A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes

Wojciech Różowski, Robin Piedeleu, Alexandra Silva, Fabio Zanasi · ICALP · 2026 · coalgebra string-diagrams · DOI · arXiv
Behavioural distances provide a quantitative approach to comparing the states of transition systems, moving beyond traditional Boolean notions of equivalence. In this paper, we develop a sound and complete axiomatisation of behavioural distance for nondeterministic processes using Milner’s charts, a model that generalises finite-state automata by incorporating variable outputs. Charts provide a compelling setting for studying behavioural distances because they shift the focus from language equivalence to bisimilarity. Their axiomatic study lays the groundwork for quantitative analysis of more expressive models, such as weighted transition systems. To formalise this approach, we adopt string diagrams as our syntax of choice. String diagrams closely mirror the graphical structure of charts, while providing a rigorous formalism that supports inductive reasoning and compositional semantics. Unlike traditional algebraic syntaxes, which require additional mechanisms such as binders and substitution, string diagrams offer a variable-free representation where recursion naturally decomposes into simpler components. This makes them well-suited for reasoning about behavioural distances and aligns with broader efforts to axiomatise automata-theoretic equivalences through a unified diagrammatic framework.

Cite
Cite as @rozowski-2026-a (helia, typst) · \cite{rozowski-2026-a} (LaTeX)
BibTeX
bibtex · 14 lines
@inproceedings{rozowski-2026-a,
  doi = {10.4230/LIPICS.ICALP.2026.190},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2026.190},
  author = {Różowski, Wojciech and Piedeleu, Robin and Silva, Alexandra and Zanasi, Fabio},
  keywords = {behavioural distance, quantitative equational reasoning, string diagrams, Theory of computation},
  language = {en},
  title = {A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes},
  volume = {374},
  pages = {190:1-190:20},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2026},
  copyright = {Creative Commons Attribution 4.0 International license},
  booktitle = {53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)}
}
hayagriva YAML (typst)
yaml · 18 lines
rozowski-2026-a:
  type: article
  title: A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes
  author:
  - Różowski, Wojciech
  - Piedeleu, Robin
  - Silva, Alexandra
  - Zanasi, Fabio
  date: 2026
  page-range: 190:1-190:20
  url: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2026.190
  serial-number:
    doi: 10.4230/LIPICS.ICALP.2026.190
  parent:
    type: proceedings
    title: 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026)
    publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
    volume: 374
Download: rozowski-2026-a.bib · rozowski-2026-a.yml
Cites 55 works (4 here)
With notes (4)

CF-GKAT: Efficient Validation of Control-Flow Transformations zhang-2025-cfPOPL · 2025
Guarded Kleene Algebra with Tests (GKAT) provides a sound and complete framework to reason about trace equivalence between simple imperative programs. However, there are still several notable limitations. First, GKAT is completely agnostic with respect to the meaning of primitives, to keep equivalence decidable. Second, GKAT excludes non-local control flow such as goto, break , and return . To overcome these limitations, we introduce Control-Flow GKAT (CF-GKAT) , a system that allows reasoning about programs that include non-local control flow as well as hardcoded values. CF-GKAT is able to soundly and completely verify trace equivalence of a larger class of programs, while preserving the nearly-linear efficiency of GKAT. This makes CF-GKAT suitable for the verification of control-flow manipulating procedures, such as decompilation and goto-elimination. To demonstrate CF-GKAT’s abilities, we validated the output of several highly non-trivial program transformations, such as Erosa and Hendren’s goto -elimination procedure and the output of Ghidra decompiler. CF-GKAT opens up the application of Kleene Algebra to a wider set of challenges, and provides an important verification tool that can be applied to the field of decompilation and control-flow transformation.
PDF · DOI · arXiv · pldb

Guarded Kleene algebra with tests: verification of uninterpreted programs in nearly linear time smolka-2019-guardedPOPL · 2020
Guarded Kleene Algebra with Tests (GKAT) is a variation on Kleene Algebra with Tests (KAT) that arises by restricting the union (+) and iteration (*) operations from KAT to predicate-guarded versions. We develop the (co)algebraic theory of GKAT and show how it can be efficiently used to reason about imperative programs. In contrast to KAT, whose equational theory is PSPACE-complete, we show that the equational theory of GKAT is (almost) linear time. We also provide a full Kleene theorem and prove completeness for an analogue of Salomaa’s axiomatization of Kleene Algebra.
PDF · DOI · arXiv · pldb

NetKAT: Semantic foundations for networks anderson2014netkatPOPL · 2014
Recent years have seen growing interest in high-level languages for programming networks. But the design of these languages has been largely ad hoc, driven more by the needs of applications and the capabilities of network hardware than by foundational principles. The lack of a semantic foundation has left language designers with little guidance in determining how to incorporate new features, and programmers without a means to reason precisely about their code. This paper presents NetKAT, a new network programming language that is based on a solid mathematical foundation and comes equipped with a sound and complete equational theory. We describe the design of NetKAT, including primitives for filtering, modifying, and transmitting packets; union and sequential composition operators; and a Kleene star operator that iterates programs. We show that NetKAT is an instance of a canonical and well-studied mathematical structure called a Kleene algebra with tests (KAT) and prove that its equational theory is sound and complete with respect to its denotational semantics. Finally, we present practical applications of the equational theory including syntactic techniques for checking reachability, proving non-interference properties that ensure isolation between programs, and establishing the correctness of compilation algorithms.
PDF · DOI · pldb

A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events KOZEN1994366I&C · 1994
We give a finitary axiomatization of the algebra of regular events involving only equations and equational implications. Unlike Salomaa′s axiomatizations, the axiomatization given here is sound for all interpretations over Kleene algebras.
DOI
External (51)
rozowski-2026-a reference entries/refs/rozowski-2026-a/rozowski-2026-a.hel