Global Caching for the Flat Coalgebraic μ-Calculus
Hausmann D, Schröder L (2015)
Publication Language: English
Publication Type: Conference contribution, Conference Contribution
Publication year: 2015
Publisher: Springer
City/Town: Berlin
Pages Range: 121-130
Conference Proceedings Title: Proceedings, 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015
Event location: Kassel
ISBN: 978-1-4673-9317-1
DOI: 10.1109/TIME.2015.15
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.
Authors with CRIS profile
Daniel Hausmann
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Lutz Schröder
Lehrstuhl für Informatik 8 (Theoretische Informatik)
Related research project(s)
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: Download