License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2008.1751
URN: urn:nbn:de:0030-drops-17510
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1751/
Go to the corresponding LIPIcs Volume Portal

Dimitrova, Rayna ; Finkbeiner, Bernd

Abstraction Refinement for Games with Incomplete Information

pdf-format:
08004.DimitrovaRayna.1751.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{dimitrova_et_al:LIPIcs:2008:1751,
  author =	{Rayna Dimitrova and Bernd Finkbeiner},
  title =	{{Abstraction Refinement for Games with Incomplete Information}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science},
  pages =	{175--186},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-08-8},
  ISSN =	{1868-8969},
  year =	{2008},
  volume =	{2},
  editor =	{Ramesh Hariharan and Madhavan Mukund and V Vinay},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2008/1751},
  URN =		{urn:nbn:de:0030-drops-17510},
  doi =		{10.4230/LIPIcs.FSTTCS.2008.1751},
  annote =	{Keywords: Automatic abstraction refinement, synthesis}
}

Keywords: Automatic abstraction refinement, synthesis
Collection: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science
Issue Date: 2008
Date of publication: 05.12.2008

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI