Abstract
We describe NLTOOLBOX, a library of data structures and algorithms for reachability computation of nonlinear dynamical systems. It provides the users with an easy way to “program” their own analysis procedures or to solve other problems beyond verification. We illustrate the use of the library for the analysis of a biological model.
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
Preview
Unable to display preview. Download preview PDF.
References
Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate reachability analysis of piecewise-linear dynamical systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 20–31. Springer, Heidelberg (2000)
Dang, T., Le Guernic, C., Maler, O.: Computing reachable states for nonlinear biological models. Theoretical Computer Science 412(21), 2095–2107 (2011)
Dang, T., Testylier, R.: Hybridization domain construction using curvature estimation. In: HSCC 2011. LNCS, pp. 123–132 (2011)
Dang, T., Testylier, R.: Reachability analysis for polynomial dynamical systems using the Bernstein expansion. Reliable Computing Journal (2011) ISSN 1573-1340
Chutinan, A., Krogh, B.H.: Computational Techniques for Hybrid System Verification. IEEE Trans. on Automatic Control 48, 64–75 (2003)
Chen, X., Ábrahám, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proc. RTSS 2012. IEEE (2012)
Benvenuti, L., Bresolin, D., Casagrande, A., Collins, P., Ferrari, A., Mazzi, E., Sangiovanni-Vincentelli, A., Villa, R.: Reachability computation for hybrid systems with Ariadne. In: Proc. the 17th IFAC World Congress (2008)
Fränzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient Solving of Large Non-Linear Arithmetic Constraint Systems with Complex Boolean Structure. J. on Satisfiability, Boolean Modeling, and Computation 1, 209–236 (2007)
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)
Kurzhanskiy, A., Varaiya, P.: Ellipsoidal Techniques for Reachability Analysis of Discrete-time Linear Systems. IEEE Trans. Automatic Control 52, 26–38 (2007)
Kvasnica, M., Grieder, P., Baotić, M., Morari, M.: Multi-Parametric Toolbox (MPT). In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 448–462. Springer, Heidelberg (2004)
Laub, M.T., Loomis, W.F.: A Molecular Network That Produces Spontaneous Oscillations in Excitable Cells of Dictyostelium. Molecular Biology of the Cell 9, 3521–3532 (1998)
Mitchell, I.M., Templeton, J.A.: A Toolbox of Hamilton-Jacobi Solvers for Analysis of Nondeterministic Continuous and Hybrid Systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 480–494. Springer, Heidelberg (2005)
Testylier, R., Dang, T.: Analysis of Parametric Biological Models. In: Workshop on Hybrid Systems and Biology HSB 2012. Springer (2012)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this paper
Cite this paper
Testylier, R., Dang, T. (2013). NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems. In: Van Hung, D., Ogawa, M. (eds) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol 8172. Springer, Cham. https://doi.org/10.1007/978-3-319-02444-8_37
Download citation
DOI: https://doi.org/10.1007/978-3-319-02444-8_37
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-02443-1
Online ISBN: 978-3-319-02444-8
eBook Packages: Computer ScienceComputer Science (R0)