The complexity of multi-mean-payoff and multi-energy games

被引:48
作者
Velner, Yaron [1 ]
Chatterjee, Krishnendu [2 ,3 ]
Doyen, Laurent [4 ]
Henzinger, Thomas A. [2 ,3 ]
Rabinovich, Alexander [1 ]
Raskin, Jean-Francois [5 ]
机构
[1] Tel Aviv Univ, Blavatn Sch Comp Sci, IL-69978 Tel Aviv, Israel
[2] IST Austria, A-3400 Klosterneuburg, Austria
[3] ENS Cachan, LSV, Cachan, France
[4] CNRS, F-75700 Paris, France
[5] Univ Libre Bruxelles, Dept Informat, Brussels, Belgium
基金
欧洲研究理事会; 奥地利科学基金会;
关键词
VECTOR ADDITION SYSTEMS;
D O I
10.1016/j.ic.2015.03.001
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
In mean-payoff games, the objective of the protagonist is to ensure that the limit average of an infinite sequence of numeric weights is nonnegative. In energy games, the objective is to ensure that the running sum of weights is always nonnegative. Multi-mean-payoff and multi-energy games replace individual weights by tuples, and the limit average (resp., running sum) of each coordinate must be (resp., remain) nonnegative. We prove finite-memory determinacy of multi-energy games and show inter-reducibility of multi-mean-payoff and multi-energy games for finite-memory strategies. We improve the computational complexity for solving both classes with finite-memory strategies: we prove coNP-completeness improving the previous known EXPSPACE bound. For memoryless strategies, we show that deciding the existence of a winning strategy for the protagonist is NP-complete. We present the first solution of multi-mean-payoff games with infinite-memory strategies: we show that mean-payoff-sup objectives can be decided in NP boolean AND coNP, whereas mean-payoff-inf objectives are coNP-complete. (C) 2015 Elsevier Inc. All rights reserved.
引用
收藏
页码:177 / 196
页数:20
相关论文
共 32 条
  • [1] ABADI M, 1989, LECT NOTES COMPUT SC, V372, P1
  • [2] Alur R, 2009, LECT NOTES COMPUT SC, V5504, P333
  • [3] Bouyer P, 2008, LECT NOTES COMPUT SC, V5215, P33, DOI 10.1007/978-3-540-85778-5_4
  • [4] Brazdil Tomas, 2012, Computer Aided Verification. Proceedings 24th International Conference, CAV 2012, P23, DOI 10.1007/978-3-642-31424-7_8
  • [5] Brazdil T, 2010, LECT NOTES COMPUT SC, V6199, P478, DOI 10.1007/978-3-642-14162-1_40
  • [6] Faster algorithms for mean-payoff games
    Brim, L.
    Chaloupka, J.
    Doyen, L.
    Gentilini, R.
    Raskin, J. F.
    [J]. FORMAL METHODS IN SYSTEM DESIGN, 2011, 38 (02) : 97 - 118
  • [7] Cerny P, 2012, EMSOFT '12: PROCEEDINGS OF THE TENTH AMC INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE 2012, P53
  • [8] Chakrabarti A, 2003, LECT NOTES COMPUT SC, V2855, P117
  • [9] Chaloupka J, 2010, LECT NOTES COMPUT SC, V6227, P104, DOI 10.1007/978-3-642-15349-5_7
  • [10] Chatterjee Krishnendu, 2013, Automated Technology for Verification and Analysis. 11th International Symposium, ATVA 2013. Proceedings: LNCS 8172, P118, DOI 10.1007/978-3-319-02444-8_10