Concavely-Priced Timed Automata.


Marcin Jurdzinski and Ashutosh Trivedi

Concavely-priced timed automata, a generalization of linearly-priced timed automata, are introduced. Computing the minimum value of a number of cost functions—including reachability price, discounted price, average time, average price, price-per-time average, and price-per-reward average—is considered in a uniform fashion for concavely-priced timed automata. All the corresponding decision problems are shown to be PSPACE-complete. This paper generalises the recent work of Bouyer et al. on deciding the minimum reachability price and the minimum ratio-price for linearly-priced timed automata.

A new type of a region graph—the boundary region graph&mdahs;is defined, which generalizes the corner-point abstraction of Bouyer et al. A broad class of cost functions—concave-regular cost functions—is introduced, and the boundary region graph is shown to be a correct abstraction for deciding the minimum value of concave-regular cost functions for concavely-priced timed automata.

Proceedings of the 6th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS 2008), Lecture Notes in Computer Science Volume 5215, 2008, pp 48-62, Springer, 2008.
PDF © 2008 Springer.