The Model Theory of Quantitative Coalgebraic Modal Logics
Die Modelltheorie der Quantitativen Koalgebraischen Modallogik
Creators: name: Wild, Paul
Publisher: name: Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU)
Year: 2024
Subjects: Coalgebra
Modal Logic
Category Theory
Behavioural Distance
Lax Extension

description: When reasoning about state-based systems, a central concern is usually to compare them only in terms of their behaviour, i.e. by the types of state transitions they can make, but otherwise regarding the states as indistinguishable. This approach is applied to a multitude of different systems, including labelled transition systems, Kripke frames and automata, and in particular also to systems with quantitative data, such as metric transition systems or Markov chains. A key notion in this regard is that of bisimilarity, which itself comes in a variety of shapes, including classical bisimulation for transition systems and probabilistic bisimulation for systems based on Markov chains. Both the system types and their notions of bisimilarity may be uniformly modelled using the methods of universal coalgebra, where a coalgebra is a map that assigns to each state a structured set of successors, with the structure dictated by a set functor chosen such that it models one time step in the behaviour of the states. For systems containing quantitative information like probabilities or fuzzy truth statements, bisimilarity is often an unsuitable analysis tool, as it is purely qualitative and as such tends to discard this quantitative information. For this reason, these systems are instead often analyzed by means of behavioural distances, which quantify the discrepancy in behaviour of two states as a distance value between 0 and 1 instead of mapping each pair of states to either of these extremes. Classically, bisimilarity has a tight connection with modal logic, exemplified by the property that any pair of bisimilar states satisfy the same modal formulae, or equivalently that each formula of modal logic is bisimulation-invariant. In the context of this thesis, we have particular interest in two more theorems, which each provide a converse of this bisimulation invariance in their own right. The first theorem, due to Hennessy and Milner, states that, in systems with finite branching, logical indistinguishability implies bisimilarity. The second theorem, due to van Benthem, characterizes modal logic as being exactly the fragment of first-order logic that is bisimulation-invariant. In this thesis, we work out quantitative analogues of both of these theorems along three axes of generalization. First, by keeping a coalgebraic level of generality, we cover a large number of system types. Second, we use quantales to abstract over the range of values of logics and distances, allowing us to apply our results to Boolean logics and equivalences, to fuzzy logics and pseudometrics, and to even more general notions of distances. Third, we stay parametric in deciding whether distances should be subject to a symmetry condition or not, which amounts to the simultaneous treatment of notions of simulation and bisimulation alike. At this level of generality, the technical realization of behavioural distances is typically achieved by lifting the functor describing the system type at hand from the category of sets to that of quantale-valued distances. These functor liftings, in turn, are often extracted from so-called lax extensions, which are native to the category of quantale-valued relations and as such allow for the comparison of states living in different systems. One of the most important constructions of such lax extensions is the coalgebraic Kantorovich extension, which is parametric in a set of predicate liftings and instantiates to a number of well-known examples. In fact, we show as part of this thesis that this ubiquity of the Kantorovich extension is not by chance, as (assuming suitable conditions on the functor) every lax extension can be expressed in Kantorovich form wrt. a suitable set of predicate liftings. We also show that within these conditions the aforementioned theorems by Hennessy/Milner and van Benthem carry over to this highly general setting. Summing up, the contents of this thesis both provide a common umbrella for a number of well-known results as well as offering some entirely new results, as in the case of certain convex-nondeterministic distances.
description: In der Theorie der zustandsbasierten Systeme befasst man sich oft mit dem Problem, Zustände dieser Systeme anhand ihres Verhaltens zu analysieren und zu vergleichen. Es gibt dabei Interesse an einer Vielzahl verschiedener Systeme, wie etwa Transitionssytemen, Kripke-Rahmen, Automaten, aber auch Systemen mit quantitativer Information, wie metrischen Transitionssytemen und Markow-Ketten. Von besonderem Interesse ist dabei der Begriff der Bisimilarität, der auf verschiedensten Arten von Systemen Anwendung findet; so gibt es neben der klassischen Bisimilarität für Transitionssyteme auch den Begriff der probabilistischen Bisimilarität für Systeme auf Basis von Markow-Ketten. All diese Systeme lassen sich einheitlich als sogenannte Koalgebren für Mengenfunktoren modellieren, also als Abbildungen, die jedem Zustand des Systems eine strukturierte Kollektion an Nachfolgern zuweisen und auf diese Weise einen Zeitschritt im Verhalten dieser Zustände beschreiben. Im Falle von Systemen mit quantitativen Daten -- etwa Wahrscheinlichkeiten oder unscharfen Wahrheitsaussagen -- ist Bisimilarität oftmals nicht das Mittel der Wahl, weil sie dazu neigt, quantitative Information zu verwerfen. Daher kommt bei solchen Systemen stattdessen oft der Begriff der Verhaltensdistanz zur Anwendung, der es erlaubt, den Unterschied im Verhalten zweier Zustände zu beziffern (als Wahrheitswert bzw. Distanz zwischen 0 und 1), anstatt nur zu konstatieren, dass die Zustände verhaltensäquivalent sind oder eben nicht. Klassische Bisimilarität hängt eng mit der Modallogik zusammen; so ist eine der direktesten Verbindungen zwischen den beiden die Aussage, dass Formeln der Modallogik bisimulationsinvariant sind, also dass bisimilare Zustände die gleichen Formeln der Modallogik erfüllen. Im Rahmen dieser Arbeit interessieren wir uns für zwei weitere Aussagen über den Zusammenhang zwischen Modallogik und Bisimilarität, die beide auf ihre Art als Umkehrung der Bisimulationsinvarianz verstanden werden können. Die erste dieser Aussagen ist der Satz von Hennessy und Milner, der besagt, dass in Systemen mit endlichem Verzweigungsgrad Bisimilarität von Zuständen bereits aus modallogischer Ununterscheidbarkeit folgt. Die zweite Aussage geht zurück auf van Benthem, und charakterisiert die Modallogik genau als dasjenige Fragment der Logik erster Stufe, das unter Bisimulationen invariant ist. In dieser Dissertation arbeiten wir quantitative Entsprechungen beider Theoreme heraus, wobei wir in drei verschiedene Richtungen verallgemeinern. Erstens halten wir unsere Resultate in koalgebraischer Allgemeinheit und decken auf diese Weise eine Vielzahl von verschiedenen Systemen ab. Zweitens verwenden wir sogenannte Quantale, um über den Wertebereich von Logiken und Distanzen zu abstrahieren. Dies erlaubt es uns, unsere Resultate sowohl auf klassische boolesche Logiken und Äquivalenzen anzuwenden, als auch auf Fuzzy-Logiken und Pseudometriken sowie auf noch allgemeinere Begriffe von Distanzen. Drittens bleiben wir parametrisch in der Entscheidung ob die untersuchten Distanzbegriffe eine Symmetriebedingung erfüllen sollen oder nicht, was es uns ermöglicht, gleichermaßen Begriffe von Simulation und Bisimulation zu behandeln. Auf diesem Allgemeinheitsgrad wird der Begriff der Verhaltensdistanz technisch dadurch realisiert, dass der den Systemtyp beschreibende Funktor auf die Kategorie der quantalwertigen Distanzen "geliftet" wird. Diese Liftings von Funktoren können wiederum auf sehr flexible Art und Weise mittels sogenannter laxer Erweiterungen gewonnen werden, die auf quantalwertigen Relationen leben und es somit auch erlauben, Zustände verschiedener Systeme miteinander zu vergleichen. Eine der wichtigsten dieser laxen Erweiterungen ist die koalgebraische Kantorowitsch-Erweiterung, die parametrisch in einer Menge von Prädikatenliftings ist und auf eine Vielzahl bekannter Beispiele instanziiert. Tatsächlich zeigen wir im Rahmen dieser Arbeit, dass diese Allgegenwart der Kantorowitsch-Erweiterung nicht von ungefähr kommt, und sich unter geeigneten Anforderungen an den Funktor jede laxe Erweiterung als eine Kantorowitsch-Erweiterung darstellen lässt. Innerhalb dieser Anforderungen zeigen wir zudem, dass die beiden eingangs erwähnten Sätze von Hennessy und Milner bzw. van Benthem auch in diesem sehr allgemeinen Rahmen gelten. Insgesamt bringen wir somit eine Reihe an bekannten Resultaten unter einen gemeinsamen Schirm und erhalten zudem einige komplett neue Resultate, etwa für bestimmte konvex-nichtdeterministische Metriken.