Skip to main content
SpringerLink
Log in

BioPSy: An SMT-based Tool for Guaranteed Parameter Set Synthesis of Biological Models

  • Conference paper
  • First Online:
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

The parameter set synthesis problem consists of identifying sets of parameter values for which a given system model satisfies a desired behaviour. This paper presents BioPSy, a tool that performs guaranteed parameter set synthesis for ordinary differential equation (ODE) biological models expressed in the Systems Biology Markup Language (SBML) given a desired behaviour expressed by time-series data. Three key features of BioPSy are: (1) BioPSy computes parameter intervals, not just single values; (2) for the identified intervals the model is formally guaranteed to satisfy the desired behaviour; and (3) BioPSy can handle virtually any Lipschitz-continuous ODEs, including nonlinear ones. BioPSy is able to achieve guaranteed synthesis by utilising Satisfiability Modulo Theory (SMT) solvers to determine acceptable parameter intervals. We have successfully applied our tool to several biological models including a prostate cancer therapy model, a human starvation model, and a cell cycle model.

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

Notes

  1. 1.

    http://capd.ii.uj.edu.pl.

  2. 2.

    Data available at: http://www.nicholasbruchovsky.com/clinicalResearch.html.

References

  1. Arkin, A.: Setting the standard in synthetic biology. Nature Biotech. 26, 771–774 (2008)

    Article  Google Scholar 

  2. Asarin, E., Dang, T., Frehse, G., Girard, A., Guernic, C.L., Maler, O.: Recent progress in continuous and hybrid reachability analysis. In: IEEE Conference on Computer Aided Control System Design, pp. 1582–1587 (2006)

    Google Scholar 

  3. Balsa-Canto, E., Banga, J.R.: AMIGO, a toolbox for advanced model identification in systems biology using global optimization. Bioinformatics 27(16), 2311–2313 (2011)

    Article  Google Scholar 

  4. 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. Biol. Bioinform. 9(3), 693–705 (2012)

    Article  Google Scholar 

  5. Batt, G., Yordanov, B., Weiss, R., Belta, C.: Robustness analysis and tuning of synthetic gene networks. Bioinformatics 23(18), 2415–2422 (2007)

    Article  Google Scholar 

  6. Bruchovsky, N., Klotz, L., et al.: Final results of the Canadian prospective phase II trial of intermittent androgen suppression for men in biochemical recurrence after radiotherapy for locally advanced prostate cancer. Cancer 107, 389–395 (2006)

    Article  Google Scholar 

  7. Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Parameter synthesis with IC3. In: FMCAD, pp. 165–168. IEEE (2013)

    Google Scholar 

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

  9. Dötschel, T., Auer, E., Rauh, A., Aschemann, H.: Thermal behavior of high-temperature fuel cells: reliable parameter identification and interval-based sliding mode control. Soft Comput. 17(8), 1329–1343 (2013)

    Article  Google Scholar 

  10. Dreossi, T., Dang, T.: Parameter synthesis for polynomial biological models. In: HSCC 2014, pp. 233–242. ACM (2014)

    Google Scholar 

  11. Gao, S., Avigad, J., Clarke, E.M.: Delta-decidability over the reals. In: LICS, pp. 305–314 (2012)

    Google Scholar 

  12. Gao, S., Kong, S., Clarke, E.M.: dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 208–214. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  13. Hoops, S., Sahle, S., Gauges, R., Lee, C., Pahle, J., Simus, N., Singhal, M., Xu, L., Mendes, P., Kummer, U.: COPASI - a Complex PAthway SImulator. Bioinformatics 22(24), 3067–3074 (2006)

    Article  Google Scholar 

  14. Hucka, M., Finney, A., Sauro, H.M., et al.: The Systems Biology Markup Language (SBML): a medium for representation and exchange of biochemical network models. Bioinformatics 19(4), 524–531 (2003)

    Article  Google Scholar 

  15. Ideta, A.M., Tanaka, G., Takeuchi, T., Aihara, K.: A mathematical model of intermittent androgen suppression for prostate cancer. J. Nonlinear Sci. 18(6), 593–614 (2008)

    Article  MATH  Google Scholar 

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

  17. Kitano, H.: Foundations of Systems Biology. MIT Press, Cambridge (2001)

    Google Scholar 

  18. Li, C., et al.: BioModels Database: an enhanced, curated and annotated resource for published quantitative kinetic models. BMC Syst. Biol. 4, 92 (2010)

    Article  Google Scholar 

  19. Little, M.P., Heidenreich, W.F., Li, G.: Parameter identifiability and redundancy: theoretical considerations. PLoS ONE 5(1), e8915 (2010)

    Article  Google Scholar 

  20. Liu, B., Kong, S., Gao, S., Zuliani, P., Clarke, E.M.: Towards personalized cancer therapy using delta-reachability analysis. In: HSCC, pp. 227–232. ACM (2015)

    Google Scholar 

  21. Maiwald, T., Timmer, J.: Dynamical modeling and multi-experiment fitting with PottersWheel. Bioinformatics 24(18), 2037–2043 (2008)

    Article  Google Scholar 

  22. Meslem, N., Ramdani, N., Candau, Y.: Guaranteed parameter set estimation with monotone dynamical systems using hybrid automata. Reliable Comput. 14, 88–104 (2010)

    MathSciNet  Google Scholar 

  23. Schmidt, H., Jirstrand, M.: Systems Biology Toolbox for MATLAB: a computational platform for research in systems biology. Bioinformatics 22(4), 514–515 (2006)

    Article  Google Scholar 

  24. Song, B., Thomas, D.: Dynamics of starvation in humans. J. Math. Biol. 54(1), 27–43 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  25. Tyson, J.J.: Modeling the cell division cycle: cdc2 and cyclin interactions. Proc. Nat. Acad. Sci. 88(16), 7328–7332 (1991)

    Article  Google Scholar 

  26. Češka, M., Dannenberg, F., Kwiatkowska, M., Paoletti, N.: Precise parameter synthesis for stochastic biochemical systems. In: Mendes, P., Dada, J.O., Smallbone, K. (eds.) CMSB 2014. LNCS, vol. 8859, pp. 86–98. Springer, Heidelberg (2014)

    Google Scholar 

  27. Yordanov, B., Belta, C.: Parameter synthesis for piecewise affine systems from temporal logic specifications. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 542–555. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  28. Zi, Z., Klipp, E.: SBML-PET: a Systems Biology Markup Language-based parameter estimation tool. Bioinformatics 22(21), 2704–2705 (2006)

    Article  Google Scholar 

Download references

Acknowledgements

C. M. has been supported by the Engineering and Physical Sciences Research Council (UK) grant EP/K039083/1; F. S. has been supported by award N00014-13-1-0090 of the US Office of Naval Research.

Author information

Authors and Affiliations

  1. School of Computing Science, Newcastle University, Newcastle upon Tyne, UK

    Curtis Madsen, Fedor Shmarov & Paolo Zuliani

Authors
  1. Curtis Madsen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fedor Shmarov
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Paolo Zuliani
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Curtis Madsen .

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

Madsen, C., Shmarov, F., Zuliani, P. (2015). BioPSy: An SMT-based Tool for Guaranteed Parameter Set Synthesis of Biological Models. 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_16

Download citation

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

  • 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