[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Model Repair Revamped

— On the Automated Synthesis of Markov Chains —

  • Chapter
  • First Online:
From Reactive Systems to Cyber-Physical Systems

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

  • 550 Accesses

Abstract

This paper outlines two approaches—based on counterexample-guided abstraction refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS), respectively—to the automated synthesis of finite-state probabilistic models and programs. Our CEGAR approach iteratively partitions the design space starting from an abstraction of this space and refines this by a light-weight analysis of verification results. The CEGIS technique exploits critical subsystems as counterexamples to prune all programs behaving incorrectly on that input. We show the applicability of these synthesis techniques to sketching of probabilistic programs, controller synthesis of POMDPs, and software product lines.

This work has been supported by the DFG RTG 2236 “UnRAVeL”, the ERC Advanced Grant 787914 “FRAPPANT”, the Czech Science Foundation grant No. AUTODEV GA19-24397S, and the IT4Innovations excellence in science project No. LQ1602.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
GBP 19.95
Price includes VAT (United Kingdom)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
GBP 35.99
Price includes VAT (United Kingdom)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
GBP 44.99
Price includes VAT (United Kingdom)
  • 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

Similar content being viewed by others

Notes

  1. 1.

    Note that \(\lnot \varphi \) is not a safety property, but the presented idea can be extended to liveness properties too.

  2. 2.

    For some suitable measure of size.

References

  1. Alur, R., Singh, R., Fisman, D., Solar-Lezama, A.: Search-based program synthesis. Commun. ACM 61(12), 84–93 (2018)

    Article  Google Scholar 

  2. Aziz, A., Singhal, V., Balarin, F., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: It usually works: the temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 155–165. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-60045-0_48

    Chapter  Google Scholar 

  3. 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_28

    Chapter  MATH  Google Scholar 

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

    MATH  Google Scholar 

  5. 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_30

    Chapter  MATH  Google Scholar 

  6. Benini, L., Bogliolo, A., Paleologo, G.A., Micheli, G.D.: Policy optimization for dynamic power management. IEEE Trans. CAD Integr. Circuits Syst. 18(6), 813–833 (1999)

    Article  Google Scholar 

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

    Article  Google Scholar 

  8. Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artif. Intell. 112(1–2), 57–104 (1999)

    Article  MathSciNet  Google Scholar 

  9. 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_9

    Chapter  Google Scholar 

  10. Chasins, S., Phothilimthana, P.M.: Data-driven synthesis of full probabilistic programs. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017, Part I. LNCS, vol. 10426, pp. 279–304. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_14

    Chapter  Google Scholar 

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

  12. Chatterjee, K., Chmelik, M., Tracol, M.: What is decidable about partially observable Markov decision processes with \(\omega \)-regular objectives. J. Comput. Syst. Sci. 82(5), 878–911 (2016)

    Article  MathSciNet  Google Scholar 

  13. Chatzieleftheriou, G., Bonakdarpour, B., Katsaros, P., Smolka, S.A.: Abstract model repair. Log. Methods Comput. Sci. 11(3) (2015)

    Google Scholar 

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

  15. Chonev, V.: Reachability in augmented interval Markov chains. CoRR arXiv:1701.02996 (2017)

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

    Article  MathSciNet  Google Scholar 

  17. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15

    Chapter  Google Scholar 

  18. Classen, A., Cordy, M., Heymans, P., Legay, A., Schobbens, P.: Model checking software product lines with SNIP. STTT 14(5), 589–612 (2012)

    Article  Google Scholar 

  19. Cubuktepe, M., Jansen, N., Junges, S., Katoen, J.-P., Topcu, U.: Synthesis in pMDPs: a tale of 1001 parameters. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 160–176. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_10

    Chapter  Google Scholar 

  20. 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_11

    Chapter  Google Scholar 

  21. Dehnert, C., Junges, S., Jansen, N., Corzilius, F., Volk, M., Bruintjes, H., Katoen, J.-P., Ábrahám, E.: PROPhESY: a PRObabilistic ParamEter SYnthesis tool. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 214–231. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_13

    Chapter  Google Scholar 

  22. Gerasimou, S., Tamburrelli, G., Calinescu, R.: Search-based synthesis of probabilistic models for quality-of-service software engineering (T). In: ASE, pp. 319–330. IEEE Computer Society (2015)

    Google Scholar 

  23. Gulwani, S., Polozov, O., Singh, R.: Program synthesis. Found. Trends Program. Lang. 4(1–2), 1–119 (2017)

    Google Scholar 

  24. Junges, S., et al.: Finite-state controllers of POMDPs using parameter synthesis. In: UAI, pp. 519–529. AUAI Press (2018)

    Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  26. Katoen, J.P.: The probabilistic model checking landscape. In: LICS, pp. 31–45. ACM (2016)

    Google Scholar 

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

  28. Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning deterministic probabilistic automata from a model checking perspective. Mach. Learn. 105(2), 255–299 (2016)

    Article  MathSciNet  Google Scholar 

  29. Meuleau, N., Kim, K., Kaelbling, L.P., Cassandra, A.R.: Solving POMDPs by searching the space of finite policies. In: UAI, pp. 417–426. Morgan Kaufmann (1999)

    Google Scholar 

  30. Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. 18(3), 325–353 (1996)

    Article  Google Scholar 

  31. Nori, A.V., Ozair, S., Rajamani, S.K., Vijaykeerthy, D.: Efficient synthesis of probabilistic programs. In: PLDI, pp. 208–217. ACM (2015)

    Article  Google Scholar 

  32. Pathak, S., Ábrahám, E., Jansen, N., Tacchella, A., Katoen, J.-P.: A greedy approach for the efficient repair of stochastic models. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 295–309. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9_21

    Chapter  Google Scholar 

  33. Rodrigues, G.N., et al.: Modeling and verification for probabilistic properties in software product lines. In: HASE, pp. 173–180. IEEE (2015)

    Google Scholar 

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

    Article  Google Scholar 

  35. Solar-Lezama, A.: Program sketching. STTT 15(5–6), 475–495 (2013)

    Article  Google Scholar 

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

  37. Češka, M., Hensel, C., Junges, S., Katoen, J.P.: Counterexample-driven synthesis for probabilistic program sketches. CoRR abs/1904.12371 (2019)

    Google Scholar 

  38. Č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_10

    Chapter  Google Scholar 

  39. Vlassis, N., Littman, M.L., Barber, D.: On the computational complexity of stochastic controller optimization in POMDPs. TOCT 4(4), 12:1–12:8 (2012)

    Article  Google Scholar 

  40. Wang, J., Sun, J., Yuan, Q., Pang, J.: Learning probabilistic models for model checking: an evolutionary approach and an empirical study. STTT 20(6), 689–704 (2018)

    Article  Google Scholar 

  41. Wimmer, R., Jansen, N., Ábrahám, E., Katoen, J., Becker, B.: Minimal counterexamples for linear-time probabilistic verification. Theor. Comput. Sci. 549, 61–100 (2014)

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FIT, IT4I Centre of Excellence, Brno University of Technology, Brno, Czech Republic

    Milan Češka

  2. RWTH Aachen University, Aachen, Germany

    Christian Dehnert, Sebastian Junges & Joost-Pieter Katoen

  3. Radboud University, Nijmegen, The Netherlands

    Nils Jansen

Authors
  1. Milan Češka
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christian Dehnert
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nils Jansen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sebastian Junges
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Joost-Pieter Katoen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Joost-Pieter Katoen .

Editor information

Editors and Affiliations

  1. Technische Universität Wien, Vienna, Austria

    Ezio Bartocci

  2. University of Maryland, College Park, MD, USA

    Rance Cleaveland

  3. Technische Universität Wien, Vienna, Austria

    Radu Grosu

  4. University of Pennsylvania, Philadelphia, PA, USA

    Oleg Sokolsky

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

Češka, M., Dehnert, C., Jansen, N., Junges, S., Katoen, JP. (2019). Model Repair Revamped. In: Bartocci, E., Cleaveland, R., Grosu, R., Sokolsky, O. (eds) From Reactive Systems to Cyber-Physical Systems. Lecture Notes in Computer Science(), vol 11500. Springer, Cham. https://doi.org/10.1007/978-3-030-31514-6_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-31514-6_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-31513-9

  • Online ISBN: 978-3-030-31514-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation