Skip to main content
SpringerLink
Log in

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

  • Chapter
  • First Online:
The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy

Part of the book series: Lecture Notes in Computer Science ((LNTCS,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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    A constraint is closed if does not contain strict inequalities and diagonal-free if there are no inequalities of the form \(x {-} y \sim c\) for \(x,y \in \mathcal {X}\), \(\sim \in \{<,\,\leqslant \,,\,\geqslant \,,>\}\) and \(c \in \mathbb {N}\).

References

  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_9

    Chapter  Google Scholar 

  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. 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_13

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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. Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: Proceedings of SSC 1998. Elsevier (1998)

    Google Scholar 

  7. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. CACM 53(9), 76–85 (2010)

    Article  Google Scholar 

  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_14

    Chapter  Google Scholar 

  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_15

    Chapter  Google Scholar 

  10. Bouyer, P., Brihaye, T., Markey, N.: Improved undecidability results on weighted timed automata. IPL 98, 188–194 (2006)

    Article  MathSciNet  Google Scholar 

  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_13

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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_9

    Chapter  Google Scholar 

  14. Bouyer, P., Markey, N., Randour, M., Larsen, K., Laursen, S.: Average-energy games. Acta Informatica 55(2), 91–127 (2018)

    Article  MathSciNet  Google Scholar 

  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. 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_15

    Chapter  Google Scholar 

  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_5

    Chapter  MATH  Google Scholar 

  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_15

    Chapter  MATH  Google Scholar 

  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_9

    Chapter  Google Scholar 

  20. Condon, A.: On algorithms for simple stochastic games. In: Advances in Computational Complexity Theory, DIMACS Series in DMTCS 13 (1993)

    Google Scholar 

  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_31

    Chapter  Google Scholar 

  22. Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, New York (1997)

    MATH  Google Scholar 

  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_11

    Chapter  Google Scholar 

  24. Forejt, V., Kwiatkowska, M., Norman, G., Trivedi, A.: Expected reachability-time games. TCS 631, 139–160 (2016)

    Article  MathSciNet  Google Scholar 

  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_103

    Chapter  Google Scholar 

  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-2

    Book  MATH  Google Scholar 

  27. van der Hoek, W., Wooldridge, M.: Model checking cooperation, knowledge, and time - a case study. Res. Econ. 57(3), 235–265 (2003)

    Article  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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_28

    Chapter  Google Scholar 

  30. Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, New York (1976). https://doi.org/10.1007/978-1-4684-9455-6

    Book  MATH  Google Scholar 

  31. Krčál, J.: Determinacy and optimal strategies in stochastic games. Master’s thesis, School of Informatics, Masaryk University, Brno (2009)

    Google Scholar 

  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_17

    Chapter  MATH  Google Scholar 

  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_47

    Chapter  Google Scholar 

  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_15

    Chapter  Google Scholar 

  35. Kwiatkowska, M., Norman, G., Parker, D.: Verification and control of turn-based probabilistic real-time games. arXiv:1906.09142 (2019)

  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_14

    Chapter  Google Scholar 

  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. Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. FMSD 29, 33–78 (2006)

    MATH  Google Scholar 

  39. Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. TCS 282, 101–150 (2002)

    Article  MathSciNet  Google Scholar 

  40. Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. IC 205(7), 1027–1077 (2007)

    MathSciNet  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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. 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_76

    Chapter  Google Scholar 

  44. Markowitch, O., Roggeman, Y.: Probabilistic non-repudiation without trusted third party. In: Proceedings of Workshop Security in Communication Networks (1999)

    Google Scholar 

  45. Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. FMSD 43(2), 164–190 (2013)

    MATH  Google Scholar 

  46. Norman, G., Parker, D., Zou, X.: Verification and control of partially observable probabilistic systems. RTS 53(3), 354–402 (2017)

    MATH  Google Scholar 

  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_15

    Chapter  Google Scholar 

  48. Rudin, W.: Principles of Mathematical Analysis, 3rd edn. McGraw-Hill, New York (1976)

    MATH  Google Scholar 

  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_40

    Chapter  Google Scholar 

  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_18

    Chapter  Google Scholar 

  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_15

    Chapter  Google Scholar 

  52. Tripakis, S., Yovine, S., Bouajjan, A.: Checking timed Büchi automata emptiness efficiently. FMSD 26(3), 267–292 (2005)

    MATH  Google Scholar 

  53. Supporting material. www.prismmodelchecker.org/files/tptgs/

Download references

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).

Author information

Authors and Affiliations

  1. Department of Computing Science, University of Oxford, Oxford, UK

    Marta Kwiatkowska

  2. School of Computing Science, University of Glasgow, Glasgow, UK

    Gethin Norman

  3. School of Computer Science, University of Birmingham, Birmingham, UK

    David Parker

Authors
  1. Marta Kwiatkowska
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Gethin Norman
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Parker
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Gethin Norman .

Editor information

Editors and Affiliations

  1. Universidade Federal de Minas Gerais, Belo Horizonte, Brazil

    Mário S. Alvim

  2. University of Athens, Athens, Greece

    Kostas Chatzikokolakis

  3. Federal University of Rio Grande do Norte - UFRN, Natal, Brazil

    Carlos Olarte

  4. CNRS & University Javeriana Cali, Palaiseau, France

    Frank Valencia

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Kwiatkowska, M., Norman, G., Parker, D. (2019). Verification and Control of Turn-Based Probabilistic Real-Time Games. In: Alvim, M., Chatzikokolakis, K., Olarte, C., Valencia, F. (eds) The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy. Lecture Notes in Computer Science(), vol 11760. Springer, Cham. https://doi.org/10.1007/978-3-030-31175-9_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-31175-9_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31174-2

  • Online ISBN: 978-3-030-31175-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation