Abstract
Reachability analysis has recently proved to be a useful technique for analysing the behaviour of under-specified biological models. In this paper, we propose a method exploiting the eigenstructure of a linear continuous system to efficiently estimate a bounded interval containing the time at which the system can reach a target set from an initial set. Then this estimation can be directly integrated in an existing algorithm for hybrid systems with linear continuous dynamics, to speed up reachability computations. Furthermore, it can also be used to improve time-efficiency of the hybridization technique that is based on a piecewise-linear approximation of non-linear continuous dynamics. The proposed method is illustrated on a number of examples including a biological model.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
H-polytopes are polytopes defined by a set of linear constraints.
References
Spaceex: State space explorer (2010). http://spaceex.imag.fr/
Bemporad, A., Filippi, C., Torrisi, F.D.: Inner and outer approximations of polytopes using boxes. Computat. Geom. 27(2), 151–178 (2004)
Moler, C.C., Van Loan, C.: Nineteen dubious ways to compute the exponential of a matrix, twenty-five years later. SIAM Rev. 45(1), 3–49 (2003)
Dang, T., Le Guernic, C., Maler, O.: Computing reachable states for nonlinear biological models. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 126–141. Springer, Heidelberg (2009)
Dang, T., Maler, O., Testylier, R.: Accurate hybridization of nonlinear systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, pp. 11–20. ACM (2010)
Duggirala, P.S., Tiwari, A.: Safety verification for linear systems. In: 2013 Proceedings of the International Conference on Embedded Software (EMSOFT), pp. 1–10. IEEE (2013)
Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)
Guernic, C.L.: Reachability analysis of hybrid systems with linear continuous dynamics. Ph.D. thesis, Université Grenoble 1 - Joseph Fourier (2009)
Lafferriere, G., Pappas, G.J., Yovine, S.: A new class of decidable hybrid systems. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 137–151. Springer, Heidelberg (1999)
Laub, M.T., Loomis, W.F.: A molecular network that produces spontaneous oscillations in excitable cells of dictyostelium. Mol. Biol. Cell 9(12), 3521–3532 (1998)
Mover, S., Cimatti, A., Tiwari, A., Tonetta, S.: Time-aware relational abstractions for hybrid systems. In: Proceedings of the Eleventh ACM International Conference on Embedded Software Press, p. 14. IEEE (2013)
Perko, L.: Linear systems. In: Differential Equations and Dynamical Systems. Springer, Heidelberg, pp. 1–63 (1991)
Testylier, R., Dang, T.: NLTOOLBOX: a library for reachability computation of nonlinear dynamical systems. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 469–473. Springer, Heidelberg (2013)
Acknowledgement
We gratefully acknowledge the support of Agence Nationale de la Recherche (ANR) through the CADMIDIA project (grant ANR-13-CESA-0008-03).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Rocca, A., Dang, T., Fanchon, E. (2015). Exploiting the Eigenstructure of Linear Systems to Speed up Reachability Computations. In: Maler, O., Halász, Á., Dang, T., Piazza, C. (eds) Hybrid Systems Biology. HSB 2014. Lecture Notes in Computer Science(), vol 7699. Springer, Cham. https://doi.org/10.1007/978-3-319-27656-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-27656-4_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-27655-7
Online ISBN: 978-3-319-27656-4
eBook Packages: Computer ScienceComputer Science (R0)