A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909003301257216 |
|---|---|
| author | Różowski, Wojciech Piedeleu, Robin Silva, Alexandra Zanasi, Fabio |
| author_facet | Różowski, Wojciech Piedeleu, Robin Silva, Alexandra Zanasi, Fabio |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_27268 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes Różowski, Wojciech Piedeleu, Robin Silva, Alexandra Zanasi, Fabio Logic in Computer Science Formal Languages and Automata Theory Programming Languages 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. |
| title | A Diagrammatic Axiomatisation of Behavioural Distance of Nondeterministic Processes |
| topic | Logic in Computer Science Formal Languages and Automata Theory Programming Languages |
| url | https://arxiv.org/abs/2604.27268 |