Abstract
In a POPL 2014 paper, Jeannet et al. showed that abstract acceleration is a relevant approach for general linear loops thanks to the Jordan decomposition of the linear transformer. Bounding the number of loop iterations involves interval-linear constraints. After identifying sources of over-approximation, we present some improvements over their method. First, we improve precision by using interval hulls in the Jordan parameters space instead of the state space, avoiding further interval arithmetic. Then, we show how to use conic hulls instead of interval hulls to further improve precision.
Furthermore, we extend their work to handle linear loops with bounded nondeterministic input. This was already attempted by Cattaruzza et al. in a SAS 2015 paper, unfortunately their method is unsound. After explaining why, we propose a sound approach to guarded LTI loops with bounded nondeterministic inputs by reduction to the autonomous case.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
To be more precise, Jeannet et al. [11] substitute \(P^{-1}{}(X_0\cap \mathcal {G})\) by its interval hull in \(P{}J_iP^{-1}{}(X_0\cap \mathcal {G})\), where \(P\) is the invertible matrix leading to the Jordan form of \(A=P{}JP^{-1}{}\). Use of this transformation is not justified and its advantage is not clear.
- 2.
When approximating \(\mathcal {K}\) with interval linear constraints the relation between the constraints parameters are lost.
- 3.
Both sets would be equal if interval arithmetic did not amplify and propagate any approximation.
- 4.
We use a similar heuristic in the experimental section to decide if an interval linear constraints can lead to a bound.
- 5.
If there are several constraints, treating each constraint independently leads to an over-approximation.
- 6.
Almost the dual cone of \(L(X_0\cap \mathcal {G})\).
- 7.
This is not how a bound N should be computed, and is only useful to asses the quality of the interval linear constraint.
- 8.
The authors attempted a correction [6], unfortunately Eq. (16) is only true if all the \(k_{ij}\) are positive and the method is still unsound.
- 9.
The corresponding constraint can be added to the loop guard.
References
Althoff, M.: An introduction to CORA 2015. In: Frehse, G., Althoff, M. (eds.) 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems, ARCH14-15. EPiC Series in Computing, vol. 34, pp. 120–151. EasyChair (2015)
Althoff, M., Krogh, B.H., Stursberg, O.: Analyzing reachability of linear dynamic systems with parametric uncertainties. In: Rauh, A., Auer, E. (eds.) Modeling, Design, and Simulation of Systems with Uncertainties. Mathematical Engineering, vol. 3, pp. 69–94. Springer, Heidelberg (2011). doi:10.1007/978-3-642-15956-5_4
Althoff, M., Le Guernic, C., Krogh, B.H.: Reachable set computation for uncertain time-varying linear systems. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, HSCC 2011, NY, USA, pp. 93–102 (2011). http://doi.acm.org/10.1145/1967701.1967717
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). doi:10.1007/3-540-49059-0_14
Cattaruzza, D., Abate, A., Schrammel, P., Kroening, D.: Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 312–331. Springer, Heidelberg (2015). doi:10.1007/978-3-662-48288-9_18
Cattaruzza, D., Abate, A., Schrammel, P., Kroening, D.: Unbounded-time analysis of guarded LTI systems with inputs by abstract acceleration (extended version). CoRR abs/1506.05607 (2015). http://arxiv.org/abs/1506.05607
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, pp. 238–252. ACM (1977). http://doi.acm.org/10.1145/512950.512973
Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24725-8_4
Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 144–160. Springer, Heidelberg (2006). doi:10.1007/11823230_10
Gonnord, L., Schrammel, P.: Abstract acceleration in linear relation analysis. Sci. Comput. Program. 93, 125–153 (2014). http://dx.doi.org/10.1016/j.scico.2013.09.016
Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, NY, USA, pp. 529–540 (2014). http://dx.doi.org/10.1145/2535838.2535843
Kurzhanskiy, A.A., Varaiya, P.: Ellipsoidal techniques for reachability analysis of discrete-time linear systems. IEEE Trans. Automat. Contr. 52(1), 26–38 (2007). http://dx.doi.org/10.1109/TAC.2006.887900
Le Guernic, C.: Toward a sound analysis of guarded LTI loops with inputs by abstract acceleration (extended version). https://hal.inria.fr/hal-01550767
Le Guernic, C.: Reachability analysis of hybrid systems with linear continuous dynamics. Ph.D. thesis, Université Joseph Fourier - Grenoble I (2009). https://tel.archives-ouvertes.fr/tel-00422569
Le Guernic, C., Girard, A.: Reachability analysis of hybrid systems using support functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 540–554. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_40
Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Anal. Hybrid Syst. 4(2), 250–262 (2010). IFACWorldCongress2008. http://dx.doi.org/10.1016/j.nahs.2009.03.002
Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24743-2_32
Roux, P., Jobredeaux, R., Garoche, P., Feron, E.: A generic ellipsoid abstract domain for linear time invariant systems. In: Hybrid Systems: Computation and Control (part of CPS Week 2012), HSCC 2012, Beijing, China, 17–19 April 2012, pp. 105–114. ACM (2012). http://doi.acm.org/10.1145/2185632.2185651
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Le Guernic, C. (2017). Toward a Sound Analysis of Guarded LTI Loops with Inputs by Abstract Acceleration. In: Ranzato, F. (eds) Static Analysis. SAS 2017. Lecture Notes in Computer Science(), vol 10422. Springer, Cham. https://doi.org/10.1007/978-3-319-66706-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-66706-5_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66705-8
Online ISBN: 978-3-319-66706-5
eBook Packages: Computer ScienceComputer Science (R0)