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

One of the central topics in the study of concurrent systems are notions of system equivalence, which define when two given systemstates have the same behaviour in a given sense. Classically, i.e. over relational transition systems, such system semantics rangeon a spectrum between branching-time and linear-time equivalences, with each equivalence reflecting a notion of possible interaction with systems, and characterized by a dedicated modal logic. In this setting, equivalences and logics are two-valued, i.e. two states are either equivalent or inequivalent, and a formula is either satisfied or not satisfied in a given state. For systems involving quantitative data, such as probabilities, weights, or more generally values in some metric space, it has been recognized that quantitative notions of equivalence, i.e. behavioural distances, and quantitative logics are more suitable for some purposes, and enable a more fine-grained analysis. For instance, while two states in Markov chains with small differences in their transition probabilities are just inequivalent under two-valued probabilistic bisimilarity, a suitable behavioural distance will retain the information that the two states are not exactly equivalent but still quite similar.As indicated above, behavioural distances by their very nature apply to settings that deviate from the classical relational model; these settings are generally less standardized and vary quite widely. This creates a need for uniform methods that apply to many system types at once. For branching-time behavioural metrics, we have developed such methods in earlier work within the framework of universal coalgebra, which encapsulates system types as functors and systems as coalgebras for the given type functor. The objective of SpeQt is to additionally parametrize these methods over the system semantics, thus providing support for spectra of behavioural distances in coalgebraic generality.The key tool we foresee for such a parametrization are graded monads, which we have successfully used in earlier work to parametrize two-valued equivalences. Central research goals include game-theoretic and logical characterization and efficient calculation of distances. Our results will enable us to derive such logics, games and algorithms in a principled way for a whole range of different types of transition systems and for the full spectrum between branching-time and linear-time semantics. We plan to test and evaluate the resulting algorithms in case studies centered around conformance testing of hybrid systems and differential privacy.

• DFG Programme: Research Grants