Faster Algorithms for Mean-Payoff Parity Games

Authors Krishnendu Chatterjee, Monika Henzinger, Alexander Svozil



PDF
Thumbnail PDF

File

LIPIcs.MFCS.2017.39.pdf
  • Filesize: 0.58 MB
  • 14 pages

Document Identifiers

Author Details

Krishnendu Chatterjee
Monika Henzinger
Alexander Svozil

Cite As Get BibTex

Krishnendu Chatterjee, Monika Henzinger, and Alexander Svozil. Faster Algorithms for Mean-Payoff Parity Games. In 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 83, pp. 39:1-39:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017) https://doi.org/10.4230/LIPIcs.MFCS.2017.39

Abstract

Graph games provide the foundation for modeling and synthesis of reactive processes. Such games are played over graphs where the vertices are controlled by two adversarial players. We consider graph games where the objective of the first player is the  
conjunction of a qualitative objective (specified as a parity condition) and a quantitative objective (specified as a mean-payoff condition). There are two variants of the problem, namely, the threshold problem where the quantitative goal is to ensure that the mean-payoff value is above a threshold, and the value problem where the quantitative goal is to ensure the optimal mean-payoff value; in both cases ensuring the qualitative parity objective. The previous best-known algorithms for game graphs with n vertices, m edges,
parity objectives with d priorities, and maximal absolute reward value W for mean-payoff objectives, are as follows: O(n^(d+1)·m·W) for the threshold problem, and O(n^(d+2)·m·W) for the value problem. 
Our main contributions are faster algorithms, and the running times of our algorithms are as follows: O(n^(d-1)·m·W) for the threshold problem, and O(n^d·m·W·log(n·W)) for the value problem. For mean-payoff parity objectives with two priorities, our algorithms match the best-known bounds of the algorithms for mean-payoff games (without conjunction with parity objectives). Our results are relevant in synthesis of reactive systems with both functional 
requirement (given as a qualitative objective) and performance requirement (given as a quantitative objective).

Subject Classification

Keywords
  • graph games
  • mean-payoff parity games

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. R. Bloem, K. Chatterjee, T. A. Henzinger, and B. Jobstmann. Better quality in synthesis through quantitative objectives. In Proc. of CAV, LNCS 5643, pages 140-156. Springer, 2009. Google Scholar
  2. Roderick Bloem, Krishnendu Chatterjee, Karin Greimel, Thomas A. Henzinger, Georg Hofferek, Barbara Jobstmann, Bettina Könighofer, and Robert Könighofer. Synthesizing robust systems. Acta Inf., 51(3-4):193-220, 2014. Google Scholar
  3. P. Bouyer, U. Fahrenberg, K. G. Larsen, N. Markey, and J. Srba. Infinite runs in weighted timed automata with energy constraints. In Proc. of FORMATS, LNCS 5215, pages 33-47. Springer, 2008. Google Scholar
  4. P. Bouyer, N. Markey, J. Olschewski, and M. Ummels. Measuring permissiveness in parity games: Mean-payoff parity games revisited. In Proc. of ATVA, LNCS 6996, pages 135-149. Springer, 2011. Google Scholar
  5. L. Brim, J. Chaloupka, L. Doyen, R. Gentilini, and J. F. Raskin. Faster algorithms for mean-payoff games. Form. Methods Syst. Des., 38(2):97-118, April 2011. URL: http://dx.doi.org/10.1007/s10703-010-0105-x.
  6. J. R. Büchi and L. H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the AMS, 138:295-311, 1969. Google Scholar
  7. P. Cerný, K. Chatterjee, T. A. Henzinger, A. Radhakrishna, and R. Singh. Quantitative synthesis for concurrent programs. In Proc. of CAV, LNCS 6806, pages 243-259. Springer, 2011. Google Scholar
  8. A. Chakrabarti, L. de Alfaro, T. A. Henzinger, and M. Stoelinga. Resource interfaces. In Proc. of EMSOFT, LNCS 2855, pages 117-133. Springer, 2003. Google Scholar
  9. K. Chatterjee and L. Doyen. Energy parity games. In Proc. of ICALP: Automata, Languages and Programming (B), LNCS 6199, pages 599-610. Springer, 2010. Google Scholar
  10. K. Chatterjee and L. Doyen. Energy and mean-payoff parity Markov decision processes. In Proc. of MFCS, LNCS 6907, pages 206-218. Springer, 2011. Google Scholar
  11. K. Chatterjee, T. A. Henzinger, and M. Jurdziński. Mean-payoff parity games. In Proc. of LICS, pages 178-187. IEEE Computer Society, 2005. Google Scholar
  12. Krishnendu Chatterjee and Laurent Doyen. Games and markov decision processes with mean-payoff parity and energy parity objectives. In MEMICS, pages 37-46, 2011. Google Scholar
  13. Krishnendu Chatterjee, Laurent Doyen, Hugo Gimbert, and Youssouf Oualhadj. Perfect-information stochastic mean-payoff parity games. In FOSSACS, pages 210-225, 2014. Google Scholar
  14. Carlo Comin and Romeo Rizzi. Improved pseudo-polynomial bound for the value problem and optimal strategy synthesis in mean payoff games. Algorithmica, 77(4):995-1021, 2017. URL: http://dx.doi.org/10.1007/s00453-016-0123-1.
  15. A. Ehrenfeucht and J. Mycielski. Positional strategies for mean payoff games. International Journal of Game Theory, 8(2):109-113, 1979. URL: http://dx.doi.org/10.1007/BF01768705.
  16. Y. M. Lifshits and D. S. Pavlov. Potential theory for mean payoff games. Journal of Mathematical Sciences, 145(3):4967-4974, 2007. URL: http://dx.doi.org/10.1007/s10958-007-0331-y.
  17. A. Pnueli and R. Rosner. On the synthesis of a reactive module. In Proc. of POPL, pages 179-190. ACM Press, 1989. Google Scholar
  18. P. J. Ramadge and W. M. Wonham. Supervisory control of a class of discrete-event processes. SIAM Journal of Control and Optimization, 25(1):206-230, 1987. Google Scholar
  19. W. Thomas. Languages, automata, and logic. In Handbook of Formal Languages, volume 3, Beyond Words, chapter 7, pages 389-455. Springer, 1997. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail