Three-Valued Abstractions of Games: Uncertainty, But With Precision

We present a framework for abstracting two-player turn-based games that preserves any formula of the alternating mu-calculus (AMC). Unlike traditional conservative abstractions which can only prove existence of winning strategies for only one of the players, our framework is based on 3-valued games and can be used to prove and disprove formulas of AMC including arbitrarily nested strategy quantifiers.