loading...
Three-Valued Abstractions of Games: Uncertainty, but with Precision
Turku, Finland July 13-July 17
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/LICS.2004.131961119th Annual IEEE Symposium on Logic i ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
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.


Suggestions