Finitary winning in omega-regular games Journal Article

Author(s): Chatterjee, Krishnendu; Henzinger, Thomas A; Horn, Florian
Article Title: Finitary winning in omega-regular games
Affiliation IST Austria
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.
Journal Title: ACM Transactions on Computational Logic (TOCL)
Volume: 11
Issue 1:2
ISSN: 1557-945X
Publisher: ACM  
Date Published: 2009-10-01
Start Page: 1
End Page: 27
Sponsor: This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, the NSF grants CCR-0132780, CNS-0720884, and CCR- 225610, by the Swiss National Science Foundation, by the COMBEST project of the European Union, and EU-TMR network Games.
DOI: 10.1145/1614431.1614432
Notes: We thank anonymous reviewers for useful comments.
Open access: yes (repository)
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work