Global Caching for the Alternation-free $\mu$-Calculus

TL;DR

This paper introduces a sound, complete, and optimal single-pass tableau algorithm for the alternation-free μ-calculus that integrates game construction and solving on-the-fly using global caching, with promising initial results.

Contribution

It presents the first single-pass tableau algorithm for the alternation-free μ-calculus that combines global caching with on-the-fly game solving, improving efficiency.

Findings

Algorithm runs in 2^{O(n)} time

Supports global caching with intermediate propagation

Prototype implementation shows promising results

Abstract

We present a sound, complete, and optimal single-pass tableau algorithm for the alternation-free $\mu$-calculus. The algorithm supports global caching with intermediate propagation and runs in time $2^{\mathcal{O}(n)}$. 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.