Advertisement

Verification and Control of Turn-Based Probabilistic Real-Time Games

  • Marta Kwiatkowska
  • Gethin NormanEmail author
  • David Parker
Chapter
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11760)

Abstract

Quantitative verification techniques have been developed for the formal analysis of a variety of probabilistic models, such as Markov chains, Markov decision process and their variants. They can be used to produce guarantees on quantitative aspects of system behaviour, for example safety, reliability and performance, or to help synthesise controllers that ensure such guarantees are met. We propose the model of turn-based probabilistic timed multi-player games, which incorporates probabilistic choice, real-time clocks and nondeterministic behaviour across multiple players. Building on the digital clocks approach for the simpler model of probabilistic timed automata, we show how to compute the key measures that underlie quantitative verification, namely the probability and expected cumulative price to reach a target. We illustrate this on case studies from computer security and task scheduling.

Notes

Acknowledgements

This work is partially supported by the EPSRC Programme Grant on Mobile Autonomy and the PRINCESS project, under the DARPA BRASS programme (contract FA8750-16-C-0045).

References

  1. 1.
    de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 144–158. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-45187-7_9CrossRefGoogle Scholar
  2. 2.
    Aljazzar, H., Fischer, M., Grunske, L., Kuntz, M., Leitner, F., Leue, S.: Safety analysis of an airbag system using probabilistic FMEA and probabilistic counter examples. In: Proceedings of QEST 2009. IEEE (2009)Google Scholar
  3. 3.
    Alur, R., Bernadsky, M., Madhusudan, P.: Optimal reachability for weighted timed games. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 122–133. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-27836-8_13CrossRefGoogle Scholar
  4. 4.
    Alvim, M., Chatzikokolakis, K., Kawamoto, Y., Palamidessi, C.: A game-theoretic approach to information-flow control via protocol composition. Entropy 20(5), 382 (2018)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Alvim, M., Chatzikokolakis, K., Palamidessi, C., Smith, G.: Measuring information leakage using generalized gain functions. In: Proceedings of CSF 2012. IEEE (2012)Google Scholar
  6. 6.
    Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: Proceedings of SSC 1998. Elsevier (1998)Google Scholar
  7. 7.
    Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. CACM 53(9), 76–85 (2010)CrossRefGoogle Scholar
  8. 8.
    Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: UPPAAL-Tiga: time for playing games!. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 121–125. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73368-3_14CrossRefGoogle Scholar
  9. 9.
    Behrmann, G., et al.: Minimum-cost reachability for priced time automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001).  https://doi.org/10.1007/3-540-45351-2_15CrossRefGoogle Scholar
  10. 10.
    Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. IPL 98, 188–194 (2006)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Bouyer, P., Cassez, F., Fleury, E., Larsen, K.G.: Optimal strategies in priced timed game automata. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 148–160. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30538-5_13CrossRefGoogle Scholar
  12. 12.
    Bouyer, P., Fahrenberg, U., Larsen, K., Markey, N.: Quantitative analysis of real-time systems using priced timed automata. Comm. ACM 54(9), 78–87 (2011)CrossRefGoogle Scholar
  13. 13.
    Bouyer, P., Forejt, V.: Reachability in stochastic timed games. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 103–114. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02930-1_9CrossRefGoogle Scholar
  14. 14.
    Bouyer, P., Markey, N., Randour, M., Larsen, K., Laursen, S.: Average-energy games. Acta Informatica 55(2), 91–127 (2018)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Brázdil, T., Hermanns, H., Krcál, J., Kretínský, J., Rehák, V.: Verification of open interactive Markov chains. In: Proceedings of FSTTCS 2012, LIPIcs 18 (2012)Google Scholar
  16. 16.
    Brázdil, T., Krčál, J., Křetínský, J., Kučera, A., Řehák, V.: Stochastic real-time games with qualitative timed automata objectives. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 207–221. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15375-4_15CrossRefGoogle Scholar
  17. 17.
    Brihaye, T., Bruyère, V., Raskin, J.-F.: On optimal timed strategies. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 49–64. Springer, Heidelberg (2005).  https://doi.org/10.1007/11603009_5CrossRefzbMATHGoogle Scholar
  18. 18.
    Cassez, F., David, A., Larsen, K.G., Lime, D., Raskin, J.-F.: Timed control with observation based and stuttering invariant strategies. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 192–206. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-75596-8_15CrossRefzbMATHGoogle Scholar
  19. 19.
    Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005).  https://doi.org/10.1007/11539452_9CrossRefGoogle Scholar
  20. 20.
    Condon, A.: On algorithms for simple stochastic games. In: Advances in Computational Complexity Theory, DIMACS Series in DMTCS 13 (1993)Google Scholar
  21. 21.
    Dehnert, C., Junges, S., Katoen, J.-P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 592–600. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63390-9_31CrossRefGoogle Scholar
  22. 22.
    Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997)zbMATHGoogle Scholar
  23. 23.
    Forejt, V., Kwiatkowska, M., Norman, G., Trivedi, A.: Expected reachability-time games. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 122–136. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15297-9_11CrossRefGoogle Scholar
  24. 24.
    Forejt, V., Kwiatkowska, M., Norman, G., Trivedi, A.: Expected reachability-time games. TCS 631, 139–160 (2016)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992).  https://doi.org/10.1007/3-540-55719-9_103CrossRefGoogle Scholar
  26. 26.
    Hermanns, H.: Interactive Markov Chains and the Quest for Quantified Quality. LNCS, vol. 2428. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45804-2CrossRefzbMATHGoogle Scholar
  27. 27.
    van der Hoek, W., Wooldridge, M.: Model checking cooperation, knowledge, and time - a case study. Res. Econ. 57(3), 235–265 (2003)CrossRefGoogle Scholar
  28. 28.
    Jovanovic, A., Kwiatkowska, M., Norman, G., Peyras, Q.: Symbolic optimal expected time reachability computation and controller synthesis for probabilistic timed automata. TCS 669, 1–21 (2017)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Jurdziński, M., Kwiatkowska, M., Norman, G., Trivedi, A.: Concavely-priced probabilistic timed automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 415–430. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-04081-8_28CrossRefGoogle Scholar
  30. 30.
    Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, New York (1976).  https://doi.org/10.1007/978-1-4684-9455-6CrossRefzbMATHGoogle Scholar
  31. 31.
    Krčál, J.: Determinacy and optimal strategies in stochastic games. Master’s thesis, School of Informatics, Masaryk University, Brno (2009)Google Scholar
  32. 32.
    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).  https://doi.org/10.1007/978-3-642-04368-0_17CrossRefzbMATHGoogle Scholar
  33. 33.
    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).  https://doi.org/10.1007/978-3-642-22110-1_47CrossRefGoogle Scholar
  34. 34.
    Kwiatkowska, M., Norman, G., Parker, D.: Symbolic verification and strategy synthesis for linearly-priced probabilistic timed automata. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 289–309. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63121-9_15CrossRefGoogle Scholar
  35. 35.
    Kwiatkowska, M., Norman, G., Parker, D.: Verification and control of turn-based probabilistic real-time games. arXiv:1906.09142 (2019)
  36. 36.
    Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automated verification of concurrent stochastic games. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 223–239. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-99154-2_14CrossRefGoogle Scholar
  37. 37.
    Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Equilibria-based probabilistic model checking for concurrent stochastic games. In: Proceeding of FM 2019, LNCS. Springer, Berlin (2019, to appear)Google Scholar
  38. 38.
    Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. FMSD 29, 33–78 (2006)zbMATHGoogle Scholar
  39. 39.
    Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. TCS 282, 101–150 (2002)MathSciNetCrossRefGoogle Scholar
  40. 40.
    Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. IC 205(7), 1027–1077 (2007)MathSciNetzbMATHGoogle Scholar
  41. 41.
    Kwiatkowska, M., Parker, D., Wiltsche, C.: PRISM-games: verification and strategy synthesis for stochastic multi-player games with multiple objectives. STTT 20(2), 195–210 (2018)CrossRefGoogle Scholar
  42. 42.
    Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Automatic analysis of a non-repudiation protocol. In: Proceedings of QAPL 2004, ENTCS 112 (2005)Google Scholar
  43. 43.
    Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-59042-0_76CrossRefGoogle Scholar
  44. 44.
    Markowitch, O., Roggeman, Y.: Probabilistic non-repudiation without trusted third party. In: Proceedings of Workshop Security in Communication Networks (1999)Google Scholar
  45. 45.
    Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. FMSD 43(2), 164–190 (2013)zbMATHGoogle Scholar
  46. 46.
    Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. RTS 53(3), 354–402 (2017)zbMATHGoogle Scholar
  47. 47.
    Oualhadj, Y., Reynier, P.-A., Sankur, O.: Probabilistic robust timed games. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 203–217. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44584-6_15CrossRefGoogle Scholar
  48. 48.
    Rudin, W.: Principles of Mathematical Analysis, 3rd edn. McGraw-Hill, New York (1976)zbMATHGoogle Scholar
  49. 49.
    La Torre, S., Mukhopadhyay, S., Murano, A.: Optimal-reachability and control for acyclic weighted timed automata. In: Baeza-Yates, R., Montanari, U., Santoro, N. (eds.) Foundations of Information Technology in the Era of Network and Mobile Computing. ITIFIP, vol. 96, pp. 485–497. Springer, Boston, MA (2002).  https://doi.org/10.1007/978-0-387-35608-2_40CrossRefGoogle Scholar
  50. 50.
    Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol. 1601, pp. 299–314. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48778-6_18CrossRefGoogle Scholar
  51. 51.
    Tripakis, S., Altisen, K.: On-the-fly controller synthesis for discrete and dense-time systems. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 233–252. Springer, Heidelberg (1999).  https://doi.org/10.1007/3-540-48119-2_15CrossRefGoogle Scholar
  52. 52.
    Tripakis, S., Yovine, S., Bouajjan, A.: Checking timed Büchi automata emptiness efficiently. FMSD 26(3), 267–292 (2005)zbMATHGoogle Scholar
  53. 53.

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Department of Computing ScienceUniversity of OxfordOxfordUK
  2. 2.School of Computing ScienceUniversity of GlasgowGlasgowUK
  3. 3.School of Computer ScienceUniversity of BirminghamBirminghamUK

Personalised recommendations