Advertisement

Pegasus: A Framework for Sound Continuous Invariant Generation

  • Andrew SogokonEmail author
  • Stefan MitschEmail author
  • Yong Kiam TanEmail author
  • Katherine CordwellEmail author
  • André PlatzerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)

Abstract

Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to automation of formal proofs of safety in hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.

Keywords

Invariant generation Continuous invariants Ordinary differential equations Theorem proving 

Notes

Acknowledgements

The authors would like to thank the anonymous reviewers for their feedback.

References

  1. 1.
    Alur, R., Henzinger, T.A., Lafferriere, G., Pappas, G.J.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000).  https://doi.org/10.1109/5.871304CrossRefGoogle Scholar
  2. 2.
    Arrowsmith, D., Place, C.M.: Dynamical Systems: Differential Equations, Maps, and Chaotic Behaviour, vol. 5. CRC Press, Boca Raton (1992)CrossRefGoogle Scholar
  3. 3.
    Beckert, B., et al.: The KeY system 1.0 (deduction component). In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 379–384. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73595-3_26CrossRefGoogle Scholar
  4. 4.
    Sassi, M.A.B., Girard, A., Sankaranarayanan, S.: Iterative computation of polyhedral invariants sets for polynomial dynamical systems. In: CDC 2014, pp. 6348–6353. IEEE (2014).  https://doi.org/10.1109/CDC.2014.7040384
  5. 5.
    Böhme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179–194. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-14052-5_14CrossRefGoogle Scholar
  6. 6.
    Bohrer, B., Tan, Y.K., Mitsch, S., Myreen, M.O., Platzer, A.: VeriPhy: verified controller executables from verified cyber-physical system models. In: Foster, J.S., Grossman, D. (eds.) PLDI 2018, pp. 617–630. ACM (2018).  https://doi.org/10.1145/3192366.3192406
  7. 7.
    Chen, M., et al.: MARS: a toolchain for modelling, analysis and verification of hybrid systems. In: Hinchey, M.G., Bowen, J.P., Olderog, E.-R. (eds.) Provably Correct Systems. NMSSE 2017, pp. 39–58. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-48628-4_3
  8. 8.
    Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975).  https://doi.org/10.1007/3-540-07407-4_17CrossRefGoogle Scholar
  9. 9.
    Cox, D.A., Little, J., O’Shea, D.: Ideals, Varieties, and Algorithms. UTM 2015. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-16721-3
  10. 10.
    Dai, L., Gan, T., Xia, B., Zhan, N.: Barrier certificates revisited. J. Symb. Comput. 80, 62–86 (2017).  https://doi.org/10.1016/j.jsc.2016.07.010MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Darboux, J.G.: Mémoire sur les équations différentielles algébriques du premier ordre et du premier degré. Bull. Sci. Math. 2(1), 151–200 (1878)zbMATHGoogle Scholar
  12. 12.
    Denman, W., Muñoz, C.: Automated real proving in PVS via MetiTarski. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 194–199. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-06410-9_14CrossRefGoogle Scholar
  13. 13.
    Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_30CrossRefGoogle Scholar
  14. 14.
    Fulton, N., Mitsch, S., Bohrer, B., Platzer, A.: Bellerophon: tactical theorem proving for hybrid systems. In: Ayala-Rincón, M., Muñoz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 207–224. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66107-0_14CrossRefzbMATHGoogle Scholar
  15. 15.
    Fulton, N., Mitsch, S., Quesel, J.-D., Völp, M., Platzer, A.: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527–538. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21401-6_36CrossRefGoogle Scholar
  16. 16.
    Gan, T., Chen, M., Li, Y., Xia, B., Zhan, N.: Reachability analysis for solvable dynamical systems. IEEE Trans. Autom. Control 63(7), 2003–2018 (2018).  https://doi.org/10.1109/TAC.2017.2763785MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 279–294. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54862-8_19CrossRefGoogle Scholar
  18. 18.
    Ghorbal, K., Sogokon, A., Platzer, A.: A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets. Comput. Lang. Syst. Struct. 47, 19–43 (2017).  https://doi.org/10.1016/j.cl.2015.11.003CrossRefzbMATHGoogle Scholar
  19. 19.
    Goriely, A.: Integrability and Nonintegrability of Dynamical Systems. World Scientific, Hackensack (2001).  https://doi.org/10.1142/3846CrossRefzbMATHGoogle Scholar
  20. 20.
    Gulwani, S., Tiwari, A.: Constraint-based approach for analysis of hybrid systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 190–203. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-70545-1_18CrossRefGoogle Scholar
  21. 21.
    Herbrand, J.: Recherches sur la théorie de la démonstration. Ph.D. thesis, Université de Paris, Faculté des Sciences (1930)Google Scholar
  22. 22.
    Immler, F., et al.: ARCH-COMP18 category report: continuous and hybrid systems with nonlinear dynamics. In: Frehse, G., Althoff, M., Bogomolov, S., Johnson, T.T. (eds.) ARCH 2018. EPiC Series in Computing, vol. 54, pp. 53–70. EasyChair (2018)Google Scholar
  23. 23.
    Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., Arechiga, N.: Simulation-guided Lyapunov analysis for hybrid dynamical systems. In: Fränzle, M., Lygeros, J. (eds.) HSCC 2014, pp. 133–142. ACM (2014).  https://doi.org/10.1145/2562059.2562139
  24. 24.
    Kong, H., Bogomolov, S., Schilling, C., Jiang, Y., Henzinger, T.A.: Safety verification of nonlinear hybrid systems based on invariant clusters. In: Frehse, G., Mitra, S. (eds.) HSCC 2017, pp. 163–172. ACM (2017).  https://doi.org/10.1145/3049797.3049814
  25. 25.
    Kong, H., He, F., Song, X., Hung, W.N.N., Gu, M.: Exponential-Condition-based barrier certificate generation for safety verification of hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 242–257. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-39799-8_17CrossRefGoogle Scholar
  26. 26.
    Lafferriere, G., Pappas, G.J., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symb. Comput. 32(3), 231–253 (2001).  https://doi.org/10.1006/jsco.2001.0472MathSciNetCrossRefzbMATHGoogle Scholar
  27. 27.
    Li, W., Passmore, G.O., Paulson, L.C.: Deciding univariate polynomial problems using untrusted certificates in Isabelle/HOL. J. Autom. Reasoning 62(1), 69–91 (2019).  https://doi.org/10.1007/s10817-017-9424-6MathSciNetCrossRefzbMATHGoogle Scholar
  28. 28.
    Liu, J., et al.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1–15. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-17164-2_1CrossRefGoogle Scholar
  29. 29.
    Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT 2011, pp. 97–106. ACM (2011).  https://doi.org/10.1145/2038642.2038659
  30. 30.
    Loeser, T., Iwasaki, Y., Fikes, R.: Safety verification proofs for physical systems. In: Proceedings of the 12th International Workshop on Qualitative Reasoning, pp. 88–95 (1998)Google Scholar
  31. 31.
    Man, Y.: Computing closed form solutions of first order ODEs using the Prelle-Singer procedure. J. Symb. Comput. 16(5), 423–443 (1993).  https://doi.org/10.1006/jsco.1993.1057MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Mishra, B.: Algorithmic Algebra. Springer, Cham (1993).  https://doi.org/10.1007/978-1-4612-4344-1CrossRefzbMATHGoogle Scholar
  33. 33.
    Mitsch, S., Platzer, A.: ModelPlex: verified runtime validation of verified cyber-physical system models. Formal Methods Syst. Des. 49(1–2), 33–74 (2016).  https://doi.org/10.1007/s10703-016-0241-zCrossRefzbMATHGoogle Scholar
  34. 34.
    Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143–189 (2008)MathSciNetCrossRefGoogle Scholar
  35. 35.
    Platzer, A.: The complete proof theory of hybrid systems. In: LICS 2012, pp. 541–550. IEEE (2012).  https://doi.org/10.1109/LICS.2012.64
  36. 36.
    Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. Formal Methods Syst. Des. 35(1), 98–120 (2009).  https://doi.org/10.1007/s10703-009-0079-8CrossRefzbMATHGoogle Scholar
  37. 37.
    Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171–178. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-71070-7_15CrossRefGoogle Scholar
  38. 38.
    Platzer, A., Quesel, J.-D., Rümmer, P.: Real world verification. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 485–501. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02959-2_35CrossRefGoogle Scholar
  39. 39.
    Platzer, A., Tan, Y.K.: Differential equation axiomatization: the impressive power of differential ghosts. In: Dawar, A., Grädel, E. (eds.) LICS 2018, pp. 819–828. ACM (2018).  https://doi.org/10.1145/3209108.3209147
  40. 40.
    Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24743-2_32CrossRefzbMATHGoogle Scholar
  41. 41.
    Prelle, M.J., Singer, M.F.: Elementary first integrals of differential equations. Trans. Am. Math. Soc. 279(1), 215–229 (1983)MathSciNetCrossRefGoogle Scholar
  42. 42.
    Rebiha, R., Moura, A.V., Matringe, N.: Generating invariants for non-linear hybrid systems. Theor. Comput. Sci. 594, 180–200 (2015).  https://doi.org/10.1016/j.tcs.2015.06.018MathSciNetCrossRefzbMATHGoogle Scholar
  43. 43.
    Renegar, J.: Recent progress on the complexity of the decision problem for the reals. In: Goodman, J.E., Pollack, R., Steiger, W. (eds.) Discrete and Computational Geometry: Papers from the DIMACS Special Year, vol. 6, pp. 287–308. DIMACS/AMS (1990)Google Scholar
  44. 44.
    Rodríguez-Carbonell, E., Tiwari, A.: Generating polynomial invariants for hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 590–605. Springer, Heidelberg (2005).  https://doi.org/10.1007/978-3-540-31954-2_38CrossRefzbMATHGoogle Scholar
  45. 45.
    Rouche, N., Habets, P., Laloy, M.: Stability Theory by Liapunov’s Direct Method. Applied Mathematical Sciences. Springer, Heidelberg (1977).  https://doi.org/10.1007/978-1-4684-9362-7CrossRefzbMATHGoogle Scholar
  46. 46.
    Roux, P., Voronin, Y., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants. Formal Methods Syst. Des. 53(2), 286–312 (2018).  https://doi.org/10.1007/s10703-017-0302-yCrossRefzbMATHGoogle Scholar
  47. 47.
    Roy, M.F.: Basic algorithms in real algebraic geometry and their complexity: from Sturm’s theorem to the existential theory of reals. De Gruyter Expositions Math. 23, 1–67 (1996)MathSciNetzbMATHGoogle Scholar
  48. 48.
    Sankaranarayanan, S.: Automatic invariant generation for hybrid systems using ideal fixed points. In: Johansson, K.H., Yi, W. (eds.) HSCC 2010, pp. 221–230. ACM (2010).  https://doi.org/10.1145/1755952.1755984
  49. 49.
    Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. Formal Methods Syst. Des. 32(1), 25–55 (2008).  https://doi.org/10.1007/s10703-007-0046-1CrossRefzbMATHGoogle Scholar
  50. 50.
    Shults, B., Kuipers, B.: Proving properties of continuous systems: qualitative simulation and temporal logic. Artif. Intell. 92(1–2), 91–129 (1997).  https://doi.org/10.1016/S0004-3702(96)00050-1MathSciNetCrossRefzbMATHGoogle Scholar
  51. 51.
    Sogokon, A., Ghorbal, K., Jackson, P.B., Platzer, A.: A method for invariant generation for polynomial continuous systems. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 268–288. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49122-5_13CrossRefGoogle Scholar
  52. 52.
    Sogokon, A., Ghorbal, K., Johnson, T.T.: Non-linear continuous systems for safety verification. In: Frehse, G., Althoff, M. (eds.) ARCH 2016. EPiC Series in Computing, vol. 43, pp. 42–51. EasyChair (2016)Google Scholar
  53. 53.
    Sogokon, A., Ghorbal, K., Tan, Y.K., Platzer, A.: Vector barrier certificates and comparison systems. In: Havelund, K., Peleska, J., Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 418–437. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-95582-7_25CrossRefGoogle Scholar
  54. 54.
    Strogatz, S.H.: Nonlinear Dynamics And Chaos. Studies in Nonlinearity. Westview Press, Boulder (2001)Google Scholar
  55. 55.
    Sturm, T., Tiwari, A.: Verification and synthesis using real quantifier elimination. In: Schost, É., Emiris, I.Z. (eds.) ISSAC 2011, pp. 329–336. ACM (2011).  https://doi.org/10.1145/1993886.1993935
  56. 56.
    Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 514–525. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-36580-X_37CrossRefzbMATHGoogle Scholar
  57. 57.
    Tiwari, A.: Abstractions for hybrid systems. Formal Methods Syst. Des. 32(1), 57–83 (2008).  https://doi.org/10.1007/s10703-007-0044-3CrossRefzbMATHGoogle Scholar
  58. 58.
    Tiwari, A.: Generating box invariants. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 658–661. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78929-1_58CrossRefGoogle Scholar
  59. 59.
    Tiwari, A., Khanna, G.: Series of abstractions for hybrid automata. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 465–478. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45873-5_36CrossRefzbMATHGoogle Scholar
  60. 60.
    Tiwari, A., Khanna, G.: Nonlinear systems: approximating reach sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 600–614. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-24743-2_40CrossRefzbMATHGoogle Scholar
  61. 61.
    Wang, S., Zhan, N., Zou, L.: An improved HHL prover: an interactive theorem prover for hybrid systems. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 382–399. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-25423-4_25CrossRefGoogle Scholar
  62. 62.
    Weber, T.: Integrating a SAT solver with an LCF-style theorem prover. Electron. Notes Theor. Comput. Sci. 144(2), 67–78 (2006).  https://doi.org/10.1016/j.entcs.2005.12.007CrossRefzbMATHGoogle Scholar
  63. 63.
    Weber, T.: SMT solvers: new oracles for the HOL theorem prover. STTT 13(5), 419–429 (2011).  https://doi.org/10.1007/s10009-011-0188-8CrossRefGoogle Scholar
  64. 64.
    Yang, Z., Huang, C., Chen, X., Lin, W., Liu, Z.: A linear programming relaxation based approach for generating barrier certificates of hybrid systems. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 721–738. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-48989-6_44CrossRefGoogle Scholar
  65. 65.
    Zaki, M.H., Denman, W., Tahar, S., Bois, G.: Integrating abstraction techniques for formal verification of analog designs. J. Aeros. Comp. Inf. Com. 6(5), 373–392 (2009).  https://doi.org/10.2514/1.44289CrossRefGoogle Scholar
  66. 66.
    Zhao, F.: Extracting and representing qualitative behaviors of complex systems in phase space. Artif. Intell. 69(1–2), 51–92 (1994).  https://doi.org/10.1016/0004-3702(94)90078-7MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Computer Science DepartmentCarnegie Mellon UniversityPittsburghUSA
  2. 2.School of InformaticsUniversity of EdinburghEdinburghUK
  3. 3.Fakultät für InformatikTechnische Universität MünchenMünchenGermany

Personalised recommendations