Infinite Runs in Recharge Automata

In this article we introduce recharge automata, a variant of priced timed au-tomata with only one resource variable. In this formalism, the resource level can be decreased at a given rate while delaying in locations and instantaneously increased to its maximum when taking discrete transitions. We focus on recharge automata with only one clock and want to find out whether for a given automaton there exists an infinite time-diverging run such that the resource never goes below 0. For this purpose we present a normal form that divides the automaton into segments, in which it is possible to freely move between locations. We then abstract such automaton segments by making use of an adaptation of energy functions. These take as input the current energy when entering the automaton segment and compute the highest possible energy we can end up with when leaving the segment. The adaptation of energy functions to this formalism results in functions that are non-decreasing and may have some points of discontinuity. We propose a rep-resentation for energy functions, describe maximum and composition operations and show how these operations can be computed in polynomial time. We then use energy functions in the construction of an abstraction of recharge automata, called energy function automata, where each transition abstracts a segment of the recharge automaton. Energy change is represented on the transi-tions through the before-mentioned functions and time information is given by a boolean value. By graph analysis we can find all reachable cycles of a certain size in the resulting automaton and find out whether one of them can be repeated infinitely while not using more than the available energy. This results in an NP-algorithm. We further show that the problem can be solved in polynomial time if we restrict to so-called flat recharge automata, where each location is only part of one cycle