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