Title :
Relating average and discounted costs for quantitative analysis of timed systems
Author :
Alur, Rajeev ; Trivedi, Ashutosh
Author_Institution :
Univ. of Pennsylvania, Philadelphia, PA, USA
Abstract :
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.
Keywords :
control engineering computing; control system synthesis; game theory; optimisation; probabilistic automata; real-time systems; controller synthesis; discounted costs; finite-state probabilistic systems; optimization; probabilistic extensions; quantitative analysis; reactive real-time systems; timed automata; timed games; timed systems; Automata; Clocks; Cost accounting; Games; Markov processes; Optimization; Probabilistic logic; Blackwell optimality; Quantitative Analysis; Tauberian Theorems; Timed Automata;
Conference_Titel :
Embedded Software (EMSOFT), 2011 Proceedings of the International Conference on
Conference_Location :
Taipei
Print_ISBN :
978-1-4503-0714-7