Jurdzinski/Kwiatkowska/Norman/Trivedi: Concavely-Priced Probabilistic Timed Automata.

Concavely-Priced Probabilistic Timed Automata.

Marcin Jurdzinski, Marta Kwiatkowska, Gethin Norma, and nAshutosh Trivedi

Concavely-priced probabilistic timed automata, an extension of probabilistic timed automata, are introduced. In this paper we consider expected reachability, discounted, and average price problems for concavely-priced probabilistic timed automata for arbitrary initial states. We prove that these problems are EXPTIME-complete for probabilistic timed automata with two or more clocks and PTIME-complete for automata with one clock. Previous work on expected price problems for probabilistic timed automata was restricted to expected reachability for linearly-priced automata and integer valued initial states. This work uses the boundary region graph introduced by Jurdziński and Trivedi to analyse properties of concavely-priced (non-probabilistic) timed automata.

Proceedings of the 20th International Conference on Concurrency Theory, CONCUR 2009, Lecture Notes in Computer Science Volume 5710, 2009, pp 415-430, Springer, 2009.