In this report we continue the work done in our previous semester report, on the subject of
Energy Games. Energy games are games played in multiweighted automata with the goal of
synthesizing a strategy for a controller, to keep the game running indefinitely. In doing so we
present the implementation of a software tool designed to synthesize these strategies, named
EgGS. Energy strategies can be used to control energy critical systems, such as satellites,
robotics, etc.
In our previous report, a prototype implementation of this tool was shown which was able
to synthesize strategies for games with a moderate amount of weighted configurations. Additionally, a language for expressing games was presented, named LEG (Language of Energy
Games). The formal syntax and semantics of LEG were also given given.
In this report we give refined theoretical definitions of energy games, as well as a discretely
timed variant of energy games. We elaborate on how a strategy can allow a system to run
infinitely, if such a strategy is possible, and we give a logical explanation of how this strategy
can be synthesized.
We also present a user’s guide to using LEG to express energy games in EgGS. While doing so,
we also present how a discretely timed game can be simulated, using only the existing syntax
of LEG.
As a follow-up to the results from our previous report, we present new methods which allow
EgGS to handle much larger games, and synthesize strategies for these within much less
time, than the former explicit approach. We will go into detail of how we obtain a symbolic
representation of energy games, and how this symbolic representation is used algorithmically
to synthesize strategies. While doing so, we show in detail how transitions are encoded using
quantified boolean expressions.
Following this, we present experimental data comparing the symbolic approach to the explicit
approach, and comment on the performance of both approaches. This is followed by a discussion of the results, and the established complexities of the symbolic representation. Finally,
we conclude the report, by summing up the established results, and explain the impact of the
achieved results, in comparison to the previous inefficient approach.