Global Caching for the Flat Coalgebraic μ-Calculus

Conference contribution
(Conference Contribution)


Publication Details

Author(s): Hausmann D, Schröder L
Editor(s): Grandi F, Lange M, Lomuscio A
Publisher: Springer
Publishing place: Berlin
Publication year: 2015
Conference Proceedings Title: Proceedings, 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015
Pages range: 121-130
ISBN: 978-1-4673-9317-1
ISSN: 1530-1311
Language: English


Abstract


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

Hausmann, Daniel
Lehrstuhl für Informatik 8 (Theoretische Informatik)


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). Kassel, DE: 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.

BibTeX: 

Last updated on 2018-19-04 at 15:51