Numerical invariants through convex relaxation and max-strategy iteration. (English) Zbl 1291.68256
Summary: 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.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 90C25 | Convex programming |
| 47H10 | Fixed-point theorems |
Software:
LUSTREReferences:
| [1] | Adjé, A.; Gaubert, S.; Goubault, E.; Gordon, AD (ed.), Coupling policy iteration with semi-definite relaxation to compute accurate numerical invariants in static analysis, No. 6012, 23-42 (2010), Berlin · Zbl 1260.68082 · doi:10.1007/978-3-642-11957-6_3 |
| [2] | Alegre F, Feron E, Pande S (2009) Using ellipsoidal domains to analyze control systems software. arXiv:0909.1977 · Zbl 0064.26004 |
| [3] | Caspi, P.; Pilaud, D.; Halbwachs, N.; Plaice, J., Lustre: a declarative language for programming synchronous systems, 178-188 (1987), New York · doi:10.1145/41625.41641 |
| [4] | Costan, A.; Gaubert, S.; Goubault, E.; Martel, M.; Putot, S., A policy iteration algorithm for computing fixed points in static analysis of programs, No. 3576, 462-475 (2005), Berlin · Zbl 1081.68616 · doi:10.1007/11513988_46 |
| [5] | Cousot, P.; Cousot, R., Static determination of dynamic properties of programs, 106-130 (1976), Paris · Zbl 0788.68094 |
| [6] | Cousot, P.; Cousot, R., Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, 238-252 (1977) |
| [7] | Dang, T.; Gawlitza, TM; Yang, H. (ed.), Template-based unbounded time verification of affine hybrid automata, No. 7078, 34-49 (2011), Berlin · Zbl 1348.68100 · doi:10.1007/978-3-642-25318-8_6 |
| [8] | Dang, T.; Gawlitza, TM; Bultan, T. (ed.); Hsiung, P-A (ed.), Discretizing affine hybrid automata with uncertainty, No. 6996, 473-481 (2011), Berlin · Zbl 1348.68099 · doi:10.1007/978-3-642-24372-1_36 |
| [9] | Fearnley, J.; Abramsky, S. (ed.); Gavoille, C. (ed.); Kirchner, C. (ed.); Meyer auf der Heide, F. (ed.); Spirakis, PG (ed.), Exponential lower bounds for policy iteration, No. 6199, 551-562 (2010), Berlin · Zbl 1288.68089 · doi:10.1007/978-3-642-14162-1_46 |
| [10] | Gawlitza, T.; Seidl, H.; Duparc, J. (ed.); Henzinger, TA (ed.), Precise relational invariants through strategy iteration, No. 4646, 23-40 (2007), Berlin · Zbl 1179.68037 · doi:10.1007/978-3-540-74915-8_6 |
| [11] | Gawlitza, T.; Seidl, H.; Nicola, RD (ed.), Precise fixpoint computation through strategy iteration, No. 4421, 300-315 (2007), Berlin · Zbl 1187.68152 · doi:10.1007/978-3-540-71316-6_21 |
| [12] | Gawlitza, T.; Seidl, H.; Cuéllar, J. (ed.); Maibaum, TSE (ed.); Sere, K. (ed.), Precise interval analysis vs. parity games, No. 5014, 342-357 (2008), Berlin · doi:10.1007/978-3-540-68237-0_24 |
| [13] | Gawlitza, TM; Seidl, H.; Cousot, R. (ed.); Martel, M. (ed.), Computing relaxed abstract semantics w.r.t. quadratic zones precisely, No. 6337, 271-286 (2010), Berlin · Zbl 1306.68025 · doi:10.1007/978-3-642-15769-1_17 |
| [14] | Gawlitza TM, Seidl H (2011) Solving systems of rational equations through strategy iteration. ACM Trans Program Lang Syst 33(3):11 · doi:10.1145/1961204.1961207 |
| [15] | Gawlitza, TM; Seidl, H.; Adjé, A.; Gaubert, S.; Goubault, É., Abstract interpretation meets convex optimization (2011) · Zbl 1246.90118 |
| [16] | Girard, A.; Morari, M. (ed.); Thiele, L. (ed.), Reachability of uncertain linear systems using zonotopes, No. 3414, 291-305 (2005), Berlin · Zbl 1078.93005 |
| [17] | Halbwachs, N., A synchronous language at work: the story of lustre, 3-11 (2005), New York |
| [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 · doi:10.1109/32.159839 |
| [19] | Larsen, KG; Larsson, F.; Pettersson, P.; Yi, W., Efficient verification of real-time systems: compact data structure and state-space reduction, 14-24 (1997), Los Alamitos |
| [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 · Zbl 1294.68061 · doi:10.1016/j.entcs.2012.09.008 |
| [21] | Miné, A.; Danvy, O. (ed.); Filinski, A. (ed.), A new numerical abstract domain based on difference-bound matrices, No. 2053, 155-172 (2001), Berlin · Zbl 0984.68034 |
| [22] | Miné, A., The octagon abstract domain, 310 (2001) · Zbl 1105.68069 |
| [23] | Nemirovski A (2005) Modern convex optimization. Department ISYE, Georgia Institute of Technology · Zbl 1348.68100 |
| [24] | Roux P, Garoche P-L (2012) Policy iterations as traditional abstract domains · Zbl 0788.68094 |
| [25] | Roux, P.; Jobredeaux, R.; Garoche, P-L; Feron, E.; Dang, T. (ed.); Mitchell, IM (ed.), A generic ellipsoid abstract domain for linear time invariant systems, 105-114 (2012), New York · Zbl 1362.93065 · doi:10.1145/2185632.2185651 |
| [26] | Sankaranarayanan, S.; Sipma, HB; Manna, Z.; Cousot, R. (ed.), Scalable analysis of linear systems using mathematical programming, No. 3385, 25-41 (2005), Berlin · Zbl 1111.68514 |
| [27] | Sankaranarayanan, S.; Dang, T.; Ivancic, F.; Egerstedt, M. (ed.); Mishra, B. (ed.), A policy iteration technique for time elapse over template polyhedra, No. 4981, 654-657 (2008), Berlin · Zbl 1144.93327 · doi:10.1007/978-3-540-78929-1_57 |
| [28] | Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5:285-309 · Zbl 0064.26004 · doi:10.2140/pjm.1955.5.285 |
| [29] | Todd MJ (2001) Semidefinite optimization. Acta Numer 10:515-560 · Zbl 1105.65334 · doi:10.1017/S0962492901000071 |
| [30] | Yovine, S.; Rozenberg, G. (ed.); Vaandrager, FW (ed.), Model checking timed automata, No. 1494, 114-152 (1996), Berlin |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
