Infinite Runs in Recharge Automata

Studenteropgave: Kandidatspeciale og HD afgangsprojekt

  • Daniel Ejsing-Duun
  • Lisa Fontani
4. semester, Datalogi, Kandidat (Kandidatuddannelse)
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.
SprogEngelsk
Udgivelsesdato7 jun. 2013
Antal sider75
ID: 77335802