Numerical invariants through convex relaxation and max-strategy iteration

We present an algorithm for computing the uniquely determined least fixpoints of self-maps on R̄ⁿ (with ̄ R∪±∞ ) 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.