Spectra of Behavioural Distances and Quantitative Logics

• Applicants: Professorin Dr. Barbara König; Professor Dr. Lutz Schröder
• Subject Area: Theoretical Computer Science
• Term: since 2020
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 434050016

A central task in the analysis of systems is the comparison of states with respect to their observable behaviour. While classically this often takes the shape of yes-or-no checks for, e.g., bisimilarity or language inclusion, measuring behavioural distances between states is often more appropriate when systems involve quantitative data such as probabilities or transition weights. Like two-valued comparisons, notions of behavioural distance vary in granularity on a linear-time/branching-time spectrum ranging from bisimilarity distances to trace-type distances. The aim of the SpeQt project is to provide a uniform semantic, logical, and algorithmic treatment of a broad variety of behavioural distances by parametrizing along three axes of generality: We encapsulate the system type as a functor on a suitable base category in the paradigm of universal coalgebra; we capture the granularity of behavioural equivalences or metrics using Galois connections and the emerging universal-algebraic notion of graded monads; and we let distances take values in a quantale, which in particular covers the two-valued case by instantiating to the quantale of Boolean truth values, and the metric case by instantiating to the unit interval quantale. Target results in this setting include the identification of expressive quantitative modal logics in generalization of the classical Hennessy-Milner theorem and the development of game-based characterizations of behavioural distances. Throughout, we aim not only to cover existing results but also to enable the generation of new results for concrete distances and system types by instantiation of the general framework. A particular focus in the second project phase SpeQt2 will lie on the algorithmic treatment of behavioural distances, both in the sense of computing distances and in the sense of certifying bounds on behavioural distance, e.g. in terms of quantitative bisimulations, winning strategies in behavioural games, or distinguishing formulae. Additionally, we will pursue the theme of approximation, e.g. defining and computing behavioural distances in systems where quantities can only be sampled and are hence uncertain, as well as considering new notions of behavioural distance that involve approximative versions of transport problems.

• DFG Programme: Research Grants