Abstract
MetiTarski, an automatic proof procedure for inequalities on elementary functions, can be used to verify control and hybrid systems. We perform a stability analysis of control systems using Nichols plots, presenting an inverted pendulum and a magnetic disk drive reader system. Given a hybrid systems specified by a system of differential equations, we use Maple to obtain a problem involving the exponential and trigonometric functions, which MetiTarski can prove automatically.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Akbarpour, B., Paulson, L.: Towards Automatic Proofs of Inequalities Involving Elementary Functions. In: Pragmatics of Decision Procedures in Automated Reasoning (PDPAR), pp. 27–37 (2006)
Akbarpour, B., Paulson, L.: Extending a Resolution Prover for Inequalities on Elementary Functions. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS, vol. 4790, pp. 47–61. Springer, Heidelberg (2007)
Akbarpour, B., Paulson, L.: Metitarski: An Automatic Prover for the Elementary Functions. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC 2008, Calculemus 2008, and MKM 2008. LNCS, vol. 5144, pp. 217–231. Springer, Heidelberg (2008)
Alur, R., Courcoubetis, C., Halbwaches, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olibero, A., Sifakis, J., Yovine, S.: The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science 138, 3–34 (1995)
Asarin, E., Dang, T., Maler, O.: The d/dt Tool for Verification of Hybrid Systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002)
Chutianan, A., Krogh, B.H.: Computational Techniques for Hybrid System Verification. IEEE Transactions on Automatic Control 48(1), 64–75 (2003)
Dorf, R.C., Bishop, R.H.: Modern Control Systems. Prentice-Hall, Englewood Cliffs (2001)
Duarte, L., Duarte, S., da Mota, L., Skea, J.: An Extension of the Prelle-Singer Method and a Maple Implementation. Computer Physics Communications 144(1), 46–62 (2002)
Frehse, G.: PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)
Hardy, R.: Formal Methods for Control Engineering: A Validated Decision Procedure for Nichols Plot Analysis. PhD thesis, St. Andrews University (2006)
Henzinger, T.A., Ho, P.H., Wong-Ti, H.: HyTech: A Model Checker for Hybrid Systems. Software Tools for Technology Transfer 1(1-2), 110–122 (1997)
Prelle, M.S.M.: Elementary First Integrals of Differential Equations. Transactions of the American Mathematical Society 279(1), 215–229 (1983)
Man, Y.: Computing closed form solutions of first order odes using the prelle-singer procedure. J. Symb. Comput. 16(5), 423–443 (1993)
Ratschan, S., She, Z.: Safety Verification of Hybrid Systems by Constraint Propagation-Based Abstraction Refinement. ACM Transactions on Embedded Computing Systems 6(1) (2007)
Ratschan, S., She, Z.: Benchmarks for Safety Verification of Hybrid Systems, June 13 (2008), http://hsolver.sourceforge.net/benchmarks
Tiwari, A.: Approximate Reachability for Linear Systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 514–525. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Akbarpour, B., Paulson, L.C. (2009). Applications of MetiTarski in the Verification of Control and Hybrid Systems. In: Majumdar, R., Tabuada, P. (eds) Hybrid Systems: Computation and Control. HSCC 2009. Lecture Notes in Computer Science, vol 5469. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-00602-9_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-00602-9_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00601-2
Online ISBN: 978-3-642-00602-9
eBook Packages: Computer ScienceComputer Science (R0)