Abstract | ||
---|---|---|
We present an algorithm for computing the uniquely determined least fixpoints of self-maps on (with ) 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. |
Year | DOI | Venue |
---|---|---|
2014 | 10.1007/s10703-013-0190-8 | Formal Methods in System Design |
Keywords | DocType | Volume |
Fixpoint algorithms,Systems verification,Convex optimization | Journal | abs/1204.1147 |
Issue | ISSN | Citations |
2 | 0925-9856 | 1 |
PageRank | References | Authors |
0.36 | 21 | 2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Thomas Martin Gawlitza | 1 | 88 | 6.37 |
Helmut Seidl | 2 | 1468 | 103.61 |