An implementation of global caching for the alternation-free coalgebraic μ-calculus
Egger C (2016)
Publication Language: English
Publication Type: Thesis
Publication year: 2016
URI: https://static.siccegge.de/pdfs/master-thesis.pdf
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.
Authors with CRIS profile
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: Download
