The coalgebraic µ-calculus is an expressive logic that generalizes the modal µ-calculus by interpreting formulas over T-coalgebras rather than Kripke structures. Due to the presence of fixpoint operators, the semantics of µ-calculi is rather involved and satisfiability checking for µ-calculus formulas typically necessitates the use of automata theoretic concepts, in particular the determinization of automata on infinite words. We introduce novel notions of automata in which all accepting runs are deterministic or linear, from some point on, and give novel determinization methods for such automata. In particular, we show that limit-deterministic parity automata with n states and k priorities can be determinized to parity automata of size O((nk)!) and with O(nk) priorities and that limit-linear Co-Büchi automata of size n can be determinized to Co-Büchi automata of size at most (n^2)(2^n). We obtain satisfiability games for the coalgebraic µ-calculus by employing tracking automata, that is, parity automata that track fixpoint formulas through pre-tableaux. The tracking automata for alternation-free formulas are parity automata with just the priorities 0 and 1, i.e. Co-Büchi automata; tracking automata for aconjunctive formulas are limit-deterministic and tracking automata for linear formulas are limit-linear. We define satisfiability games via determinization, that is, satisfiability games for the coalgebraic µ-calculus that are constructed by determinizing tracking automata, and show that Eloise wins such a game if and only if the corresponding formula is satisfiable. We also prove that for coalgebraic µ-calculus formulas of size n and with alternation depth k, the number of Abelard-nodes in the corresponding satisfiability game via determinization is bounded by (n^2)(2^n) for linear formulas and by 3^n for alternation-free formulas, and is in O((nk)!) for aconjunctive formulas and in O(n!(nk)^(nk)) for unrestricted formulas. As models are built over Abelard-nodes, we obtain corresponding bounds on the sizes of models for satisfiable formulas from the mentioned fragments. We also introduce satisfiability games via focusing that can be constructed without determinizing automata but only work for formulas that are both alternation-free and aconjunctive. We present an algorithm that can be instantiated to any of the presented games and solves the satisfiability problem of the (corresponding fragment of the) coalgebraic µ-calculus in ExpTime and on-the-fly. The algorithm has been implemented (see https://www8.cs.fau.de/research:software:cool) and it has been shown that both the asymptotically smaller games obtained by the new determinization procedures and on-the-fly solving allows for shorter runtimes in comparison with other satisfiability checking tools.

Die Theorie der universellen Koalgebra stellt ein mathematisches Rahmenwerk zur formalen Behandlung von reaktiven Systemen in der Informatik dar. Die koalgebraische Modallogik verwendet in diesem Rahmenwerk Koalgebren als logische Modelle und ermöglicht es somit, das Verhalten von allgemeinen reaktiven Systemen präzise zu Beschreiben. Der koalgebraische µ-Kalkül erweitert koalgebraische Modallogik um Fixpunktoperatoren mit deren Hilfe es möglich ist, differenzierte Aussagen über unendliches Verhalten von reaktiven Systemen zu treffen. Diese Arbeit behandelt das Erfüllbarkeitsproblem des koalgebraischen µ-Kalküls; hierzu werden sogenannte Erfüllbarkeitsspiele zunächst definiert und kommen sodann in einem generischen Algorithmus zur Anwendung um die Erfüllbarkeit von koalgebraischen µ-Kalkülformeln in ExpTime zu überprüfen. Die Konstruktion der Erfüllbarkeitsspiele determinisiert dabei Automaten über unendlichen Wörtern; zwei neuartige Algorithmen zur Determinisierung sogenannter limes-linearer und limes-deterministischer Automaten stellen ein zentrales Ergebnis der Arbeit dar. Für bestimmte Fragmente des koalgebraischen µ-Kalküls haben die resultierenden Erfüllbarkeitsspiele sodann eine asymptotisch kleinere Größe, als die mit bisherigen Determinisierungsmethoden erzeugbaren Erfüllbarkeitspiele.

Die zentralen theoretischen Ergebnisse dieser Dissertation wurden als wissenschaftliche Publikationen veröffentlicht.

Der entwickelte Erfüllbarkeitsprüfungsalgorithmus wurde als Erweiterung des Beweiswerkzeugs Coalgebraic Ontology Logic Reasoner (COOL) implementiert; der Quellcode, Testformeln, ein Formelgenerator sowie weiterführende Informationen sind unter https://www8.cs.fau.de/research:software:cool zu finden. Die Implementierung unerstützt das sogenannte on-the-fly-Lösen der jeweiligen Erfüllbarkeitspiele; somit kann die Erfüllbarkeit bzw. Unerfüllbarkeit einer Formel gegebenfalls erkannt werden, bevor das Spiel vollständig konstruiert wurde.