nach oben

Acta Informatica

Erschienen in:

16.07.2016 | Original Article

Average-energy games

verfasst von: Patricia Bouyer, Nicolas Markey, Mickael Randour, Kim G. Larsen, Simon Laursen

Erschienen in: Acta Informatica | Ausgabe 2/2018

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Two-player quantitative zero-sum games provide a natural framework to synthesize controllers with performance guarantees for reactive systems within an uncontrollable environment. Classical settings include mean-payoff games, where the objective is to optimize the long-run average gain per action, and energy games, where the system has to avoid running out of energy. We study average-energy games, where the goal is to optimize the long-run average of the accumulated energy. We show that this objective arises naturally in several applications, and that it yields interesting connections with previous concepts in the literature. We prove that deciding the winner in such games is in \(\mathsf{NP}\cap \mathsf{coNP}\) and at least as hard as solving mean-payoff games, and we establish that memoryless strategies suffice to win. We also consider the case where the system has to minimize the average-energy while maintaining the accumulated energy within predefined bounds at all times: this corresponds to operating with a finite-capacity storage for energy. We give results for one-player and two-player games, and establish complexity bounds and memory requirements.

Vorheriger Artikel Preface for the special issue GandALF 2015

Nächster Artikel Parameterized linear temporal logics meet costs: still not costlier than LTL

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

We slightly abuse the notation as we see cycles as sequences of edges. The concatenation of cycles \(\mathcal {C}_{a} = s\,s'\ldots {} s\) and \(\mathcal {C}_{b} = s\,s'' \ldots {} s\) is to be understood as its natural interpretation \(\mathcal {C}_{a} \cdot \mathcal {C}_{b} = s\,s'\ldots {} s\,s'' \ldots {} s\): the origin state s only appears once in the middle and not twice as it would with \(\mathcal {C}_{a}\) and \(\mathcal {C}_{b}\) seen as true sequences of states.

Observe that given a state in \(G''\), it is indeed possible to build any neighboring state using only E and w from the original game: one can effectively build the graph \(G''\) on-the-fly.

In \({ EG}_{{ LU}}\) games with only \(\mathcal {P}_{2} \) (i.e., \(S_{1} = \emptyset \)), \(\mathcal {P}_{2} \) does not need memory to play as he can pick beforehand which of the energy bounds (lower or upper) he will transgress, and then do so with a memoryless strategy.

Aminof, B., Rubin, S.: First cycle games. In: Proceedings of SR, EPTCS 146, pp. 83–90 (2014)

Björklund, H., Sandberg, S., Vorobyov, S.: Memoryless determinacy of parity and mean payoff games: a simple proof. Theor. Comput. Sci. 310(1–3), 365–378 (2004)MathSciNetCrossRefMATH

Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Proceedings of CAV, LNCS 5643, pp 140–156. Springer, Berlin (2009)

Bohy, A., Bruyère, V., Filiot, E., Raskin, J.-F.: Synthesis from LTL specifications with mean-payoff objectives. In: Proceedings of of TACAS, LNCS 7795, pp. 169–184. Springer, Berlin (2013)

Boros, E., Elbassioni, K., Gurvich, V., Makino, K.: Markov decision processes and stochastic games with total effective payoff. In: Proceedings of STACS, LIPIcs 30, pp. 103–115. Schloss Dagstuhl—LZI (2015)

Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N., Srba, J.: Infinite runs in weighted timed automata with energy constraints. In: Proceedings of FORMATS, LNCS 5215, pp. 33–47. Springer, Berlin (2008)

Bouyer, P., Markey, N., Randour, M., Larsen, K.G., Laursen, S.: Average-energy games. In: Proceedings of GandALF, EPTCS 193, pp. 1–15 (2015)

Brázdil, T., Klaška, D., Kučera, A., Novotný, P.: Minimizing running costs in consumption systems. In: Proceedings of CAV, LNCS 8559, pp. 457–472. Springer, Berlin (2014)

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

10.

Cassez, F., Jensen, J.J., Larsen, K.G., Raskin, J.-F., Reynier, P.-A.: Automatic synthesis of robust and optimal controllers—an industrial case study. In: Proceedings of HSCC, LNCS 5469, pp. 90–104. Springer, Berlin (2009)

11.

Chakrabarti, A., de Alfaro, L., Henzinger, T.A., Stoelinga, M.: Resource interfaces. In: Proceedings of EMSOFT, LNCS 2855, pp. 117–133. Springer, Berlin (2003)

12.

Chatterjee, K., Doyen, L.: Energy parity games. In: Proceedings of ICALP, LNCS 6199, pp. 599–610. Springer, Berlin (2010)

13.

Chatterjee, K., Velner, Y.: Mean-payoff pushdown games. In: Proceedings of LICS, pp. 195–204. IEEE (2012)

14.

Chatterjee, K., Prabhu, V.S.: Quantitative timed simulation functions and refinement metrics for real-time systems. In: Proceedings of HSCC, pp. 273–282. ACM (2013)

15.

Chatterjee, K., Randour, M., Raskin, J.-F.: Strategy synthesis for multi-dimensional quantitative objectives. Acta Inf. 51(3–4), 129–163 (2014)MathSciNetCrossRefMATH

16.

Chatterjee, K., Doyen, L., Randour, M., Raskin, J.-F.: Looking at mean-payoff and total-payoff through windows. Inf. Comput. 242, 25–52 (2015)MathSciNetCrossRefMATH

17.

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

18.

Fearnley, J., Jurdziński, M.: Reachability in two-clock timed automata is PSPACE-complete. In: Proceedings of ICALP, LNCS 7966, pp. 212–223. Springer, Berlin (2013)

19.

Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Berlin (1997)MATH

20.

Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, New York (1979)MATH

21.

Gawlitza, T., Seidl, H.: Games through nested fixpoints. In: Proceedings of CAV, LNCS 5643, pp. 291–305. Springer, Berlin (2009)

22.

Gimbert, H., Zielonka, W.: When can you play positionnaly? In: Proceedings of MFCS, LNCS 3153, pp. 686–697. Springer, Berlin (2004)

23.

Gimbert, H., Zielonka, W.: Games where you can play optimally without any memory. In: Proceedings of CONCUR, LNCS 3653, pp. 428–442. Springer, Berlin (2005)

24.

Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research, LNCS 2500. Springer, Berlin (2002)

25.

Juhl, L., Larsen, K.G., Raskin, J.-F.: Optimal bounds for multiweighted and parametrised energy games. In: Theories of Programming and Formal Methods, LNCS 8051, pp. 244–255. Springer, Berlin (2013)

26.

Jurdziński, M.: Deciding the winner in parity games is in UP\(\cap \)co-UP. Inf. Process. Lett. 68(3), 119–124 (1998)MathSciNetCrossRefMATH

27.

Jurdziński, M., Sproston, J., Laroussinie, F.: Model checking probabilistic timed automata with one or two clocks. Logical Methods Comput. Sci. 4(3), 1–28 (2008)MathSciNetMATH

28.

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

29.

Kopczynski, E.: Half-positional determinacy of infinite games. In: Proceedings of ICALP, LNCS 4052, pp. 336–347. Springer, Berlin (2006)

30.

Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for AC-like equational theories with homomorphisms. Research Report LSV-04-16, Laboratoire Spécification et Vérification, ENS Cachan, France (2004)

31.

Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for AC-like equational theories with homomorphisms. In: Proceedings of RTA, LNCS 3467, pp. 308–322. Springer, Berlin (2005)

32.

Larsen, K.G., Laursen, S., Zimmermann, M.: Limit your consumption! Finding bounds in average-energy games. In: Proceedings of QAPL, EPTCS (2016)

33.

Randour, M.: Automated synthesis of reliable and efficient systems through game theory: a case study. In: Proceedings of the European Conference on Complex Systems 2012, Springer Proceedings in Complexity XVII, pp. 731–738. Springer, Berlin (2013)

34.

Randour, M.: Synthesis in Multi-Criteria Quantitative Games. Ph.D. Thesis, Université de Mons, Belgium (2014)

35.

Sipser, M.: Introduction to the Theory of Computation. PWS Publishing Company, Boston (1997)MATH

36.

Thuijsman, F., Vrieze, O.J.: The bad match; a total reward stochastic game. OR Spektrum 9(2), 93–99 (1987)

37.

Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A.M., Raskin, J.-F.: The complexity of multi-mean-payoff and multi-energy games. Inf. Comput. 241, 177–196 (2015)MathSciNetCrossRefMATH

38.

Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci. 158(1–2), 343–359 (1996)MathSciNetCrossRefMATH

Titel: Average-energy games
verfasst von: Patricia Bouyer
Nicolas Markey
Mickael Randour
Kim G. Larsen
Simon Laursen
Publikationsdatum: 16.07.2016
Verlag: Springer Berlin Heidelberg
Erschienen in: Acta Informatica / Ausgabe 2/2018
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI: https://doi.org/10.1007/s00236-016-0274-1

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"