Skip to main content

Exploiting the Eigenstructure of Linear Systems to Speed up Reachability Computations

  • Conference paper
  • First Online:
Hybrid Systems Biology (HSB 2014)

Part of the book series: Lecture Notes in Computer Science ((LNBI,volume 7699))

Included in the following conference series:

  • 343 Accesses

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 34.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    H-polytopes are polytopes defined by a set of linear constraints.

References

  1. Spaceex: State space explorer (2010). http://spaceex.imag.fr/

  2. Bemporad, A., Filippi, C., Torrisi, F.D.: Inner and outer approximations of polytopes using boxes. Computat. Geom. 27(2), 151–178 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  3. 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)

    Article  MathSciNet  MATH  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. 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)

    Google Scholar 

  6. 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)

    Google Scholar 

  7. 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)

    Chapter  Google Scholar 

  8. Guernic, C.L.: Reachability analysis of hybrid systems with linear continuous dynamics. Ph.D. thesis, Université Grenoble 1 - Joseph Fourier (2009)

    Google Scholar 

  9. 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)

    Chapter  Google Scholar 

  10. 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)

    Article  Google Scholar 

  11. 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)

    Google Scholar 

  12. Perko, L.: Linear systems. In: Differential Equations and Dynamical Systems. Springer, Heidelberg, pp. 1–63 (1991)

    Google Scholar 

  13. 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)

    Chapter  Google Scholar 

Download references

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

Authors

Corresponding author

Correspondence to Alexandre Rocca .

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics