Skip to main content
SpringerLink
Log in

Strategy Synthesis for Multi-Dimensional Quantitative Objectives

  • Conference paper
CONCUR 2012 – Concurrency Theory (CONCUR 2012)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7454))

Included in the following conference series:

Abstract

Multi-dimensional mean-payoff and energy games provide the mathematical foundation for the quantitative study of reactive systems, and play a central role in the emerging quantitative theory of verification and synthesis. In this work, we study the strategy synthesis problem for games with such multi-dimensional objectives along with a parity condition, a canonical way to express ω-regular conditions. While in general, the winning strategies in such games may require infinite memory, for synthesis the most relevant problem is the construction of a finite-memory winning strategy (if one exists). Our main contributions are as follows. First, we show a tight exponential bound (matching upper and lower bounds) on the memory required for finite-memory winning strategies in both multi-dimensional mean-payoff and energy games along with parity objectives. This significantly improves the triple exponential upper bound for multi energy games (without parity) that could be derived from results in literature for games on VASS (vector addition systems with states). Second, we present an optimal symbolic and incremental algorithm to compute a finite-memory winning strategy (if one exists) in such games. Finally, we give a complete characterization of when finite memory of strategies can be traded off for randomness. In particular, we show that for one-dimension mean-payoff parity games, randomized memoryless strategies are as powerful as their pure finite-memory counterparts.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Chen, Y.-F., Holík, L., Mayr, R., Vojnar, T.: When Simulation Meets Antichains. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 158–174. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  2. Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)

    Article  MathSciNet  Google Scholar 

  3. Bernet, J., Janin, D., Walukiewicz, I.: Permissive strategies: from parity games to safety games. ITA 36(3), 261–275 (2002)

    MathSciNet  MATH  Google Scholar 

  4. Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better Quality in Synthesis through Quantitative Objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140–156. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  5. Bloem, R., Greimel, K., Henzinger, T.A., Jobstmann, B.: Synthesizing robust systems. In: Proc. of FMCAD, pp. 85–92. IEEE (2009)

    Google Scholar 

  6. Borosh, I., Treybig, B.: Bounds on positive integral solutions of linear diophantine equations. Proc. of the American Mathematical Society 55(2), 299–304 (1976)

    Article  MathSciNet  MATH  Google Scholar 

  7. Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Timed automata with observers under energy constraints. In: Proc. of HSCC, pp. 61–70. ACM (2010)

    Google Scholar 

  8. Bouyer, P., Markey, N., Olschewski, J., Ummels, M.: Measuring Permissiveness in Parity Games: Mean-Payoff Parity Games Revisited. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 135–149. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  9. Brázdil, T., Jančar, P., Kučera, A.: Reachability Games on Extended Vector Addition Systems with States. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010, Part II. LNCS, vol. 6199, pp. 478–489. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  10. Černý, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative Synthesis for Concurrent Programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 243–259. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Cerný, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. Theor. Comput. Sci. 413(1), 21–35 (2012)

    Article  MATH  Google Scholar 

  12. Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource Interfaces. In: Alur, R., Lee, I. (eds.) EMSOFT 2003. LNCS, vol. 2855, pp. 117–133. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Chatterjee, K., Doyen, L.: Energy Parity Games. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010, Part II. LNCS, vol. 6199, pp. 599–610. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  14. Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM Trans. Comput. Log. 11(4) (2010)

    Google Scholar 

  15. Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Generalized mean-payoff and energy games. In: Proc. of FSTTCS. LIPIcs, vol. 8, pp. 505–516. Schloss Dagstuhl - LZI (2010)

    Google Scholar 

  16. Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: Proc. of LICS, pp. 178–187. IEEE Computer Society (2005)

    Google Scholar 

  17. Chatterjee, K., Randour, M., Raskin, J.-F.: Strategy synthesis for multi-dimensional quantitative objectives. CoRR, abs/1201.5073 (2012), http://arxiv.org/abs/1201.5073

  18. Church, A.: Logic, arithmetic, and automata. In: Proceedings of the International Congress of Mathematicians, pp. 23–35. Institut Mittag-Leffler (1962)

    Google Scholar 

  19. de Alfaro, L., Henzinger, T.A.: Interface Theories for Component-Based Design. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 148–165. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  20. 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)

    Chapter  Google Scholar 

  21. Doyen, L., Raskin, J.-F.: Antichain Algorithms for Finite Automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 2–22. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  22. Doyen, L., Raskin, J.-F.: Games with imperfect information: Theory and algorithms. In: Lectures in Game Theory for Computer Scientists, pp. 185–212 (2011)

    Google Scholar 

  23. Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. Int. Journal of Game Theory 8(2), 109–113 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  24. Emerson, E.A., Jutla, C.: The complexity of tree automata and logics of programs. In: Proc. of FOCS, pp. 328–337. IEEE (1988)

    Google Scholar 

  25. Emerson, E.A., Jutla, C.: Tree automata, mu-calculus and determinacy. In: Proc. of FOCS, pp. 368–377. IEEE (1991)

    Google Scholar 

  26. Fahrenberg, U., Juhl, L., Larsen, K.G., Srba, J.: Energy Games in Multiweighted Automata. In: Cerone, A., Pihlajasaari, P. (eds.) ICTAC 2011. LNCS, vol. 6916, pp. 95–115. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  27. Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol. 2500. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  28. Gurevich, Y., Harrington, L.: Trees, automata, and games. In: Proc. of STOC, pp. 60–65. ACM (1982)

    Google Scholar 

  29. Henzinger, T.A., Kupferman, O., Rajamani, S.: Fair simulation. Information and Computation 173(1), 64–81 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  30. Martin, D.A.: The determinacy of Blackwell games. The Journal of Symbolic Logic 63(4), 1565–1581 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  31. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. of POPL, pp. 179–190 (1989)

    Google Scholar 

  32. Rackoff, C.: The covering and boundedness problems for vector addition systems. Theor. Comput. Sci. 6, 223–231 (1978)

    Article  MathSciNet  MATH  Google Scholar 

  33. Ramadge, P.J., Wonham, W.M.: Supervisory control of a class of discrete-event processes. SIAM Journal of Control and Optimization 25(1), 206–230 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  34. Rosier, L.E., Yen, H.-C.: A multiparameter analysis of the boundedness problem for vector addition systems. J. Comput. Syst. Sci. 32(1), 105–135 (1986)

    Article  MathSciNet  MATH  Google Scholar 

  35. Thomas, W.: Languages, automata, and logic. In: Handbook of Formal Languages, vol.3: Beyond Words, ch. 7, pp. 389–455. Springer (1997)

    Google Scholar 

  36. Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. of FOCS, pp. 327–338. IEEE Computer Society (1985)

    Google Scholar 

  37. Velner, Y., Rabinovich, A.: Church Synthesis Problem for Noisy Input. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 275–289. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  38. Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science 200(1-2), 135–183 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  39. Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theoretical Computer Science 158, 343–359 (1996)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IST Austria (Institute of Science and Technology Austria), Austria

    Krishnendu Chatterjee

  2. Institut d’Informatique, Université de Mons (UMONS), Belgium

    Mickael Randour

  3. Départment d’Informatique, Université Libre de Bruxelles (U.L.B.), Belgium

    Jean-François Raskin

Authors
  1. Krishnendu Chatterjee
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mickael Randour
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jean-François Raskin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computing Science, Newcastle University, Claremont Tower, Claremont Road, NE1 7RU, Newcastle upon Tyne, UK

    Maciej Koutny

  2. Department of Computer Science, University of Leicester, Computer Science Building, University Road, LE1 7RH, Leicester, UK

    Irek Ulidowski

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chatterjee, K., Randour, M., Raskin, JF. (2012). Strategy Synthesis for Multi-Dimensional Quantitative Objectives. In: Koutny, M., Ulidowski, I. (eds) CONCUR 2012 – Concurrency Theory. CONCUR 2012. Lecture Notes in Computer Science, vol 7454. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32940-1_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-32940-1_10

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-32939-5

  • Online ISBN: 978-3-642-32940-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation