Berwanger, Dietmar; Chatterjee, Krishnendu; De Wulf, Martin; Doyen, Laurent; Henzinger, Thomas A.
Strategy construction for parity games with imperfect information. (English) Zbl 1232.91007
Inf. Comput. 208, No. 10, 1206-1220 (2010).
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.
91A05 2-person games
Alpaga; Antichains; CUDD
\textit{D. Berwanger} et al., Inf. Comput. 208, No. 10, 1206--1220 (2010; Zbl 1232.91007)
[1] Thomas, W., On the synthesis of strategies in infinite games, (), 1-13 · Zbl 1379.68233
[2] ()
[3] Emerson, E.A.; Jutla, C.S., Tree automata, mu-calculus and determinacy, (), 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
[6] K. Chatterjee, L. Doyen, T.A. Henzinger, J.-F. Raskin, Algorithms for omega-regular games of incomplete information, Logical Methods in Computer Science 3(3:4) (2007). · Zbl 1125.91028
[7] Henzinger, T.A.; Jhala, R.; Majumdar, R., Counterexample-guided control, (), 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)
[11] D. Berwanger, L. Doyen, On the power of imperfect information, in: Proc. of FSTTCS 2008, Dagstuhl Seminar Proceedings 08004, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), 2008. · Zbl 1248.68233
[12] De Wulf, M.; Doyen, L.; Henzinger, T.A.; Raskin, J.-F., Antichains: a new algorithm for checking universality of finite automata, (), 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, (), 63-77 · Zbl 1134.68404
[14] M. De Wulf, L. Doyen, J.-F. Raskin, A lattice theory for solving games of imperfect information, in: Proc. of HSCC 2006, LNCS 3927, Springer-Verlag, 2006, pp. 153-168, ISBN 3-540-33170-0. · Zbl 1178.93072
[15] Berwanger, D.; Chatterjee, K.; De Wulf, M.; Doyen, L.; Henzinger, T.A., Alpaga: a tool for solving parity games with imperfect information, (), 58-61
[16] F. Somenzi, CUDD: Colorado University Decision Diagram Package, 2005. Available from: <http://vlsi.colorado.edu/∼/fabio/CUDD/>.
[17] B. Jobstmann, A. Griesmayer, R. Bloem, Program repair as a game, in: Proc. of CAV: Computer-Aided Verification, LNCS 3576, Springer, 2005, pp. 226-238. · Zbl 1081.68572
[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
[19] K. Chatterjee, T.A. Henzinger, Assume-guarantee synthesis, in: Proc. of TACAS 2007, LNCS 4424, Springer, 2007, pp. 261-275. · Zbl 1186.68284
[20] A. Bouajjani, P. Habermehl, L. Holı´k, T. Touili, T. Vojnar, Antichain-based universality and inclusion testing over nondeterministic finite tree automata, in: Proc. of CIAA 2008, LNCS 5148, Springer, 2008, pp. 57-67. · Zbl 1172.68493
[21] L. Doyen, J.-F. Raskin, Antichains for the automata-based approach to model-checking, Journal Logical Methods in Computer Science 5(1:5) (2009). · Zbl 1164.68021