Skip to main content
SpringerLink
Log in

Computing Differential Invariants as Fixed Points

  • Chapter
  • First Online:
Book cover Logical Analysis of Hybrid Systems

  • 1383 Accesses

Synopsis

We introduce a fixed-point algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use differential induction as a continuous generalisation of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixed-point algorithm works with differential dynamic logic as a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively by differential cuts with differential invariants until the property becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout manoeuvres in air traffic control and collision avoidance in train control.

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 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 109.99
Price excludes VAT (USA)
  • Durable hardcover 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. Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. Symb. Comput. 12(3), 299–328 (1991). DOI 10.1016/S0747-7171(08)80152-6

    Article  MATH  MathSciNet  Google Scholar 

  2. Rodríguez-Carbonell, E., Tiwari, A.: Generating polynomial invariants for hybrid systems. In: Morari and Thiele [212], pp. 590–605. DOI 10.1007/b106766

    Google Scholar 

  3. Anai, H., Weispfenning, V.: Reach set computations using real quantifier elimination. In: M.D.D. Benedetto, A.L. Sangiovanni-Vincentelli (eds.) HSCC, LNCS, vol. 2034, pp. 63–76. Springer (2001). DOI 10.1007/3-540-45351-2_9

    Google Scholar 

  4. Donzé, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad et al. [41], pp. 174–189. DOI 10.1007/978-3-540-71493-4_16

    Google Scholar 

  5. Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur and Pappas [14], pp. 477–492. DOI 10.1007/b96398

    Google Scholar 

  6. Platzer, A.: Differential dynamic logic for hybrid systems. Journal of Automated Reasoning 41(2), 143–189 (2008). DOI 10.1007/s10817-008-9103-8

    Article  MATH  MathSciNet  Google Scholar 

  7. Massink, M., Francesco, N.D.: Modelling free flight with collision avoidance. In: Andler and Offutt [16], pp. 270–280. DOI 10.1109/ICECCS.2001.930186

    Google Scholar 

  8. Platzer, A.: Differential-algebraic dynamic logic for differential-algebraic programs. Journal of Logic and Computation 20(1), 309–352 (2010). DOI 10.1093/logcom/exn070. Advance Access published on November 18, 2008

    Article  MATH  MathSciNet  Google Scholar 

  9. Damm,W., Pinto, G., Ratschan, S.: Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems. In: Peled and Tsay [226], pp. 99–113. DOI 10.1007/11562948_10

    Google Scholar 

  10. Clarke, E.M.: Program invariants as fixedpoints. Computing 21(4), 273–294 (1979). DOI 10.1007/BF02248730

    Article  MATH  Google Scholar 

  11. Platzer, A.: Differential dynamic logic for verifying parametric hybrid systems. In: N. Olivetti (ed.) TABLEAUX, LNCS, vol. 4548, pp. 216–232. Springer (2007). DOI 10.1007/978-3-540-73099-6_17

    Google Scholar 

  12. Rodríguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial invariants of bounded degree using abstract interpretation. Sci. Comput. Program. 64(1), 54–75 (2007). DOI 10.1016/j.scico.2006.03.003

    Article  MATH  Google Scholar 

  13. Tomlin, C., Pappas, G.J., Sastry, S.: Conflict resolution for air traffic management: a study in multi-agent hybrid systems. IEEE T. Automat. Contr. 43(4), 509–521 (1998). DOI 10.1109/9.664154

    Article  MATH  MathSciNet  Google Scholar 

  14. Platzer, A., Quesel, J.D.: KeYmaera: A hybrid theorem prover for hybrid systems. In: Armando et al. [18], pp. 171–178. DOI 10.1007/978-3-540-71070-7_15

    Google Scholar 

  15. Henzinger, T.A.: The theory of hybrid automata. In: LICS, pp. 278–292. IEEE Computer Society, Los Alamitos (1996)

    Google Scholar 

  16. Hwang, I., Kim, J., Tomlin, C.: Protocol-based conflict resolution for air traffic control. Air Traffic Control Quarterly 15(1), 1–34 (2007)

    Google Scholar 

  17. Piazza, C., Antoniotti, M., Mysore, V., Policriti, A., Winkler, F., Mishra, B.: Algorithmic algebraic model checking I: Challenges from systems biology. In: Etessami and Rajamani [118], pp. 5–19. DOI 10.1007/11513988_3

    Google Scholar 

  18. Mansfield, E.L.: Differential Gröbner bases. Ph.D. thesis, University of Sydney (1991)

    Google Scholar 

  19. Dowek, G., Muñoz, C., Carreño, V.A.: Provably safe coordinated strategy for distributed conflict resolution. In: Proceedings of the AIAA Guidance Navigation, and Control Conference and Exhibit 2005, AIAA-2005-6047 (2005)

    Google Scholar 

  20. Asarin, E., Dang, T., Girard, A.: Reachability analysis of nonlinear systems using conservative approximation. In: Maler and Pnueli [200], pp. 20–35. DOI 10.1007/3-540-36580-X_5

    Google Scholar 

  21. Fränzle, M.: Analysis of hybrid systems: An ounce of realism can save an infinity of states. In: J. Flum, M. Rodr´ıguez-Artalejo (eds.) CSL, LNCS, vol. 1683, pp. 126–140. Springer (1999)

    Google Scholar 

  22. Lanotte, R., Tini, S.: Taylor approximation for hybrid systems. In: Morari and Thiele [212], pp. 402–416. DOI 10.1007/b106766

    Google Scholar 

  23. Rodríguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. J. Symb. Comput. 42(4), 443–476 (2007). DOI 10.1016/j.jsc.2007.01.002

    Article  MATH  Google Scholar 

  24. Parrilo, P.A.: Semidefinite programming relaxations for semialgebraic problems. Math. Program. 96(2), 293–320 (2003). DOI 10.1007/s10107-003-0387-5

    Article  MATH  MathSciNet  Google Scholar 

  25. Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE T. Automat. Contr. 52(8), 1415–1429 (2007). DOI 10.1109/TAC.2007.902736

    Article  MathSciNet  Google Scholar 

  26. Rodríguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: R. Giacobazzi (ed.) SAS, Lecture Notes in Computer Science, vol. 3148, pp. 280–295. Springer (2004). DOI 10.1007/b99688

    Google Scholar 

  27. Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: Bemporad et al. [41], pp. 473–486. DOI 10.1007/978-3-540-71493-4_37

    Google Scholar 

  28. Sankaranarayanan, S., Sipma, H., Manna, Z.: Constructing invariants for hybrid systems. In: Alur and Pappas [14], pp. 539–554. DOI 10.1007/b96398

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computer Science, Carnegie Mellon University, 5000 Forbes Ave., Pittsburgh, PA, 15213, USA

    Dr. André Platzer

Authors
  1. Dr. André Platzer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to André Platzer .

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Platzer, A. (2010). Computing Differential Invariants as Fixed Points. In: Logical Analysis of Hybrid Systems. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14509-4_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14509-4_6

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14508-7

  • Online ISBN: 978-3-642-14509-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation