% Encoding: UTF-8
@COMMENT{BibTeX export based on data in FAU CRIS: https://cris.fau.de/}
@COMMENT{For any questions please write to cris-support@fau.de}
@masterthesis{faucris.123632564,
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.
},
author = {Egger, Christoph},
faupublication = {yes},
peerreviewed = {automatic},
school = {Friedrich-Alexander-Universität Erlangen-Nürnberg},
title = {{An} implementation of global caching for the alternation-free coalgebraic μ-calculus},
url = {https://static.siccegge.de/pdfs/master-thesis.pdf},
year = {2016}
}