[{"publisher":"Springer","year":"2006","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","oa_version":"None","acknowledgement":"This research was supported in part by the Swiss National Science Foundation.","title":"Solving games without determinization","_id":"4437","date_updated":"2026-08-21T11:30:47Z","page":"395 - 410","volume":4207,"OA_type":"closed access","abstract":[{"text":"The synthesis of reactive systems requires the solution of two-player games on graphs with ω-regular objectives. When the objective is specified by a linear temporal logic formula or nondeterministic Büchi automaton, then previous algorithms for solving the game require the construction of an equivalent deterministic automaton. However, determinization for automata on infinite words is extremely complicated, and current implementations fail to produce deterministic automata even for relatively small inputs. We show how to construct, from a given nondeterministic Büchi automaton, an equivalent nondeterministic parity automaton that is good for solving games with objective . The main insight is that a nondeterministic automaton is good for solving games if it fairly simulates the equivalent deterministic automaton. In this way, we omit the determinization step in game solving and reactive synthesis. The fact that our automata are nondeterministic makes them surprisingly simple, amenable to symbolic implementation, and allows an incremental search for winning strategies.","lang":"eng"}],"intvolume":"      4207","month":"09","type":"conference","doi":"10.1007/11874683_26","status":"public","article_processing_charge":"No","language":[{"iso":"eng"}],"citation":{"apa":"Henzinger, T. A., &#38; Piterman, N. (2006). Solving games without determinization. In <i>Proceedings of the 20th international conference on Computer Science Logic</i> (Vol. 4207, pp. 395–410). Szeged, Hungary: Springer. <a href=\"https://doi.org/10.1007/11874683_26\">https://doi.org/10.1007/11874683_26</a>","ieee":"T. A. Henzinger and N. Piterman, “Solving games without determinization,” in <i>Proceedings of the 20th international conference on Computer Science Logic</i>, Szeged, Hungary, 2006, vol. 4207, pp. 395–410.","chicago":"Henzinger, Thomas A, and Nir Piterman. “Solving Games without Determinization.” In <i>Proceedings of the 20th International Conference on Computer Science Logic</i>, 4207:395–410. Springer, 2006. <a href=\"https://doi.org/10.1007/11874683_26\">https://doi.org/10.1007/11874683_26</a>.","short":"T.A. Henzinger, N. Piterman, in:, Proceedings of the 20th International Conference on Computer Science Logic, Springer, 2006, pp. 395–410.","ama":"Henzinger TA, Piterman N. Solving games without determinization. In: <i>Proceedings of the 20th International Conference on Computer Science Logic</i>. Vol 4207. Springer; 2006:395-410. doi:<a href=\"https://doi.org/10.1007/11874683_26\">10.1007/11874683_26</a>","mla":"Henzinger, Thomas A., and Nir Piterman. “Solving Games without Determinization.” <i>Proceedings of the 20th International Conference on Computer Science Logic</i>, vol. 4207, Springer, 2006, pp. 395–410, doi:<a href=\"https://doi.org/10.1007/11874683_26\">10.1007/11874683_26</a>.","ista":"Henzinger TA, Piterman N. 2006. Solving games without determinization. Proceedings of the 20th international conference on Computer Science Logic. CSL: Computer Science Logic, LNCS, vol. 4207, 395–410."},"publication_status":"published","conference":{"location":"Szeged, Hungary","name":"CSL: Computer Science Logic","end_date":"2006-09-29","start_date":"2006-09-25"},"publication":"Proceedings of the 20th international conference on Computer Science Logic","author":[{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Piterman","full_name":"Piterman, Nir","first_name":"Nir"}],"date_created":"2018-12-11T12:08:51Z","extern":"1","publist_id":"295","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783540454595"],"isbn":["9783540454588"]},"alternative_title":["LNCS"],"date_published":"2006-09-20T00:00:00Z","day":"20"},{"date_created":"2018-12-11T12:05:44Z","title":"Concurrent games with tail objectives","_id":"3891","author":[{"first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","last_name":"Chatterjee","orcid":"0000-0002-4561-241X","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87"}],"date_updated":"2026-08-27T07:36:31Z","OA_type":"closed access","alternative_title":["LNCS "],"extern":"1","publist_id":"2272","volume":4207,"page":"256 - 270","publication_identifier":{"isbn":["9783540454588"],"eisbn":["9783540454595"]},"intvolume":"      4207","date_published":"2006-09-28T00:00:00Z","month":"09","abstract":[{"text":"We study infinite stochastic games played by two-players over a finite state space, with objectives specified by sets of infinite traces. The games are concurrent (players make moves simultaneously and independently), stochastic (the next state is determined by a probability distribution that depends on the current state and chosen moves of the players) and infinite (proceeds for infinite number of rounds). The analysis of concurrent stochastic games can be classified into: quantitative analysis, analyzing the optimum value of the game; and qualitative analysis, analyzing the set of states with optimum value 1. We consider concurrent games with tail objectives, i.e., objectives that are independent of the finite-prefix of traces, and show that the class of tail objectives are strictly richer than the omega-regular objectives. We develop new proof techniques to extend several properties of concurrent games with omega-regular objectives to concurrent games with tail objectives. We prove the positive limit-one property for tail objectives, that states for all concurrent games if the optimum value for a player is positive for a tail objective Phi at some state, then there is a state where the optimum value is 1 for Phi, for the player. We also show that the optimum values of zero-sum (strictly conflicting objectives) games with tail objectives can be related to equilibrium values of nonzero-sum (not strictly conflicting objectives) games with simpler reachability objectives. A consequence of our analysis presents a polynomial time reduction of the quantitative analysis of tail objectives to the qualitative analysis for the sub-class of one-player stochastic games (Markov decision processes).","lang":"eng"}],"day":"28","type":"conference","publisher":"Springer Nature","doi":"10.1007/11874683_17","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","citation":{"mla":"Chatterjee, Krishnendu. “Concurrent Games with Tail Objectives.” <i>Proceedings of the 20th International Conference on Computer Science Logic</i>, vol. 4207, Springer Nature, 2006, pp. 256–70, doi:<a href=\"https://doi.org/10.1007/11874683_17\">10.1007/11874683_17</a>.","ista":"Chatterjee K. 2006. Concurrent games with tail objectives. Proceedings of the 20th international conference on Computer Science Logic. CSL: Computer Science Logic, LNCS , vol. 4207, 256–270.","ama":"Chatterjee K. Concurrent games with tail objectives. In: <i>Proceedings of the 20th International Conference on Computer Science Logic</i>. Vol 4207. Springer Nature; 2006:256-270. doi:<a href=\"https://doi.org/10.1007/11874683_17\">10.1007/11874683_17</a>","chicago":"Chatterjee, Krishnendu. “Concurrent Games with Tail Objectives.” In <i>Proceedings of the 20th International Conference on Computer Science Logic</i>, 4207:256–70. Springer Nature, 2006. <a href=\"https://doi.org/10.1007/11874683_17\">https://doi.org/10.1007/11874683_17</a>.","short":"K. Chatterjee, in:, Proceedings of the 20th International Conference on Computer Science Logic, Springer Nature, 2006, pp. 256–270.","apa":"Chatterjee, K. (2006). Concurrent games with tail objectives. In <i>Proceedings of the 20th international conference on Computer Science Logic</i> (Vol. 4207, pp. 256–270). Szeged, Hungary: Springer Nature. <a href=\"https://doi.org/10.1007/11874683_17\">https://doi.org/10.1007/11874683_17</a>","ieee":"K. Chatterjee, “Concurrent games with tail objectives,” in <i>Proceedings of the 20th international conference on Computer Science Logic</i>, Szeged, Hungary, 2006, vol. 4207, pp. 256–270."},"article_processing_charge":"No","language":[{"iso":"eng"}],"year":"2006","status":"public","publication_status":"published","oa_version":"None","conference":{"location":"Szeged, Hungary","end_date":"2006-09-29","name":"CSL: Computer Science Logic","start_date":"2006-09-25"},"publication":"Proceedings of the 20th international conference on Computer Science Logic"},{"month":"11","intvolume":"      4207","abstract":[{"text":"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 Buchi 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.","lang":"eng"}],"OA_type":"closed access","page":"287 - 302","volume":4207,"date_updated":"2026-08-27T08:04:08Z","title":"Algorithms for omega-regular games with imperfect information","_id":"3889","acknowledgement":"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.","oa_version":"None","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2006","publisher":"Springer Nature","day":"13","date_published":"2006-11-13T00:00:00Z","alternative_title":["LNCS"],"publication_identifier":{"issn":["0302-9743"],"eissn":["1611-3349"],"isbn":["9783540454588"],"eisbn":["9783540454595"]},"publist_id":"2276","extern":"1","date_created":"2018-12-11T12:05:43Z","author":[{"full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"first_name":"Laurent","full_name":"Doyen, Laurent","last_name":"Doyen"},{"first_name":"Thomas A","full_name":"Henzinger, Thomas A","last_name":"Henzinger","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Raskin","full_name":"Raskin, Jean","first_name":"Jean"}],"publication":"Proceedings of the 20th international conference on Computer Science Logic","conference":{"start_date":"2006-09-25","name":"CSL: Computer Science Logic","end_date":"2006-09-29","location":"Szeged, Hungary"},"publication_status":"published","citation":{"ama":"Chatterjee K, Doyen L, Henzinger TA, Raskin J. Algorithms for omega-regular games with imperfect information. In: <i>Proceedings of the 20th International Conference on Computer Science Logic</i>. Vol 4207. Springer Nature; 2006:287-302. doi:<a href=\"https://doi.org/10.1007/11874683_19\">10.1007/11874683_19</a>","mla":"Chatterjee, Krishnendu, et al. “Algorithms for Omega-Regular Games with Imperfect Information.” <i>Proceedings of the 20th International Conference on Computer Science Logic</i>, vol. 4207, Springer Nature, 2006, pp. 287–302, doi:<a href=\"https://doi.org/10.1007/11874683_19\">10.1007/11874683_19</a>.","ista":"Chatterjee K, Doyen L, Henzinger TA, Raskin J. 2006. Algorithms for omega-regular games with imperfect information. Proceedings of the 20th international conference on Computer Science Logic. CSL: Computer Science Logic, LNCS, vol. 4207, 287–302.","apa":"Chatterjee, K., Doyen, L., Henzinger, T. A., &#38; Raskin, J. (2006). Algorithms for omega-regular games with imperfect information. In <i>Proceedings of the 20th international conference on Computer Science Logic</i> (Vol. 4207, pp. 287–302). Szeged, Hungary: Springer Nature. <a href=\"https://doi.org/10.1007/11874683_19\">https://doi.org/10.1007/11874683_19</a>","ieee":"K. Chatterjee, L. Doyen, T. A. Henzinger, and J. Raskin, “Algorithms for omega-regular games with imperfect information,” in <i>Proceedings of the 20th international conference on Computer Science Logic</i>, Szeged, Hungary, 2006, vol. 4207, pp. 287–302.","chicago":"Chatterjee, Krishnendu, Laurent Doyen, Thomas A Henzinger, and Jean Raskin. “Algorithms for Omega-Regular Games with Imperfect Information.” In <i>Proceedings of the 20th International Conference on Computer Science Logic</i>, 4207:287–302. Springer Nature, 2006. <a href=\"https://doi.org/10.1007/11874683_19\">https://doi.org/10.1007/11874683_19</a>.","short":"K. Chatterjee, L. Doyen, T.A. Henzinger, J. Raskin, in:, Proceedings of the 20th International Conference on Computer Science Logic, Springer Nature, 2006, pp. 287–302."},"language":[{"iso":"eng"}],"article_processing_charge":"No","status":"public","doi":"10.1007/11874683_19","type":"conference"},{"date_published":"2006-09-28T00:00:00Z","day":"28","date_created":"2018-12-11T12:03:39Z","author":[{"id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","last_name":"Chatterjee","full_name":"Chatterjee, Krishnendu","first_name":"Krishnendu"}],"alternative_title":["LNCS "],"publist_id":"2888","extern":"1","publication_identifier":{"eissn":["1611-3349"],"issn":["0302-9743"],"eisbn":["9783540454595"],"isbn":["9783540454588"]},"publication_status":"published","conference":{"start_date":"2006-09-25","name":"CSL: Computer Science Logic","end_date":"2006-09-29","location":"Szeged, Hungary"},"publication":"Proceedings of the 20th international conference on Computer Science Logic","type":"conference","doi":"10.1007/11874683_18","article_processing_charge":"No","citation":{"short":"K. Chatterjee, in:, Proceedings of the 20th International Conference on Computer Science Logic, Springer Nature, 2006, pp. 271–286.","chicago":"Chatterjee, Krishnendu. “Nash Equilibrium for Upward-Closed Objectives.” In <i>Proceedings of the 20th International Conference on Computer Science Logic</i>, 4207:271–86. Springer Nature, 2006. <a href=\"https://doi.org/10.1007/11874683_18\">https://doi.org/10.1007/11874683_18</a>.","ieee":"K. Chatterjee, “Nash equilibrium for upward-closed objectives,” in <i>Proceedings of the 20th international conference on Computer Science Logic</i>, Szeged, Hungary, 2006, vol. 4207, pp. 271–286.","apa":"Chatterjee, K. (2006). Nash equilibrium for upward-closed objectives. In <i>Proceedings of the 20th international conference on Computer Science Logic</i> (Vol. 4207, pp. 271–286). Szeged, Hungary: Springer Nature. <a href=\"https://doi.org/10.1007/11874683_18\">https://doi.org/10.1007/11874683_18</a>","ista":"Chatterjee K. 2006. Nash equilibrium for upward-closed objectives. Proceedings of the 20th international conference on Computer Science Logic. CSL: Computer Science Logic, LNCS , vol. 4207, 271–286.","mla":"Chatterjee, Krishnendu. “Nash Equilibrium for Upward-Closed Objectives.” <i>Proceedings of the 20th International Conference on Computer Science Logic</i>, vol. 4207, Springer Nature, 2006, pp. 271–86, doi:<a href=\"https://doi.org/10.1007/11874683_18\">10.1007/11874683_18</a>.","ama":"Chatterjee K. Nash equilibrium for upward-closed objectives. In: <i>Proceedings of the 20th International Conference on Computer Science Logic</i>. Vol 4207. Springer Nature; 2006:271-286. doi:<a href=\"https://doi.org/10.1007/11874683_18\">10.1007/11874683_18</a>"},"language":[{"iso":"eng"}],"status":"public","intvolume":"      4207","month":"09","abstract":[{"lang":"eng","text":"We study infinite stochastic games played by n-players on a finite graph with goals specified by sets of infinite traces. The games are concurrent (each player simultaneously and independently chooses an action at each round), stochastic (the next state is determined by a probability distribution depending on the current state and the chosen actions), infinite (the game continues for an infinite number of rounds), nonzero-sum (the players’ goals are not necessarily conflicting), and undiscounted. We show that if each player has an upward-closed objective, then there exists an ε-Nash equilibrium in memoryless strategies, for every ε&gt;0; and exact Nash equilibria need not exist. Upward-closure of an objective means that if a set Z of infinitely repeating states is winning, then all supersets of Z of infinitely repeating states are also winning. Memoryless strategies are strategies that are independent of history of plays and depend only on the current state. We also study the complexity of finding values (payoff profile) of an ε-Nash equilibrium. We show that the values of an ε-Nash equilibrium in nonzero-sum concurrent games with upward-closed objectives for all players can be computed by computing ε-Nash equilibrium values of nonzero-sum concurrent games with reachability objectives for all players and a polynomial procedure. As a consequence we establish that values of an ε-Nash equilibrium can be computed in TFNP (total functional NP), and hence in EXPTIME. "}],"title":"Nash equilibrium for upward-closed objectives","_id":"3499","date_updated":"2026-08-28T11:22:40Z","OA_type":"closed access","volume":4207,"page":"271 - 286","oa_version":"None","acknowledgement":"This research was supported in part by the NSF grants CCR-0225610 and CCR- 0234690, and by the SNSF under the Indo-Swiss Joint Research Programme.","publisher":"Springer Nature","user_id":"317138e5-6ab7-11ef-aa6d-ffef3953e345","year":"2006"}]
