Skip to main content
SpringerLink
Log in

Parameter Synthesis by Parallel Coloured CTL Model Checking

  • Conference paper
  • First Online:
Book cover Computational Methods in Systems Biology (CMSB 2015)

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

Included in the following conference series:

Abstract

We propose a new distributed-memory parallel algorithm for parameter synthesis from CTL hypotheses. The algorithm colours the state space transitions by different parameterisations and extends CTL model checking to identify the maximal set of parameters that guarantee the satisfaction of the given CTL property. We experimentally confirm good scalability of our approach and demonstrate its applicability in the case study of a genetic switch controlling decisions in the cell cycle.

This work has been partially supported by the Czech Science Foundation grant GA15-110895S and the Czech Ministry of Education, Youth, and Sport project No. CZ.1.07/2.3.00/30.0009 (Milan Češka).

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

Access this chapter

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 EPUB and 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

Institutional subscriptions

References

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

    Article  Google Scholar 

  2. Barnat, J., Brim, L., Krejci, A., Streck, A., Safranek, D., Vejnar, M., Vejpustek, T.: On parameter synthesis by parallel model checking. IEEE/ACM Trans. Comput. Bio. Bioinform. 9(3), 693–705 (2012)

    Article  Google Scholar 

  3. Barnat, J., Brim, L., Safránek, D.: High-performance analysis of biological systems dynamics with the divine model checker. Brief. Bioinform. 11(3), 301–312 (2010)

    Article  Google Scholar 

  4. Batt, G., Belta, C., Weiss, R.: Model checking liveness properties of genetic regulatory networks. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 323–338. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  5. Batt, G., Page, M., Cantone, I., Gössler, 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 

  6. Batt, G., Ropers, D., Jong, H.D., Geiselmann, J., Mateescu, R., Schneider, D.: Validation of qualitative models of genetic regulatory networks by model checking: analysis of the nutritional stress response in escherichia coli. Bioinformatics 21, 19–28 (2005)

    Article  Google Scholar 

  7. Brim, L., Češka, M., Šafránek, D.: Model checking of biological systems. In: Bernardo, M., de Vink, E., Di Pierro, A., Wiklicky, H. (eds.) SFM 2013. LNCS, vol. 7938, pp. 63–112. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  8. Brim, L., Yorav, K., Zidkova, J.: Assumption-based distribution of CTL model checking. STTT 7(1), 61–73 (2005)

    Article  Google Scholar 

  9. 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, 244–263 (1986)

    Article  MATH  Google Scholar 

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

    Google Scholar 

  11. Donaldson, R., Gilbert, D.: A model checking approach to the parameter estimation of biochemical pathways. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 269–287. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Donzé, A., Clermont, G., Langmead, C.J.: Parameter synthesis in nonlinear dynamical systems: application to systems biology. J. Comput. Biol. 17(3), 325–336 (2010)

    Article  MathSciNet  Google Scholar 

  13. Donzé, A., Fanchon, E., Gattepaille, L.M., Maler, O., Tracqui, P.: Robustness analysis and behavior discrimination in enzymatic reaction networks. PLoS ONE 6(9), e24246 (2011)

    Article  Google Scholar 

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

  15. Fröhlich, F., Theis, F.J., Hasenauer, J.: Uncertainty analysis for non-identifiable dynamical systems: profile likelihoods, bootstrapping and more. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 61–72. Springer, Heidelberg (2014)

    Google Scholar 

  16. Gábor, A., Banga, J.R.: Improved parameter estimation in kinetic models: selection and tuning of regularization methods. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 45–60. Springer, Heidelberg (2014)

    Google Scholar 

  17. Gilbert, D., Breitling, R., Heiner, M., Donaldson, R.: An introduction to biomodel engineering, illustrated for signal transduction pathways. In: Corne, D.W., Frisco, P., Păun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2008. LNCS, vol. 5391, pp. 13–28. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

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

  19. Jha, S.K., Langmead, C.J.: Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement. Theor. Comput. Sci. 412(21), 2162–2187 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  20. Jha, S., Shyamasundar, R.K.: Adapting biochemical kripke structures for distributed model checking. In: Priami, C., Ingólfsdóttir, A., Mishra, B., Riis Nielson, H. (eds.) Transactions on Computational Systems Biology VII. LNCS (LNBI), vol. 4230, pp. 107–122. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  21. Liu, B., Kong, S., Gao, S., Zuliani, P., Clarke, E.M.: Parameter synthesis for cardiac cell hybrid models using \(\delta \)-decisions. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 99–113. Springer, Heidelberg (2014)

    Google Scholar 

  22. Mittnacht, S.: Control of prb phosphorylation. Curr. Opin. Genet. Dev. 8(1), 21–27 (1998)

    Article  Google Scholar 

  23. Monteiro, P.T., Ropers, D., Mateescu, R., Freitas, A.T., de Jong, H.: Temporal logic patterns for querying qualitative models of genetic regulatory networks. In: ECAI. FAIA, vol. 178, pp. 229–233. IOS Press (2008)

    Google Scholar 

  24. Raue, A., Karlsson, J., Saccomani, M.P., Jirstrand, M., Timmer, J.: Comparison of approaches for parameter identifiability analysis of biological systems. Bioinformatics 30, 1440–1448 (2014)

    Article  Google Scholar 

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

    Article  Google Scholar 

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

Download references

Author information

Authors and Affiliations

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

    Luboš Brim, Milan Češka, Martin Demko, Samuel Pastva & 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. Martin Demko
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Samuel Pastva
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. David Šafránek
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Milan Češka .

Editor information

Editors and Affiliations

  1. École Centrale de Nantes, Nantes, France

    Olivier Roux

  2. Université de Nantes, Nantes, France

    Jérémie Bourdon

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Brim, L., Češka, M., Demko, M., Pastva, S., Šafránek, D. (2015). Parameter Synthesis by Parallel Coloured CTL Model Checking. In: Roux, O., Bourdon, J. (eds) Computational Methods in Systems Biology. CMSB 2015. Lecture Notes in Computer Science(), vol 9308. Springer, Cham. https://doi.org/10.1007/978-3-319-23401-4_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-23401-4_21

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-23400-7

  • Online ISBN: 978-3-319-23401-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation