Hausmann D, Schröder L (2015)
Publication Status: Published
Publication Type: Conference contribution, Original article
Publication year: 2015
Publisher: IEEE
Pages Range: 121-130
Conference Proceedings Title: Proc. 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015
DOI: 10.1109/TIME.2015.15
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 single-pass, 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.
APA:
Hausmann, D., & Schröder, L. (2015). Global Caching for the Flat Coalgebraic mu-Calculus. In Proc. 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015 (pp. 121-130). IEEE.
MLA:
Hausmann, Daniel, and Lutz Schröder. "Global Caching for the Flat Coalgebraic mu-Calculus." Proceedings of the 22nd International Symposium on Temporal Representation and Reasoning, TIME 2015 IEEE, 2015. 121-130.
BibTeX: Download