Alur/Trivedi:Relating average and discounted costs for quantitative analysis of timed systems .

Relating average and discounted costs for quantitative analysis of timed systems

Rajeev Alur and Ashutosh Trivedi

Quantitative analysis and controller synthesis problems for reactive real-time systems can be formalized as optimization problems on timed automata, timed games, and their probabilistic extensions. The limiting average cost and the discounted cost are two standard criteria for such optimization problems. In theory of finite-state probabilistic systems, a number of interesting results are available relating the optimal values according to these two different performance objectives. These results, however, do not directly apply to timed systems due to the infinite state-space of clock valuations. In this paper, we present some conditions under which the existence of the limit of optimal discounted cost objective implies the the existence of limiting average cost to the same value. Using these results we answer an open question posed by Fahrenberg and Larsen, and give simpler proofs of some known decidability results on (probabilistic) timed automata. We also show the determinacy and decidability of average-time games on timed automata, and expected average-time games on probabilistic timed automata.

Proceedings of the ninth ACM international conference on Embedded software, EMSOFT 11, Pages 165-174, ACM, 2011.