Document Open Access Logo

Abstraction Refinement for Games with Incomplete Information

Authors Rayna Dimitrova, Bernd Finkbeiner



PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2008.1751.pdf
  • Filesize: 441 kB
  • 12 pages

Document Identifiers

Author Details

Rayna Dimitrova
Bernd Finkbeiner

Cite AsGet BibTex

Rayna Dimitrova and Bernd Finkbeiner. Abstraction Refinement for Games with Incomplete Information. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science. Leibniz International Proceedings in Informatics (LIPIcs), Volume 2, pp. 175-186, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2008)
https://doi.org/10.4230/LIPIcs.FSTTCS.2008.1751

Abstract

Counterexample-guided abstraction refinement (CEGAR) is used in automated software analysis to find suitable finite-state abstractions of infinite-state systems. In this paper, we extend CEGAR to games with incomplete information, as they commonly occur in controller synthesis and modular verification. The challenge is that, under incomplete information, one must carefully account for the knowledge available to the player: the strategy must not depend on information the player cannot see. We propose an abstraction mechanism for games under incomplete information that incorporates the approximation of the players\' moves into a knowledge-based subset construction on the abstract state space. This abstraction results in a perfect-information game over a finite graph. The concretizability of abstract strategies can be encoded as the satisfiability of strategy-tree formulas. Based on this encoding, we present an interpolation-based approach for selecting new predicates and provide sufficient conditions for the termination of the resulting refinement loop.
Keywords
  • Automatic abstraction refinement
  • synthesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail