Global Caching for the Flat Coalgebraic μ-Calculus
Author(s): Hausmann D, Schröder L
Editor(s): Grandi F, Lange M, Lomuscio A
Publishing place: Berlin
Publication year: 2015
Conference Proceedings Title: Proceedings, 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015
Pages range: 121-130
Event: 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015
Event location: Kassel
Start date of the event: 23/09/2015
End date of the event: 25/09/2015
Branching-time temporal logics generalizing relational temporal logics such as CTL have been proposed for various system types beyond the purely relational world. This includes, e.g., alternating-time logics, which talk about winning strategies over concurrent game structures, and Parikh’s game logic, which is interpreted over monotone neighbourhood frames, as well as probabilistic fixpoint logics. Coalgebraic logic has emerged as a unifying semantic and algorithmic framework for logics featuring generalized modalities of this type. Here, we present a generic global caching algorithm for satisfiability checking in the flat coalgebraic mu-calculus, which realizes known tight exponential-time upper complexity bounds but offers potential for heuristic optimization. It is based on a tableau system that makes do without additional labelling of nodes beyond formulas from the standard Fischer-Ladner closure, such as foci or termination counters for eventualities. Moreover, the tableau system is singlepass, i.e. avoids building an exponential-sized structure in a first pass; to our best knowledge, optimal single-pass systems without numeric time-outs were not previously available even for CTL.
FAU Authors / FAU Editors How to cite
APA: Hausmann, D., & Schröder, L. (2015). Global Caching for the Flat Coalgebraic μ-Calculus. In Grandi F, Lange M, Lomuscio A (Eds.), Proceedings, 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015 (pp. 121-130). Berlin: Springer.
MLA: Hausmann, Daniel, and Lutz Schröder. "Global Caching for the Flat Coalgebraic μ-Calculus." Proceedings of the 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015, Kassel Ed. Grandi F, Lange M, Lomuscio A, Berlin: Springer, 2015. 121-130.