Symbolic BDD and ADD Algorithms for Energy Games
Shahar Maoz (Tel Aviv University), Or Pistiner (Tel Aviv University),, Jan Oliver Ringert (Tel Aviv University)

TL;DR
This paper introduces a fully symbolic algorithm for energy games, utilizing BDD and ADD representations, and compares their performance in synthesizing controllers for resource-constrained reactive systems.
Contribution
It presents a novel symbolic algorithm that handles both quantitative values and game states, implemented with BDD and ADD, advancing energy game synthesis techniques.
Findings
BDD and ADD implementations show different performance characteristics.
The symbolic approach improves scalability for energy game synthesis.
Experimental results compare the efficiency of BDD and ADD methods.
Abstract
Energy games, which model quantitative consumption of a limited resource, e.g., time or energy, play a central role in quantitative models for reactive systems. Reactive synthesis constructs a controller which satisfies a given specification, if one exists. For energy games a synthesized controller ensures to satisfy not only the safety constraints of the specification but also the quantitative constraints expressed in the energy game. A symbolic algorithm for energy games, recently presented by Chatterjee et al., is symbolic in its representation of quantitative values but concrete in the representation of game states and transitions. In this paper we present an algorithm that is symbolic both in the quantitative values and in the underlying game representation. We have implemented our algorithm using two different symbolic representations for reactive games, Binary Decision Diagrams…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
