Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Numerical Software Verification

NSV 2016: Numerical Software Verification pp 15–30Cite as

Proving Properties on PWA Systems Using Copositive and Semidefinite Programming

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10152))

Abstract

In this paper, we present a model based on copositive programming and semidefinite relaxations of it to prove properties on discrete-time piecewise affine systems. We consider invariant i.e. properties represented by a set and formulated as all reachable values are included in the set. Also, we restrict the analysis to sublevel sets of quadratic forms i.e. ellipsoids. In this case, to check the property is equivalent to solve a quadratic maximization problem under the constraint that the decision variable belongs to the reachable values set. This maximization problem is relaxed using an abstraction of reachable values set by a union of truncated ellipsoids.

The author has been supported by the CIMI (Centre International de Mathématiques et d’Informatique) Excellence program ANR-11-LABX-0040-CIMI within the program ANR-11-IDEX-0002-02 during a postdoctoral fellowship.

This is a preview of subscription content, 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 EPUB and 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

Learn about institutional subscriptions

References

  1. Adjé, A., Garoche, P.-L.: Automatic synthesis of piecewise linear quadratic invariants for programs. In: D’Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 99–116. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46081-8_6

    Google Scholar 

  2. Adjé, A., Garoche, P.-L., Magron, V.: Property-based polynomial invariant generation using sums-of-squares optimization. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 235–251. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48288-9_14

    Chapter  Google Scholar 

  3. Allamigeon, X.: Static analysis of memory manipulations by abstract interpretation – Algorithmics of tropical polyhedra, and application to abstract interpretation. Ph.D. thesis, École Polytechnique, Palaiseau, France, November 2009

    Google Scholar 

  4. Allamigeon, X., Gaubert, S., Goubault, E., Putot, S., Stott, N.: A scalable algebraic method to infer quadratic invariants of switched systems. In: 2015 International Conference on Embedded Software, EMSOFT 2015, Amsterdam, Netherlands, October 4–9, 2015, pp. 75–84 (2015)

    Google Scholar 

  5. Bomze, I.M., Schachinger, W., Uchida, G.: Think co(mpletely)positive ! matrix properties, examples and a clustered bibliography on copositive optimization. J. Glob. Optim. 52(3), 423–445 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  6. Bundfuss, S., Dür, M.: An adaptive linear approximation algorithm for copositive programs. SIAM J. Optim. 20(1), 30–53 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  7. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 238–252. Los Angeles, California, NY (1977)

    Google Scholar 

  8. Diananda, P.H.: On non-negative forms in real variables some or all of which are non-negative. Math. Proc. Camb. Philos. Soc. 58(1), 17–25 (1962)

    Article  MathSciNet  MATH  Google Scholar 

  9. Johansson, M.: On modeling, analysis and design of piecewise linear control systems. In: Proceedings of the 2003 International Symposium on Circuits and Systems, 2003. ISCAS 2003, vol. 3, pp. III-646–III-649 (2003)

    Google Scholar 

  10. Martin, D.H., Jacobson, D.H.: Copositive matrices and definiteness of quadratic forms subject to homogeneous linear inequality constraints. Linear Algebra Appl. 35, 227–258 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  11. Maxfield, J.E., Minc, H.: On the matrix equation X’X = A. Proc. Edinb. Math. Soc. (Series 2) 13(12), 125–129 (1962)

    Article  MATH  Google Scholar 

  12. Mignone, D., Ferrari-Trecate, G., Morari, M.: Stability and stabilization of piecewise affine and hybrid systems: an lmi approach. In: Proceedings of the 39th IEEE Conference on Decision and Control, vol. 1, pp. 504–509 (2000)

    Google Scholar 

  13. Motzkin, T.S.: Two consequences of the transposition theorem on linear inequalities. Econometrica 19(2), 184–185 (1951)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut de Recherche en Informatique de Toulouse, Université Paul Sabatier, Toulouse, France

    Assalé Adjé

Authors
  1. Assalé Adjé
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Assalé Adjé .

Editor information

Editors and Affiliations

  1. IST Austria, Klosterneuburg, Austria

    Sergiy Bogomolov

  2. Université de Perpignan, Perpignan, France

    Matthieu Martel

  3. Kansas State University, Manhattan, Kansas, USA

    Pavithra Prabhakar

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Adjé, A. (2017). Proving Properties on PWA Systems Using Copositive and Semidefinite Programming. In: Bogomolov, S., Martel, M., Prabhakar, P. (eds) Numerical Software Verification. NSV 2016. Lecture Notes in Computer Science(), vol 10152. Springer, Cham. https://doi.org/10.1007/978-3-319-54292-8_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-54292-8_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-54291-1

  • Online ISBN: 978-3-319-54292-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation