Global Caching for the Alternation-free $\mu$-Calculus
Logic in Computer Science
2016-09-22 v1
Abstract
We present a sound, complete, and optimal single-pass tableau algorithm for the alternation-free -calculus. The algorithm supports global caching with intermediate propagation and runs in time . In game-theoretic terms, our algorithm integrates the steps for constructing and solving the B\"uchi game arising from the input tableau into a single procedure; this is done on-the-fly, i.e. may terminate before the game has been fully constructed. This suggests a slogan to the effect that global caching = game solving on-the-fly. A prototypical implementation shows promising initial results.
Cite
@article{arxiv.1609.06379,
title = {Global Caching for the Alternation-free $\mu$-Calculus},
author = {Daniel Hausmann and Lutz Schröder and Christoph Egger},
journal= {arXiv preprint arXiv:1609.06379},
year = {2016}
}