On the interval-bound problem for weighted timed automata

Abstract

A weighted timed automaton is a timed automaton equipped with weights on transitions and weight rates on locations. These weights may be positive or negative, corresponding to the production and consumption of some resources. We consider the interval-bound problem: does there exist an infinite run such that the accumulated weight for each prefix of the run is within some given bounds? We show that this problem is undecidable if the weighted timed automaton has more than one clock and more than one weight variable. We further prove that the problem is PSPACE-complete if we restrict the time domain to the natural numbers. © 2011 Springer-Verlag.