Infinite Runs in Recharge Automata
Translated title
Authors
Term
4. term
Education
Publication year
2013
Submitted on
2013-06-07
Pages
75
Abstract
We consider recharge automata, a variant of weighted/priced timed automata with a single, bounded cost variable that can be decreased when delaying in locations and fully recharged when taking discrete transitions. Given such an automaton with just one clock, we investigate whether there exists an infinite time-divergent run where the resource always stays above zero. Our method includes a notion of energy functions for abstracting runs by only considering the initial and final energy. By means of these, we provide a polynomial time algorithm for solving the problem for ’flat’ recharge automata and prove that the general problem for any automaton is in NP.
Keywords
Documents