Title
Numerical Invariants through Convex Relaxation and Max-Strategy Iteration
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 Gawlitza1886.37
Helmut Seidl21468103.61