Różowski, Wojciech Krzysztof; (2025) Completeness Theorems for Behavioural Distances and Equivalences. Doctoral thesis (Ph.D), UCL (University College London).

Preview

Text thesis.pdf - Accepted Version Download (1MB) | Preview

Abstract

In theoretical computer science, it is customary to provide expression languages for representing the behaviour of transition systems and to study formal systems for reasoning about the equivalence or similarity of behaviours represented by expressions of interest. The key example of this approach is Kleene's regular expressions, a specification language for deterministic finite automata, as well as complete axiomatisations of language equivalence of regular expressions due to Salomaa and Kozen. The first part of this thesis studies axiomatisations of behavioural distances. Originally considered for probabilistic and stochastic systems, behavioural distances provide a quantitative measure of the dissimilarity of behaviours that can be defined meaningfully for a variety of transition systems. As a first contribution, we consider deterministic automata and provide a sound and complete quantitative inference system for reasoning about the shortest-distinguishing-word distance between languages represented by regular expressions. Then, we move on to a more complicated case of behavioural distance of Milner's charts, which provide a compelling setting for studying behavioural distances because they shift the focus from language equivalence to bisimilarity. As a syntax of choice, we rely on string diagrams, which provide a rigorous formalism that enables compositional reasoning by supporting a variable-free representation where recursion naturally decomposes into simpler components. The second part focuses on generative probabilistic transition systems and presents a sound and complete axiomatisation of language equivalence of behaviours specified through the syntax of probabilistic regular expressions (PRE), a probabilistic analogue of regular expressions denoting probabilistic languages in which every word is assigned a probability of being generated. The completeness proof makes use of technical tools from the recently developed theory of proper functors and convex algebra, arising from the rich structure of probabilistic languages.

Download activity - last month

Export as CSVXMLJSON

Download activity - last 12 months

Export as XMLCSVJSON

Downloads by country - last 12 months

Export as JSONCSVXML

Archive Staff Only

View Item