Infinite Runs in Weighted Timed Automata with Energy Constraints

International audienceWe~study the problems of existence and construction of infinite schedules for finite weighted automata and one-clock weighted timed automata, subject to boundary constraints on the accumulated weight. More specifically, we~consider automata equipped with positive and negative weights on transitions and locations, corresponding to the production and consumption of some resource (\emphe.g.~energy). We~ask the question whether there exists an infinite path for which the accumulated weight for any finite prefix satisfies certain constraints (\emphe.g.~remains between~\(0\) and some given upper-bound). We~also consider a game version of the above, where certain transitions may be uncontrollable