nach oben

Acta Informatica

Erschienen in:

28.03.2016 | Original Article

Precise parameter synthesis for stochastic biochemical systems

verfasst von: Milan Češka, Frits Dannenberg, Nicola Paoletti, Marta Kwiatkowska, Luboš Brim

Erschienen in: Acta Informatica | Ausgabe 6/2017

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We consider the problem of synthesising rate parameters for stochastic biochemical networks so that a given time-bounded CSL property is guaranteed to hold, or, in the case of quantitative properties, the probability of satisfying the property is maximised or minimised. Our method is based on extending CSL model checking and standard uniformisation to parametric models, in order to compute safe bounds on the satisfaction probability of the property. We develop synthesis algorithms that yield answers that are precise to within an arbitrarily small tolerance value. The algorithms combine the computation of probability bounds with the refinement and sampling of the parameter space. Our methods are precise and efficient, and improve on existing approximate techniques that employ discretisation and refinement. We evaluate the usefulness of the methods by synthesising rates for three biologically motivated case studies: infection control for a SIR epidemic model; reliability analysis of molecular computation by a DNA walker; and bistability in the gene regulation of the mammalian cell cycle.

Vorheriger Artikel Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

In [9], a linear-time specification equivalent to \(\phi \) is given.

In [42], we believe that there is a typo in the figure illustrating bistability (Figure 2B). The range of \(\phi _{pRB}\) (corresponding to \(\gamma _A)\) should read 0.005–0.035.

Abate, A., Brim, L., Češka, M., Kwiatkowska, M.: Adaptive aggregation of markov chains: quantitative analysis of chemical reaction networks. In: Kroening, D., Păsăreanu, C.S. (eds.) Computer Aided Verification (CAV), LNCS, vol. 9206, pp. 195–213. Springer (2015)

Andreychenko, A., Mikeev, L., Spieler, D., Wolf, V.: Parameter identification for Markov models of biochemical reactions. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification (CAV), LNCS, pp. 83–98. Springer (2011)

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

Baier, C., Haverkort, B., Hermanns, H., Katoen, J.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans Softw Eng 29(6), 524–541 (2003)CrossRefMATH

Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Gupta, A., Henzinger, T.A. (eds.) Computational Methods in Systems Biology (CMSB), pp. 164–177. Springer (2013)

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

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

Billingsley, P.: Probability and Measure. Wiley, Hoboken (2008)MATH

Bortolussi, L., Milios, D., Sanguinetti, G.: Smoothed model checking for uncertain continuous time markov chains. CoRR. arXiv:1402.1450 (2014)

10.

Bortolussi, L., Sanguinetti, G.: Learning and designing stochastic processes from logical constraints. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) Quantitative Evaluation of Systems (QEST), LNCS, vol. 8054, pp. 89–105. Springer (2013)

11.

Brim, L., Češka, M., Dražan, S., Šafránek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification (CAV), LNCS, vol. 8044, pp. 107–123. Springer (2013)

12.

Caron, R., Traynor, T.: The zero set of a polynomial. Technical report, University of Windsor (2005)

13.

Č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.) Computational Methods in Systems Biology (CMSB), pp. 86–98. Springer (2014)

14.

Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: Theoretical Aspects of Software Engineering (TASE), pp. 85–92. IEEE (2013)

15.

Courant, R., John, F.: Introduction to Calculus and Analysis, vol. 2. Springer, Berlin (2012)MATH

16.

Dannenberg, F., Hahn, E.M., Kwiatkowska, M.: Computing cumulative rewards using fast adaptive uniformisation. In: Gupta, A., Henzinger, T.A. (eds.) Computational Methods in Systems Biology (CMSB), LNCS, vol. 8130, pp. 33–49. Springer (2013)

17.

Dannenberg, F., Kwiatkowska, M., Thachuk, C., Turberfield, A.: DNA walker circuits: computational potential, design, and verification. Nat. Comput. 14, 195–211 (2014)MathSciNetCrossRefMATH

18.

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

19.

Fox, B.L., Glynn, P.W.: Computing Poisson probabilities. CACM 31(4), 440–445 (1988)

20.

Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81(25), 2340–2381 (1977)CrossRef

21.

Grassmann, W.: Transient solutions in Markovian queueing systems. Comput. Oper. Res. 4(1), 47–53 (1977)CrossRef

22.

Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transf. (STTT) 13(1), 3–19 (2011)CrossRef

23.

Han, T., Katoen, J., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: Real-Time Systems Symposium (RTSS), pp. 173–182. IEEE (2008)

24.

Jensen, A.: Markoff chains as an aid in the study of Markoff processes. Skand. Aktuarietidskr. 36, 87–91 (1953)MathSciNetMATH

25.

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

26.

Katoen, J.P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time markov chains. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification (CAV), LNCS, vol. 4590, pp. 311–324. Springer (2007)

27.

Kermack, W., McKendrick, A.: Contributions to the mathematical theory of epidemicsii. The problem of endemicity. Bull. Math. Biol. 53(1), 57–87 (1991)

28.

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.) Computational Methods in Systems Biology (CMSB), pp. 207–226. Springer (2012)

29.

Koksal, A.S., Pu, Y., Srivastava, S., Bodik, R., Fisher, J., Piterman, N.: Synthesis of biological models from mutation experiments. SIGPLAN Not. 48(1), 469–482 (2013)CrossRefMATH

30.

Kwiatkowska, M., Norman, G., Pacheco, A.: Model checking expected time and expected reward formulae with random time bounds. Comput. Math. Appl. 51, 305–316 (2006)MathSciNetCrossRefMATH

31.

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

32.

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 (2011)

33.

Madsen, C., Myers, C., Roehner, N., Winstead, C., Zhang, Z.: Utilizing stochastic model checking to analyze genetic circuits. In: Computational Intelligence in Bioinformatics and Computational Biology (CIBCB), pp. 379–386. IEEE (2012)

34.

Mateescu, M., Wolf, V., Didier, F., Henzinger, T.A.: Fast adaptive uniformization of the chemical master equation. IET Syst. Biol. 4(6), 441–452 (2010)CrossRef

35.

Michaelis, L., Menten, M.L.: Die kinetik der invertinwirkung. Biochem. z 49(333–369), 352 (1913)

36.

Paoletti, N., Yordanov, B., Hamadi, Y., Wintersteiger, C.M., Kugler, H.: Analyzing and synthesizing genomic logic functions. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification (CAV), pp. 343–357. Springer (2014)

37.

Rao, C.V., Arkin, A.P.: Stochastic chemical kinetics and the quasi-steady-state assumption: application to the gillespie algorithm. J. Chem. Phys. 118(11), 4999–5010 (2003)CrossRef

38.

Reibman, A.: Numerical transient analysis of Markov models. Comput. Oper. Res. 15(1), 19–36 (1988)CrossRefMATH

39.

Sanft, K.R., Gillespie, D.T., Petzold, L.R.: Legitimacy of the stochastic Michaelis-Menten approximation. Syst. Biol., IET 5(1), 58–69 (2011)

40.

Sassi, B., Amin, M., Girard, A.: Control of polynomial dynamical systems on rectangles. In: European Control Conference (ECC), pp. 658–663. IEEE (2013)

41.

Sen, K., Viswanathan, M., Agha, G.: Model-checking markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, vol. 3920, pp. 394–410. Springer (2006)

42.

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

43.

Wickham, S.F.J., Bath, J., Katsuda, Y., Endo, M., Hidaka, K., Sugiyama, H., Turberfield, A.J.: A DNA-based molecular motor that can navigate a network of tracks. Nat. Nanotechnol. 7, 169–173 (2012)CrossRef

44.

Zhang, J., Watson, L.T., Cao, Y.: Adaptive aggregation method for the chemical master equation. Int. J. Comput. Biol. Drug Des. 2(2), 134–148 (2009)CrossRef

Titel: Precise parameter synthesis for stochastic biochemical systems
verfasst von: Milan Češka
Frits Dannenberg
Nicola Paoletti
Marta Kwiatkowska
Luboš Brim
Publikationsdatum: 28.03.2016
Verlag: Springer Berlin Heidelberg
Erschienen in: Acta Informatica / Ausgabe 6/2017
Print ISSN: 0001-5903
Elektronische ISSN: 1432-0525
DOI: https://doi.org/10.1007/s00236-016-0265-2

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"