Numerical invariants through convex relaxation and max-strategy iteration |
| |
Authors: | Email author" target="_blank">Thomas?Martin?GawlitzaEmail author Helmut?Seidl |
| |
Affiliation: | 1.Carl von Ossietzky Universit?t Oldenburg,Oldenburg,Germany;2.The University of Sydney,Sydney,Australia;3.Technische Universit?t München,Munich,Germany |
| |
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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|