Skip to main content
SpringerLink
Log in

Numerical invariants through convex relaxation and max-strategy iteration

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

We present an algorithm for computing the uniquely determined least fixpoints of self-maps on \(\overline{\mathbb{R}}^{n}\) (with \(\overline{\mathbb{R}} = \mathbb{R} \cup\{ \pm\infty\}\)) that are point-wise maximums of finitely many monotone and order-concave self-maps. This natural problem occurs in the context of systems analysis and verification. As an example application we discuss how our method can be used to compute template-based quadratic invariants for linear systems with guards. The focus of this article, however, lies on the discussion of the underlying theory and the properties of the algorithm itself.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Algorithm 1

Similar content being viewed by others

Notes

  1. Note that, since \(\mathbb{R}^{n}\) is not a complete lattice, the greatest pre-fixpoint of f is not necessarily the greatest fixpoint of f. The greatest fixpoint of the monotone operators f 1,f 2 defined by \(f_{1}(x) = \frac{1}{2}x\) and f 2(x)=2x for all \(x \in\mathbb{R}\), for instance, is 0. This is also the greatest pre-fixpoint of f 1, but not the greatest pre-fixpoint of f 2, since f 2 has no greatest pre-fixpoint.

  2. The order-convexity of f can be shown as follows. Let \(x = (x_{1},x_{2})^{\top}, y=(y_{1},y_{2})^{\top}\in\mathbb{R}^{2}\) with x≤y, d=y−x, and λ∈[0,1]. We have d≥0. We get f((1−λ)x+λy)=f(x+λd)=(x 1+λd 1)(x 2+λd 2)=x 1 x 2+λx 1 d 2+λx 2 d 1+λ 2 d 1 d 2≤(1−λ)x 1 x 2+λx 1 x 2+λx 1 d 2+λx 2 d 1+λd 1 d 2=(1−λ)x 1 x 2+λ(x 1+d 1)(x 2+d 2)=(1−λ)f(x)+λf(x+d)=(1−λ)f(x)+λf(y).

  3. Recall that, by definition of \(\operatorname{\mathsf{fdom}}\), we have \(\operatorname{\mathsf{fdom}}(f^{(I)}) \subseteq\mathbb{R}^{n}\) and \(\operatorname{\mathsf{codom}}( f^{(I)}|_{\operatorname{\mathsf {fdom}}(f^{(I)})} ) \subseteq\mathbb{R}\). Hence, \(f^{(I)}|_{\operatorname{\mathsf{fdom}}(f^{(I)})}\) is a function from \(\operatorname{\mathsf{fdom}}(f^{(I)}) \subseteq\mathbb{R}^{n}\) into \(\mathbb{R}\). Thus, the previously defined notion of (order-)concavity applies.

  4. The assumption that we can solve all occurring convex optimization problems precisely is not realistic in practice. In practice one has to take numerical issues into account. However, this is beyond the scope of this article.

  5. Strictly speaking, this is not correct, since it might be the case that there does not exist an optimal solution—even though the optimization problem is bounded. However, the statement is at least correct in the limit. We can state it as follows: in our case, in the limit, there always exists a uniquely determined optimal solution. That is, all sequences \((\hat{\rho}_{k})_{k\in\mathbb{N}}\) with \(\hat{\rho}_{k} : \mathbf{X} '_{\rho}\to \mathbb{R}\) and \(\hat{\rho}_{k} \leq[\![{\mathcal{E}}' ]\!] \hat{\rho}_{k}\) for all \(k \in\mathbb{N}\), whose sequences of sums \((\sum_{\mathbf{x}\in\mathbf{X}'} \hat{\rho}_{k}(\mathbf{x}))_{k\in\mathbb{N}}\) converge towards the optimal value of the optimization problem, converge themselves to the same uniquely determined value.

  6. A monotone function \(g : {\overline{\mathbb{R}}}^{n}\to{\overline{\mathbb{R}}}\) is upward-chain-continuous on an upward-closed set \(X \subseteq{\overline {\mathbb{R}}}^{n}\) if and only if g(⋁C)=⋁g(C) for all non-empty chains C⊆X.

  7. A monotone function \(Y : {\overline{\mathbb{R}}}^{n} \to2^{\mathbb{R}^{k}}\) is upward-chain-continuous on an upward-closed set \(X \subseteq{\overline {\mathbb{R}}}^{n}\) if and only if Y(⋁C)=⋃Y(C) for all non-empty chains C⊆X.

References

  1. Adjé A, Gaubert S, Goubault E (2010) Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis. In: Gordon AD (ed) ESOP. Lecture notes in computer science, vol 6012. Springer, Berlin, pp 23–42. ISBN 978-3-642-11956-9

    Chapter  Google Scholar 

  2. Alegre F, Feron E, Pande S (2009) Using ellipsoidal domains to analyze control systems software. arXiv:0909.1977

  3. Caspi P, Pilaud D, Halbwachs N, Plaice J (1987) Lustre: a declarative language for programming synchronous systems. In: POPL. ACM, New York, pp 178–188. ISBN 0-89791-215-2

    Chapter  Google Scholar 

  4. Costan A, Gaubert S, Goubault E, Martel M, Putot S (2005) A policy iteration algorithm for computing fixed points in static analysis of programs. In: Computer aided verification, 17th int conf (CAV). Lecture notes in computer science, vol 3576. Springer, Berlin, pp 462–475

    Chapter  Google Scholar 

  5. Cousot P, Cousot R (1976) Static determination of dynamic properties of programs. In: Second int symp on programming. Dunod, Paris, pp 106–130

    Google Scholar 

  6. Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp 238–252

    Google Scholar 

  7. Dang T, Gawlitza TM (2011) Template-based unbounded time verification of affine hybrid automata. In: Yang H (ed) APLAS. Lecture notes in computer science, vol 7078. Springer, Berlin, pp 34–49. ISBN 978-3-642-25317-1

    Chapter  Google Scholar 

  8. Dang T, Gawlitza TM (2011) Discretizing affine hybrid automata with uncertainty. In: Bultan T, Hsiung P-A (eds) ATVA. Lecture notes in computer science, vol 6996. Springer, Berlin, pp 473–481. ISBN 978-3-642-24371-4

    Chapter  Google Scholar 

  9. Fearnley J (2010) Exponential lower bounds for policy iteration. In: Abramsky S, Gavoille C, Kirchner C, Meyer auf der Heide F, Spirakis PG (eds) ICALP (2). Lecture notes in computer science, vol 6199. Springer, Berlin, pp 551–562. ISBN 978-3-642-14161-4

    Chapter  Google Scholar 

  10. Gawlitza T, Seidl H (2007) Precise relational invariants through strategy iteration. In: Duparc J, Henzinger TA (eds) CSL. Lecture notes in computer science, vol 4646. Springer, Berlin, pp 23–40. ISBN 978-3-540-74914-1

    Chapter  Google Scholar 

  11. Gawlitza T, Seidl H (2007) Precise fixpoint computation through strategy iteration. In: Nicola RD (ed) ESOP. Lecture notes in computer science, vol 4421. Springer, Berlin, pp 300–315. ISBN 978-3-540-71314-2

    Chapter  Google Scholar 

  12. Gawlitza T, Seidl H (2008) Precise interval analysis vs. parity games. In: Cuéllar J, Maibaum TSE, Sere K (eds) FM. Lecture notes in computer science, vol 5014. Springer, Berlin, pp 342–357. ISBN 978-3-540-68235-6

    Chapter  Google Scholar 

  13. Gawlitza TM, Seidl H (2010) Computing relaxed abstract semantics w.r.t. quadratic zones precisely. In: Cousot R, Martel M (eds) SAS. Lecture notes in computer science, vol 6337. Springer, Berlin, pp 271–286. ISBN 978-3-642-15768-4

    Chapter  Google Scholar 

  14. Gawlitza TM, Seidl H (2011) Solving systems of rational equations through strategy iteration. ACM Trans Program Lang Syst 33(3):11

    Article  Google Scholar 

  15. Gawlitza TM, Seidl H, Adjé A, Gaubert S, Goubault É (2011) Abstract interpretation meets convex optimization. In: WING-JSC

    Google Scholar 

  16. Girard A (2005) Reachability of uncertain linear systems using zonotopes. In: Morari M, Thiele L (eds) HSCC. Lecture notes in computer science, vol 3414. Springer, Berlin, pp 291–305. ISBN 3-540-25108-1

    Google Scholar 

  17. Halbwachs N (2005) A synchronous language at work: the story of lustre. In: MEMOCODE. IEEE Press, New York, pp 3–11

    Google Scholar 

  18. Halbwachs N, Lagnier F, Ratel C (1992) Programming and verifying real-time systems by means of the synchronous data-flow language lustre. IEEE Trans Softw Eng 18(9):785–793

    Article  Google Scholar 

  19. Larsen KG, Larsson F, Pettersson P, Yi W (1997) Efficient verification of real-time systems: compact data structure and state-space reduction. In: IEEE real-time systems symposium. IEEE Comput Soc, Los Alamitos, pp 14–24

    Google Scholar 

  20. Massé D (2012) Proving termination by policy iteration. Electron Notes Theor Comput Sci 287:77–88. doi:10.1016/j.entcs.2012.09.008

    Article  Google Scholar 

  21. Miné A (2001) A new numerical abstract domain based on difference-bound matrices. In: Danvy O, Filinski A (eds) PADO. Lecture notes in computer science, vol 2053. Springer, Berlin, pp 155–172. ISBN 3-540-42068-1

    Google Scholar 

  22. Miné A (2001) The octagon abstract domain. In: WCRE, p 310

    Google Scholar 

  23. Nemirovski A (2005) Modern convex optimization. Department ISYE, Georgia Institute of Technology

  24. Roux P, Garoche P-L (2012) Policy iterations as traditional abstract domains

  25. Roux P, Jobredeaux R, Garoche P-L, Feron E (2012) A generic ellipsoid abstract domain for linear time invariant systems. In: Dang T, Mitchell IM (eds) HSCC. ACM, New York, pp 105–114. ISBN 978-1-4503-1220-2

    Chapter  Google Scholar 

  26. Sankaranarayanan S, Sipma HB, Manna Z (2005) Scalable analysis of linear systems using mathematical programming. In: Cousot R (ed) VMCAI. Lecture notes in computer science, vol 3385. Springer, Berlin, pp 25–41. ISBN 3-540-24297-X

    Google Scholar 

  27. Sankaranarayanan S, Dang T, Ivancic F (2008) A policy iteration technique for time elapse over template polyhedra. In: Egerstedt M, Mishra B (eds) HSCC. Lecture notes in computer science, vol 4981. Springer, Berlin, pp 654–657. ISBN 978-3-540-78928-4

    Chapter  Google Scholar 

  28. Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5:285–309

    Article  MATH  MathSciNet  Google Scholar 

  29. Todd MJ (2001) Semidefinite optimization. Acta Numer 10:515–560

    Article  MATH  MathSciNet  Google Scholar 

  30. Yovine S (1996) Model checking timed automata. In: Rozenberg G, Vaandrager FW (eds) European educational forum: school on embedded systems. Lecture notes in computer science, vol 1494. Springer, Berlin, pp 114–152. ISBN 3-540-65193-4

    Google Scholar 

Download references

Acknowledgements

The authors would like to thank the anonymous reviewers for their valuable comments and suggestions.

Author information

Authors and Affiliations

  1. Carl von Ossietzky Universität Oldenburg, Oldenburg, Germany

    Thomas Martin Gawlitza

  2. The University of Sydney, Sydney, Australia

    Thomas Martin Gawlitza

  3. Technische Universität München, Munich, Germany

    Helmut Seidl

Authors
  1. Thomas Martin Gawlitza
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Helmut Seidl
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Thomas Martin Gawlitza.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Gawlitza, T.M., Seidl, H. Numerical invariants through convex relaxation and max-strategy iteration. Form Methods Syst Des 44, 101–148 (2014). https://doi.org/10.1007/s10703-013-0190-8

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-013-0190-8

Keywords

Search

Navigation