loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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
Luca de Alfaro, University of California, Santa Cruz
Patrice Godefroid, Bell Laboratories, Lucent Technologies
Radha Jagadeesan, School of CTI, DePaul University
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.