Parameter Synthesis for Probabilistic Timed Automata Using Stochastic Game Abstractions

  • Aleksandra Jovanović
  • Marta Kwiatkowska
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8762)


We propose a method to synthesise optimal values of timing parameters for probabilistic timed automata, 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. In the parametric setting, our method is able to determine all the possible maximum (or minimum) reachability probabilities that arise for different values of timing parameters, and yields optimal valuations represented as a set of symbolic constraints between parameters.


Markov Decision Process Stochastic Game Parameter Synthesis Symbolic State Reachability Graph 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183–235 (1994)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Alur, R., Henzinger, T.A., Vardi, M.Y.: Parametric real-time reasoning. In: STOC 1993, pp. 592–601. ACM Press (1993)Google Scholar
  3. 3.
    André, É., Fribourg, L., Sproston, J.: An extension of the inverse method to probabilistic timed automata. FMSD 42, 119–145 (2013)zbMATHGoogle Scholar
  4. 4.
    Chamseddine, N., Duflot, M., Fribourg, L., Picaronny, C., Sproston, J.: Computing expected absorption times for parametric determinate probabilistic timed automata. In: QEST 2008, pp. 254–263. IEEE CS Press (2008)Google Scholar
  5. 5.
    Condon, A.: The complexity of stochastic games. Information and Computation 96, 203–224 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Diciolla, M., Kim, C.H.P., Kwiatkowska, M., Mereacre, A.: Synthesising optimal timing delays for timed i/o automata. In: EMSOFT 2014, ACM (2014)Google Scholar
  7. 7.
    Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric markov models. In: SPIN, pp. 88–106 (2009)Google Scholar
  8. 8.
    Han, T., Katoen, J.-P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: RTSS, pp. 173–182. IEEE Computer Society (2008)Google Scholar
  9. 9.
    Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming 53-53, 183–220 (2002)Google Scholar
  10. 10.
    Jovanović, A., Kwiatkowska, M.: Parameter synthesis for probabilistic timed automata using stochastic game abstractions. Technical Report CS-RR-14-06, Oxford University (June 2014)Google Scholar
  11. 11.
    Jovanović, A., Lime, D., Roux, O.H.: Integer parameter synthesis for timed automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 401–415. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  12. 12.
    Jovanović, A., Lime, D., Roux, O.H.: Synthesis of bounded integer parameters for parametric timed reachability games. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 87–101. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  13. 13.
    Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. FMSD 36(3), 246–280 (2010)zbMATHGoogle Scholar
  14. 14.
    Kwiatkowska, M., Norman, G., Parker, D.: Game-based abstraction for Markov decision processes. In: QEST 2006, pp. 157–166. IEEE CS Press (2006)Google Scholar
  15. 15.
    Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 212–227. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. 16.
    Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  17. 17.
    Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. FMSD 29, 33–78 (2006)zbMATHGoogle Scholar
  18. 18.
    Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. TCS 282, 101–150 (2002)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Aleksandra Jovanović
    • 1
  • Marta Kwiatkowska
    • 1
  1. 1.Department of Computer ScienceUniversity of OxfordOxfordUK

Personalised recommendations