An implementation of global caching for the alternation-free coalgebraic μ-calculus

Abschlussarbeit
(Masterarbeit)


Details zur Publikation

Autorinnen und Autoren: Egger C
Jahr der Veröffentlichung: 2016
Sprache: Englisch


Abstract


This thesis presents a first implementation of a global caching algorithm for the alternation-


free fragment of the coalgebraic


μ-calculus, COOL. COOL can decide satisfiability of formu-


lae in the alternation-free coalgebraic


μ-calculus which includes the relational, alternation-free


μ-calculus,


CTL


as well as


ATL


and several other logics. The global caching algorithm is the


first optimal single-pass tableaux algorithm for all the mentioned logics and builds upon the


global caching algorithm for the flat coalgebraic


μ


-calculus.


Especially for


CTL


, model checking is regularly used in practice and there are several appli-


cations for reasoning. Consequently there already exist a number of different implementations.


COOL in general performs comparable to other implementations and is significantly faster for


certain kinds of formulae.


The thesis provides a summary of the global caching algorithm and a description of the im-


plementation in COOL as well as a performance comparison between COOL and other state of


the art reasoners. Finally it provides several suggestions for further optimization.


FAU-Autorinnen und Autoren / FAU-Herausgeberinnen und Herausgeber

Egger, Christoph
Lehrstuhl für Informatik 8 (Theoretische Informatik)


Zitierweisen

APA:
Egger, C. (2016). An implementation of global caching for the alternation-free coalgebraic μ-calculus (Master thesis).

MLA:
Egger, Christoph. An implementation of global caching for the alternation-free coalgebraic μ-calculus. Master thesis, 2016.

BibTeX: 

Zuletzt aktualisiert 2018-08-08 um 15:10