Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Methods in Macro-Biology

FMMB 2014: Formal Methods in Macro-Biology pp 1–22Cite as

Model-Checking in Systems Biology - From Micro to Macro

  • Conference paper

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

Abstract

In this paper, we will address some of the main challenges in the development of efficient, rigorous methods for model-checking the multiscale, highly uncertain dynamic systems arising in biological applications, and provide some theory and methods which address these. We will focus on three main aspects: 1) how to represent and compute with continuous data-types in a mathematically sound way, 2) how to handle modular and hierarchical systems, including abstraction of dynamics and system reduction, and 3) how to model uncertainties and handle the resulting models numerically. We will illustrate some of these issues and possible approaches for a model arising in cardiac electrophysiology.

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ariadne: An open tool for hybrid systems analysis, http://fsv.dimi.uniud.it/ariadne/

  2. Asarin, E., Dang, T., Maler, O.: The d/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  3. Aubin, J.P., Cellina, A.: Differential inclusions. Grundlehren der Mathematischen Wissenschaften, vol. 264. Springer, Berlin (1984)

    MATH  Google Scholar 

  4. Baier, C., Katoen, J.P.: Principles of model checking. MIT Press, Cambridge (2008), with a foreword by Kim Guldstrand Larsen

    Google Scholar 

  5. Baier, R., Gerdts, M.: A computational method for non-convex reachable sets using optimal control. In: Proceedings of the European Control Conference, pp. 97–102 (2009)

    Google Scholar 

  6. Balluchi, A., Casagrande, A., Collins, P., Ferrari, A., Villa, T., Sangiovanni-Vincentelli, A.L.: Ariadne: a framework for reachability analysis of hybrid automata. In: Proceedings of the 17th International Symposium on the Mathematical Theory of Networks and Systems, Kyoto, Japan, July 24-28, pp. 1269–1267 (2006)

    Google Scholar 

  7. Barnat, J., Brim, L., Cerna, I., Drazan, S., Fabrikova, J., Lanik, J., Safranek, D., Ma, H.: BioDiVinE: A framework for parallel analysis of biological models. In: Computational Models for Cell Processes, pp. 31–45 (2009)

    Google Scholar 

  8. Bauer, A.: The Realizability Approach to Computable Analysis and Topology. Ph.D. thesis, Carnegie Mellon University (2000)

    Google Scholar 

  9. Bect, J., Baili, H., Fleury, G.: Generalized Fokker-Planck equation for piecewise-diffusion processes with boundary hitting resets. In: Proceedings of the 17th International Symposium on the Mathematical Theory of Networks and Systems, Kyoto, Japan, July 24-28 (2006)

    Google Scholar 

  10. Belta, C., Habets, L.: Controlling a class of nonlinear systems on rectangles. IEEE Trans. Autom. Control 51(11), 1749–1759 (2006)

    Article  MathSciNet  Google Scholar 

  11. Beyn, W.J., Rieger, J.: Numerical fixed grid methods for differential inclusions. Computing 81(1), 91–106 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  12. Boehm, H.J., Cartwright, R., Riggle, M., O’Donnell, M.: Exact real arithmetic: a case study in higher order programming. In: Proceedings of the ACM Symposium on Lisp and Functional Programming, pp. 162–173 (1986)

    Google Scholar 

  13. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: An analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  14. Clerx, M., Collins, P.: Reducing run-times of excitable cell models by replacing computationally expensive functions with splines. In: Proceedings of the International Symposium on the Mathematical Theory of Networks and Systems (2014)

    Google Scholar 

  15. Collins, P.: Computable analysis with applications to dynamic systems. Tech. rep., Centrum Wiskunde en Informatica, Amsterdam, cWI Report MAC-1002 (2010)

    Google Scholar 

  16. Collins, P.: Optimal semicomputable approximations to reachable and invariant sets. Theory Comput. Syst. 41(1), 33–48 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  17. Collins, P.: Computable types for dynamic systems. In: Proceedings of the Fifth Conference on Computability in Europe (2009)

    Google Scholar 

  18. Collins, P.: Computable stochastic processes (in preparation, 2014)

    Google Scholar 

  19. Collins, P.: Input-output representations for verifying safety properties. In: Proceedings of the International Symposium on the Mathematical Theory of Networks and Systems (2014)

    Google Scholar 

  20. Collins, P., Graça, D.: Effective computability of solutions of differential inclusions — the ten thousand monkeys approach. J. Universal Comput. Sci. 15(6), 1162–1185 (2009)

    MATH  Google Scholar 

  21. Collins, P., Zapreev, I.S.: Computable semantics for CTL* on discrete-time and continuous-space dynamic systems. Int. J. Found. Comput. Sci. 22(4), 801–821 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  22. Coquand, T., Spitters, B.: Integrals and valuations. J. Logic Analysis 1(3), 1–22 (2009)

    MathSciNet  Google Scholar 

  23. Day, S., Junge, O., Mischaikow, K.: A rigorous numerical method for the global analysis of infinite-dimensional discrete dynamical systems. SIAM J. Appl. Dyn. Syst. 3(2), 117–160 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  24. Deimling, K.: Multivalued differential equations. de Gruyter Series in Nonlinear Analysis and Applications, vol. 1. Walter de Gruyter & Co., Berlin (1992)

    Book  MATH  Google Scholar 

  25. Dellnitz, M., Froyland, G., Junge, O.: The algorithms behind GAIO-set oriented numerical methods for dynamical systems. In: Ergodic Theory, Analysis, and Efficient Simulation of Dynamical Systems, pp. 145–174, 805–807. Springer (2001)

    Google Scholar 

  26. Edalat, A.: Domains for computation in mathematics, physics and exact real arithmetic. Bull. Symbolic Logic 151(4), 401–452 (1997)

    Article  MathSciNet  Google Scholar 

  27. Fousse, L., Hanrot, G., Lefèvre, V., Pélissier, P., Zimmermann, P.: MPFR: A multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33(2) (2007), http://www.mpfr.org/

  28. Frehse, G., et al.: 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 

  29. Friedman, A.: Stochastic Differential Equations. Dover (1975)

    Google Scholar 

  30. Geuvers, H., Niqui, M., Spitters, B., Wiedijk, F.: Constructive analysis, types and exact real numbers. Math. Structures Comp. Sci. 17(1), 3–36 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  31. Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., Scott, D.: Continuous lattices and domains. Cambridge University Press (2003)

    Google Scholar 

  32. Goebel, R., Teel, A.R.: Solutions to hybrid inclusions via set and graphical convergence with stability theory applications. Automatica J. IFAC 42(4), 573–587 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  33. Gorban, A., Karlin, I., Zinovyev, A.: Invariant grids: Method of complexity reduction in reaction networks. Complexus 2004–2005 (2), 110–127 (2005)

    Google Scholar 

  34. Grosu, R., Batt, G., Fenton, F.H., Glimm, J., Le Guernic, C., Smolka, S.A., Bartocci, E.: From cardiac cells to genetic regulatory networks. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 396–411. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  35. Grosu, R., Smolka, S.A., Corradini, F., Wasilewska, A., Entcheva, E., Bartocci, E.: Learning and detecting emergent behavior in networks of cardiac myocytes. Commun. ACM 52(3), 97–105 (2009)

    Article  Google Scholar 

  36. Heijman, J., Volders, P.G., Westra, R.L., Rudy, Y.: Local control of beta-adrenergic stimulation: Effects on ventricular myocyte electrophysiology and ca(2+)-transient. Journal of Molecular and Cellular Cardiology (2011)

    Google Scholar 

  37. Hodgkin, A.L., Huxley, A.F.: A quantitative description of membrane current and its application to conduction and excitation in nerve. The Journal of Physiology 117(4), 500–544 (1952)

    Article  Google Scholar 

  38. Jones, C., Plotkin, G.: A probabilistic powerdomain of evaluations. In: Proceedings of the Fourth Annual Symposium on Logic in Computer Science, pp. 186–195 (1989), http://dl.acm.org/citation.cfm?id=77350.77370

  39. de Jong, H., Geiselmann, J., Hernandez, C., Page, M.: Genetic Network Analyzer: Qualitative simulation of genetic regulatory networks. Mathematical Biology 66(2), 261–300 (2004)

    Article  MathSciNet  Google Scholar 

  40. Kleene, S.C.: Mathematical Logic (1967)

    Google Scholar 

  41. Kurzhanski, A., Valyi, I.: Ellipsoidal calculus for estimation and control. In: Systems and Control: Foundations and Applications, Birkhäuser (1997)

    Google Scholar 

  42. Kushner, H., Yin, G.G.: Stochastic Approximation and Recursive Algorithms and Applications. Stochastic Modelling and Applied Probability, vol. 35. Springer (2003)

    Google Scholar 

  43. Lohner, R.J.: AWA–software for the computation of guaranteed bounds for solutions of ordinary initial value problems. Tech. rep., Institut fur Angewandte Mathematik (2006)

    Google Scholar 

  44. Mrozek, M., et al.: CAPD Library (2007), http://capd.ii.uj.edu.pl/

  45. Makino, K., Berz, M.: COSY INFINITY Version 9. Nuclear Instruments and Methods A558, 346–350 (2006)

    Google Scholar 

  46. Mannella, R., McClintock, P.V.E.: Itô versus Stratonovic: 30 years later. Fluctuation Noise Lett. 11(1) (2012)

    Google Scholar 

  47. Menissier-Morain, V.: Arbitrary precision real arithmetic: design and algorithms. J. Logic Algebraic Programming 64, 13–39 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  48. Müller, N.T.: The iRRAM: Exact arithmetic in C++. In: Blank, J., Brattka, V., Hertling, P. (eds.) CCA 2000. LNCS, vol. 2064, pp. 222–252. Springer, Heidelberg (2001), http://irram.uni-trier.de/

    Chapter  Google Scholar 

  49. Nedialkov, N.: VNODE-LP. Tech. rep., cAS-06-06-NN (2006)

    Google Scholar 

  50. Perrin, D., Pin, J.E.: Infinite Words: Automata, Semigroups, Logic and Games. Elsevier (2004)

    Google Scholar 

  51. Polderman, J.W., Willems, J.C.: ntroduction to mathematical systems theory: A behavioral approach. Texts in Applied Mathematics, vol. 26. Springer, New York (1998)

    Book  Google Scholar 

  52. Puri, A., Varaiya, P., Borkar, V.: Epsilon-approximation of differential inclusions. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 362–376. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  53. Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Transactions in Embedded Computing Systems 6(1) (2007)

    Google Scholar 

  54. Rizk, A., Batt, G., Fages, F., Soliman, S.: Continuous valuations of temporal logic specifications with applications to parameter optimization and robustness measures. Theor. Comput. Sci. 412(26), 2827–2839 (2011)

    Article  MATH  MathSciNet  Google Scholar 

  55. Ruohonen, K.: An effective Cauchy-Peano existence theorem for unique solutions. Internat. J. Found. Comput. Sci. 7(2), 151–160 (1996)

    Article  MATH  Google Scholar 

  56. Spitters, B.: Constructive algebraic integration theory. Ann. Pure Appl. Logic 137(1-3), 380–390 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  57. Taylor, P.: A lambda calculus for real analysis (2008), http://www.monad.me.uk/

  58. Tran, D.X., Sato, D., Yochelis, A., Weiss, J.N., Garfinkel, A., Qu, Z.: Bifurcation and chaos in a model of cardiac early afterdepolarizations. Phys. Rev. Lett. 102(25), 258103 (2009)

    Article  Google Scholar 

  59. Weihrauch, K.: Computable Analysis: An introduction. Texts in Theoretical Computer Science. Springer, Berlin (2000)

    Book  Google Scholar 

  60. Zgliczynski, P., Kapela, T.A.: Lohner algorithm for perturbation of ODEs and differential inclusions. Discrete Contin. Dyn. Syst. Ser. B 11(2), 365–385 (2009)

    MATH  MathSciNet  Google Scholar 

  61. Zgliczyński, P., Mischaikow, K.: Rigorous numerics for partial differential equations: The KuramotoSivashinsky equation. Found. Comput. Math. 1, 255–288 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  62. Živanović, S., Collins, P.: Numerical solutions to noisy systems. In: Proc. 49th IEEE Conference on Decision and Control (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Knowledge Engineering, Maastricht University, The Netherlands

    Pieter Collins

Authors
  1. Pieter Collins
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Inria,, Bâtiment 8, Domaine de Voluceau, 78150, Rocquencourt, France

    François Fages

  2. Department of Mathematics and Computer Science, University of Udine, Via le Scienze 206, 33100, Udine, Italy

    Carla Piazza

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Collins, P. (2014). Model-Checking in Systems Biology - From Micro to Macro. In: Fages, F., Piazza, C. (eds) Formal Methods in Macro-Biology. FMMB 2014. Lecture Notes in Computer Science(), vol 8738. Springer, Cham. https://doi.org/10.1007/978-3-319-10398-3_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10398-3_1

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10397-6

  • Online ISBN: 978-3-319-10398-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation