Satisfiability Checking for the Coalgebraic µ-Calculus

Erfüllbarkeitsprüfung für den Koalgebraischen µ-Kalkül

Please always quote using this URN: urn:nbn:de:bvb:29-opus4-99325
  • 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 prioritiesThe 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.show moreshow less
  • 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 kommenDie 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.show moreshow less

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar Statistics
Metadaten
Author:Daniel Hausmann
Persistent identifiers - URN:urn:nbn:de:bvb:29-opus4-99325
Referee:Lutz Schröder, Alexander Kurz
Advisor:Lutz Schröder
Document Type:Doctoral Thesis
Language:English
Year of publication:2018
Date of online publication (Embargo Date):2018/09/04
Publishing Institution:Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU)
Granting institution:Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU), Technische Fakultät
Acceptance date of the thesis:2018/06/28
Release Date:2018/09/11
Tag:Automatendeterminisierung; Paritätsautomat; Paritätsspiel
SWD-Keyword:Fixpunkt-Logik; Koalgebra; Erfüllbarkeitsproblem; Büchi-Automat; Mathematisches Spiel
Length/size:104
Institutes:Technische Fakultät
CCS-Classification:F. Theory of Computation / F.3 LOGICS AND MEANINGS OF PROGRAMS / F.3.1 Specifying and Verifying and Reasoning about Programs (D.2.1, D.2.4, D.3.1, E.1) / Specification techniques
F. Theory of Computation / F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES / F.4.1 Mathematical Logic (F.1.1, I.2.2-4) / Mechanical theorem proving
F. Theory of Computation / F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES / F.4.1 Mathematical Logic (F.1.1, I.2.2-4) / Modal logic (NEW)
F. Theory of Computation / F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES / F.4.1 Mathematical Logic (F.1.1, I.2.2-4) / Temporal logic (NEW)
G. Mathematics of Computing / G.2 DISCRETE MATHEMATICS / G.2.2 Graph Theory (F.2.2) / Path and circuit problems
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 006 Spezielle Computerverfahren
MSC-Classification:03-XX MATHEMATICAL LOGIC AND FOUNDATIONS / 03Bxx General logic / 03B45 Modal logic (including the logic of norms) (For knowledge and belief, see 03B42; for temporal logic, see 03B44; for provability logic, see also 03F45)
03-XX MATHEMATICAL LOGIC AND FOUNDATIONS / 03Bxx General logic / 03B62 Combined logics
open_access (DINI-Set):open_access
Licence (German):Creative Commons - CC BY - Namensnennung 4.0 International
Einverstanden ✔
Diese Webseite verwendet technisch erforderliche Session-Cookies. Durch die weitere Nutzung der Webseite stimmen Sie diesem zu. Unsere Datenschutzerklärung finden Sie hier.