Efficient Algorithms for Omega-Regular Energy Games

ω-regular energy games are two-player ω-regular games augmented with a requirement to avoid the exhaustion of a finite resource, e.g., battery or disk space. ω-regular energy games can be reduced to ω-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 ω-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 ω-regular energy games by seamless reuse of existing symbolic fixed-point algorithms for ordinary ω-regular games. We base our work on the introduction of energy µ-calculus, a multi-valued extension of game µ-calculus. We have implemented our ideas and evaluated them. The empirical evaluation provides evidence for the efficiency of our work.