Abstract
We explore uses of a link we have constructed between the KeYmaera hybrid systems theorem prover and the MetiTarski proof engine for problems involving special functions such as sin, cos, exp, etc. Transcendental functions arise in the specification of hybrid systems and often occur in the solutions of the differential equations that govern how the states of hybrid systems evolve over time. To date, formulas exchanged between KeYmaera and external tools have involved polynomials over the reals, but not transcendental functions, chiefly because of the lack of tools capable of proving such goals.
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.
Similar content being viewed by others
References
Ahmadi, A.A., Krstic, M., Parrilo, P.A.: A globally asymptotically stable polynomial vector field with no polynomial Lyapunov function. In: CDC-ECE, pp. 7579–7580 (2011)
Brown, C.W.: Qepcad b: a program for computing with semi-algebraic sets using cads. SIGSAM Bull. 37(4), 97–108 (2003), http://doi.acm.org/10.1145/968708.968710
Chesi, G.: Estimating the domain of attraction for non-polynomial systems via LMI optimizations. Automatica 45(6), 1536–1541 (2009)
Denman, W., Akbarpour, B., Tahar, S., Zaki, M., Paulson, L.: Formal verification of analog designs using metitarski. In: Formal Methods in Computer-Aided Design, FMCAD 2009, pp. 93–100 (2009)
Fränzle, M., Herde, C.: Hysat: An efficient proof engine for bounded model checking of hybrid systems. Formal Methods in System Design 30(3), 179–198 (2007)
Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: Spaceex: Scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)
Heemels, W., Lehmann, D., Lunze, J., De Schutter, B.: Introduction to hybrid systems. In: Lunze, J., Lamnabhi-Lagarrigue, F. (eds.) Handbook of Hybrid Systems Control – Theory, Tools, Applications, ch. 1, pp. 3–30. Cambridge University Press, Cambridge (2009)
Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Hytech: A model checker for hybrid systems. STTT 1(1-2), 110–122 (1997)
de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Paulson, L.C.: MetiTarski: Past and Future. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 1–10. Springer, Heidelberg (2012)
Paulson, L.C.: University of Cambridge (2013), http://www.cl.cam.ac.uk/~lp15/papers/Arith/
Platzer, A.: Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics. Springer, Heidelberg (2010)
Platzer, A.: Carnegie Mellon Uniersity (2013), http://symbolaris.com/info/KeYmaera.html
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)
Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embedded Comput. Syst. 6(1) (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Jackson, P., Sogokon, A., Bridge, J., Paulson, L. (2014). Verifying Hybrid Systems Involving Transcendental Functions. In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-06200-6_14
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06199-3
Online ISBN: 978-3-319-06200-6
eBook Packages: Computer ScienceComputer Science (R0)