Coalgebraic Semantics and Minimization in Sets and Beyond

Language
en
Document Type
Doctoral Thesis
Issue Date
2020-08-03
Issue Year
2020
Authors
Wißmann, Thorsten
Editor
Abstract

The theory of coalgebras provides a uniform view on state-based systems, which are omnipresent throughout computer science. The notion of coalgebras is parametric in the choice of a functor F on a category. Depending on this choice, the notion of an F-Coalgebra instanitates to different kinds of state-based systems, for example, Markov chains, deterministic automata, and transition systems. The present thesis contributes to the coalgebraic framework in two aspects: 1. the characterization of more systems in coalgebraic terms, and 2. the development of generic methods applicable to different systems that are coalgebras.

In the preliminaries, we recall the basic coalgebraic definitions and further categorical notions that are needed later. We illustrate the notions using the well-studied examples of coalgebras in sets.

Part I is dedicated to the semantics of two new (families of) instances of the generic framework of coalgebras beyond sets. By embedding these systems into the coalgebraic framework, we make existing generic coalgebraic methods applicable for the respective kind of state-based systems:

In Chapter 3 in Part I, we characterize the orbit-finite coalgebraic behaviours in nominal sets by relating them to the well-understood finite behaviours in sets, where orbit-finite is the canonical finiteness notion in nominal sets. Concretely, we define a special class of functors on nominal sets and call them localizable liftings of a set-functor. Then we characterize the rational fixpoint of such a functor, which captures the semantics of finitary coalgebras, i.e. orbit-finite coalgebras in nominal sets. We prove that the rational fixpoint of localizable liftings lifts from the rational fixpoint of the corresponding set functor. Secondly, we establish a sufficient property on functors F on nominal sets such that the rational fixpoint of quotient functors is given by quotienting the rational fixpoint of F . By combining these two observations, we obtain an explicit description of the rational fixpoint, i.e. the finitary semantics, of a large family of functors involving name binding, exponentiation, finite branching, and polynomial constructs. Their orbit-finite behaviours are thus equivalence classes of the finite coalgebra semantics of their set-theoretic representation. For example, for the functor modelling λ-terms, the orbit-finite behaviours are α-equivalence classes of rational λ-trees, which are possibly infinite λ-terms that have a finite representation as a coalgebra in sets.

In Chapter 4 in Part I, we model coalgebraic systems with upgrades. These are systems that run in a specific version. For each version, only a certain set of transitions are available, and the higher the version, the more transitions are available. The corresponding notion of bisimilarity, called ‘conditional bisimulation’, has been defined previously for a particular type of system called conditional transition system. In Chapter 4 we define it generically for a functor that satisfies certain axioms, generalizing the concrete notion. For this, we consider functors on the Kleisli category of the reader monad on the category of partially ordered sets. In this Kleisli category, we prove for coalgebras satisfying a sufficient condition called ‘upgrade preservation’ that the generic notion of coalgebraic bisimilarity is characterized precisely by conditional bisimilarity. Furthermore, we reduce the computation of the behavioural equivalence in the Kleisli category to that in the base category of partially ordered sets.

Part II is dedicated to the development of minimization methods for state-based systems on a coalgebraic level of generality. The minimization of a system consists of two tasks. One task is to restrict the system to those states that are reachable from a distinguished initial state. This task is called reachability construction or simply reachability. The other task of minimization is to identify states that exhibit the same behaviour. This task removes the redundancy from the system and is usually called bisimilarity minimization or also partition refinement, describing the algorithm scheme often used to solve this task. The presented methods range from abstract categorical constructions to efficient algorithmic implementations.

In Chapter 5 in Part II, we construct the reachable subcoalgebra of a given pointed coalgebra. The point of the coalgebra serves as the initial state. The construction is iterative, has at most countably many steps, works in a general categorical setting, and is proven correct for an existing concise definition of reachability of a pointed coalgebra. We discuss instances in sets and beyond. In the special case of Set, the reachability in a coalgebra is equivalent to the usual graph-theoretical reachability in the so-called canonical graph of the coalgebra. Furthermore, our construction resembles the standard breadth-first search that computes the reachable hull in the canonical graph. We also discuss examples beyond sets. While instances in nominal sets or multisorted sets are direct, more assumptions need to be fulfilled to instantiate the construction in Kleisli categories. As an alternative, we reduce the reachability problem for coalgebras in the Kleisli category to reachability in the base category.

In Chapter 6 in Part II, we discuss the task of bisimilarity minimization of coalgebras using partition refinement algorithms. We solve this task by a categorical construction that is subsequently refined towards an efficient algorithmic implementation and a running partition refinement tool, CoPaR. For many concrete system types, concrete partition refinement algorithms have been developed throughout the past 50 years. These efficient algorithms typically run in O((m + n) ⋅ log n) time, where n is the number of states in the system and m is the number of edges. It is a common assumption that every state is involved in at least one edge, m ≥ n, and so one typically calls them m ⋅ log n algorithms. In Chapter 6 we start by showing their similarities looking at two concrete example runs of the respective algorithms for (labelled) transition systems and Markov chains. We then formalize the most significant similarities by defining a categorical partition refinement construction that works in every regular category and computes the behavioural equivalence in a coalgebra. The construction is parametric in a heuristic that tells the algorithm which information to process next in the partition refinement. By a special choice for this heuristic, we obtain an existing partition refinement algorithm for coalgebras by König and Küpper [84] as an instance. By another heuristic that involves size considerations, we formalize the so-called ‘process the smaller half’ strategy that is used in all efficient partition refinement algorithms and that contributes to their low run-time complexity. As a next step towards a generic and efficient algorithm for coalgebras, we introduce zippable functors and instantiate the construction to sets. These assumptions allow us to make an optimization where we compute the refined partitions incrementally. Finally, we formalize the remaining functor specific aspects of the algorithm in a so-called refinement interface that we implement for many functors of interest.

We then design a generic algorithm in pseudocode that is only given as parameters the input coalgebra and an implementation of the abstract refinement interface of the functor. This algorithm is proven correct on the generic level, i.e. that it indeed computes the behavioural equivalence in the input coalgebra. Moreover, we analyse the run-time complexity of the algorithm and show that it runs in O((m + n) ⋅ log n) time, where n is the number of states and m the number of edges in the input coalgebra. This directly instantiates to m⋅log n partition refinement algorithms for transition systems, Markov chains (possibly with weights in a cancellative monoid), deterministic automata, and to colour refinement for graphs (also called the 1-dimensional Weisfeiler-Lehman algorithm), where each of these instances matches the run-time of the best concrete algorithm known. In order to cover weighted systems with weights in a non-cancellative monoid, we generalize the complexity analysis of the main algorithm, relaxing the complexity requirements of the functor’s refinement interface. In this relaxed setting, we can handle weighted systems with weights in a (possibly non-cancellative) monoid M in O((m + n) ⋅ log n ⋅ log min(∣M ∣, m)). Since zippable functors are not closed under composition, we define a separate modularity construction to handle composites of such system types. This construction introduces explicit intermediate states, possibly affecting the run-time complexity. For example, Segala systems combine non-deterministic and probabilistic behaviour, and the generic algorithm minimizes them in mp ⋅ log ma where mp is the number of probabilistic edges and ma the number of non-deterministic edges. This instance matches the run- time of an explicit algorithm developed independently and at the same time [53] and improves the previously best-known algorithm for Segala systems [17]. With the modularity reduction, the generic framework also supports minimization of weighted tree automata under backwards bisimulation in O(m ⋅ log m) run-time, improving the previously best-known algorithm [62]. A comparison of all instances can be found in Table 6.1 on page 145. A case-study of an actual tool implementation called CoPaR shows that our generic category-based algorithm can be of use in practise and is capable of handling input coalgebras with millions of edges within a few minutes.

In Chapter 7 in Part II, we compare the two previously discussed aspects of minimality. We show that they are dual concepts by defining an abstract notion of minimality and minimization in a category. The instance of this general minimization in the category of pointed coalgebras is the reachability construction and its instance in the dual category is bisimilarity minimization. Thus, these two minimization methods have many properties in common – up to duality. Finally, we consider the minimization of F -coalgebras under both reachability and bisimilarity. If F preserves inverse images, we show that we obtain the same minimized coalgebra no matter in which order we solve the two minimization tasks.

Abstract

Die Theorie der Koalgebren liefert eine einheitliche Sicht auf zustandsbasierte Systeme, wie sie in der Informatik allgegenwärtig sind. Das Konzept der Koalgebra ist parametrisch in der Wahl eines Funktors F auf einer Kategorie C. Je nach Wahl dieses Funktors F konkretisiert sich das Konzept F-Koalgebra zu unterschiedlichen Arten von zustandsbasierten Systemen, u. a. zu Markov- Ketten, deterministischen Automaten und Transitionssystemen. In der vorliegenden Arbeit werden die koalgebraische Semantik und koalgebraische Minimiermethoden in der Kategorie der Mengen und darüber hinaus studiert. Da die koalgebraische Semantik in der Kategorie der Mengen bereits umfassend studiert wurde, wird diese lediglich im Grundlagenkapitel 2 wiederholt. Der erste Teil der Arbeit (Kapitel 3 und 4) beschäftigt sich mit der koalgebraischen Semantik jenseits der vertrauten Kategorie der Mengen, und der zweite Teil der Arbeit (Kapitel 5, 6 und 7) mit Methoden der Minimierung von Koalgebren in allgemeinen Kategorien und speziell auch in Mengen.

In Kapitel 3 betrachten wir Koalgebren in der Kategorie der nominellen Mengen. Diese erlauben es, die Konzepte von gebundenen bzw. frischen Namen und deren Umbenennung zu formalisieren, wie man es aus dem λ-Kalkül kennt. Hier sind die Koalgebren zustandsbasierte Systeme, die unter anderem Namen als Eingabe lesen oder allozieren können. In Kapitel 3 geben wir eine explizite Beschreibung der Verhalten von Orbit-endlichen Koalgebren für verschiedene Arten von Funktoren auf nominellen Mengen. Viele Funktoren, die in nominellen Anwendungsbeispielen auftreten, sind Quotient eines Mengen-Funktors, die bereits ausführlich in der Literatur studiert wurden. Beispiele hierfür sind der Bindungsfunktor, dessen koalgebraische Semantik das Allozieren von Namen ist, und wie wir zeigen auch der Exponentiationsfunktor, dessen koalgebraische Semantik das Einlesen von Namen ist. Für solche Funktoren und Kombinationen derer beweisen wir, dass die Verhalten von Orbit-endlichen Koalgebren durch Äquivalenz-Klassen von Verhalten von endlichen Koalgebren des zu Grunde liegenden quotientierten Mengenfunktors gegeben sind. Konkret leiten wir hier für eine große Familie von Funktoren auf nominellen Mengen explizite Beschreibungen der Orbit-endlichen Verhalten aus wohlverstandenen Mengenfunktoren ab. Zum Beispiel bestehen die Orbit-endlichen Verhalten des Typfunktors, der die Ausdrücke des λ-Kalküls beschreibt, aus den α-Äquivalenzklassen von rationalen λ-Bäumen. Das sind unendliche λ-Ausdrücke, die eine endliche Beschreibung haben. Allgemein besteht das Verhalten von Orbit-endlichen F-Koalgebren aus Äquivalenzklassen, wobei sich die Äquivalenzrelation kanonisch aus dem Quotientenfunktor ergibt, z. B. α-Äquivalenz im Falle der λ-Ausdrücke.

In Kapitel 4 betrachten wir Conditional Transition Systems (CTS), die eine Variante von Transitionssystemen darstellen, bei denen dynamisch zur Laufzeit Übergänge aktiviert werden können. Zur Laufzeit eines CTS befindet sich das System in einer bestimmten Version, die ein Element einer gegebenen halbgeordneten Menge von Versionen ist. Im CTS ist auf monotone Weise für jede Version festgelegt, welche Übergänge darin aktiviert sind: in höheren Versionen sind mindestens genau so viele Übergänge verfügbar. Ein CTS kann jederzeit in eine höhere Version wechseln, um zusätzliche Übergänge freizuschalten. CTSen sind Koalgebren für eine Variante des Funktors für Transitionssysteme, die in der Kleisli-Kategorie der Reader-Monade auf der Kategorie der halbgeordneten Mengen leben. Wir beweisen, dass der Bisimulationsbegriff, der zuvor ad-hoc für CTSen definiert wurde, mit dem generischen Begriff der koalgebraischen Verhaltensäquivalenz übereinstimmt.

In Kapitel 5 konstruieren wir den erreichbaren Teil einer Koalgebra bezüglich eines gegebenen Startzustands, d. h. wir verkleinern Koalgebren durch Eliminierung unerreichbarer Zustände. Formal definieren wir eine iterative Konstruktion auf punktierten Koalgebren, wobei die Punktierung einem oder mehreren Startzuständen entspricht. Diese Konstruktion berechnet in abzählbar vielen Schritten den erreichbaren Teil der punktierten Koalgebra. Instanziiert man die Konstruktion für Koalgebren in Mengen, so führt die Konstruktion effektiv eine Breitensuche auf dem kanonischen Graphen der Koalgebra aus. Die Voraussetzungen der Konstruktion sind in vielen Kategorien gegeben, z. B. in der Kategorie der nominellen Mengen und sogar in manchen Kleisli-Kategorien für gewichtete Systeme. Um den erreichbaren Teil von Koalgebren in weiteren Kleisli-Kategorien konstruieren zu können, reduzieren wir das Problem der Erreichbarkeitssuche dort auf die Erreichbarkeitssuche in der darunterliegenden Grundkategorie.

In Kapitel 6 identifizieren wir verhaltensäquivalente Zustände in einer Koalgebra, d. h. wir verkleinern Koalgebren durch Eliminierung von Redundanz. Für verschiedene Varianten von zustandsbasierten Systemen wurden hierfür in den letzten 50 Jahren konkrete effiziente Algorithmen entworfen; so zum Beispiel der Algorithmus von Hopcroft zur Automatenminimierung oder der Algorithmus von Paige und Tarjan zum Berechnen von Bisimilarität in einem Transitionssystem. All diese Algorithmen haben ein ähnliches Vorgehen, bei dem eine Partition auf dem Zustandsraum sukzessive verfeinert wird, bis ein größter Fixpunkt erreicht wird. Außerdem eint diese Algorithmen eine Laufzeitkomplexität von O(m ⋅ log n), wobei n die Zahl der Zustände und m die der Transitionen im System ist. In Kapitel 6 definieren wir eine kategorielle Konstruktion, die das gemeinsame Vorgehen dieser Algorithmen formalisiert, das Systemtyp-Spezifische im Funktor abstrahiert und alle verhaltensäquivalenten Zustände in einer Koalgebra identifiziert. Formal konstruieren wir den sogenannten einfachen Quotienten einer Koalgebra. Wir zeigen die Korrektheit der Konstruktion in koalgebraischer Allgemeinheit und instanziieren diese anschließend in der Kategorie der Mengen. Dort optimieren wir einen Schritt in der Konstruktion und entwerfen einen Algorithmus, der die optimierte kategorielle Konstruktion berechnet. Hierbei werden die verbleibenden Funktor-spezifischen Operationen hinter einer Schnittstelle verborgen. Der Algorithmus erhält somit als Eingabe lediglich eine F-Koalgebra und eine Implementierung der Schnittstelle des Funktors F . Wir beweisen, dass die verhaltensäquivalenten Zustände in einer Laufzeit von O(m ⋅ log n) korrekt identifiziert werden. In einer weiteren Konstruktion zeigen wir, dass sich der generische Algorithmus auch auf kombinierte Systemtypen anwenden lässt. Beispiele hierfür sind Segala-Systeme, die probabilistisches und nicht-deterministisches Verhalten kombinieren, aber auch Gewichtete Baum-Automaten die eine Kombination aus gewichteten Automaten und Baumautomaten darstellen. Fast alle Instanzen des generischen Algorithmus haben dieselbe Laufzeitkomplexität wie die jeweils schnellsten maßgeschneiderten Algorithmen für die entsprechenden Systemtypen, und im Falle von gewichteten Baumautomaten sogar eine bessere. Der generische Algorithmus und die Modularitätskonstruktion sind in der Software CoPaR implementiert, die es dem Nutzer erlaubt, zur Laufzeit aus den bestehenden Bausteinen neue Systemtypen zu konstruieren und Koalgebren dieses Typs zu minimieren.

In Kapitel 7 vergleichen wir die vorherigen zwei Aspekte der Koalgebrenminimierung: Erreichbarkeit und Konstruktion des einfachen Quotienten einer Koalgebra. Zuerst zeigen wir, dass beide Konzepte Instanz eines allgemeineren Minimalitätskonzepts in einer Kategorie sind. Erreichbarkeit entspricht dem allgemeinen Minimalitätsbegriff in der Kategorie der punktierten Koalgebren und Einfachheit von Koalgebren entspricht dem Minimalitätsbegriff in der zur Kategorie der Koalgebren dualen Kategorie. Folglich haben beide Minimalitätsbegriffe bis auf Dualität die gleichen Eigenschaften. Außerdem untersuchen wir, wie man Koalgebren bezüglich beider Begriffe minimieren kann. Wenn der Funktor F Urbilder erhält, dann kann man F-Koalgebren minimieren, indem man die vorherigen zwei Minimiermethoden – Erreichbarkeit und Berechnen von Verhaltensäquivalenz – in beliebiger Reihenfolge anwendet.

DOI
Faculties & Collections
Zugehörige ORCIDs