Thesis
(Master thesis)


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


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.


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
Share link
Last updated on 2017-11-23 at 02:57
PDF downloaded successfully