Paper: Three-Valued Abstractions of Games: Uncertainty, but with Precision (at LICS 2004)

Authors: Luca de Alfaro Patrice Godefroid Radha Jagadeesan

Abstract

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.

BibTeX

  @InProceedings{deAlfaroGodefroidJa-ThreeValuedAbstract,
    author = 	 {Luca de Alfaro and Patrice Godefroid and Radha Jagadeesan},
    title = 	 {Three-Valued Abstractions of Games: Uncertainty, but with Precision},
    booktitle =  {Proceedings of the Nineteenth Annual IEEE Symposium on Logic in Computer Science (LICS 2004)},
    year =	 {2004},
    month =	 {July}, 
    pages =      {170--179},
    location =   {Turku, Finland}, 
    publisher =	 {IEEE Computer Society Press}
  }