Skip to main content
SpringerLink
Log in
Book cover

International Conference on Concurrency Theory

CONCUR 2013: CONCUR 2013 – Concurrency Theory pp 500–515Cite as

Hyperplane Separation Technique for Multidimensional Mean-Payoff Games

  • Conference paper

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

Abstract

Two-player games on graphs are central in many problems in formal verification and program analysis such as synthesis and verification of open systems. In this work, we consider both finite-state game graphs, and recursive game graphs (or pushdown game graphs) that model the control flow of sequential programs with recursion. The objectives we study are multidimensional mean-payoff objectives, where the goal of player 1 is to ensure that the mean-payoff is non-negative in all dimensions. In pushdown games two types of strategies are relevant: (1) global strategies, that depend on the entire global history; and (2) modular strategies, that have only local memory and thus do not depend on the context of invocation. Our main contributions are as follows: (1) We show that finite-state multidimensional mean-payoff games can be solved in polynomial time if the number of dimensions and the maximal absolute value of the weights are fixed; whereas if the number of dimensions is arbitrary, then the problem is known to be coNP-complete. (2) We show that pushdown graphs with multidimensional mean-payoff objectives can be solved in polynomial time. For both (1) and (2) our algorithms are based on hyperplane separation technique. (3) For pushdown games under global strategies both one and multidimensional mean-payoff objectives problems are known to be undecidable, and we show that under modular strategies the multidimensional problem is also undecidable; under modular strategies the one-dimensional problem is NP-complete. We show that if the number of modules, the number of exits, and the maximal absolute value of the weights are fixed, then pushdown games under modular strategies with one-dimensional mean-payoff objectives can be solved in polynomial time, and if either the number of exits or the number of modules is unbounded, then the problem is NP-hard. (4) Finally we show that a fixed parameter tractable algorithm for finite-state multidimensional mean-payoff games or pushdown games under modular strategies with one-dimensional mean-payoff objectives would imply the fixed parameter tractability of parity games.

The research was supported by Austrian Science Fund (FWF) Grant No P 23499-N23, FWF NFN Grant No S11407-N23 (RiSE), ERC Start grant (279307: Graph Games), Microsoft faculty fellows award, the RICH Model Toolkit (ICT COST Action IC0901), and was carried out in partial fulfillment of the requirements for the Ph.D. degree of the second author.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., La Torre, S., Madhusudan, P.: Modular strategies for recursive game graphs. Theor. Comput. Sci. 354(2), 230–249 (2006)

    Article  MATH  Google Scholar 

  2. Beeri, C.: On the membership problem for functional and multivalued dependencies in relational databases. ACM Trans. on Database Systems 5, 241–259 (1980)

    Article  MATH  Google Scholar 

  3. 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 

  4. Bohy, A., Bruyère, V., Filiot, E., Raskin, J.-F.: Synthesis from ltl specifications with mean-payoff objectives. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 169–184. Springer, Heidelberg (2013)

    Google Scholar 

  5. Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. In: LICS, pp. 43–52 (2011)

    Google Scholar 

  6. Brázdil, T., Chatterjee, K., Kučera, A., Novotný, P.: Efficient controller synthesis for consumption games with multiple resource types. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 23–38. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Brim, L., Chaloupka, J., Doyen, L., Gentilini, R., Raskin, J.-F.: Faster algorithms for mean-payoff games. Formal Methods in System Design 38(2), 97–118 (2011)

    Article  MATH  Google Scholar 

  8. Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Transactions of the AMS 138, 295–311 (1969)

    MATH  Google Scholar 

  9. Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. ACM ToCL (2010)

    Google Scholar 

  10. Chatterjee, K., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Generalized mean-payoff and energy games. In: FSTTCS, pp. 505–516 (2010)

    Google Scholar 

  11. Chatterjee, K., Velner, Y.: Finite-state and pushdown games with multi-dimensional mean-payoff objectives. CoRR, abs/1210.3141 (2012)

    Google Scholar 

  12. Chatterjee, K., Velner, Y.: Mean-payoff pushdown games. In: LICS (2012)

    Google Scholar 

  13. Droste, M., Meinecke, I.: Describing average- and longtime-behavior by weighted MSO logics. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 537–548. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  14. Ehrenfeucht, A., Mycielski, J.: Positional strategies for mean payoff games. IJGT 8, 109–113 (1979)

    MathSciNet  MATH  Google Scholar 

  15. Gordan, P.: Ueber die auflosung linearer gleichungen mit reellen coeffizienten. Mathematische Annalen 6, 23–28 (1873)

    Article  MathSciNet  MATH  Google Scholar 

  16. Grötschel, M., Lovász, L., Schrijver, A.: The ellipsoid method and its consequences in combinatorial optimization. Combinatorica 1(2), 169–197 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  17. Gurvich, V.A., Karzanov, A.V., Khachiyan, L.G.: Cyclic games and an algorithm to find minimax cycle means in directed graphs. USSR Comp. Math. Phys. 28(5), 85–91 (1990)

    Article  MathSciNet  Google Scholar 

  18. Immerman, N.: Number of quantifiers is better than number of tape cells. Journal of Computer and System Sciences 22, 384–406 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  19. Jurdzinski, M.: Deciding the winner in parity games is in UP ∩ co-UP. IPL 68 (1998)

    Google Scholar 

  20. Karp, R.M.: A characterization of the minimum cycle mean in a digraph. Discrete Mathematics 23, 309–311 (1978)

    MathSciNet  MATH  Google Scholar 

  21. Kosaraju, S.R., Sullivan, G.F.: Detecting cycles in dynamic graphs in polynomial time. In: STOC, pp. 398–406 (1988)

    Google Scholar 

  22. Papadimitriou, C.H.: On the complexity of integer programming. JACM 28, 765–768 (1981)

    Article  MathSciNet  MATH  Google Scholar 

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

    Google Scholar 

  24. 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 

  25. 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 

  26. Walukiewicz, I.: Pushdown processes: Games and model-checking. Inf. Comput. 164(2), 234–263 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  27. 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. Tel Aviv University, Israel

    Yaron Velner

Authors
  1. Krishnendu Chatterjee
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yaron Velner
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Facultad de Matemáticas, Astronomía y Física, Universidad Nacional de Córdoba – CONICET, Medina Allende s/n,, X5000HUA, Córdoba, Argentina

    Pedro R. D’Argenio

  2. Departamento de Computación,, Universidad de Buenos Aires - Conicet, Intendente Güirales 2160, C1428EGA, Ciudad Autónoma de Buenos Aires, Argentina

    Hernán Melgratti

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chatterjee, K., Velner, Y. (2013). Hyperplane Separation Technique for Multidimensional Mean-Payoff Games. In: D’Argenio, P.R., Melgratti, H. (eds) CONCUR 2013 – Concurrency Theory. CONCUR 2013. Lecture Notes in Computer Science, vol 8052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40184-8_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40184-8_35

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40183-1

  • Online ISBN: 978-3-642-40184-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation