Advertisement

Counterexample-Driven Synthesis for Probabilistic Program Sketches

  • Milan Češka
  • Christian Hensel
  • Sebastian JungesEmail author
  • Joost-Pieter Katoen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

Probabilistic programs are key to deal with uncertainty in, e.g., controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring quantitative reasoning over a myriad of alternative designs. To mitigate this complexity, we adopt counterexample-guided inductive synthesis (CEGIS) to automatically synthesise finite-state probabilistic programs. Our approach leverages efficient model checking, modern SMT solving, and counterexample generation at program level. Experiments on practically relevant case studies show that design spaces with millions of candidate designs can be fully explored using a few thousand verification queries.

References

  1. 1.
    Abate, A., David, C., Kesseli, P., Kroening, D., Polgreen, E.: Counterexample guided inductive synthesis modulo theories. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 270–288. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96145-3_15CrossRefGoogle Scholar
  2. 2.
    Ábrahám, E., Becker, B., Dehnert, C., Jansen, N., Katoen, J.-P., Wimmer, R.: Counterexample generation for discrete-time Markov models: an introductory survey. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 65–121. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-07317-0_3CrossRefzbMATHGoogle Scholar
  3. 3.
    Alur, R., et al.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, NATO Science for Peace and Security Series, vol. 40, pp. 1–25. IOS Press (2015)Google Scholar
  4. 4.
    Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun. ACM 61(12), 84–93 (2018)CrossRefGoogle Scholar
  5. 5.
    Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bull. EATCS 95, 94–129 (2008)MathSciNetzbMATHGoogle Scholar
  6. 6.
    Baier, C., de Alfaro, L., Forejt, V., Kwiatkowska, M.: Model checking probabilistic systems. Handbook of Model Checking, pp. 963–999. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-10575-8_28CrossRefzbMATHGoogle Scholar
  7. 7.
    Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  8. 8.
    Balsamo, S., Di Marco, A., Inverardi, P., Simeoni, M.: Model-based performance prediction in software development: a survey. IEEE Trans. Softw. Eng. 30(5), 295–310 (2004)CrossRefGoogle Scholar
  9. 9.
    Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C.R., Smolka, S.A.: Model repair for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 326–340. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-19835-9_30CrossRefzbMATHGoogle Scholar
  10. 10.
    Becker, S., Koziolek, H., Reussner, R.: The Palladio component model for model-driven performance prediction. J. Syst. Softw. 82(1), 3–22 (2009)CrossRefGoogle Scholar
  11. 11.
    Benes, N., Kretínský, J., Larsen, K.G., Møller, M.H., Sickert, S., Srba, J.: Refinement checking on parametric modal transition systems. Acta Inf. 52(2–3), 269–297 (2015)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Beneš, N., Křetínský, J., Guldstrand Larsen, K., Møller, M.H., Srba, J.: Dual-priced modal transition systems with time durations. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 122–137. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28717-6_12CrossRefGoogle Scholar
  13. 13.
    Benini, L., Bogliolo, A., Paleologo, G., Micheli, G.D.: Policy optimization for dynamic power management. IEEE Trans. CAD Integr. Circ. Syst. 8(3), 299–316 (2000)Google Scholar
  14. 14.
    Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)Google Scholar
  15. 15.
    Bohnenkamp, H.C., D’Argenio, P.R., Hermanns, H., Katoen, J.P.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812–830 (2006)CrossRefGoogle Scholar
  16. 16.
    Bondy, A.B.: Foundations of Software and System Performance Engineering. Addison Wesley, Boston (2014)Google Scholar
  17. 17.
    Bornholt, J., Torlak, E., Grossman, D., Ceze, L.: Optimizing synthesis with metasketches. In: POPL, pp. 775–788. ACM (2016)Google Scholar
  18. 18.
    Budde, C.E., Dehnert, C., Hahn, E.M., Hartmanns, A., Junges, S., Turrini, A.: JANI: quantitative model and tool interaction. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 151–168. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54580-5_9CrossRefGoogle Scholar
  19. 19.
    Calinescu, R., Ghezzi, C., Johnson, K., et al.: Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Trans. Reliab. 65(1), 107–125 (2016)CrossRefGoogle Scholar
  20. 20.
    Calinescu, R., Ghezzi, C., Kwiatkowska, M.Z., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55(9), 69–77 (2012)CrossRefGoogle Scholar
  21. 21.
    Calinescu, R., Češka, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Designing robust software systems through parametric Markov chain synthesis. In: ICSA, pp. 131–140. IEEE (2017)Google Scholar
  22. 22.
    Calinescu, R., Češka, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: RODES: a robust-design synthesis tool for probabilistic systems. In: Bertrand, N., Bortolussi, L. (eds.) QEST 2017. LNCS, vol. 10503, pp. 304–308. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66335-7_20CrossRefGoogle Scholar
  23. 23.
    Calinescu, R., Češka, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Efficient synthesis of robust models for stochastic systems. J. Syst. Softw. 143, 140–158 (2018)CrossRefGoogle Scholar
  24. 24.
    Cardelli, L., et al.: Syntax-guided optimal synthesis for chemical reaction networks. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 375–395. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63390-9_20CrossRefGoogle Scholar
  25. 25.
    Černý, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 243–259. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_20CrossRefGoogle Scholar
  26. 26.
    Češka, M., Dannenberg, F., Paoletti, N., Kwiatkowska, M., Brim, L.: Precise parameter synthesis for stochastic biochemical systems. Acta Inf. 54(6), 589–623 (2017)MathSciNetCrossRefGoogle Scholar
  27. 27.
    Češka, M., Jansen, N., Junges, S., Katoen, J.-P.: Shepherding hordes of Markov chains. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 172–190. Springer, Cham (2019).  https://doi.org/10.1007/978-3-030-17465-1_10CrossRefGoogle Scholar
  28. 28.
    Chadha, R., Viswanathan, M.: A counterexample-guided abstraction-refinement framework for markov decision processes. ACM Trans. Comput. Log. 12(1), 1:1–1:49 (2010)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Chatterjee, K., Chmelik, M., Davies, J.: A symbolic SAT-based algorithm for almost-sure reachability with small strategies in POMDPs. In: AAAI, pp. 3225–3232. AAAI Press (2016)Google Scholar
  30. 30.
    Chaudhuri, S., Clochard, M., Solar-Lezama, A.: Bridging boolean and quantitative synthesis using smoothed proof search. In: POPL. ACM (2014)Google Scholar
  31. 31.
    Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M.Z., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: TASE, pp. 85–92. IEEE (2013)Google Scholar
  32. 32.
    Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Aspects Comput. 30(1), 45–75 (2018)MathSciNetCrossRefGoogle Scholar
  33. 33.
    Dehnert, C., Jansen, N., Wimmer, R., Ábrahám, E., Katoen, J.-P.: Fast debugging of PRISM models. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 146–162. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-11936-6_11CrossRefGoogle Scholar
  34. 34.
    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
  35. 35.
    Delahaye, B., et al.: Abstract probabilistic automata. Inf. Comput. 232, 66–116 (2013)MathSciNetCrossRefGoogle Scholar
  36. 36.
    Dureja, R., Rozier, K.Y.: More scalable LTL model checking via discovering design-space dependencies (\(D^{3}\)). In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 309–327. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89960-2_17CrossRefGoogle Scholar
  37. 37.
    Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans. Softw. Eng. 42(1), 75–99 (2016)CrossRefGoogle Scholar
  38. 38.
    Fiondella, L., Puliafito, A. (eds.): Principles of Performance and Reliability Modeling and Evaluation. SSRE. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-30599-8CrossRefGoogle Scholar
  39. 39.
    Gerasimou, S., Tamburrelli, G., Calinescu, R.: Search-based synthesis of probabilistic models for quality-of-service software engineering. In: ASE, pp. 319–330. IEEE Computer Society (2015)Google Scholar
  40. 40.
    Ghezzi, C., Sharifloo, A.M.: Model-based verification of quantitative non-functional properties for software product lines. Inf. Softw. Technol. 55(3), 508–524 (2013)CrossRefGoogle Scholar
  41. 41.
    Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found. Trends Programm. Lang. 4(1–2), 1–119 (2017)Google Scholar
  42. 42.
    Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric markov models. Softw. Tools Technol. Transf. 13(1), 3–19 (2011)CrossRefGoogle Scholar
  43. 43.
    Henzinger, T.A.: Quantitative reactive modeling and verification. Comput. Sci.- Res. Dev. 28(4), 331–344 (2013)CrossRefGoogle Scholar
  44. 44.
    Hessel, A., Larsen, K.G., Mikucionis, M., Nielsen, B., Pettersson, P., Skou, A.: Testing real-time systems using UPPAAL. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 77–117. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78917-8_3CrossRefGoogle Scholar
  45. 45.
    Jansen, N., Humphrey, L.R., Tumova, J., Topcu, U.: Structured synthesis for probabilistic systems. CoRR abs/1807.06106, at NFM 2019 (2018, to appear)Google Scholar
  46. 46.
    Junges, S., Jansen, N., Dehnert, C., Topcu, U., Katoen, J.-P.: Safety-constrained reinforcement learning for MDPs. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 130–146. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_8CrossRefGoogle Scholar
  47. 47.
    Junges, S., et al.: Finite-state controllers of POMDPs using parameter synthesis. In: UAI, pp. 519–529. AUAI Press (2018)Google Scholar
  48. 48.
    Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artif. Intell. 101(1–2), 99–134 (1998)MathSciNetCrossRefGoogle Scholar
  49. 49.
    Křetínský, J.: 30 years of modal transition systems: survey of extensions and analysis. 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. 36–74. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-63121-9_3CrossRefGoogle Scholar
  50. 50.
    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
  51. 51.
    Kwiatkowska, M.Z., Norman, G., Parker, D., Vigliotti, M.G.: Probabilistic mobile ambients. Theor. Comput. Sci. 410(12–13), 1272–1303 (2009)MathSciNetCrossRefGoogle Scholar
  52. 52.
    Larsen, K.G.: Verification and performance analysis of embedded and cyber-physical systems using UPPAAL. In: MODELSWARD 2014, pp. IS-11 (2014)Google Scholar
  53. 53.
    Larsen, K.G., Thomsen, B.: A modal process logic. In: LICS, pp. 203–210. IEEE Computer Society (1988)Google Scholar
  54. 54.
    Lindemann, C.: Performance modelling with deterministic and stochastic Petri nets. Perf. Eval. Review 26(2), 3 (1998)MathSciNetCrossRefGoogle Scholar
  55. 55.
    Meuleau, N., Kim, K.E., Kaelbling, L.P., Cassandra, A.R.: Solving POMDPs by searching the space of finite policies. In: UAI, pp. 417–426. Morgan Kaufmann Publishers Inc. (1999)Google Scholar
  56. 56.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  57. 57.
    Nori, A.V., Ozair, S., Rajamani, S.K., Vijaykeerthy, D.: Efficient synthesis of probabilistic programs. In: PLDI, pp. 208–217. ACM (2015)Google Scholar
  58. 58.
    Quatmann, T., Dehnert, C., Jansen, N., Junges, S., Katoen, J.-P.: 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).  https://doi.org/10.1007/978-3-319-46520-3_4CrossRefzbMATHGoogle Scholar
  59. 59.
    Rodrigues, et al.: Modeling and verification for probabilistic properties in software product lines. In: HASE, pp. 173–180. IEEE (2015)Google Scholar
  60. 60.
    Rosenblum, D.S.: The power of probabilistic thinking. In: ASE, p. 3. ACM (2016)Google Scholar
  61. 61.
    Sharma, V.S., Trivedi, K.S.: Quantifying software performance, reliability and security: an architecture-based approach. J. Syst. Softw. 80(4), 493–509 (2007)CrossRefGoogle Scholar
  62. 62.
    Solar-Lezama, A., Jones, C.G., Bodik, R.: Sketching concurrent data structures. In: PLDI, pp. 136–148. ACM (2008)Google Scholar
  63. 63.
    Solar-Lezama, A., Rabbah, R.M., Bodík, R., Ebcioglu, K.: Programming by sketching for bit-streaming programs. In: PLDI, pp. 281–294. ACM (2005)Google Scholar
  64. 64.
    Solar-Lezama, A., Tancau, L., Bodik, R., Seshia, S., Saraswat, V.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404–415. ACM (2006)Google Scholar
  65. 65.
    Stewart, W.J.: Probability, Markov Chains, Queues, and Simulation: The Mathematical Basis of Performance Modeling. Princeton university press (2009)Google Scholar
  66. 66.
    Vandin, A., ter Beek, M.H., Legay, A., Lluch Lafuente, A.: QFLan: a tool for the quantitative analysis of highly reconfigurable systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 329–337. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-95582-7_19CrossRefGoogle Scholar
  67. 67.
    Varshosaz, M., Khosravi, R.: Discrete time Markov chain families: modeling and verification of probabilistic software product lines. In: SPLC Workshops, pp. 34–41. ACM (2013)Google Scholar
  68. 68.
    Češka, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-driven synthesis for probabilistic program sketches. CoRR abs/1904.12371 (2019)Google Scholar
  69. 69.
    Vlassis, N., Littman, M.L., Barber, D.: On the computational complexity of stochastic controller optimization in POMDPs. ACM Trans. Comput. Theor. 4(4), 12:1–12:8 (2012).  https://doi.org/10.1145/2382559.2382563CrossRefzbMATHGoogle Scholar
  70. 70.
    Wimmer, R., Jansen, N., Ábrahám, E., Becker, B., Katoen, J.-P.: Minimal critical subsystems for discrete-time Markov models. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 299–314. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28756-5_21CrossRefzbMATHGoogle Scholar
  71. 71.
    Wimmer, R., Jansen, N., Vorpahl, A., Ábrahám, E., Katoen, J.-P., Becker, B.: High-Level Counterexamples for Probabilistic Automata. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 39–54. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-40196-1_4CrossRefGoogle Scholar
  72. 72.
    Woodside, M., Petriu, D., Merseguer, J., Petriu, D., Alhaj, M.: Transformation challenges: from software models to performance models. J. Softw. Syst. Model. 13(4), 1529–1552 (2014)CrossRefGoogle Scholar
  73. 73.
    Wu, S., Smolka, S.A., Stark, E.W.: Composition and behaviors of probabilistic I/O automata. Theor. Comput. Sci. 176(1–2), 1–38 (1997)MathSciNetCrossRefGoogle Scholar
  74. 74.
    Zhou, W., Li, W.: Safety-aware apprenticeship learning. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 662–680. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-96145-3_38CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Milan Češka
    • 1
  • Christian Hensel
    • 2
  • Sebastian Junges
    • 2
    Email author
  • Joost-Pieter Katoen
    • 2
  1. 1.Brno University of Technology, FIT, IT4I Centre of ExcellenceBrnoCzech Republic
  2. 2.RWTH Aachen UniversityAachenGermany

Personalised recommendations