Abstract
We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller that does not see the private state of the plant. Our main results are twofold. First, we give a fixed-point algorithm for computing the set of states from which a player can win with a deterministic observation-based strategy for any omega-regular objective. The fixed point is computed in the lattice of antichains of state sets. This algorithm has the advantages of being directed by the objective and of avoiding an explicit subset construction on the game graph. Second, we give an algorithm for computing the set of states from which a player can win with probability 1 with a randomized observation-based strategy for a Büchi objective. This set is of interest because in the absence of perfect information, randomized strategies are more powerful than deterministic ones. We show that our algorithms are optimal by proving matching lower bounds.
This research was supported in part by the NSF grants CCR-0225610 and CCR-0234690, by the SNSF under the Indo-Swiss Joint Research Programme, and by the FRFC project “Centre Fédéré en Vérification” funded by the FNRS under grant 2.4530.02.
A fuller version with proofs is available as UC Berkeley Tech. Rep. EECS-2006-89.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1–17. Springer, Heidelberg (1989)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)
Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. J. ACM 28, 114–133 (1981)
Chatterjee, K., Henzinger, T.A.: Semiperfect information games. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 1–18. Springer, Heidelberg (2005)
de Alfaro, L., Henzinger, T.A.: Concurrent ω-regular games. In: Proc. LICS, pp. 141–154. IEEE Computer Society Press, Los Alamitos (2000)
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proc. FSE, pp. 109–120. ACM Press, New York (2001)
de Alfaro, L., Henzinger, T.A., Kupferman, O.: Concurrent reachability games. In: Proc. FOCS, pp. 564–575. IEEE Computer Society Press, Los Alamitos (1998)
de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: Dynamic programs for ω-regular objectives. In: Proc. LICS, pp. 279–290. IEEE Computer Society Press, Los Alamitos (2001)
De Wulf, M., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: A new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 17–30. Springer, Heidelberg (2006)
De Wulf, M., Doyen, L., Raskin, J.-F.: A lattice theory for solving games of imperfect information. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 153–168. Springer, Heidelberg (2006)
Dill, D.: Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. MIT Press, Cambridge (1989)
Emerson, E.A., Jutla, C.S.: Tree automata, μ-calculus, and determinacy. In: Proc. FOCS, pp. 368–377. IEEE Computer Society Press, Los Alamitos (1991)
Kechris, A.: Classical Descriptive Set Theory. Springer, Heidelberg (1995)
Kupferman, O., Vardi, M.Y.: Synthesis with incomplete informatio. In: Barringer, H., et al. (eds.) Advances in Temporal Logic, pp. 109–127. Kluwer, Dordrecht (1999)
Littman, M.L.: Algorithms for Sequential Decision Making. PhD Thesis, Brown Univ. (1996)
Martin, D.: Borel determinacy. Annals of Mathematics 102, 363–371 (1975)
Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652–671. Springer, Heidelberg (1989)
Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete-event processes. SIAM J. Control and Optimization 25, 206–230 (1987)
Reif, J.H.: The complexity of two-player games of incomplete information. J. Computer and System Sciences 29, 274–301 (1984)
Thomas, W.: Languages, automata, and logic. In: Rozenberg, G., et al. (eds.) Handbook of Formal Languages, vol. 3, pp. 389–455. Springer, Heidelberg (1997)
Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state systems. In: Proc. FOCS, pp. 327–338. IEEE Computer Society, Los Alamitos (1985)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, JF. (2006). Algorithms for Omega-Regular Games with Imperfect Information . In: Ésik, Z. (eds) Computer Science Logic. CSL 2006. Lecture Notes in Computer Science, vol 4207. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11874683_19
Download citation
DOI: https://doi.org/10.1007/11874683_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-45458-8
Online ISBN: 978-3-540-45459-5
eBook Packages: Computer ScienceComputer Science (R0)