Skip to main content
SpringerLink
Log in

Constructing Invariants for Hybrid Systems

  • Conference paper
Hybrid Systems: Computation and Control (HSCC 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2993))

Included in the following conference series:

Abstract

An invariant of a system is a predicate that holds for every reachable state. In this paper, we present techniques to generate invariants for hybrid systems. This is achieved by reducing the invariant generation problem to a constraint solving problem using methods from the theory of ideals over polynomial rings. We extend our previous work on the generation of algebraic invariants for discrete transition systems in order to generate algebraic invariants for hybrid systems. In doing so, we present a new technique to handle consecution across continuous differential equations. The techniques we present allow a trade-off between the complexity of the invariant generation process and the strength of the resulting invariants.

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

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. Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998)

    Google Scholar 

  2. Bensalem, S., Bozga, M., Fernandez, J.-C., Ghirvu, L., Lakhnech, Y.: A transformational approach for generating non-linear invariants. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  3. Bockmayr, A., Weispfenning, V.: Solving numerical constraints. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch. 12, pp. 751–842. Elsevier Science, Amsterdam (2001)

    Chapter  Google Scholar 

  4. Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation 12(3), 299–328 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  5. Colón, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Somenzi, F., Hunt Jr., W. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–433. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  6. Cousot, P., Cousot, R.: Abstract Interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM Principles of Programming Languages, pp. 238–252 (1977)

    Google Scholar 

  7. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: ACM Principles of Programming Languages, pp. 84–97 (January 1978)

    Google Scholar 

  8. Cox, D., Little, J., O’Shea, D.: Ideals, Varieties and Algorithms: An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer, Heidelberg (1991)

    Google Scholar 

  9. Dolzmann, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin 31(2), 2–9 (1997)

    Article  MathSciNet  Google Scholar 

  10. Halbwachs, N., Proy, Y., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Formal Methods in System Design 11(2), 157–185 (1997)

    Article  Google Scholar 

  11. Henzinger, T., Ho, P.-H.: Algorithmic analysis of nonlinear hybrid systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 225–238. Springer, Heidelberg (1995)

    Google Scholar 

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

    Google Scholar 

  13. Karr, M.: Affine relationships among variables of a program. Acta Inf. 6, 133–151 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  14. Lafferriere, G., Pappas, G., Yovine, S.: Symbolic reachability computation for families of linear vector fields. J. Symbolic Computation 32, 231–253 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  15. Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)

    Google Scholar 

  16. Mishra, B., Yap, C.: Notes on Gröbner bases. Information Sciences 48, 219–252 (1989)

    Article  MATH  MathSciNet  Google Scholar 

  17. Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear loop invariant generation using Gröbner bases. In: ACM Principles of Programming Languages, POPL (2004) (to appear)

    Google Scholar 

  18. Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 514–525. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  19. Tiwari, A., Rueß, H., Saïdi, H., Shankar, N.: A technique for invariant generation. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 113–127. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  20. Windsteiger, W., Buchberger, B.: Gröbner: A library for computing Gröbner bases based on saclib. Tech. rep., RISC-Linz (1993)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science Department, Stanford University, Stanford, CA, 94305-9045, USA

    Sriram Sankaranarayanan, Henny B. Sipma & Zohar Manna

Authors
  1. Sriram Sankaranarayanan
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Henny B. Sipma
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zohar Manna
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. University of Pennsylvania,  

    Rajeev Alur

  2. School of Engineering and Applied Science, University of Pennsylvania,  

    George J. Pappas

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sankaranarayanan, S., Sipma, H.B., Manna, Z. (2004). Constructing Invariants for Hybrid Systems. In: Alur, R., Pappas, G.J. (eds) Hybrid Systems: Computation and Control. HSCC 2004. Lecture Notes in Computer Science, vol 2993. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24743-2_36

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24743-2_36

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-21259-1

  • Online ISBN: 978-3-540-24743-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation