Abstract
Aiming at automatic verification and analysis techniques for hybrid systems, we present a novel combination of enclosure methods for ordinary differential equations (ODEs) with the iSAT solver for large Boolean combinations of arithmetic constraints. Improving on our previous work, the contribution of this paper lies in combining iSAT with VNODE-LP, as a state-of-the-art enclosure method for ODEs, and with bracketing systems which exploit monotonicity properties to find enclosures for problems that VNODE-LP alone cannot enclose tightly. We apply our method to the analysis of a non-linear hybrid system by solving predicative encodings of an inductive stability argument and evaluate the impact of different methods and their combination.
This work has been supported by the German Research Council DFG within SFB/TR 14 “Automatic Verification and Analysis of Complex Systems” ( www.avacs.org ) and by the Natural Sciences and Engineering Research Council of Canada.
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
Preview
Unable to display preview. Download preview PDF.
References
Berz, M.: COSY INFINITY version 8 reference manual. Tech. Rep. MSUCL–1088, National Superconducting Cyclotron Lab., Michigan State University, USA (1997)
Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Commun. ACM 5, 394–397 (1962)
Davis, M., Putnam, H.: A Computing Procedure for Quantification Theory. Journal of the ACM 7(3), 201–215 (1960)
Eggers, A., Fränzle, M., Herde, C.: SAT modulo ODE: A direct SAT approach to hybrid systems. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 171–185. Springer, Heidelberg (2008)
Fränzle, M., Herde, C., Ratschan, S., Schubert, T., Teige, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. JSAT Special Issue on Constraint Programming and SAT 1(3-4), 209–236 (2007)
Goldsztejn, A., Mullier, O., Eveillard, D., Hosobe, H.: Including ordinary differential equations based constraints in the standard CP framework. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 221–235. Springer, Heidelberg (2010)
Henzinger, T., Horowitz, B., Majumdar, R., Wong-Toi, H.: Beyond HYTECH: Hybrid systems analysis using interval numerical methods. In: Lynch, N., Krogh, B. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 130–144. Springer, Heidelberg (2000)
Ishii, D., Ueda, K., Hosobe, H.: An interval-based SAT modulo ODE solver for model checking nonlinear hybrid systems. International Journal on Software Tools for Technology Transfer (STTT), 1–13 (March 2011)
Ishii, D., Ueda, K., Hosobe, H., Goldsztejn, A.: Interval-based solving of hybrid constraint systems. In: Proceedings of the 3rd IFAC Conference on Analysis and Design of Hybrid Systems, pp. 144–149 (2009)
Kieffer, M., Walter, E., Simeonov, I.: Guaranteed nonlinear parameter estimation for continuous-time dynamical models. In: Proceedings 14th IFAC Symposium on System Identification, Newcastle, Aus, pp. 843–848 (2006)
Müller, M.: Über das Fundamentaltheorem in der Theorie der gewöhnlichen Differentialgleichungen. Mathematische Zeitschrift 26, 619–645 (1927)
Nedialkov, N.S.: VNODE-LP — a validated solver for initial value problems in ordinary differential equations. Tech. Rep. CAS-06-06-NN, Department of Computing and Software, McMaster University, Hamilton, Ontario, L8S 4K1 (2006), VNODE-LP http://www.cas.mcmaster.ca/~nedialk/vnodelp
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, Mathematical Engineering, vol. 3, pp. 3–19. Springer, Heidelberg (2011)
Nedialkov, N.S.: Computing Rigorous Bounds on the Solution of an Initial Value Problem for an Ordinary Differential Equation. Ph.D. thesis, Department of Computer Science, University of Toronto, Toronto, Canada, M5S 3G4 (February 1999)
Podelski, A., Wagner, S.: Region stability proofs for hybrid systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 320–335. Springer, Heidelberg (2007)
Ramdani, N., Meslem, N., Candau, Y.: A hybrid bounding method for computing an over-approximation for the reachable space of uncertain nonlinear systems. IEEE Transactions on Automatic Control 54(10), 2352–2364 (2009)
Ramdani, N., Meslem, N., Candau, Y.: Computing reachable sets for uncertain nonlinear monotone systems. Nonlinear Analysis: Hybrid Systems 4(2), 263–278 (2010)
Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Transactions in Embedded Computing Systems 6(1) (2007)
Shtrichman, O.: Tuning SAT checkers for bounded model checking. In: Emerson, E., Sistla, A. (eds.) CAV 2000. LNCS, vol. 1855, pp. 480–494. Springer, Heidelberg (2000)
Stursberg, O., Kowalewski, S., Hoffmann, I., Preußig, J.: Comparing timed and hybrid automata as approximations of continuous systems. In: Antsaklis, P., Kohn, W., Nerode, A., Sastry, S. (eds.) HS 1996. LNCS, vol. 1273, pp. 361–377. Springer, Heidelberg (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Eggers, A., Ramdani, N., Nedialkov, N., Fränzle, M. (2011). Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods. In: Barthe, G., Pardo, A., Schneider, G. (eds) Software Engineering and Formal Methods. SEFM 2011. Lecture Notes in Computer Science, vol 7041. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24690-6_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-24690-6_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24689-0
Online ISBN: 978-3-642-24690-6
eBook Packages: Computer ScienceComputer Science (R0)