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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
While this is new in the context of SAT modulo ODE, this is quite common in mathematics. For example, Zermelo-Fraenkel set theory uses such an approach to define sets, relations, etc. within first-order predicate logic.
- 2.
- 3.
- 4.
- 5.
- 6.
References
Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)
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_35
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_11
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)
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)
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)
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)
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)
Edelkamp, S., Schroedl, S.: Heuristic Search: Theory and Applications. Morgan Kaufmann, Burlington (2012)
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)
Gao, S., Kong, S., Clarke, E.M.: Satisfiability modulo ODEs. In: 2013 Formal Methods in Computer-Aided Design, pp. 105–112. IEEE (2013)
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-1
Kolárik, T.: UN/SOT v0.7 experiments report. https://gitlab.com/Tomaqa/unsot/blob/master/doc/experiments/v0.7/report.pdf (2020)
Melquiond, G.: Floating-point arithmetic in the Coq system. Inf. Comput. 216, 14–23 (2012)
Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to interval analysis. In: SIAM (2009)
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)
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_1
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)
Wilczak, D., Zgliczyński, P.: \(\cal{C}^r\)-Lohner algorithm. Schedae Informaticae 20, 9–46 (2011)
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.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Kolárik, T., Ratschan, S. (2020). SAT Modulo Differential Equation Simulations. In: Ahrendt, W., Wehrheim, H. (eds) Tests and Proofs. TAP 2020. Lecture Notes in Computer Science(), vol 12165. Springer, Cham. https://doi.org/10.1007/978-3-030-50995-8_5
Download citation
DOI: https://doi.org/10.1007/978-3-030-50995-8_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-50994-1
Online ISBN: 978-3-030-50995-8
eBook Packages: Computer ScienceComputer Science (R0)