1 CISS - Center for Embedded Software Systems, The Faculty of Engineering and Science, Aalborg University, VBN2 Distributed Systems and Semantics, The Faculty of Engineering and Science, Aalborg University, VBN3 Department of Computer Science, The Faculty of Engineering and Science, Aalborg University, VBN4 Aalborg U Robotics, The Faculty of Humanities, Aalborg University, VBN
We introduce a new discounting semantics for priced timed automata. Discounting provides a way to model optimal-cost problems for infinite traces and has applications in optimal scheduling and other areas. In the discounting semantics, prices decrease exponentially, so that the contribution of a certain part of the behaviour to the overall cost depends on how far into the future this part takes place. We consider the optimal infinite run problem under this semantics: Given a priced timed automaton, find an infinite path with minimal discounted price. We show that this problem is computable, by a reduction to a similar problem on finite weighted graphs. The proof relies on a new theorem on minimization of monotonous functions defined on infinite-dimensional zones, which is of interest in itself.
Electronic Notes in Theoretical Computer Science, 2009, Vol 239, p. 179-191
Main Research Area:
The 8th, 9th, and 10th International Workshops on Verification of Infinite-State Systems (INFINITY 2006, 2007, 2008)-- INFINITY 08