×

Strategy construction for parity games with imperfect information. (English) Zbl 1232.91007

Summary: We consider two-player parity games with imperfect information in which strategies rely on observations that provide imperfect information about the history of a play. To solve such games, i.e., to determine the winning regions of players and corresponding winning strategies, one can use the subset construction to build an equivalent perfect-information game. Recently, an algorithm that avoids the inefficient subset construction has been proposed. The algorithm performs a fixed-point computation in a lattice of antichains, thus maintaining a succinct representation of state sets. However, this representation does not allow to recover winning strategies.
In this paper, we build on the antichain approach to develop an algorithm for constructing the winning strategies in parity games of imperfect information. One major obstacle in adapting the classical procedure is that the complementation of attractor sets would break the invariant of downward-closedness on which the antichain representation relies. We overcome this difficulty by decomposing problem instances recursively into games with a combination of reachability, safety, and simpler parity conditions. We also report on an experimental implementation of our algorithm; to our knowledge, this is the first implementation of a procedure for solving imperfect-information parity games on graphs.

MSC:

91A05 2-person games

Software:

CUDD; Alpaga; Antichains
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Thomas, W., On the synthesis of strategies in infinite games, (Proc. of STACS 1995 (1995), Springer-Verlag), 1-13 · Zbl 1379.68233
[2] (Grädel, E.; Thomas, W.; Wilke, T., Automata, Logics, and Infinite Games. Automata, Logics, and Infinite Games, LNCS 2500 (2002), Springer-Verlag) · Zbl 1011.00037
[3] Emerson, E. A.; Jutla, C. S., Tree automata, mu-calculus and determinacy, (Proc. of FoCS 1991 (1991), IEEE), 368-377
[4] Fudenberg, D.; Tirole, J., Game Theory (1991), MIT Press · Zbl 1339.91001
[5] Reif, J., The complexity of two-player games of incomplete information, Journal of Computer and System Sciences, 29, 274-301 (1984) · Zbl 0551.90100
[7] Henzinger, T. A.; Jhala, R.; Majumdar, R., Counterexample-guided control, (Proc. of ICALP 2003. Proc. of ICALP 2003, LNCS 2719 (2003), Springer-Verlag), 886-902 · Zbl 1039.68555
[8] McNaughton, R., Infinite games played on finite graphs, Annals of Pure and Applied Logic, 65, 2, 149-184 (1993) · Zbl 0798.90151
[9] Zielonka, W., Infinite games on finitely coloured graphs with applications to automata on infinite trees, Theoretical Computer Science, 200, 135-183 (1998) · Zbl 0915.68120
[10] Thomas, W., Languages, automata, and logic, Handbook of Formal Languages, 3, 389-455 (1997)
[12] De Wulf, M.; Doyen, L.; Henzinger, T. A.; Raskin, J.-F., Antichains: a new algorithm for checking universality of finite automata, (Proc. of CAV 2006. Proc. of CAV 2006, LNCS 4144 (2006), Springer-Verlag), 17-30 · Zbl 1188.68171
[13] De Wulf, M.; Doyen, L.; Maquet, N.; Raskin, J.-F., Antichains: alternative algorithms for LTL satisfiability and model-checking, (Proc. of TACAS 2008. Proc. of TACAS 2008, LNCS 4693 (2008), Springer-Verlag), 63-77 · Zbl 1134.68404
[15] Berwanger, D.; Chatterjee, K.; De Wulf, M.; Doyen, L.; Henzinger, T. A., Alpaga: a tool for solving parity games with imperfect information, (Proc. of TACAS 2009. Proc. of TACAS 2009, LNCS 5505 (2009), Springer), 58-61
[18] Bernet, J.; Janin, D.; Walukiewicz, I., Permissive strategies: from parity games to safety games, Informatique Théorique et Applications, 36, 3, 261-275 (2002) · Zbl 1090.91514
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.