Abstract
The theory of games is a prominent tool in the controller synthesis problem. The class of ω-regular games, in particular, offers a clear and robust model of specifications, and present an alternative vision of several logic-related problems. Each ω-regular condition can be expressed by a combination of safety and liveness conditions. An issue with the classical definition of liveness specifications is that there is no control over the time spent between two successive occurrences of the desired events. Finitary logics were defined to handle this problem, and recently, Chatterjee and Henzinger introduced games based on a finitary notion of liveness. They defined and studied finitary parity and Streett winning conditions. We present here faster algorithms for these games, as well as an improved upper bound on the memory needed by Eve in the Streett case.
Work supported by the EU-TMR network GAMES. Some of this work was done in RWTH, Aachen.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Henzinger, T.A.: Finitary Fairness. In: Proceedings of Logic In Computer Science, LICS’94, pp. 52–61. IEEE Computer Society Press, Los Alamitos (1994)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49, 672–713 (2002)
Bojanczyk, M., Colcombet, T.: Bounds in ω-regularity. In: Proceedings of Logic In Computer Science, LICS’06, pp. 285–296. IEEE Computer Society Press, Los Alamitos (2006)
Buhrke, N., Lescow, H., Vöge, J.: Strategy Construction in Infinite Games with Streett and Rabin Chain Winning Conditions. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 207–224. Springer, Heidelberg (1996)
Chatterjee, K., Henzinger, T.A.: Finitary Winning in omega-Regular Games. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol. 3920, pp. 257–271. Springer, Heidelberg (2006)
Chatterjee, K.: Linear Time Algorithm for Weak Parity Games. Technical Report No. UCB/EECS-2006-153. University of California at Berkeley (2006)
Dziembowski, S., Jurdziński, M., Walukiewicz, I.: How Much Memory Is Needed to Win Infinite Games? In: Proceedings of Logic In Computer Science, LICS’97, pp. 99–110. IEEE Computer Society Press, Los Alamitos (1997)
Jurdziński, M.: Small Progress Measures for Solving Parity Games. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 290–301. Springer, Heidelberg (2000)
Horn, F.: Streett Games on Finite Graphs. In: Games in Design and Verification, Workshop collocated with Computer Aided Verfication (2005)
Löding, C., Thomas, W.: Alternating Automata and Logics over Infinite Words. In: Watanabe, O., et al. (eds.) TCS 2000. LNCS, vol. 1872, pp. 521–535. Springer, Heidelberg (2000)
Manna, Z., Pnueli, A.: The Temporal Logic of Concurrent and Reactive System. Springer, Heidelberg (2002)
Neumann, J., Szepietowski, A., Walukiewicz, I.: Complexity of weak acceptance conditions in tree automata. Information Processing Letters 84, 181–187 (2002)
Thomas, W.: On the Synthesis of Strategies in Infinite Games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)
Vöge, J., Jurdziński, M.: A Discrete Strategy Improvement Algorithm for Solving Parity Games. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 202–215. Springer, Heidelberg (2000)
Wallmeier, N., Hutten, P., Thomas, W.: Symbolic Synthesis of Finite-State Controllers for Request-Response Specifications. In: H. Ibarra, O., Dang, Z. (eds.) CIAA 2003. LNCS, vol. 2759, pp. 11–22. Springer, Heidelberg (2003)
Zielonka, W.: Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees. Theoretical Computer Science 200(1-2), 135–183 (1998)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Horn, F. (2007). Faster Algorithms for Finitary Games. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_36
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)