On the Energy LTL Game Problem
摘要
In this short chapter, we introduce the energy LTL game problem by extending the LTL game problem defined in Chap. 3 with resources. This is also a variant of the energy parity game problem investigated in Chap. 4 in which the objectives are expressed by LTL formulae instead of parity conditions. The problem is shown 2EXPTIME-complete: the 2EXPTIME-hardness because the LTL game problem is already 2EXPTIME-complete and the 2EXPTIME-membership is by reduction to the energy parity game problem. The second part of the chapter is dedicated to show that the core model-checking problem for ATL* with resources can be reduced to the energy LTL game problem, and conversely the energy LTL game problem can be reduced to the core model-checking problem for ATL* with resources. The reductions hold for LTL fragments (both at the logical side and at the game side) and this allows us to get membership and hardness results. For instance, the energy LTL game problem restricted to one resource and with depth-one temporal objectives can be solved in polynomial-space.