research-article

Stochastic Model Checking of Genetic Circuits

Authors:

Nicholas Roehner,

Chris Winstead,

Chris MyersAuthors Info & Claims

ACM Journal on Emerging Technologies in Computing Systems (JETC), Volume 11, Issue 3

Article No.: 23, Pages 1 - 21

https://doi.org/10.1145/2644817

Published: 30 December 2014 Publication History

Abstract

Synthetic genetic circuits have a number of exciting potential applications such as cleaning up toxic waste, hunting and killing tumor cells, and producing drugs and bio-fuels more efficiently. When designing and analyzing genetic circuits, researchers are often interested in the probability of observing certain behaviors. Discerning these probabilities typically involves simulating the circuit to produce some time series data and computing statistics over the resulting data. However, for very rare behaviors of complex genetic circuits, it becomes computationally intractable to obtain good results as the number of required simulation runs grows exponentially. It is, therefore, necessary to apply numerical methods to determine these probabilities directly. This article describes how stochastic model checking, a method for determining the likelihood that certain events occur in a system, can by applied to models of genetic circuits by translating them into continuous-time Markov chains (CTMCs) and analyzing them using Markov chain analysis to check continuous stochastic logic (CSL) properties. The utility of this approach is demonstrated with several case studies illustrating how this method can be used to perform design space exploration of two genetic oscillators and two genetic state-holding elements. Our results show that this method results in a substantial speedup as compared with conventional simulation-based approaches.

References

[1]

J. C. Anderson, E. J. Clarke, and A. P. Arkin. 2006. Environmentally controlled invasion of cancer cells by engineering bacteria. J. Mol. Biol. 355, 619--627.

[2]

A. Arkin. 2008. Setting the standard in synthetic biology. Nature Biotech. 26, 771--774.

[3]

S. Atsumi and J. C. Liao 2008. Metabolic engineering for advanced biofuels production from Escherichia coli. Curr. Opin. Biotech. 19, 5, 414--419. Tissue, cell and pathway engineering.

[4]

A. Aziz, K. Sanwal, V. Singhal, and R. Brayton. 2000. Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic 1, 162--170.

Digital Library

[5]

J. Beal and J. Bachrach. 2008. Cells are plausible targets for high-level spatial languages. In Proceedings of the 2nd IEEE International Conference on Slef-Adaptive and Self-Organizing Systems Workshops (SASOW'08). 284--291.

Digital Library

[6]

S. Bhatia and D. Densmore. 2013. Pigeon: A design visualizer for synthetic biology. ACS Synth. Biol. 2, 6, 348--350.

[7]

L. Bilitchenko, A. Liu, S. Cheung, E. Weeding, B. Xia, M. Leguia, J. C. Anderson, and D. Densmore. 2011. Eugene - A domain specific language for specifying and constraining synthetic biological parts, devices, and systems. PLoS ONE 6, 4.

[8]

K. Burrage, M. Hegland, S. Macnamara, and R. Sidje. 2006. A Krylov-based finite state projection algorithm for solving the chemical master equation arising in the discrete modelling of biological systems. In Mam 2006: Markov Anniversary Meeting: An International Conference to Celebrate the 150th Anniversary of the birth of A.A. Markov, A. N. Langville and W. J. Stewart, Eds., Boston Books, Charleston, SC, 21--38.

[9]

Y. Cai, M. L. Wilson, and J. Peccoud. 2010. GenoCAD for iGEM: A grammatical approach to the design of standard-compliant constructs. Nucleic Acids Res. 38, 8, 2637--2644.

[10]

Y. Cao, D. T. Gillespie, and L. R. Petzold. 2006. Efficient step size selection for the tau-leaping simulation method. J. Chem. Phys. 124.

[11]

I. Cases and V. de Lorenzo. 2005. Genetically modified organisms for the environment: Stories of success and failure and what we have learned from them. Int. Microbiol. 8, 213--222.

[12]

D. Chandran, F. T. Bergmann, and H. M. Sauro. 2009. TinkerCell: Modular CAD tool for synthetic biology. J. Biol. Eng. 3, 19.

[13]

F. Ciocchetta, A. Degasperi, J. Hillston, and M. Calder. 2009. Some investigations concerning the CTMC and the ODE model derived from Bio-PEPA. Electron. Notes Theor. Computer Science 229, 1, 145--163. (Proceedings of the 2nd Workshop from Biology to Concurrency and Back (FBTC'08)).

Digital Library

[14]

M. Elowitz and S. Leibler. 2000. A synthetic oscillatory network of transcriptional regulators. Nature 403, 6767, 335--338.

[15]

D. Endy. 2005. Foundations for engineering biology. Nature 438, 449--453.

[16]

T. S. Gardner, C. R. Cantor, and J. J. Collins. 2000. Construction of a genetic toggle switch in Escherichia coli. Nature 403, 339--342.

[17]

M. Gibson and J. Bruck. 2000. Efficient exact stochastic simulation of chemical systems with many species and many channels. J. Phys. Chem. A 104, 1876--1889.

[18]

D. T. Gillespie. 1977. Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81, 25, 2340--2361.

[19]

D. T. Gillespie and L. R. Petzold. 2003. Tau leaping. J. Chem. Phys. 119, 8229--8234.

[20]

D. T. Gillespie, M. Roh, and L. R. Petzold. 2009. Refining the weighted stochastic simulation algorithm. J. Chem Phys. 130, 17.

[21]

E. M. Hahn, H. Hermanns, B. Wachter, and L. Zhang. 2009. Time-bounded model checking of infinite-state continuous-time Markov chains. Fundam. Inf. 95, 129--155.

Digital Library

[22]

T. Henzinger, M. Mateescu, and V. Wolf. 2009. Sliding window abstraction for infinite Markov chains. In Computer Aided Verification, A. Bouajjani and O. Maler, Eds., Lecture Notes in Computer Science Series, vol. 5643, Springer, Berlin/Heidelberg, 337--352.

Digital Library

[23]

A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. 2006. PRISM: A tool for automatic verification of probabilistic systems. In Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'06), H. Hermanns and J. Palsberg, Eds., Lecture Notes in Computer Science, vol. 3920, Springer, 441--444.

Digital Library

[24]

J.-P. Katoen, D. Klink, M. Leucker, and V. Wolf. 2012. Three-valued abstraction for probabilistic systems. J. Log. Algebr. Program. 81, 4, 356--389.

[25]

H. Kuwahara. 2007. Model abstraction and temporal behavior analysis of genetic regulatory networks. Ph.D. thesis, U. of Utah.

Digital Library

[26]

H. Kuwahara, C. Madsen, I. Mura, C. Myers, A. Tejada, and C. Winstead. 2010. Efficient stochastic simulation to analyze targeted properties of biological systems. In Stochastic Control, C. Myers, Ed., Sciyo, 505--532.

[27]

H. Kuwahara and I. Mura. 2008. An efficient and exact stochastic simulation method to analyze rare events in biochemical systems. J. Chem. Phys. 129, 16.

[28]

H. Kuwahara, C. Myers, N. Barker, M. Samoilov, and A. Arkin. 2006. Automated abstraction methodology for genetic regulatory networks. Trans. Comp. Syst. Biol. VI, 150--175.

Digital Library

[29]

M. Kwiatkowska, G. Norman, and D. Parker 2007. Stochastic model checking. In Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM'07), M. Bernardo and J. Hillston, Eds., Lecture Notes in Computer Science (Tutorial Volume), vol. 4486, Springer, 220--270.

Digital Library

[30]

C. Madsen. 2013. Stochastic analysis of synthetic genetic circuits. Ph.D. thesis, University of Utah.

[31]

M. A. Marchisio and J. Stelling. 2008. Computational design of synthetic gene circuits with composable parts. Bioinform. 24, 17, 1903--1910.

Digital Library

[32]

M. A. Marchisio and J. Stelling. 2011. Automatic design of digital synthetic gene circuits. PLoS Comput. Biol. 7, 2.

[33]

H. H. McAdams and A. Arkin. 1999. Genetic regulation at the nanomolar scale: It's a noisy business. Trends Genet. 15, 2, 65--69.

[34]

D. E. Muller and W. S. Bartky. 1959. A theory of asynchronous circuits. In Proceedings of the International Symposium on the Theory of Switching. Harvard University Press, Cambridge, MA, 204--243.

[35]

B. Munsky and M. Khammash. 2006. The finite state projection algorithm for the solution of the chemical master equation. J. Chem. Phys. 124, 4.

[36]

C. J. Myers. 2009. Engineering Genetic Circuits. Chapman and Hall/CRC.

[37]

C. J. Myers, N. Barker, K. Jones, H. Kuwahara, C. Madsen, and N.-P. D. Nguyen. 2009. iBioSim: A tool for the analysis and design of genetic circuits. Bioinform. 25, 21, 2848--2849.

Digital Library

[38]

N. Nguyen, C. Myers, H. Kuwahara, C. Winstead, and J. Keener. 2010. Design and analysis of a robust genetic Muller C-element. J. Theoret. Biol. 264, 2, 174--187.

[39]

M. Pedersen and A. Phillips. 2009. Towards programming languages for genetic engineering of living cells. J. Roy. Soc. Interface 6, (Suppl. 4), S437--S450.

[40]

W. H. Press, B. P. Flannery, S. A. Teukolsky, and W. T. Vetterling. 1992. Numerical Recipes in C: The Art of Scientific Computing, 2nd ed. Cambridge University Press.

Digital Library

[41]

J. Quinn, J. Beal, S. Bhatia, P. Cai, J. Chen, K. Clancy, N. J. Hillson, M. Galdzicki, A. Maheshwari, P. Umesh, M. Pocock, C. Rodriguez, G.-B. Stan, and D. Endy. 2013. Synthetic biology open language visual (SBOL Visual), Version 1.0.0. BBF RFC 93.

[42]

C. V. Rao and A. P. Arkin. 2003. Stochastic chemical kinetics and the quasi-steady-state assumption: Application to the gillespie algorithm. J. Phys. Chem. 118, 11.

[43]

D.-K. Ro, E. M. Paradise, M. Ouellet, K. J. Fisher, K. L. Newman, J. M. Ndungu, K. A. Ho, R. A. Eachus, T. S. Ham, J. Kirby, M. C. Y. Chang, S. T. Withers, Y. Shiba, R. Sarpong, and J. D. Keasling. 2006. Production of the antimalarial drug percursor artemisinic acid in engineered yeast. Nature 440.

[44]

A. Slepoy, A. P. Thompson, and S. J. Plimpton. 2008. A constant-time kinetic monte carlo algorithm for simulation of large biochemical reaction networks. J. Chem. Phys. 128, 20, 205101.

[45]

W. J. Stewart. 1994. Introduction to the Numerical Solution of Markov Chains. Priceton University Press, Princeton, NJ.

[46]

J. Stricker, S. Cookson, M. Bennett, W. Mather, L. Tsimring, and J. Hasty. 2008. A fast, robust and tunable synthetic gene oscillator. Nature 456, 516--519.

[47]

S. H. Strogatz. 1994. Nonlinear Dynamics and Chaos: With Applications to Physics, Biology, Chemistry and Engineering. Westview Press.

[48]

D. Thieffry and R. Thomas. 1995. Dynamical behaviour of biological networks: Immunity control in bacteriophage lamabda. Bull. Math. Biol. 57, 2, 277--297.

[49]

R. Thomas. 1991. Regulatory metworks seen as asynchronous automata: A logical description. J. Theoret. Biol. 153, 1--23.

[50]

J. Tyson and H. Othmer. 1978. The dynamics of feedback control circuits in biochemical pathways. Prog. Theoret. Biol. 5, 1--62.

[51]

P. Waage and C. M. Guldberg. 1864. Studies concerning affinity. Forhandlinger: Videnskabs - Selskabet i Christinia 35.

[52]

C. Winstead, C. Madsen, and C. J. Myers. 2010. iSSA: An incremental stochastic simulation algorithm for genetic circuits. In Proceedings of the International Symposium on Circuits and Systems (ISCAS). IEEE, 553--556.

[53]

B. Yordanov, J. Tumova, C. Belta, I. Cerna, and J. Barnat. 2010. Formal analysis of piecewise affine systems through formula-guided refinement. In Proceedings of the 49th IEEE Conference on Decision and Control (CDC). 5899--5904.

[54]

H. Younes, M. Kwiatkowska, G. Norman, and D. Parker. 2006. Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Tech. Trans. (STTT) 8, 216--228.

Digital Library

Cited By

Andriushchenko RBork ABudde CČeška MGrover KHahn EHartmanns AIsraelsen BJansen NJeppson JJunges SKöhl MKönighofer BKřetínský JMeggendorfer TParker DPranger SQuatmann TRuijters ETaylor LVolk MWeininger MZhang Z(2024)Tools at the Frontiers of Quantitative VerificationTOOLympics Challenge 202310.1007/978-3-031-67695-6_4(90-146)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_4
Jeppson JVolk MIsraelsen BRoberts RWilliams ABuecherl LMyers CZheng HWinstead CZhang Z(2023)STAMINA in C++: Modernizing an Infinite-State Probabilistic Model CheckerQuantitative Evaluation of Systems10.1007/978-3-031-43835-6_7(101-109)Online publication date: 15-Sep-2023
https://doi.org/10.1007/978-3-031-43835-6_7
Nguyen TJones TFontanarrosa PMante JZundel ZDensmore DMyers C(2019)Design of Asynchronous Genetic CircuitsProceedings of the IEEE10.1109/JPROC.2019.2916057107:7(1356-1368)Online publication date: Jul-2019
https://doi.org/10.1109/JPROC.2019.2916057
Show More Cited By

Recommendations

Genetic Algorithm for Generating Counterexample in Stochastic Model Checking
ICNCC '18: Proceedings of the 2018 VII International Conference on Network, Communication and Computing

Counterexamples are the most effective feature to convince system engineers about the value of formal verification. Generating the smallest counterexample in stochastic model checking has been proved to be NP-complete. In this paper, we apply the ...
CSRL model checking with closed-form bounding distributions
ValueTools '08: Proceedings of the 3rd International Conference on Performance Evaluation Methodologies and Tools

Continuous Stochastic Logic (CSL) which lets to express real time probabilistic properties on Continuous Time Markov Chains (CTMC) has been augmented by reward structures to check also performability measures. Thus Continuous Stochastic Reward Logic (...
Fluid model checking
CONCUR'12: Proceedings of the 23rd international conference on Concurrency Theory

In this paper we investigate a potential use of fluid approximation techniques in the context of stochastic model checking of CSL formulae. We focus on properties describing the behaviour of a single agent in a (large) population of agents, exploiting a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Journal on Emerging Technologies in Computing Systems

ACM Journal on Emerging Technologies in Computing Systems Volume 11, Issue 3

Special Issue on Computational Synthetic Biology and Regular Papers

December 2014

219 pages

ISSN:1550-4832

EISSN:1550-4840

DOI:10.1145/2711453

Editor:
Krishnendu Chakrabarty
Duke University, USA

Issue’s Table of Contents

Copyright © 2014 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 30 December 2014

Accepted: 01 July 2014

Revised: 01 July 2014

Received: 01 January 2014

Published in JETC Volume 11, Issue 3

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

National Science Foundation

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
311
Total Downloads

Downloads (Last 12 months)16
Downloads (Last 6 weeks)1

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Andriushchenko RBork ABudde CČeška MGrover KHahn EHartmanns AIsraelsen BJansen NJeppson JJunges SKöhl MKönighofer BKřetínský JMeggendorfer TParker DPranger SQuatmann TRuijters ETaylor LVolk MWeininger MZhang Z(2024)Tools at the Frontiers of Quantitative VerificationTOOLympics Challenge 202310.1007/978-3-031-67695-6_4(90-146)Online publication date: 26-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-67695-6_4
Jeppson JVolk MIsraelsen BRoberts RWilliams ABuecherl LMyers CZheng HWinstead CZhang Z(2023)STAMINA in C++: Modernizing an Infinite-State Probabilistic Model CheckerQuantitative Evaluation of Systems10.1007/978-3-031-43835-6_7(101-109)Online publication date: 15-Sep-2023
https://doi.org/10.1007/978-3-031-43835-6_7
Nguyen TJones TFontanarrosa PMante JZundel ZDensmore DMyers C(2019)Design of Asynchronous Genetic CircuitsProceedings of the IEEE10.1109/JPROC.2019.2916057107:7(1356-1368)Online publication date: Jul-2019
https://doi.org/10.1109/JPROC.2019.2916057
Neupane TMyers CMadsen CZheng HZhang Z(2019)STAMINA: STochastic Approximate Model-Checker for INfinite-State AnalysisComputer Aided Verification10.1007/978-3-030-25540-4_31(540-549)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25540-4_31
Neupane TZhang ZMadsen CZheng HMyers C(2019)Approximation Techniques for Stochastic Analysis of Biological SystemsAutomated Reasoning for Systems Biology and Medicine10.1007/978-3-030-17297-8_12(327-348)Online publication date: 12-Jun-2019
https://doi.org/10.1007/978-3-030-17297-8_12
Watanabe LBarhak JMyers C(2018)Toward reproducible disease models using the Systems Biology Markup LanguageSIMULATION10.1177/0037549718793214(003754971879321)Online publication date: 6-Sep-2018
https://doi.org/10.1177/0037549718793214
Watanabe LNguyen TZhang MZundel ZZhang ZMadsen CRoehner NMyers C(2018) i B io S im 3: A Tool for Model-Based Genetic Circuit Design ACS Synthetic Biology10.1021/acssynbio.8b000788:7(1560-1563)Online publication date: 26-Jun-2018
https://doi.org/10.1021/acssynbio.8b00078
Myers CBeal JGorochowski TKuwahara HMadsen CMcLaughlin JMısırlı GNguyen TOberortner ESamineni MWipat AZhang MZundel Z(2017)A standard-enabled workflow for synthetic biologyBiochemical Society Transactions10.1042/BST2016034745:3(793-803)Online publication date: 15-Jun-2017
https://doi.org/10.1042/BST20160347
Katoen JKoskinen EGrohe MShankar N(2016)The Probabilistic Model Checking LandscapeProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/2933575.2934574(31-45)Online publication date: 5-Jul-2016
https://dl.acm.org/doi/10.1145/2933575.2934574
Myers C(2015)Computational Synthetic Biology: Progress and the Road AheadIEEE Transactions on Multi-Scale Computing Systems10.1109/TMSCS.2015.24784421:1(19-32)Online publication date: 1-Jan-2015
https://doi.org/10.1109/TMSCS.2015.2478442

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents