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

Thesis
(Master thesis)


Publication Details

Author(s): Egger C
Publication year: 2016
Language: English


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 Authors / FAU Editors

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


How to cite

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: 

Last updated on 2018-19-04 at 04:01