Infinite Runs in Recharge Automata
Authors
Ejsing-Duun, Daniel ; Fontani, Lisa
Term
4. term
Education
Publication year
2013
Submitted on
2013-06-07
Pages
75
Abstract
Denne afhandling undersøger recharge automata, en variant af vægtede/prissatte tidsautomater med én begrænset ressourcevariabel. Ressourcens niveau falder, mens systemet venter i en tilstand, og bliver fuldt opladt, når systemet tager en diskret overgang. For automater med ét ur spørger vi, om der findes et uendeligt forløb, hvor tiden bliver ved med at gå (tidsdivergerer), og ressourcen aldrig kommer under nul. Vi introducerer energifunktioner, der opsummerer et forløb ved kun at se på start- og slutniveau for ressourcen. Denne abstraktion gør det muligt at analysere mange forløb på én gang. Med den giver vi en polynomiel-tids algoritme til problemet for "flade" recharge automata og beviser, at det generelle problem for vilkårlige automater ligger i NP (en standard kompleksitetsklasse).
This thesis studies recharge automata, a variant of weighted/priced timed automata with a single bounded resource variable. The resource decreases while the system waits in a state and is fully recharged when the system takes a discrete transition. For automata with one clock, we ask whether there exists an infinite run in which time keeps increasing (time-divergent) and the resource never drops below zero. We introduce energy functions that summarize a run by its starting and ending resource levels, allowing us to reason about many runs at once. Using this abstraction, we present a polynomial-time algorithm for the problem on "flat" recharge automata and prove that, in general, the problem for arbitrary automata lies in NP (a standard computational complexity class).
[This abstract was generated with the help of AI]
Keywords
Documents