Refine
Year of publication
- 2020 (1)
Document Type
- Doctoral Thesis (1)
Language
- English (1)
Has Fulltext
- yes (1)
Keywords
- Category Theory (1)
- Coalgebra (1)
- Nominal Sets (1)
- Partition Refinement (1)
- Theoretical Computer Science (1)
Institute
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.