Oxford logo
[JK14] A. Jovanovic, and M. Kwiatkowska,. Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Games. In Proc. 8th International Workshop on Reachability Problems (RP'14), volume 8762 of LNCS, pages 176-189, Springer. 2014. [pdf] [bib]
Downloads:  pdf pdf (404 KB)  bib bib
Notes: The original publication is available at link.springer.com.
Abstract. We propose a method to synthesise optimal values of timing parameters for probabilistic timed automata (PTA), in the sense that the probability of reaching some set of states is either maximised or minimised. Our first algorithm, based on forward exploration of the symbolic states, can only guarantee parameter values that correspond to upper (resp. lower) bounds on maximum (resp. minimum) reachability probability. To ensure precise reachability probabilities, we adapt the game-based abstraction refinement method.