Efficient Algorithms for Omega-Regular Energy Games

w-regular energy games are two-player omega-regular games augmented with a requirement to avoid the exhaustion of a finite resource, e.g., battery or disk space. omega-regular energy games can be reduced to omega-regular games by encoding the energy level into the state space. As this approach blows up the state space, it performs poorly. Moreover, it is highly affected by the chosen energy bound denoting the resource's capacity. In this work, we present an alternative approach for solving omega-regular energy games, with two main advantages. First, our approach is efficient: it avoids the encoding of the energy level within the state space, and its performance is independent of the engineer's choice of the energy bound. Second, our approach is defined at the logic level, not at the algorithmic level, and thus allows solving omega-regular energy games by seamless reuse of existing symbolic fixed-point algorithms for ordinary omega-regular games. We base our work on the introduction of energy mu-calculus, a multi-valued extension of game mu-calculus. We have implemented our ideas and evaluated them. The empirical evaluation provides evidence for the efficiency of our work.