Advertisement

SAT Modulo Differential Equation Simulations

  • Tomáš Kolárik
  • Stefan RatschanEmail author
Conference paper
  • 36 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12165)

Abstract

Differential equations are of immense importance for modeling physical phenomena, often in combination with discrete modeling formalisms. In current industrial practice, properties of the resulting models are checked by testing, using simulation tools. Research on SAT solvers that are able to handle differential equations has aimed at replacing tests by correctness proofs. However, there are fundamental limitations to such approaches in the form of undecidability, and moreover, the resulting solvers do not scale to problems of the size commonly handled by simulation tools. Also, in many applications, classical mathematical semantics of differential equations often does not correspond well to the actual intended semantics, and hence a correctness proof wrt. mathematical semantics does not ensure correctness of the intended system.

In this paper, we head at overcoming those limitations by an alternative approach to handling differential equations within SAT solvers. This approach is usually based on the semantics used by tests in simulation tools, but still may result in mathematically precise correctness proofs wrt. that semantics. Experiments with a prototype implementation confirm the promise of such an approach.

Notes

Acknowledgements

This work was funded by institutional support of the Institute of Computer Science (RVO:67985807) and by CTU project SGS20/211/OHK3/3T/18.

References

  1. 1.
    Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)
  2. 2.
    Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512–526. Springer, Heidelberg (2006).  https://doi.org/10.1007/11916277_35CrossRefGoogle Scholar
  3. 3.
    Barrett, C., Tinelli, C.: Satisfiability modulo theories. Handbook of Model Checking, pp. 305–343. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-10575-8_11CrossRefGoogle Scholar
  4. 4.
    Bouissou, O., Mimram, S., Chapoutot, A.: Hyson: set-based simulation of hybrid systems. In: 23rd IEEE International Symposium on Rapid System Prototyping (RSP), pp. 79–85. IEEE (2012)Google Scholar
  5. 5.
    Bournez, O., Campagnolo, M.L.: A survey on continuous time computations. In: Cooper, S., Löwe, B., Sorbi, A. (eds.) New Computational Paradigms, pp. 383–423. Springer, New York (2008)CrossRefGoogle Scholar
  6. 6.
    Brain, M., Tinelli, C., Rümmer, P., Wahl, T.: An automatable formal semantics for IEEE-754 floating-point arithmetic. In: 22nd IEEE Symposium on Computer Arithmetic, pp. 160–167. IEEE (2015)Google Scholar
  7. 7.
    Chen, S., O’Kelly, M., Weimer, J., Sokolsky, O., Lee, I.: An intraoperative glucose control benchmark for formal verification. In: Analysis and Design of Hybrid Systems ADHS, vol. 48 of IFAC-PapersOnLine, pp. 211–217. Elsevier (2015)Google Scholar
  8. 8.
    de Moura, L., Jovanović, D.: A model-constructing satisfiability calculus. In: 14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI, Rome, Italy (2013)Google Scholar
  9. 9.
    Edelkamp, S., Schroedl, S.: Heuristic Search: Theory and Applications. Morgan Kaufmann, Burlington (2012)Google Scholar
  10. 10.
    Eggers, A., Fränzle, M., Herde, C.: SAT modulo ODE: a direct SAT approach to hybrid systems. In: Automated Technology for Verification and Analysis, vol. 5311, LNCS (2008)Google Scholar
  11. 11.
    Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo ODEs. In: 2013 Formal Methods in Computer-Aided Design, pp. 105–112. IEEE (2013)Google Scholar
  12. 12.
    Hairer, E., Nørsett, S.P., Wanner, G.: Solving Ordinary Differential Equations I. Springer, Heidelberg (1987).  https://doi.org/10.1007/978-3-540-78862-1CrossRefzbMATHGoogle Scholar
  13. 13.
    Kolárik, T.: UN/SOT v0.7 experiments report. https://gitlab.com/Tomaqa/unsot/blob/master/doc/experiments/v0.7/report.pdf (2020)
  14. 14.
    Melquiond, G.: Floating-point arithmetic in the Coq system. Inf. Comput. 216, 14–23 (2012)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to interval analysis. In: SIAM (2009)Google Scholar
  16. 16.
    Mosterman, P.J., Zander, J., Hamon, G., Denckla, B.: A computational model of time for stiff hybrid systems applied to control synthesis. Control Eng. Pract. 20(1), 2–13 (2012)CrossRefGoogle Scholar
  17. 17.
    Nedialkov, N.S.: Implementing a rigorous ODE solver through literate programming. In: Rauh, A., Auer, E. (eds.) Modeling Design and Simulation of Systems with Uncertainties, pp. 3–19. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-15956-5_1CrossRefGoogle Scholar
  18. 18.
    Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM (JACM) 53(6), 937–977 (2006)MathSciNetCrossRefGoogle Scholar
  19. 19.
    Wilczak, D., Zgliczyński, P.: \(\cal{C}^r\)-Lohner algorithm. Schedae Informaticae 20, 9–46 (2011)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  1. 1.Faculty of Information TechnologyCzech Technical University in PraguePragueCzech Republic
  2. 2.Institute of Computer Science of the Czech Academy of SciencesPragueCzech Republic

Personalised recommendations