Hyperplane separation technique for multidimensional mean-payoff games

被引:3
作者
Chatterjee, Krishnendu [1 ]
Velner, Yaron [2 ]
机构
[1] IST Austria, Klosterneuburg, Austria
[2] Tel Aviv Univ, Tel Aviv, Israel
基金
奥地利科学基金会;
关键词
Finite-state graph games; Mean-payoff objectives; Multidimensional objectives; Pushdown graphs and games; Computer-aided verification; COMPLEXITY; REACHABILITY;
D O I
10.1016/j.jcss.2017.04.005
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
We consider finite-state and recursive game graphs with multidimensional mean-payoff objectives. In recursive games two types of strategies are relevant: global strategies and modular strategies. Our contributions are: (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 weights are fixed; whereas for arbitrary dimensions the problem is coNP-complete. (2) We show that one-player recursive games with multidimensional mean-payoff objectives can be solved in polynomial time. Both above algorithms are based on hyperplane separation technique. (3) For recursive games we show that under modular strategies the multidimensional problem is undecidable. We show that if the number of modules, exits, and the maximal absolute value of the weights are fixed, then one-dimensional recursive mean-payoff games under modular strategies can be solved in polynomial time, whereas for unbounded number of exits or modules the problem is NP-hard. (C) 2017 Elsevier Inc. All rights reserved.
引用
收藏
页码:236 / 259
页数:24
相关论文
共 43 条
[1]   Modular strategies for recursive game graphs [J].
Alur, R ;
La Torre, S ;
Madhusudan, P .
THEORETICAL COMPUTER SCIENCE, 2006, 354 (02) :230-249
[2]  
Alur R, 2009, LECT NOTES COMPUT SC, V5504, P333
[3]  
[Anonymous], 1989, C RECORD 16 ANN ACM, DOI [DOI 10.1145/75277.75293, 10.1145/75277.75293]
[4]  
Beeri C., 1980, ACM Transactions on Database Systems, V5, P241, DOI 10.1145/320613.320614
[5]  
Bohy A., 2013, TACAS
[6]   Temporal Specifications with Accumulative Values [J].
Boker, Udi ;
Chatterjee, Krishnendu ;
Henzinger, Thomas A. ;
Kupferman, Orna .
ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2014, 15 (04)
[7]  
Brazdil Tomas, 2012, Computer Aided Verification. Proceedings 24th International Conference, CAV 2012, P23, DOI 10.1007/978-3-642-31424-7_8
[8]   Reachability in recursive Markov decision processes [J].
Brazdil, Tomas ;
Brozek, Vaclav ;
Forejt, Vojtech ;
Kucera, Antonin .
INFORMATION AND COMPUTATION, 2008, 206 (05) :520-537
[9]   Qualitative reachability in stochastic BPA games [J].
Brazdil, Tomas ;
Brozek, Vaclav ;
Kucera, Antonin ;
Obdrzalek, Jan .
INFORMATION AND COMPUTATION, 2011, 209 (08) :1160-1183
[10]   Faster algorithms for mean-payoff games [J].
Brim, L. ;
Chaloupka, J. ;
Doyen, L. ;
Gentilini, R. ;
Raskin, J. F. .
FORMAL METHODS IN SYSTEM DESIGN, 2011, 38 (02) :97-118