19th Annual IEEE Symposium on Logic in Computer Science (LICS'04) Three-Valued Abstractions of Games: Uncertainty, but with Precision Turku, Finland July 13-July 17 ISBN: 0-7695-2192-4
We present a framework for abstracting two-player turn-based games that preserves any formula of the alternating μ-calculus (AMC). Unlike traditional conservativ abstractions which can only prove the existence of winning strategies for only one of the players, our framework is based on 3-valued games, and it can be used to prove and disprove formulas of AMC including arbitrarily nested strategy quantifiers.Our main contributions are as follows. We define abstract 3-valued games and an alternating refinement relation on these that preserves winning strategies fo both players. We provide a logical characterization of the alternating refinement relation. We show that our abstractions are as precise as can be via completeness results. We present AMC formulas that solve 3-valued games with w-regular objectives, and we show that such games are determined in a 3-valued sense. We also discuss the complexity of model checking arbitrary AMC formulas on 3-valued games and of checking alternating refinement.
Citation:
Luca de Alfaro, Patrice Godefroid, Radha Jagadeesan, "Three-Valued Abstractions of Games: Uncertainty, but with Precision," lics, pp.170-179, 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), 2004 Usage of this product signifies your acceptance of the Terms of Use. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||