Abstract
This paper is concerned with proof methods for the temporal property of eventuality (a type of liveness) in systems of polynomial ordinary differential equations (ODEs) evolving under constraints. This problem is of a more general interest to hybrid system verification, where reasoning about temporal properties in the continuous fragment is often a bottleneck. Much of the difficulty in handling continuous systems stems from the fact that closed-form solutions to non-linear ODEs are rarely available. We present a general method for proving eventuality properties that works with the differential equations directly, without the need to compute their solutions. Our method is intuitively simple, yet much less conservative than previously reported approaches, making it highly amenable to use as a rule of inference in a formal proof calculus for hybrid systems.
This material is based upon work supported by the UK Engineering and Physical Sciences Research Council (EPSRC) under grant EP/I010335/1.
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
Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4), 181–185 (1985)
Berz, M., Makino, K.: Verified integration of ODEs and flows using differential algebraic methods on high-order Taylor models. Reliable Computing 4(4), 361–369 (1998)
Bhatia, N.P., Szegő, G.P.: Stability Theory of Dynamical Systems. Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, vol. 161. Springer (1970)
Blanchini, F.: Set invariance in control. Automatica 35(11), 1747–1767 (1999)
Blanchini, F., Miani, S.: Set-Theoretic Methods in Control. Systems & Control: Foundations & Applications. Birkhäuser (2008)
Collins, G.E.: Hauptvortrag: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975)
Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1/2), 29–35 (1988)
Demyanov, V.F.: The solution of minimaximin problems. USSR Computational Mathematics and Mathematical Physics 10(3), 44–55 (1970)
Dolzmann, A., Sturm, T., Weispfenning, V.: Real Quantifier Elimination in Practice. In: Algorithmic Algebra and Number Theory, pp. 221–247 (1998)
Ekici, E.: On the directional differentiability properties of the max-min function. Boletín de la Asociación Matemática Venezolana X(1), 35–42 (2003)
Fehnker, A., Krogh, B.H.: Hybrid system verification is not a sinecure. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 263–277. Springer, Heidelberg (2004)
Ghorbal, K., Platzer, A.: Characterizing algebraic invariants by differential radical invariants. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 279–294. Springer, Heidelberg (2014)
Henzinger, T.A.: The theory of hybrid automata. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pp. 278–292 (1996)
Immler, F.: Formally verified computation of enclosures of solutions of ordinary differential equations. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 113–127. Springer, Heidelberg (2014)
Immler, F.: Verified reachability analysis of continuous systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 37–51. Springer, Heidelberg (2015)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3(2), 125–143 (1977)
Liu, J., Lv, J., Quan, Z., Zhan, N., Zhao, H., Zhou, C., Zou, L.: A calculus for hybrid CSP. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 1–15. Springer, Heidelberg (2010)
Liu, J., Zhan, N., Zhao, H.: Computing semi-algebraic invariants for polynomial dynamical systems. In: Chakraborty, S., Jerraya, A., Baruah, S.K., Fischmeister, S. (eds.) EMSOFT, pp. 97–106. ACM (2011)
Lyapunov, A.M.: The general problem of stability of motion. Kharkov Mathematical Society, Kharkov (1892)
Nagumo, M.: Über die Lage der Integralkurven gewöhnlicher Differentialgleichungen. In: Proceedings of the Physico-Mathematical Society of Japan, vol. 24, pp. 551–559 (May 1942)
Navarro-López, E.M., Carter, R.: Hybrid automata: an insight into the discrete abstraction of discontinuous systems. International Journal of Systems Science 42(11), 1883–1898 (2011)
Neher, M., Jackson, K.R., Nedialkov, N.S.: On Taylor model based integration of ODEs. SIAM Journal on Numerical Analysis 45(1), 236–262 (2007)
Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 4(3), 455–495 (1982)
Parrilo, P.A.: Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. Engineering and applied science, control and dynamical systems, California Institute of Technology (May 2000)
Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143–189 (2008)
Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010)
Platzer, A., Clarke, E.M.: Computing differential invariants of hybrid systems as fixedpoints. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 176–189. Springer, Heidelberg (2008)
Poincaré, H.: Mémoire sur les courbes définies par une équation différentielle. Journal de Mathématiques Pures et Appliquées 7, 3, 4, 375–422, 251–296, 167–224 (1881, 1882, 1885)
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)
Prajna, S., Rantzer, A.: Primal–dual tests for safety and reachability. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 542–556. Springer, Heidelberg (2005)
Ratschan, S., She, Z.: Providing a basin of attraction to a target region of polynomial systems by computation of Lyapunov-like functions. SIAM J. Control Optim. 48(7), 4377–4394 (2010)
Richardson, D.: Some undecidable problems involving elementary functions of a real variable. Journal of Symbolic Logic 33(4), 514–520 (1968)
Stiver, J.A., Koutsoukos, X.D., Antsaklis, P.J.: An invariant-based approach to the design of hybrid control systems. International Journal of Robust and Nonlinear Control 11(5), 453–478 (2001)
Taly, A., Tiwari, A.: Deductive verification of continuous dynamical systems. In: Kannan, R., Kumar, K.N. (eds.) FSTTCS. LIPIcs, vol. 4, pp. 383–394. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2009)
Tarski, A.: A decision method for elementary algebra and geometry. Bulletin of the American Mathematical Society 59 (1951)
Wang, T.C., Lall, S., West, M.: Polynomial level-set method for polynomial system reachable set estimation. IEEE Transactions on Automatic Control 58(10), 2508–2521 (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Sogokon, A., Jackson, P.B. (2015). Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems. In: Bjørner, N., de Boer, F. (eds) FM 2015: Formal Methods. FM 2015. Lecture Notes in Computer Science(), vol 9109. Springer, Cham. https://doi.org/10.1007/978-3-319-19249-9_32
Download citation
DOI: https://doi.org/10.1007/978-3-319-19249-9_32
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-19248-2
Online ISBN: 978-3-319-19249-9
eBook Packages: Computer ScienceComputer Science (R0)