Oxford logo
[JKN15] A. Jovanovic, M. Kwiatkowska and G. Norman. Symbolic Minimum Expected Time Controller Synthesis for Probabilistic Timed Automata. In Sankaranarayanan, Sriram and Vicario, Enrico (editors), Proceedings of the 13th International Conference on Formal Modeling and Analysis of Timed Systems, volume 9268 of LNCS, pages 140-155, Springer. 2015. [pdf] [bib]
Downloads:  pdf pdf (404 KB)  bib bib
Notes: An extended version of this paper, including proofs, can be found at http://www.cs.ox.ac.uk/publications/publication9621-abstract.html. The original publication is available at link.springer.com.
Abstract. In this paper we consider the problem of computing the minimum expected time to reach a target and the synthesis of the corresponding optimal controller for a probabilistic timed automaton (PTA). Although this problem admits solutions that employ the digital clocks abstraction or statistical model checking, symbolic methods based on zones and priced zones fail due to the difficulty of incorporating probabilistic branching in the context of dense time. We work in a generalisation of the setting introduced by Asarin and Maler for the corresponding problem for timed automata, where simple and nice functions are introduced to ensure finiteness of the dense-time representation. We find restrictions sufficient for value iteration to converge to the minimum expected time on the uncountable Markov decision process representing the semantics of a PTA. We formulate a Bellman operator on the backwards zone graph of a PTA and prove that value iteration using this operator equals that computed over the PTA's semantics. This enables us to extract an epsilon-optimal controller from value iteration in the standard way.