Abstract
This paper presents counterexample-guided inductive synthesis (CEGIS) to automatically synthesise probabilistic models. The starting point is a family of finite-stateMarkov chains with related but distinct topologies. Such families can succinctly be described by a sketch of a probabilistic program. Program sketches are programs containing holes. Every hole has a finite repertoire of possible program snippets by which it can be filled.We study several synthesis problems—feasibility, optimal synthesis, and complete partitioning—for a given quantitative specification \(\varphi\). Feasibility amounts to determine a family member satisfying \(\varphi\), optimal synthesis amounts to find a family member that maximises the probability to satisfy \(\varphi\), and complete partitioning splits the family in satisfying and refuting members. Each of these problems can be considered under the additional constraint of minimising the total cost of instantiations, e.g., what are all possible instantiations for \(\varphi\) that are within a certain budget? The synthesis problems are tackled using a CEGIS approach. The crux is to aggressively prune the search space by using counterexamples provided by a probabilistic model checker. Counterexamples can be viewed as sub-Markov chains that rule out all family members that share this sub-chain. Our CEGIS approach leverages efficient probabilisticmodel checking,modern SMT solving, and programsnippets as counterexamples. Experiments on case studies froma diverse nature—controller synthesis, program sketching, and security—show that synthesis among up to a million candidate designs can be done using a few thousand verification queries.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Ábrahám E, Becker B, Dehnert C, Jansen N, Katoen J-P, Wimmer R (2014) Counterexample generation for discrete-time Markov models: An introductory survey, Springer, vol 8483 of LNCS, pp 65–121
Alur R, Bodík R, Dallal E, Fisman D, Garg P, Juniwal G, Kress-Gazit H, Madhusudan P, Martin MMK, Raghothaman M, Saha S, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2015) Syntax-guided synthesis. In: Dependable software systems engineering, IOS Press, vol 40 of NATO Science for Peace and Security Series, pp 1–25
Abate A, David C, Kesseli P, Kroening D, Polgreen E (2018) Counterexample guided inductive synthesis modulo theories. In: CAV (1), Springer, vol 10981 of LNCS, pp 270–288
Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bulletin of the EATCS 95, 94–129 (2008)
Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun ACM 61(12), 84–93 (2018)
Benini, L., Bogliolo, A., Paleologo, G.A., De Micheli, G.: Policy optimization for dynamic power management. IEEE Trans CAD Integr Circuits Syst 18(6), 813–833 (1999)
Baier C, de Alfaro L, Forejt V, Kwiatkowska M (2018) Model checking probabilistic systems. In: Handbook of model checking, Springer, pp 963–999
Budde CE, Dehnert C, Hahn EM, Hartmanns A, Junges S, Turrini A (2017) JANI: quantitative model and tool interaction. In: TACAS, vol 10206 of LNCS, pp 151–168
Bartocci E, Grosu R, Katsaros P, Ramakrishnan CR, Smolka SA (2011) Model repair for probabilistic systems. In: TACAS, Springer, vol 6605 of LNCS, pp 326–340
Biere A, Heule M, van Maaren H, Walsh T (eds) (2009) Handbook of Satisfiability, IOS Press, vol 185 of Frontiers in artificial intelligence and applications
Baier C, Katoen J-P (2008) Principles of model checking MIT Press
Benes N, Křetínský J, Larsen KG, Møller MH, Srba J (2012) Dual-priced modal transition systems with time durations. In: LPAR, Springer, vol 7180 of LNCS, pp 122–137
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)
Bornholt J, Torlak E, Grossman D, Ceze L (2016) Optimizing synthesis with metasketches. In: POPL, ACM, pp 775–788
Cardelli L, Češka M, Fränzle M, Kwiatkowska M, Laurenti L, Paoletti N, Whitby M (2017) Syntax-guided optimal synthesis for chemical reaction networks. In: CAV, Springer, vol 10427 of LNCS, pp 375–395
Černý P, Chatterjee K, Henzinger TA, Radhakrishna A, Singh R (2011) Quantitative synthesis for concurrent programs. In: CAV, Springer, vol 6806 of LNCS, pp 243–259
Chaudhuri S, Clochard M, Solar-Lezama A (2014) Bridging boolean and quantitative synthesis using smoothed proof search. In: POPL, ACM, pp 207–220
Chrszon, P., Dubslaff, C., Klüppelholz, S., Baier, C.: ProFeat: feature-oriented engineering for family-based probabilistic model checking. Formal Asp Comput 30(1), 45–75 (2018)
Č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)
Calinescu, R., Ghezzi, C., Johnson, K., Pezzé, M., Rafiq, Y., Tamburrelli, G.: Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Trans Rel 65(1), 107–125 (2016)
Calinescu, R., Ghezzi, C., Kwiatkowska, M.Z., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun ACM 55(9), 69–77 (2012)
Chen T, Hahn EM, Han T, Kwiatkowska MZ, Qu H, Zhang L (2013) Model repair for Markov decision processes. In: TASE, IEEE, pp 85–92
Češka M, Hensel C, Junges S, Katoen J-P (2019) Counterexample-driven synthesis for probabilistic program sketches. In: Formal methods – the next 30 years, Springer International Publishing, vol 11800 of LNCS, pp 101–120
Chonev V (2017) Reachability in augmented interval Markov chains. CoRR abs/1701.02996
Češka M, Jansen N, Junges S, Katoen J-P (2019) Shepherding hordes of Markov chains. In: TACAS, Springer, vol 11428 of LNCS
Calinescu R, Češka M, Gerasimou S, Kwiatkowska M, Paoletti N (2017) Designing robust software systems through parametric Markov chain synthesis. In: ICSA, IEEE, pp 131–140
Calinescu R, Češka M, Gerasimou S, Kwiatkowska M, Paoletti N (2017) RODES: A robust-design synthesis tool for probabilistic systems. In: QEST, Springer, pp 304–308
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)
Dehnert C, Junges S, Katoen J-P, Volk M (2017) A storm is coming: A modern probabilistic model checker. In: CAV, Springer, vol 10427 of LNCS, pp 592–600
Dehnert C, Jansen N, Wimmer R, Ábrahám E, Katoen J-P (2014) Fast debugging of PRISM models. In ATVA, Springer, vol 8837 of LNCS, pp 146–162
Delahaye, B., Katoen, J.-P., Larsen, K.G., Legay, A., Pedersen, M.L., Sher, F., Wasowski, A.: Abstract probabilistic automata. Inf Comput 232, 66–116 (2013)
de Moura LM, Bjørner N (2008) Z3: an efficient SMT solver. In: TACAS, Springer, vol 4963 of LNCS, pp 337–340
Dureja R, Rozier KY (2018) More scalable LTL model checking via discovering design-space dependencies. In: TACAS (1), Springer, vol 10805 of LNCS, pp 309–327
Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. IEEE Trans Software Eng 42(1), 75–99 (2016)
Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found Trends Program Lang 4(1–2), 1–119 (2017)
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)
Gerasimou S, Tamburrelli G, Calinescu R (2015) Search-based synthesis of probabilistic models for quality-of-service software engineering. In: ASE, IEEE Computer Society, pp 319–330
Henzinger, T.A.: Quantitative reactive modeling and verification. Comput Sci - R&D 28(4), 331–344 (2013)
Hensel C (2018) The probabilistic model checker storm: Symbolic methods for probabilistic model checking. PhD thesis, RWTH Aachen University, Germany
Hartmanns A, Hermanns H (2014) The modest toolset: An integrated environment for quantitative modelling and verification. In: TACAS, Springer, pp 593–598
Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Softw Tools Technol Transf 13(1), 3–19 (2011)
Han, T., Katoen, J.-P., Damman, B.: Counterexample generation in probabilistic model checking. IEEE Trans Software Eng 35(2), 241–257 (2009)
Hartmanns A, Klauck M, Parker D, Quatmann T, Ruijters E (2019) The quantitative verification benchmark set. In: TACAS (1), Springer, vol 11427 of Lecture Notes in Computer Science, pp 344–350
Jansen N, Humphrey L, Tumova J, Topcu U (2019) Structured synthesis for probabilistic systems. In: NFM, Springer, vol 11460 of LNCS, pp 237–254
Junges S, Jansen N, Dehnert C, Topcu U, Katoen J-P (2016) Safety-constrained reinforcement learning for MDPs. In: TACAS, Springer, vol 9636 of LNCS, pp 130–146
Junges S, Jansen N, Wimmer R, Quatmann T, Winterer L, Katoen J-P, Becker B (2018) Finite-state controllers of POMDPs using parameter synthesis. In: UAI, AUAI Press, pp 519–529
Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Inf 54(7), 693–726 (2017)
Junges S (2020) Parameter synthesis in Markov models. PhD thesis, RWTH Aachen University, Germany, to appear
Katoen J-P (2016) The probabilistic model checking landscape. In: LICS, ACM, pp 31–45
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)
Kwiatkowska M, Norman G, Parker D (2011) Prism 4.0: Verification of probabilistic real-time systems. In: CAV, vol 6806 of LNCS, Springer, pp 585–591
Kwiatkowska, M.Z., Norman, G., Parker, D., Vigliotti, M.G.: Probabilistic mobile ambients. Theor Comput Sci 410(12–13), 1272–1303 (2009)
Kretínský J (2017) 30 years of modal transition systems: Survey of extensions and analysis. In: Models, algorithms, logics and tools, Springer, vol 10460 of LNCS, pp 36–74
Lanna, A., Castro, T., Alves, V., Rodrigues, G., Schobbens, P.-Y., Apel, S.: Feature-family-based reliability analysis of software product lines. Inform Softw Technol 94, 59–81 (2018)
Larsen KG, Thomsen B (1988) A modal process logic. In: LICS, IEEE Computer Society, pp 203–210
Meuleau N, Kim K-E, Kaelbling LP, Cassandra AR (1999) Solving POMDPs by searching the space of finite policies. In: UAI, Morgan Kaufmann Publishers Inc., pp 417–426
Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans Program Lang Syst 18(3), 325–353 (1996)
Nori AV, Ozair S, Rajamani SK, Vijaykeerthy D (2015) Efficient synthesis of probabilistic programs. In: PLDI, ACM, pp 208–217
Quatmann T, Dehnert C, Jansen N, Junges S, Katoen J-P (2016) Parameter synthesis for Markov models: Faster than ever. In: ATVA, vol 9938 of LNCS, pp 50–67
Quatmann T, Jansen N, Dehnert C, Wimmer R, Ábrahám E, Katoen J-P, Becker B (2015) Counterexamples for expected rewards. In: FM, Springer, vol 9109 of LNCS, pp 435–452
Rodrigues GN, Alves V, Nunes V, Lanna A, Cordy M, Schobbens P-Y, Sharifloo AM, Legay A (2015) Modeling and verification for probabilistic properties in software product lines. In: HASE, IEEE pp 173–180
Rosenblum DS (2016) The power of probabilistic thinking. In: ASE, ACM, p 3
Sesic, A., Dautovic, S., Malbasa, V.: Dynamic power management of a system with a two-priority request queue using probabilistic-model checking. IEEE Trans CAD Integr Circuits Syst 27(2), 403–407 (2008)
Solar-Lezama A, Jones CG, Bodik R (2008) Sketching concurrent data structures. In: PLDI, ACM, pp 136–148
Solar-Lezama A, Tancau L, Bodik R, Seshia S, Saraswat V (2006) Combinatorial sketching for finite programs. In: ASPLOS, ACM, pp 404–415
Solar-Lezama, A.: Program sketching. STTT 15(5–6), 475–495 (2013)
Solar-Lezama A, Rabbah RM, Bodík R, Ebcioglu K (2005) Programming by sketching for bit-streaming programs. In: PLDI, ACM, pp 281–294
Varshosaz M, Khosravi R (2013) Discrete time Markov chain families: modeling and verification of probabilistic software product lines. In: SPLC Workshops, ACM, pp 34–41
Vandin A, ter Beek MH, Legay A, Lluch-Lafuente A (2018) Qflan: A tool for the quantitative analysis of highly reconfigurable systems. In: FM, Springer, vol 10951 of LNCS, pp 329–337
Wimmer R, Jansen N, Ábrahám E, Becker B, Katoen J-P (2012) Minimal critical subsystems for discrete-time Markov models. In TACAS, Springer, vol 7214 of LNCS, pp 299–314
Wimmer, R., Jansen, N., Ábrahám, E., Katoen, J.-P., Becker, B.: Minimal counterexamples for linear-time probabilistic verification. Theor Comput Sci 549, 61–100 (2014)
Wimmer, R., Jansen, N., Vorpahl, A., Ábrahám, E., Katoen, J.-P., Becker, B.: High-level counterexamples for probabilistic automata. Log Methods Comput Sci 11(1), (2015)
Zhou W, Li W (2018) Safety-aware apprenticeship learning. In CAV'18, Springer, vol 10981 of LNCS, pp 662–680
Acknowledgements
We thank the reviewers for their detailed and constructive comments. We thank Roman Andriushchenko for help with some experiments. M. Češka is funded by the Czech Science Foundation grant GJ20-02328Y. S. Junges was supported in part by NSF grants 1545126 (VeHICaL) and 1646208, by theDARPA Assured Autonomy program and the DARPA SDCPS program (Contract: FA8750-20-C-0156), by Berkeley Deep Drive, and by Toyota under the iCyPhy center. J.P. Katoen is funded by the ERC Advanced Research Grant 787914 FRAPPANT.
Author information
Authors and Affiliations
Corresponding author
Additional information
Annabelle McIver, Maurice ter Beek and Cliff Jones
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
About this article
Cite this article
Češka, M., Hensel, C., Junges, S. et al. Counterexample-guided inductive synthesis for probabilistic systems. Form Asp Comp 33, 637–667 (2021). https://doi.org/10.1007/s00165-021-00547-2
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-021-00547-2