EgGS - The Energy Game Strategizer

Jacobsen, Rasmus Søgaard ; Carlsen, Mads Vestergaard

4. term

Computer Science, Master

2014

2014-06-10

98

Dette arbejde fortsætter vores studie af energispil, matematiske modeller hvor en controller spiller mod et miljø på en automat, der holder styr på flere ressourcer (fx energi) med tællere. Målet er automatisk at syntetisere en strategi, som holder systemet kørende uendeligt uden at overskride ressourcegrænser. Sådanne strategier er relevante for energikritiske systemer som satellitter og robotter. Med afsæt i vores tidligere prototype præsenterer vi EgGS, et softwareværktøj der syntetiserer strategier ud fra spilbeskrivelser skrevet i LEG (Language of Energy Games). Vi skærper de formelle definitioner af energispil og introducerer en diskret tidsvariant, hvor tiden skrider frem i trin. Vi forklarer, hvornår uendelig drift er mulig, og hvordan en korrekt strategi kan beregnes. Vi giver desuden en praktisk brugervejledning til at skrive spil i LEG og viser, hvordan diskrete tidsspil kan udtrykkes med den eksisterende syntaks. Den væsentligste tekniske nyhed er et skifte fra en eksplicit, tilstand-for-tilstand-tilgang til en symbolsk tilgang, der repræsenterer store mængder tilstande kompakt. Vi beskriver i detalje, hvordan overgange kodes som kvantificerede boolske udtryk, og hvordan algoritmer udnytter denne repræsentation til at syntetisere strategier. Afslutningsvis præsenterer vi eksperimentelle resultater, der sammenligner den symbolske og den eksplicitte metode, diskuterer ydeevne og kompleksitet, og opsummerer forbedringerne i forhold til den tidligere, mindre effektive tilgang.

This work continues our study of energy games—mathematical models where a controller plays against an environment on an automaton that tracks multiple resources (such as energy) with counters. The goal is to automatically synthesize a strategy that keeps the system running forever without exceeding resource limits. Such strategies are relevant for energy‑critical systems like satellites and robots. Building on our earlier prototype, we present EgGS, a software tool that synthesizes strategies from game descriptions written in LEG (Language of Energy Games). We refine the formal definitions of energy games and introduce a discretely timed variant, where time advances in steps. We explain when infinite operation is possible and how a correct strategy can be computed. We also provide a practical user guide to writing games in LEG and show how discretely timed games can be expressed using the existing syntax. The main technical contribution is a shift from an explicit, state‑by‑state approach to a symbolic approach that represents large sets of states compactly. We detail how transitions are encoded as quantified Boolean formulas and how algorithms use this representation to synthesize strategies. Finally, we present experimental results comparing the symbolic and explicit methods, discuss performance and complexity, and summarize the improvements over the previous, less efficient approach.

[This abstract was generated with the help of AI]

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

Download
View record in AAU Student Projects