Skip to main content
SpringerLink
Log in

Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems

  • Conference paper
FM 2015: Formal Methods (FM 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9109))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alpern, B., Schneider, F.B.: Defining liveness. Information Processing Letters 21(4), 181–185 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  2. 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)

    Article  MATH  MathSciNet  Google Scholar 

  3. 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)

    Google Scholar 

  4. Blanchini, F.: Set invariance in control. Automatica 35(11), 1747–1767 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  5. Blanchini, F., Miani, S.: Set-Theoretic Methods in Control. Systems & Control: Foundations & Applications. Birkhäuser (2008)

    Google Scholar 

  6. 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)

    Google Scholar 

  7. Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5(1/2), 29–35 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  8. Demyanov, V.F.: The solution of minimaximin problems. USSR Computational Mathematics and Mathematical Physics 10(3), 44–55 (1970)

    Article  MathSciNet  Google Scholar 

  9. Dolzmann, A., Sturm, T., Weispfenning, V.: Real Quantifier Elimination in Practice. In: Algorithmic Algebra and Number Theory, pp. 221–247 (1998)

    Google Scholar 

  10. 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)

    Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. 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)

    Google Scholar 

  13. Henzinger, T.A.: The theory of hybrid automata. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, pp. 278–292 (1996)

    Google Scholar 

  14. 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)

    Chapter  Google Scholar 

  15. 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)

    Chapter  Google Scholar 

  16. Lamport, L.: Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering 3(2), 125–143 (1977)

    Article  MATH  MathSciNet  Google Scholar 

  17. 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)

    Chapter  Google Scholar 

  18. 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)

    Google Scholar 

  19. Lyapunov, A.M.: The general problem of stability of motion. Kharkov Mathematical Society, Kharkov (1892)

    Google Scholar 

  20. 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)

    Google Scholar 

  21. 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)

    Article  MATH  MathSciNet  Google Scholar 

  22. 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)

    Article  MATH  MathSciNet  Google Scholar 

  23. Owicki, S., Lamport, L.: Proving liveness properties of concurrent programs. ACM Transactions on Programming Languages and Systems (TOPLAS) 4(3), 455–495 (1982)

    Article  MATH  Google Scholar 

  24. 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)

    Google Scholar 

  25. Platzer, A.: Differential dynamic logic for hybrid systems. J. Autom. Reasoning 41(2), 143–189 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  26. Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. J. Log. Comput. 20(1), 309–352 (2010)

    Article  MATH  MathSciNet  Google Scholar 

  27. 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)

    Chapter  Google Scholar 

  28. 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)

    Google Scholar 

  29. 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)

    Chapter  Google Scholar 

  30. 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)

    Chapter  Google Scholar 

  31. 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)

    Article  MATH  MathSciNet  Google Scholar 

  32. Richardson, D.: Some undecidable problems involving elementary functions of a real variable. Journal of Symbolic Logic 33(4), 514–520 (1968)

    Article  MATH  MathSciNet  Google Scholar 

  33. 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)

    Article  MATH  MathSciNet  Google Scholar 

  34. 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)

    Google Scholar 

  35. Tarski, A.: A decision method for elementary algebra and geometry. Bulletin of the American Mathematical Society 59 (1951)

    Google Scholar 

  36. 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)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LFCS, School of Informatics, University of Edinburgh, Edinburgh, UK

    Andrew Sogokon & Paul B. Jackson

Authors
  1. Andrew Sogokon
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paul B. Jackson
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrew Sogokon .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Nikolaj Bjørner

  2. Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands

    Frank de Boer

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics

Search

Navigation