Skip to main content
SpringerLink
Log in
Book cover

International School on Formal Methods for the Design of Computer, Communication and Software Systems

SFM 2013: Formal Methods for Dynamical Systems pp 63–112Cite as

Model Checking of Biological Systems

  • Chapter

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7938))

Abstract

Model checking together with other formal methods and techniques is being adapted for applications to biological systems. We present a selection of approaches used for modeling biological systems and formalizing their interesting properties in temporal logics. We also give a brief account of high performance model checking techniques and add a few case studies that demonstrate the use of model checking in computational systems biology. The primary aim is to give a reference for further reading.

This work has been partially supported by the Czech Science Foundation grant No. GAP202/11/0312. M. Češka has been supported by Ministry of Education, Youth, and Sport project No. CZ.1.07/2.3.00/30.0009 – Employment of Newly Graduated Doctors of Science for Scientific Excellence. D. Šafránek has been supported by EC OP project No. CZ.1.07/2.3.00/20.0256.

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   49.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. Allmaier, S., Dalibor, S., Kreische, D.: Parallel Graph Generation Algorithms for Shared and Distributed Memory Machines. In: Parallel Computing Conference (PARCO). LNCS, vol. 1253, pp. 207–218. Springer (1997)

    Google Scholar 

  2. Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Information and Computation 104, 2–34 (1993)

    Article  MathSciNet  MATH  Google Scholar 

  3. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  4. Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–203 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  5. Antoniotti, M., Policriti, A., Ugel, N., Mishra, B.: Model building and model checking for biochemical processes. Cell Biochemistry and Biophysics 38, 271–286 (2003)

    Article  Google Scholar 

  6. Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 269–276. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  7. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model Checking Continuous-Time Markov Chains by Transient Analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358–372. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  8. Ballarini, P., Forlin, M., Mazza, T., Prandi, D.: Efficient parallel statistical model checking of biochemical networks. In: Parallel and Distributed Methods in verifiCation (PDMC). EPTCS, vol. 14, pp. 47–61 (2009)

    Google Scholar 

  9. Ballarini, P., Guerriero, M.L.: Query-based verification of qualitative trends and oscillations in biochemical systems. Theor. Comput. Sci. 411(20), 2019–2036 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  10. Ballarini, P., Guido, R., Mazza, T., Prandi, D.: Taming the complexity of biological pathways through parallel computing. Briefings in Bioinformatics 10(3), 278–288 (2009)

    Article  Google Scholar 

  11. Barbuti, R., Caravagna, G., Maggiolo-Schettini, A., Milazzo, P., Tini, S.: Foundational aspects of multiscale modeling of biological systems with process algebras. Theor. Comput. Sci. 431, 96–116 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  12. Barnat, J., Bauch, P., Brim, L., Češka, M.: Computing Strongly Connected Components in Parallel on CUDA. In: International Parallel & Distributed Processing Symposium (IPDPS), pp. 541–552. IEEE Computer Society (2011)

    Google Scholar 

  13. Barnat, J., Brim, L., Krejci, A., Streck, A., Safranek, D., Vejnar, M., Vejpustek, T.: On Parameter Synthesis by Parallel Model Checking. IEEE/ACM Transactions on Computational Biology and Bioinformatics 9(3), 693–705 (2012)

    Article  Google Scholar 

  14. Barnat, J., Brim, L., Ročkai, P.: Scalable Multi-core LTL Model-Checking. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 187–203. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  15. Barnat, J., Brim, L., Ročkai, P.: A Time-Optimal On-the-Fly Parallel Algorithm for Model Checking of Weak LTL Properties. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 407–425. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  16. Barnat, J., Brim, L., Ročkai, P.: Parallel Partial Order Reduction with Topological Sort Proviso. In: Software Engineering and Formal Methods (SEFM), pp. 222–231. IEEE Computer Society (2010)

    Google Scholar 

  17. Barnat, J., Brim, L., Stříbrná, J.: Distributed LTL Model-Checking in SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 200–216. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Barnat, J., Brim, L., Černá, I., Dražan, S., Fabriková, J., Láník, J., Šafránek, D., Ma, H.: BioDiVinE: A Framework for Parallel Analysis of Biological Models. In: Computational Models for Cell Processes (COMPMOD). EPTCS, vol. 6, pp. 31–45 (2009)

    Google Scholar 

  19. Barnat, J., Brim, L., Černá, I., Moravec, P., Ročkai, P., Šimeček, P.: DiVinE – A Tool for Distributed Verification. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 278–281. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  20. Barnat, J., Brim, L., Šafránek, D.: High-Performance Analysis of Biological Systems Dynamics with the DiVinE Model Checker. Briefings in Bioinformatics 11(3), 301–312 (2010)

    Article  Google Scholar 

  21. Barnat, J., Brim, L., Šafránek, D., Vejnár, M.: Parameter Scanning by Parallel Model Checking with Applications in Systems Biology. In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2010), pp. 95–104. IEEE Computer Society (2010)

    Google Scholar 

  22. Barnat, J., Ročkai, P.: Shared Hash Tables in Parallel Model Checking. In: Parallel and Distributed Methods in verifiCation (PDMC). ENTCS, vol. 198, pp. 79–91 (2008)

    Google Scholar 

  23. Barnat, J., Bauch, P., Brim, L., Češka, M.: Designing fast LTL model checking algorithms for many-core GPUs. Journal of Parallel and Distributed Computing 72(9), 1083–1097 (2012)

    Article  Google Scholar 

  24. Bartocci, E., Corradini, F., Merelli, E., Tesei, L.: Detecting synchronisation of biological oscillators by model checking. Theoretical Computer Science 411(20), 1999–2018 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  25. Batt, G., Belta, C., Weiss, R.: Model checking genetic regulatory networks with parameter uncertainty. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 61–75. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  26. Batt, G., Page, M., Cantone, I., Goessler, G., Monteiro, P., de Jong, H.: Efficient parameter search for qualitative models of regulatory networks using symbolic model checking. Bioinformatics 26(18), 603–610 (2010)

    Article  Google Scholar 

  27. Batt, G., Ben Salah, R., Maler, O.: On timed models of gene networks. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 38–52. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  28. Behrmann, G., Hune, T., Vaandrager, F.: Distributed Timed Model Checking — How the Search Order Matters. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 216–231. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  29. Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  31. Bernot, G., Comet, J.P., Richard, A., Guespin, J.: Application of formal methods to biological regulatory networks: extending thomas’ asynchronous logical approach with temporal logic. Journal of Theoretical Biology 229(3), 339–347 (2004)

    Article  MathSciNet  Google Scholar 

  32. Bonzanni, N., Krepska, E., Feenstra, K.A., Fokkink, W., Kielmann, T., Bal, H.E., Heringa, J.: Executing multicellular differentiation: quantitative predictive modelling of C.elegans vulval development. Bioinformatics 25(16), 2049–2056 (2009)

    Article  Google Scholar 

  33. Bortolussi, L., Hillston, J.: Fluid model checking. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 333–347. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  34. Bortolussi, L., Policriti, A.: Hybrid systems and biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 424–448. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  35. Bošnački, D., Edelkamp, S., Sulewski, D.: Efficient Probabilistic Model Checking on General Purpose Graphics Processors. In: Păsăreanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 32–49. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  36. Bošnački, D., ten Eikelder, H.M.M., Steijaert, M.N., de Vink, E.P.: Stochastic analysis of amino acid substitution in protein synthesis. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 367–386. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  37. Brenan, K.E., Campbell, S.L., Petzold, L.R.: Numerical Solution of Initial-Value Problems in Differential-Algebraic Equations. SIAM (1987)

    Google Scholar 

  38. Brim, L., Černá, I., Moravec, P., Šimša, J.: Accepting predecessors are better than back edges in distributed LTL model-checking. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 352–366. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  39. Brim, L., Barnat, J.: Platform Dependent Verification: On Engineering Verification Tools for 21st Century. In: Parallel and Distributed Methods in verifiCation (PDMC). EPTCS, vol. 72, pp. 1–12 (2011)

    Google Scholar 

  40. Brim, L., Česka, M., Dražan, S., Šafránek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. Tech. rep., Faculty of Informatics, Masaryk University (2013), http://sybila.fi.muni.cz/TR-01-2013.pdf

  41. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  42. Calder, M., Vyshemirsky, V., Gilbert, D., Orton, R.: Analysis of signalling pathways using continuous time markov chains. In: Priami, C., Plotkin, G. (eds.) Transactions on Computational Systems Biology VI. LNCS (LNBI), vol. 4220, pp. 44–67. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  43. Calzone, L., Chabrier-Rivier, N., Fages, F., Soliman, S.: Machine learning biochemical networks from temporal logic properties. In: Priami, C., Plotkin, G. (eds.) Transactions on Computational Systems Biology VI. LNCS (LNBI), vol. 4220, pp. 68–94. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  44. Campagna, D., Piazza, C.: Hybrid automata in systems biology: How far can we go? In: From Biology to Concurrency and Back (FBTC). ENTCS, vol. 229, pp. 93–108 (2009)

    Google Scholar 

  45. Caravagna, G., Hillston, J.: Modeling biological systems with delays in Bio-PEPA. In: Proceedings Fourth Workshop on Membrane Computing and Biologically Inspired Process Calculi 2010. EPTCS, vol. 40, pp. 85–101 (2010)

    Google Scholar 

  46. Carrillo, M., Góngora, P.A., Rosenblueth, D.A.: An overview of existing modeling tools making use of model checking in the analysis of biochemical networks. Front Plant Sci. 3(155), 1–13 (2012)

    Google Scholar 

  47. Caselli, S., Conte, G., Marenzoni, P.: Parallel state space exploration for GSPN models. In: DeMichelis, G., Díaz, M. (eds.) ICATPN 1995. LNCS, vol. 935, pp. 181–200. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  48. Černá, I., Pelánek, R.: Distributed explicit fair cycle detection (Set based approach). In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 49–73. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  49. Chaouiya, C.: Petri net modelling of biological networks. Briefings in Bioinformatics 8(4), 210–219 (2007)

    Article  Google Scholar 

  50. Chaouiya, C., Remy, E., Mossé, B., Thieffry, D.: Qualitative analysis of regulatory graphs: A computational tool based on a discrete formal framework. In: Benvenuti, L., De Santis, A., Farina, L. (eds.) Positive Systems. LNCIS, vol. 294, pp. 830–832. Springer, Heidelberg (2003)

    Google Scholar 

  51. Che, S., Li, J., Sheaffer, J., Skadron, K., Lach, J.: Accelerating Compute-Intensive Applications with GPUs and FPGAs. In: IEEE Symposium on Application Specific Processors (SASP), pp. 101–107. IEEE Computer Society (2008)

    Google Scholar 

  52. Ciardo, G., Gluckman, J., Nicol, D.: Distributed state-space generation of discrete-state stochastic models. INFORMS J. Comp. 10(1), 82–93 (1998)

    Article  Google Scholar 

  53. Ciardo, G.: Automated parallelization of discrete state-space generation. J. Parallel Distrib. Comput. 47, 153–167 (1997)

    Article  Google Scholar 

  54. Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: a new symbolic model checker. J. Softw. Tools Technol. Transf. 2, 410–425 (2000)

    Article  MATH  Google Scholar 

  55. Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  56. Ciocchetta, F., Hillston, J.: Bio-PEPA: A framework for the modelling and analysis of biological systems. Theor. Comput. Sci. 410(33-34), 3065–3084 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  57. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986)

    Article  MATH  Google Scholar 

  58. Clarke, E.M., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Form. Methods Syst. Des. 9(1-2), 77–104 (1996)

    Article  Google Scholar 

  59. Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model checking. MIT Press (1999)

    Google Scholar 

  60. Clarke, E.M., Zuliani, P.: Statistical Model Checking for Cyber-Physical Systems. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 1–12. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  61. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Progress on the State Explosion Problem in Model Checking. In: Wilhelm, R. (ed.) Informatics: 10 Years Back, 10 Years Ahead. LNCS, vol. 2000, pp. 176–194. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  62. Collins, P., Habets, L.C., van Schuppen, J.H., Černá, I., Fabriková, J., Šafránek, D.: Abstraction of biochemical reaction systems on polytopes. In: Proceedings of the 18th IFAC World Congress, vol. 18, pp. 14869–14875 (2011)

    Google Scholar 

  63. Courcoubetis, C., Vardi, M., Wolper, P., Yannakakis, M.: Memory-Efficient Algorithms for the Verification of Temporal Properties. Formal Methods in System Design 1, 275–288 (1992)

    Article  MATH  Google Scholar 

  64. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM 42(4), 857–907 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  65. Crudu, A., Debussche, A., Radulescu, O.: Hybrid stochastic simplifications for multiscale gene networks. BMC Systems Biology 3(1), 89 (2009)

    Article  Google Scholar 

  66. NVIDIA CUDA Compute Unified Device Architecture - Programming Guide Version 2.0, (2009), http://www.nvidia.com/object/cuda_develop.html

  67. Dang, T., Guernic, C.L., Maler, O.: Computing reachable states for nonlinear biological models. Theor. Comput. Sci. 412(21), 2095–2107 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  68. Danos, V., Laneve, C.: Formal molecular biology. Theor. Comput. Sci. 325(1), 69–110 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  69. Darling, R., Norris, J.: Differential equation approximations for markov chains. Probab. Surveys 5, 37–79 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  70. David, A., Du, D., Larsen, K.G., Legay, A., Mikucionis, M., Poulsen, D.B., Sedwards, S.: Statistical model checking for stochastic hybrid systems. In: Hybrid Systems and Biology (HSB). EPTCS, vol. 92, pp. 122–136 (2012)

    Google Scholar 

  71. Derman, C.: Finite State Markovian Decision Processes. Academic Press, Inc., Orlando (1970)

    MATH  Google Scholar 

  72. Didier, F., Henzinger, T.A., Mateescu, M., Wolf, V.: Fast Adaptive Uniformization for the Chemical Master Equation. In: Parallel and Distributed Methods in Verification and High Performance Computational Systems Biology (HiBi/PDMC 2009), pp. 118–127. IEEE Computer Society (2009)

    Google Scholar 

  73. Didier, F., Henzinger, T.A., Mateescu, M., Wolf, V.: Sabre: A tool for stochastic analysis of biochemical reaction networks. CoRR abs/1005.2819 (2010)

    Google Scholar 

  74. Dluhoš, P., Brim, L., Šafránek, D.: On expressing and monitoring oscillatory dynamics. In: Hybrid Systems and Biology (HSB). EPTCS, vol. 92, pp. 73–87 (2012)

    Google Scholar 

  75. Doi, A., Fujita, S., Matsuno, H., Nagasaki, M., Miyano, S.: Constructing Biological Pathway Models with Hybrid Functional Petri Nets. In Silico Biology 4(3), 271–291 (2004)

    Google Scholar 

  76. Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  77. Donzé, A., Clermont, G., Langmead, C.J.: Parameter synthesis in nonlinear dynamical systems: Application to systems biology. Journal of Computational Biology 17(3), 325–336 (2010)

    Article  MathSciNet  Google Scholar 

  78. Edelkamp, S., Sulewski, D.: Parallel State Space Search on the GPU (2009), symposium on Combinatorial Search (SoCS)

    Google Scholar 

  79. Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Meseguer, J., Sonmez, K.: Pathway logic: Symbolic analysis of biological signaling. In: Pacific Symposium on Biocomputing, pp. 400–412 (2002)

    Google Scholar 

  80. El Samad, H., Khammash, M., Petzold, L., Gillespie, D.: Stochastic Modelling of Gene Regulatory Networks. Int. J. of Robust and Nonlinear Control 15(15), 691–711 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  81. Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Form. Methods Syst. Des. 9(1-2), 105–131 (1996)

    Article  Google Scholar 

  82. Engl, H.W., Flamm, C., Kügler, P., Lu, J., Müller, S., Schuster, P.: Inverse problems in systems biology. Inverse Problems 25(12), 123014 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  83. Ezekiel, J., Lüttgen, G., Ciardo, G.: Parallelising symbolic state-space generators. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 268–280. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  84. Fages, F., Soliman, S.: Formal cell biology in Biocham. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 54–80. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  85. Fages, F., Soliman, S., Rivier, C.N.: Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM. Journal of Biological Physics and Chemistry 4(2), 64–73 (2004)

    Article  Google Scholar 

  86. Fages, F., Rizk, A.: On temporal logic constraint solving for analyzing numerical data time series. Theor. Comput. Sci. 408(1), 55–65 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  87. Fisher, J., Henzinger, T.A.: Executable cell biology. Nature Biotechnology 25(11), 1239–1249 (2007)

    Article  Google Scholar 

  88. Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  89. Fromentin, J., Eveillard, D., Roux, O.: Hybrid modeling of biological networks: mixing temporal and qualitative biological properties. BMC Systems Biology 4(1), 79 (2010)

    Article  Google Scholar 

  90. Galpin, V., Hillston, J., Bortolussi, L.: HYPE Applied to the Modelling of Hybrid Biological Systems. ENTCS 218, 33–51 (2008)

    MATH  Google Scholar 

  91. Garavel, H., Mateescu, R., Lang, F., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  92. Garavel, H., Mateescu, R., Smarandache, I.: Parallel State Space Construction for Model-Checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 217–234. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  93. Geldenhuys, J., de Villiers, P.J.A.: Runtime efficient state compaction in SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 12–21. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  94. Gillespie, D.T.: Exact Stochastic Simulation of Coupled Chemical Reactions. Journal of Physical Chemistry 81(25), 2340–2381 (1977)

    Article  Google Scholar 

  95. Gillespie, D.T.: A rigorous derivation of the chemical master equation. Physica A: Statistical Mechanics and its Applications 188(1-3), 404–425 (1992)

    Article  Google Scholar 

  96. Gillespie, D.T.: Stochastic Simulation of Chemical Kinetics. Annual Review of Physical Chemistry 58(1), 35–55 (2007)

    Article  MathSciNet  Google Scholar 

  97. Goethem, S.V., Jacquet, J.M., Brim, L., Šafránek, D.: Timed modelling of gene networks with arbitrary expression level discretization. In: Interactions between Computer Science and Biology. ENTCS. Elsevier (in press, 2013)

    Google Scholar 

  98. Grumberg, O., Heyman, T., Schuster, A.: A work-efficient distributed algorithm for reachability analysis. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 54–66. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  99. Habets, L., van Schuppen, J.H.: A control problem for affine dynamical systems on a full-dimensional polytope. Automatica 40(1), 21–35 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  100. Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6, 512–535 (1994)

    Article  MATH  Google Scholar 

  101. Haverkort, B.R., Bell, A., Bohnenkamp, H.C.: On the efficient sequential and distributed generation of very large Markov chains from stochastic Petri nets. In: Petri Net and Performance Models (PNPM), pp. 12–21. IEEE Computer Society Press (1999)

    Google Scholar 

  102. Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theoretical Computer Science 319(3), 239–257 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  103. Heiner, M., Gilbert, D., Donaldson, R.: Petri nets for systems and synthetic biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 215–264. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  104. Heljanko, K., Khomenko, V., Koutny, M.: Parallelisation of the Petri Net Unfolding Algorithm. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 371–385. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  105. Henzinger, T.: The theory of hybrid automata. In: Logic in Computer Science (LICS), pp. 278 –292. IEEE Computer Society (1996)

    Google Scholar 

  106. Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What’s decidable about hybrid automata? In: Proceedings of the Twenty-Seventh Annual ACM Symposium on Theory of Computing, pp. 373–382. ACM (1995)

    Google Scholar 

  107. Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley (2003)

    Google Scholar 

  108. Holzmann, G.J.: A Stack-Slicing Algorithm for Multi-Core Model Checking. Electonic Notes in Theoretical Computer Science 198(1), 3–16 (2008)

    Article  MathSciNet  MATH  Google Scholar 

  109. Holzmann, G.J., Bosnacki, D.: The design of a multicore extension of the spin model checker. IEEE Trans. Software Eng. 33(10), 659–674 (2007)

    Article  Google Scholar 

  110. Horn, F., Jackson, R.: General mass action kinetics. Archive for Rational Mechanics and Analysis 47, 81–116 (1972), doi:10.1007/BF00251225

    Article  MathSciNet  Google Scholar 

  111. Inggs, C.P., Barringer, H.: CTL* Model Checking on a Shared-Memory Architecture. Electronic Notes in Theoretical Computer Science 128(3), 107–123 (2005)

    Article  MATH  Google Scholar 

  112. Iyengar, M.S.: Symbolic Systems Biology: Theory and Methods. Jones & Bartlett Publishers (2010)

    Google Scholar 

  113. Jayachandran, G., Vishal, V., Pande, V.S.: Using massively parallel simulations and Markovian models to study protein folding: examining the villin head-piece. Journal of Chemical Physics 124(6), 903–914 (2006)

    Google Scholar 

  114. Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218–234. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  115. de Jong, H.: Modeling and Simulation of Genetic Regulatory Systems: A Literature Review. Journal of Computational Biology 9(1), 67–103 (2002)

    Article  Google Scholar 

  116. de Jong, H., Gouzé, J., Hernandez, C., Page, M., Sari, T., Geiselmann, J.: Qualitative simulations of genetic regulatory networks using piecewise linear models. Bull. Math. Biol. 66, 301–340 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  117. Kahn, A.B.: Topological sorting of large networks. Commun. ACM 5(11), 558–562 (1962)

    Article  MATH  Google Scholar 

  118. Keener, J.P., Sneyd, J.: Mathematical Physiology. Springer (1998)

    Google Scholar 

  119. Khademi, S., O’Connell III, J., Remis, J., Robles-Colmenares, Y., Miercke, L., Stroud, R.: Mechanism of ammonia transport by Amt/MEP/Rh: Structure of AmtB at 1.35. Science 305(5690), 1587–1594 (2004)

    Article  Google Scholar 

  120. Kholodenko, B.N.: Cell-signalling dynamics in time and space. Nature Molecular Cell Biology 7, 165–176 (2006)

    Article  Google Scholar 

  121. Klarner, H., Streck, A., Šafránek, D., Kolčák, J., Siebert, H.: Parameter identification and model ranking of thomas networks. In: Gilbert, D., Heiner, M. (eds.) CMSB 2012. LNCS, vol. 7605, pp. 207–226. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  122. Knottenbelt, W., Mestern, M., Harrison, P., Kritzinger, P.: Probability, parallelism and the state space exploration problem. In: Puigjaner, R., Savino, N.N., Serra, B. (eds.) TOOLS 1998. LNCS, vol. 1469, pp. 165–179. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  123. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2, 255–299 (1990)

    Article  Google Scholar 

  124. Kumar, R., Mercer, E.G.: Load Balancing Parallel Explicit State Model Checking. In: Parallel and Distributed Methods in Verification (PDMC). ENTCS, vol. 128, pp. 19–34. Elsevier (2005)

    Google Scholar 

  125. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  126. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  127. Kwiatkowska, M.Z., Norman, G., Parker, D.: Using probabilistic model checking in systems biology. SIGMETRICS Performance Evaluation Review 35(4), 14–21 (2008)

    Article  Google Scholar 

  128. Laarman, A., van de Pol, J., Weber, M.: Boosting Multi-Core Reachability Performance with Shared Hash Tables. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 247–255. IEEE Computer Science (2010)

    Google Scholar 

  129. Lerda, F., Sisto, R.: Distributed-memory Model Checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 22–39. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  130. Lerda, F., Visser, W.: Addressing Dynamic Issues of Program Model Checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 80–102. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  131. Ma, H., Boogerd, F., Goryanin, I.: Modelling nitrogen assimilation of Escherichia coli at low ammonium concentration. Journal of Biotechnology 144(3), 175–183 (2009)

    Article  Google Scholar 

  132. Madsen, C., Myers, C., Roehner, N., Winstead, C., Zhang, Z.: Utilizing Stochastic Model Checking to Analyze Genetic Circuits. In: IEEE Symposium on Computational Intelligence in Bioinformatics and Computational Biology (CIBCB), pp. 379–386 (2012)

    Google Scholar 

  133. Maler, O., Batt, G.: Approximating continuous systems by timed automata. In: Fisher, J. (ed.) FMSB 2008. LNCS (LNBI), vol. 5054, pp. 77–89. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  134. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  135. Maler, O., Nickovic, D., Pnueli, A.: Checking temporal properties of discrete, timed and continuous behaviors. In: Avron, A., Dershowitz, N., Rabinovich, A. (eds.) Pillars of Computer Science. LNCS, vol. 4800, pp. 475–505. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  136. Mateescu, R., Monteiro, P.T., Dumas, E., de Jong, H.: CTRL: Extension of CTL with regular expressions and fairness operators to verify genetic regulatory networks. Theoretical Computer Science 412(26), 2854–2883 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  137. Melham, T., Bard, J., Werner, E., Noble, D.: Conceptual foundations of systems biology. Prog. Biophys. Mol. Biol. (2012)

    Google Scholar 

  138. Merrill, D., Garland, M., Grimshaw, A.: Scalable GPU Graph Traversal. In: ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), pp. 117–128. ACM (2012)

    Google Scholar 

  139. Pelánek, R.: Fighting State Space Explosion: Review and Evaluation. In: Cofer, D., Fantechi, A. (eds.) FMICS 2008. LNCS, vol. 5596, pp. 37–52. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  140. Peled, D.: Ten years of partial order reduction. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 17–28. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  141. Phillips, A., Cardelli, L.: Efficient, correct simulation of biological processes in the stochastic π-calculus. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS (LNBI), vol. 4695, pp. 184–199. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  142. Pnueli, A.: The temporal semantics of concurrent programs. Theoretical Computer Science 13(1), 45–60 (1981)

    Article  MathSciNet  MATH  Google Scholar 

  143. Popova-Zeugmann, L., Heiner, M., Koch, I.: Time Petri Nets for Modelling and Analysis of Biochemical Networks. Fundam. Inform. 67(1-3), 149–162 (2005)

    MathSciNet  MATH  Google Scholar 

  144. Priami, C.: Algorithmic systems biology. Commun. ACM 52(5), 80–88 (2009)

    Article  Google Scholar 

  145. Regev, A., Silverman, W., Shapiro, E.Y.: Representation and Simulation of Biochemical Processes Using the π-Calculus Process Algebra. In: Pacific Symposium on Biocomputing, pp. 459–470 (2001)

    Google Scholar 

  146. Reif, J.: Depth-first Search is Inherently Sequential. Information Proccesing Letters 20(5), 229–234 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  147. Rizk, A., Batt, G., Fages, F., Soliman, S.: A general computational method for robustness analysis with applications to synthetic gene networks. Bioinformatics 25(12) (2009)

    Google Scholar 

  148. Satish, N., Harris, M., Garland, M.: Designing efficient sorting algorithms for manycore gpus. In: IEEE International Parallel & Distributed Processing Symposium (IPDPS), pp. 1–10. IEEE Computer Society (2009)

    Google Scholar 

  149. Schaub, M., Henzinger, T., Fisher, J.: Qualitative networks: a symbolic approach to analyze biological signaling networks. BMC Systems Biology 1(1), 4 (2007)

    Article  Google Scholar 

  150. Schivo, D.S., Scholma, J., Wanders, B., Urquidi Camacho, R., van der Vet, P., Karperien, H., Langerak, R., van de Pol, J., Post, J.: Modelling biological pathway dynamics with timed automata. In: IEEE International Conference on Bioinformatics and Bioengineering (ICBB), pp. 447–453. IEEE Computer Society (2012)

    Google Scholar 

  151. Schwarick, M., Heiner, M.: CSL model checking of biochemical networks with interval decision diagrams. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 296–312. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  152. Schwarick, M., Rohr, C., Heiner, M.: MARCIE - Model checking and Reachability analysis done effiCIEntly. In: Quantitative Evaluation of SysTems (QEST 2011), pp. 91–100. IEEE Computer Society (2011)

    Google Scholar 

  153. Siebert, H., Bockmayr, A.: Incorporating time delays into the logical analysis of gene regulatory networks. In: Priami, C. (ed.) CMSB 2006. LNCS (LNBI), vol. 4210, pp. 169–183. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  154. Singh, A., Hespanha, J.P.: Stochastic hybrid systems for studying biochemical processes. Physical and Engineering Sciences 368(1930), 4995–5011 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  155. Stern, U., Dill, D.L.: Parallelizing the murϕ verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 256–267. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  156. Stern, U., Dill, D.L.: Using Magnetic Disk Instead of Main Memory in the Murϕ Verifier. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 172–183. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  157. Swat, M., Kel, A., Herzel, H.: Bifurcation analysis of the regulatory modules of the mammalian G1/S transition. Bioinformatics 20(10), 1506–1511 (2004)

    Article  Google Scholar 

  158. Tarjan, R.: Depth First Search and Linear Graph Algorithms. SIAM Journal on Computing 1(2), 146–160 (1972)

    Article  MathSciNet  MATH  Google Scholar 

  159. Thomas, R.: Regulatory networks seen as asynchronous automata: A logical description. Journal of Theoretical Biology 153(1), 1–23 (1991)

    Article  Google Scholar 

  160. Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 332–344. IEEE Computer Society Press (1986)

    Google Scholar 

  161. Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press (1995)

    Google Scholar 

  162. Yang, E., van Nimwegen, E., Zavolan, M., Rajewsky, N., Schroeder, M., Magnasco, M., Darnell, J.E.: Decay Rates of Human mRNAs: Correlation With Functional Characteristics and Sequence Attributes. Genome Research 13(8), 1863–1872 (2003)

    Google Scholar 

  163. Yang, H.T., Ko, M.S.H.: Stochastic modeling for the expression of a gene regulated by competing transcription factors. PLoS ONE 7(3), e32376 (2012)

    Google Scholar 

  164. Yovine, S.: Kronos: a verification tool for real-time systems. International Journal on Software Tools for Technology Transfer 1, 123–133 (1997)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Systems Biology Laboratory at Faculty of Informatics, Masaryk University, Botanická 68a, 602 00, Brno, Czech Republic

    Luboš Brim, Milan Češka & David Šafránek

Authors
  1. Luboš Brim
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Milan Češka
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Šafránek
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Scienze di Base e Fondamenti, Università di Urbino "Carlo Bo", , ,, Piazza della Repubblica 13, 61029, Urbino, Italy

    Marco Bernardo

  2. Department of Mathematics and Computer Science, Technische Universiteit Eindhoven, Den Dolech 2, 5612 AZ, Eindhoven, The Netherlands

    Erik de Vink

  3. Dipartimento di Informatica,, Università di Verona, Ca’ Vignal 2, Strada le Grazie 15, 37134, Verona, Italy

    Alessandra Di Pierro

  4. Department of Computing, Imperial College London, Huxley Building,180 Queen’s Gate, SW7 2BZ, London, UK

    Herbert Wiklicky

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Brim, L., Češka, M., Šafránek, D. (2013). Model Checking of Biological Systems. In: Bernardo, M., de Vink, E., Di Pierro, A., Wiklicky, H. (eds) Formal Methods for Dynamical Systems. SFM 2013. Lecture Notes in Computer Science, vol 7938. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38874-3_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-38874-3_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-38873-6

  • Online ISBN: 978-3-642-38874-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation