Safe and Infinite Resource Scheduling Using Energy Timed Automata

We study the existence of infinite and safe schedules for resource-aware timed systems, in the setting of multiple continuous resources. Specifically, we explore the multi-variable extension of Energy Timed Automata, where variables are constrained by polyhedra in \(\mathbb {R}^n\) . We ask the question of whether there exist infinite runs satisfying such boundary constraints and show how schedules can be synthesized by characterising these runs as limit sets using quantifier elimination for linear real arithmetic. Additionally, we show that this existential problem is decidable under the assumption that limit sets are linear, we relate this to an earlier decidability result for single-variable Energy Timed Automata that are flat and segmented, and show constructively that there exist flat and segmented multi-variable Energy Timed Automata that give rise to non-linear limit sets.