@inproceedings{3357, abstract = {We consider two-player graph games whose objectives are request-response condition, i.e conjunctions of conditions of the form "if a state with property Rq is visited, then later a state with property Rp is visited". The winner of such games can be decided in EXPTIME and the problem is known to be NP-hard. In this paper, we close this gap by showing that this problem is, in fact, EXPTIME-complete. We show that the problem becomes PSPACE-complete if we only consider games played on DAGs, and NP-complete or PTIME-complete if there is only one player (depending on whether he wants to enforce or spoil the request-response condition). We also present near-optimal bounds on the memory needed to design winning strategies for each player, in each case.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Horn, Florian}, editor = {Dediu, Adrian-Horia and Inenaga, Shunsuke and Martín-Vide, Carlos}, location = {Tarragona, Spain}, pages = {227 -- 237}, publisher = {Springer}, title = {{The complexity of request-response games}}, doi = {10.1007/978-3-642-21254-3_17}, volume = {6638}, year = {2011}, } @inproceedings{489, abstract = {Graph games of infinite length are a natural model for open reactive processes: one player represents the controller, trying to ensure a given specification, and the other represents a hostile environment. The evolution of the system depends on the decisions of both players, supplemented by chance. In this work, we focus on the notion of randomised strategy. More specifically, we show that three natural definitions may lead to very different results: in the most general cases, an almost-surely winning situation may become almost-surely losing if the player is only allowed to use a weaker notion of strategy. In more reasonable settings, translations exist, but they require infinite memory, even in simple cases. Finally, some traditional problems becomes undecidable for the strongest type of strategies.}, author = {Cristau, Julien and David, Claire and Horn, Florian}, booktitle = {Proceedings of GandALF 2010}, location = {Minori, Amalfi Coast, Italy}, pages = {30 -- 39}, publisher = {Open Publishing Association}, title = {{How do we remember the past in randomised strategies? }}, doi = {10.4204/EPTCS.25.7}, volume = {25}, year = {2010}, } @inproceedings{3854, abstract = {Graph games of infinite length provide a natural model for open reactive systems: one player (Eve) represents the controller and the other player (Adam) represents the environment. The evolution of the system depends on the decisions of both players. The specification for the system is usually given as an ω-regular language L over paths and Eve’s goal is to ensure that the play belongs to L irrespective of Adam’s behaviour. The classical notion of winning strategies fails to capture several interesting scenarios. For example, strong fairness (Streett) conditions are specified by a number of request-grant pairs and require every pair that is requested infinitely often to be granted infinitely often: Eve might win just by preventing Adam from making any new request, but a “better” strategy would allow Adam to make as many requests as possible and still ensure fairness. To address such questions, we introduce the notion of obliging games, where Eve has to ensure a strong condition Φ, while always allowing Adam to satisfy a weak condition Ψ. We present a linear time reduction of obliging games with two Muller conditions Φ and Ψ to classical Muller games. We consider obliging Streett games and show they are co-NP complete, and show a natural quantitative optimisation problem for obliging Streett games is in FNP. We also show how obliging games can provide new and interesting semantics for multi-player games.}, author = {Chatterjee, Krishnendu and Horn, Florian and Löding, Christof}, location = {Paris, France}, pages = {284 -- 296}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik}, title = {{Obliging games}}, doi = {10.1007/978-3-642-15375-4_20}, volume = {6269}, year = {2010}, } @misc{5394, abstract = {We consider two-player games played on graphs with request-response and finitary Streett objectives. We show these games are PSPACE-hard, improving the previous known NP-hardness. We also improve the lower bounds on memory required by the winning strategies for the players.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Horn, Florian}, issn = {2664-1690}, pages = {11}, publisher = {IST Austria}, title = {{Improved lower bounds for request-response and finitary Streett games}}, doi = {10.15479/AT:IST-2009-0002}, year = {2009}, } @article{3870, abstract = {Games on graphs with omega-regular objectives provide a model for the control and synthesis of reactive systems. Every omega-regular objective can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens “eventually.” Two main strengths of the classical, infinite-limit formulation of liveness are robustness (independence from the granularity of transitions) and simplicity (abstraction of complicated time bounds). However, the classical liveness formulation suffers from the drawback that the time until something good happens may be unbounded. A stronger formulation of liveness, so-called finitary liveness, overcomes this drawback, while still retaining robustness and simplicity. Finitary liveness requires that there exists an unknown, fixed bound b such that something good happens within b transitions. While for one-shot liveness (reachability) objectives, classical and finitary liveness coincide, for repeated liveness (Buchi) objectives, the finitary formulation is strictly stronger. In this work we study games with finitary parity and Streett objectives. We prove the determinacy of these games, present algorithms for solving these games, and characterize the memory requirements of winning strategies. We show that finitary parity games can be solved in polynomial time, which is not known for infinitary parity games. For finitary Streett games, we give an EXPTIME algorithm and show that the problem is NP-hard. Our algorithms can be used, for example, for synthesizing controllers that do not let the response time of a system increase without bound.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Horn, Florian}, journal = {ACM Transactions on Computational Logic (TOCL)}, number = {1}, publisher = {ACM}, title = {{Finitary winning in omega-regular games}}, doi = {10.1145/1614431.1614432}, volume = {11}, year = {2009}, } @inproceedings{4543, abstract = {The synthesis of a reactive system with respect to all omega-regular specification requires the solution of a graph game. Such games have been extended in two natural ways. First, a game graph can be equipped with probabilistic choices between alternative transitions, thus allowing the, modeling of uncertain behaviour. These are called stochastic games. Second, a liveness specification can he strengthened to require satisfaction within all unknown but bounded amount of time. These are called finitary objectives. We study. for the first time, the, combination of Stochastic games and finitary objectives. We characterize the requirements on optimal strategies and provide algorithms for Computing the maximal achievable probability of winning stochastic games with finitary parity or Street, objectives. Most notably the set of state's from which a player can win with probability . for a finitary parity objective can he computed in polynomial time even though no polynomial-time algorithm is known in the nonfinitary case.}, author = {Chatterjee, Krishnendu and Henzinger, Thomas A and Horn, Florian}, location = {High Tatras, Slovakia}, pages = {34 -- 54}, publisher = {Springer}, title = {{Stochastic games with finitary objectives}}, doi = {10.1007/978-3-642-03816-7_4}, volume = {5734}, year = {2009}, }