EgGS - The Energy Game Strategizer

Jacobsen, Rasmus Søgaard ; Carlsen, Mads Vestergaard

4. term

Computer Science, Master

2014

2014-06-10

98 pages

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.

Energy games ; Strategy ; Synthesis ; LEG ; BDD ; Binary Decision Diagram ; Energy game ; EgGS ; Energy Game Strategizer

Download
View record in AAU Student Projects