Skip to main content
SpringerLink
Log in
Book cover

International Conference on Quantitative Evaluation of Systems

QEST 2017: Quantitative Evaluation of Systems pp 259–274Cite as

Automated Experiment Design for Data-Efficient Verification of Parametric Markov Decision Processes

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10503))

Abstract

We present a new method for statistical verification of quantitative properties over a partially unknown system with actions, utilising a parameterised model (in this work, a parametric Markov decision process) and data collected from experiments performed on the underlying system. We obtain the confidence that the underlying system satisfies a given property, and show that the method uses data efficiently and thus is robust to the amount of data available. These characteristics are achieved by firstly exploiting parameter synthesis to establish a feasible set of parameters for which the underlying system will satisfy the property; secondly, by actively synthesising experiments to increase amount of information in the collected data that is relevant to the property; and finally propagating this information over the model parameters, obtaining a confidence that reflects our belief whether or not the system parameters lie in the feasible set, thereby solving the verification problem.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    A multinomial distribution is defined by its density function \(f(\cdot \mid p, N) \propto \prod _{i=1}^{k}p_i^{n_i}\), for \(n_i \in \{0,1,\ldots ,N\}\) and such that \(\sum _{i=1}^{k}n_i = N\), where \(N \in \mathbb {N}\) is a parameter and p is a discrete distribution over k outcomes.

References

  1. Araya-López, M., Buffet, O., Thomas, V., Charpillet, F.: Active learning of MDP models. In: Sanner, S., Hutter, M. (eds.) EWRL 2011. LNCS (LNAI), vol. 7188, pp. 42–53. Springer, Heidelberg (2012). doi:10.1007/978-3-642-29946-9_8

    Chapter  Google Scholar 

  2. Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  3. Chen, Y., Nielsen, T.D.: Active learning of Markov decision processes for system verification. In: ICMLA, vol. 2, pp. 289–294. IEEE (2012)

    Google Scholar 

  4. D’Argenio, P., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of Markov decision processes. STTT 17(4), 469–484 (2015)

    Article  Google Scholar 

  5. Friedman, N., Singer, Y.: Efficient Bayesian parameter estimation in large discrete domains. In: NIPS, pp. 417–423. The MIT Press (1998)

    Google Scholar 

  6. Galassi, M., Davies, J., Theiler, J., Gough, B., Jungman, G.: GNU Scientific Library - Reference Manual, GSL Version 1.12, 3rd edn. Network Theory Ltd., Bristol (2009)

    Google Scholar 

  7. Gevers, M., Bombois, X., Hildebrand, R., Solari, G.: Optimal experiment design for open and closed-loop system identification. Comm. Inf. Syst. 11(3), 197–224 (2011)

    MathSciNet  MATH  Google Scholar 

  8. Gretton, C., Price, D., Thiébaux, S.: Implementation and comparison of solution methods for decision processes with non-Markovian rewards. In: UAI, pp. 289–296. Morgan Kaufmann (2003)

    Google Scholar 

  9. Guan, P., Raginsky, M., Willett, R.M.: Online Markov decision processes with Kullback-Leibler control cost. IEEE Trans. Autom. Control 59(6), 1423–1438 (2014)

    Article  MathSciNet  MATH  Google Scholar 

  10. Haesaert, S., Van den Hof, P.M.J., Abate, A.: Data-driven property verification of grey-box systems by Bayesian experiment design. In: 2015 American Control Conference (ACC), pp. 1800–1805, July 2015

    Google Scholar 

  11. Haesaert, S., Van den Hof, P.M.J., Abate, A.: Experiment design for formal verification via stochastic optimal control. In: ECC, pp. 427–432. IEEE (2016)

    Google Scholar 

  12. Henriques, D., Martins, J., Zuliani, P., Platzer, A., Clarke, E.M.: Statistical model checking for Markov decision processes. In: QEST, pp. 84–93. IEEE Computer Society (2012)

    Google Scholar 

  13. Hoffman, M.D., de Freitas, N., Doucet, A., Peters, J.: An expectation maximization algorithm for continuous Markov decision processes with arbitrary reward. In: AISTATS, JMLR Proceedings, vol. 5, pp. 232–239. JMLR.org (2009)

    Google Scholar 

  14. Kwiatkowska, M.Z., 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). doi:10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  15. Kwiatkowska, M.Z., Parker, D.: Automated verification and strategy synthesis for probabilistic systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 5–22. Springer, Cham (2013). doi:10.1007/978-3-319-02444-8_2

    Chapter  Google Scholar 

  16. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_11

    Chapter  Google Scholar 

  17. Pasanisi, A., Fu, S., Bousquet, N.: Estimating discrete Markov models from various incomplete data schemes. Comput. Stat. Data Anal. 56(9), 2609–2625 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  18. Peter Eichelsbacher, A.G.: Bayesian inference for Markov chains. J. Appl. Probab. 39(1), 91–99 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  19. Polgreen, E., Wijesuriya, V.B., Haesaert, S., Abate, A.: Data-efficient Bayesian verification of parametric Markov chains. In: Agha, G., Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 35–51. Springer, Cham (2016). doi:10.1007/978-3-319-43425-4_3

    Chapter  Google Scholar 

  20. Poupart, P., Vlassis, N.A., Hoey, J., Regan, K.: An analytic solution to discrete Bayesian reinforcement learning. In: ICML. ACM International Conference Proceeding Series, vol. 148, pp. 697–704. ACM (2006)

    Google Scholar 

  21. Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.: Parameter synthesis for Markov models: faster than ever. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 50–67. Springer, Cham (2016). doi:10.1007/978-3-319-46520-3_4

    Chapter  Google Scholar 

  22. Ross, S., Pineau, J., Chaib-draa, B., Kreitmann, P.: A Bayesian approach for learning and planning in partially observable Markov decision processes. J. Mach. Learn. Res. 12, 1729–1770 (2011)

    MathSciNet  MATH  Google Scholar 

  23. Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27813-9_16

    Chapter  Google Scholar 

  24. Younes, H.L.S.: Probabilistic verification for black-box systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 253–265. Springer, Heidelberg (2005). doi:10.1007/11513988_25

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Elizabeth Polgreen, Viraj B. Wijesuriya & Alessandro Abate

  2. Department of Electrical Engineering, Eindhoven University of Technology, Eindhoven, The Netherlands

    Sofie Haesaert

Authors
  1. Elizabeth Polgreen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Viraj B. Wijesuriya
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sofie Haesaert
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alessandro Abate
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Elizabeth Polgreen .

Editor information

Editors and Affiliations

  1. Inria, Rennes, France

    Nathalie Bertrand

  2. University of Trieste, Trieste, Italy

    Luca Bortolussi

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Polgreen, E., Wijesuriya, V.B., Haesaert, S., Abate, A. (2017). Automated Experiment Design for Data-Efficient Verification of Parametric Markov Decision Processes. In: Bertrand, N., Bortolussi, L. (eds) Quantitative Evaluation of Systems. QEST 2017. Lecture Notes in Computer Science(), vol 10503. Springer, Cham. https://doi.org/10.1007/978-3-319-66335-7_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66335-7_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66334-0

  • Online ISBN: 978-3-319-66335-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation