zbMATH — the first resource for mathematics

Verifying chemical reaction network implementations: a pathway decomposition approach. (English) Zbl 1423.68292
Summary: The emerging fields of genetic engineering, synthetic biology, DNA computing, DNA nanotechnology, and molecular programming herald the birth of a new information technology that acquires information by directly sensing molecules within a chemical environment, stores information in molecules such as DNA, RNA, and proteins, processes that information by means of chemical and biochemical transformations, and uses that information to direct the manipulation of matter at the nanometer scale. To scale up beyond current proof-of-principle demonstrations, new methods for managing the complexity of designed molecular systems will need to be developed. Here we focus on the challenge of verifying the correctness of molecular implementations of abstract chemical reaction networks, where operation in a well-mixed “soup” of molecules is stochastic, asynchronous, concurrent, and often involves multiple intermediate steps in the implementation, parallel pathways, and side reactions. This problem relates to the verification of Petri nets, but existing approaches are not sufficient for providing a single guarantee covering an infinite set of possible initial states (molecule counts) and an infinite state space potentially explored by the system given any initial state. We address these issues by formulating a new theory of pathway decomposition that provides an elegant formal basis for comparing chemical reaction network implementations, and we present an algorithm that computes this basis. Our theory naturally handles certain situations that commonly arise in molecular implementations, such as what we call “delayed choice,” that are not easily accommodated by other approaches. We further show how pathway decomposition can be combined with weak bisimulation to handle a wider class that includes most currently known enzyme-free DNA implementation techniques. We anticipate that our notion of logical equivalence between chemical reaction network implementations will be valuable for other molecular implementations such as biochemical enzyme systems, and perhaps even more broadly in concurrency theory.

68Q60 Specification and verification (program logics, model checking, etc.)
68Q05 Models of computation (Turing machines, etc.) (MSC2010)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
92C40 Biochemistry, molecular biology
ABC; BioNetGen; SPIN
Full Text: DOI
[1] Ackermann, Jörg; Einloft, Jens; Nöthen, Joachim; Koch, Ina, Reduction techniques for network validation in systems biology, J. Theoret. Biol., 315, 71-80, (2012) · Zbl 1397.92247
[2] Badelt, Stefan; Shin, Seung Woo; Johnson, Robert F.; Dong, Qing; Thachuk, Chris; Winfree, Erik, A general-purpose CRN-to-DSD compiler with formal verification, optimization, and simulation capabilities, (Brijder, Robert; Qian, Lulu, DNA Computing and Molecular Programming. DNA Computing and Molecular Programming, Lecture Notes in Computer Science (LNCS), vol. 10467, (2017), Springer), 232-248 · Zbl 06833544
[3] Behr, Nicolas; Danos, Vincent; Garnier, Ilias, Stochastic mechanics of graph rewriting, (Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, (2016), ACM), 46-55 · Zbl 1401.68132
[4] Brayton, Robert; Mishchenko, Alan, ABC: an academic industrial-strength verification tool, (Computer Aided Verification, (2010), Springer), 24-40
[5] Buchholz, Peter, Bisimulation relations for weighted automata, Theoret. Comput. Sci., 393, 109-123, (2008) · Zbl 1136.68032
[6] Cardelli, Luca, Strand algebras for DNA computing, Nat. Comput., 10, 407-428, (2011) · Zbl 1221.68164
[7] Cardelli, Luca, Two-domain DNA strand displacement, Math. Structures Comput. Sci., 23, 247-271, (2013) · Zbl 1271.68105
[8] Cardelli, Luca, Morphisms of reaction networks that couple structure to function, BMC Syst. Biol., 8, 84, (2014)
[9] Chen, Yuan-Jyue; Dalchau, Neil; Srinivas, Niranjan; Phillips, Andrew; Cardelli, Luca; Soloveichik, David; Seelig, Georg, Programmable chemical controllers made from DNA, Nat. Nanotechnol., 8, 755-762, (2013)
[10] Condon, Anne; Hu, Alan J.; Maňuch, Ján; Thachuk, Chris, Less haste, less waste: on recycling and its limits in strand displacement systems, Interface Focus, 2, 512-521, (2012) · Zbl 1347.68132
[11] Danos, Vincent; Feret, Jérôme; Fontana, Walter; Harmer, Russell; Krivine, Jean, Rule-based modelling of cellular signalling, (Caires, Luís; Vasconcelos, Vasco T., International Conference on Concurrency Theory. International Conference on Concurrency Theory, CONCUR 2007. International Conference on Concurrency Theory. International Conference on Concurrency Theory, CONCUR 2007, Lecture Notes in Computer Science, vol. 4703, (2007), Springer), 17-41 · Zbl 1151.68723
[12] Danos, Vincent; Krivine, Jean, Transactions in RCCS, (Proc. of CONCUR. Proc. of CONCUR, LNCS, vol. 3653, (2005), Springer), 398-412 · Zbl 1134.68432
[13] Dong, Qing, A Bisimulation Approach to Verification of Molecular Implementations of Formal Chemical Reaction Networks, (2012), Stony Brook University, Master’s thesis
[14] Douglas, Shawn M.; Bachelet, Ido; Church, George M., A logic-gated nanorobot for targeted transport of molecular payloads, Science, 335, 831-834, (2012)
[15] Doye, Jonathan P. K.; Ouldridge, Thomas E.; Louis, Ard A.; Romano, Flavio; Šulc, Petr; Matek, Christian; Snodin, Benedict E. K.; Rovigatti, Lorenzo; Schreck, John S.; Harrison, Ryan M.; Smith, William P. J., Coarse-graining DNA for simulations of DNA nanotechnology, Phys. Chem. Chem. Phys., 15, 20395-20414, (2013)
[16] Esparza, Javier; Nielsen, Mogens, Decidability issues for Petri nets, Petri Nets Newsl., 94, 5-23, (1994) · Zbl 0791.68123
[17] Faeder, James R.; Blinov, Michael L.; Hlavacek, William S., Rule-based modeling of biochemical systems with BioNetGen, Methods Mol. Biol., 500, 113-167, (2009)
[18] Grun, Casey; Sarma, Karthik; Wolfe, Brian; Shin, Seung Woo; Winfree, Erik, A domain-level DNA strand displacement reaction enumerator allowing arbitrary non-pseudoknotted secondary structures, (Verification of Engineered Molecular Devices and Programs (VEMDP), (2014)), (2015), Originally appeared
[19] Gu, Hongzhou; Chao, Jie; Xiao, Shou-Jun; Seeman, Nadrian C., A proximity-based programmable DNA nanoscale assembly line, Nature, 465, 202-205, (2010)
[20] Heiner, Monika; Gilbert, David; Donaldson, Robin, Petri nets for systems and synthetic biology, Lecture Notes in Comput. Sci., 5016, 215-264, (2008)
[21] Holzmann, Gerard J., The model checker SPIN, IEEE Trans. Softw. Eng., 23, 279-295, (1997)
[22] Jančar, Petr; Esparza, Javier; Moller, Faron, Petri nets and regular processes, J. Comput. System Sci., 59, 476-503, (1999) · Zbl 0958.68121
[23] Johnson, Robert F.; Dong, Qing; Winfree, Erik, Verifying chemical reaction network implementations: a bisimulation approach, (Rondelez, Yannick; Woods, Damien, DNA Computing and Molecular Programming. DNA Computing and Molecular Programming, Lecture Notes in Computer Science (LNCS), vol. 9818, (2016), Springer), 114-134 · Zbl 1423.68287
[24] Kim, Jongmin; White, Kristin S.; Winfree, Erik, Construction of an in vitro bistable circuit from synthetic transcriptional switches, Mol. Syst. Biol., 2, 68, (2006)
[25] Matthew R. Lakin, Andrew Phillips, Visual DSD, Microsoft Research.
[26] Lakin, Matthew R.; Stefanovic, Darko; Phillips, Andrew, Modular verification of chemical reaction network encodings via serializability analysis, Theoret. Comput. Sci., 632, 21-42, (2016) · Zbl 1339.92105
[27] Leroy, Xavier, Formal verification of a realistic compiler, Commun. ACM, 52, 107-115, (2009)
[28] Lipton, Richard, The Reachability Problem Requires Exponential Space, (1976), Department of Computer Science, Yale University: Department of Computer Science, Yale University New Haven, Connecticut, Research Report 62
[29] Mayr, Ernst, Persistence of vector replacement systems is decidable, Acta Inform., 15, 309-318, (1981) · Zbl 0454.68048
[30] Milner, Robin, Communication and Concurrency, (1989), Prentice Hall · Zbl 0683.68008
[31] Montagne, Kevin; Plasson, Raphael; Sakai, Yasuyuki; Fujii, Teruo; Rondelez, Yannick, Programming an in vitro DNA oscillator using a molecular networking strategy, Mol. Syst. Biol., 7, 466, (2011)
[32] Qian, Lulu; Soloveichik, David; Winfree, Erik, Efficient Turing-universal computation with DNA polymers, (Sakakibara, Yasubumi; Mi, Yongli, DNA Computing and Molecular Programming. DNA Computing and Molecular Programming, Lecture Notes in Computer Science (LNCS), vol. 6518, (2011)), 123-140 · Zbl 1309.68071
[33] Rival, Xavier, Symbolic transfer function-based approaches to certified compilation, (Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’04, (2004), ACM: ACM New York, NY, USA), 1-13 · Zbl 1325.68070
[34] Schaeffer, Joseph, Stochastic Simulation of the Kinetics of Multiple Interacting Nucleic Acid Strands, (2013), California Institute of Technology, PhD thesis · Zbl 1403.92222
[35] Schnoebelen, Philippe; Sidorova, Natalia, Bisimulation and the reduction of Petri nets, Lecture Notes in Comput. Sci., 1825, 409-423, (2000) · Zbl 0986.68074
[36] Shin, Seung Woo, Compiling and Verifying DNA-Based Chemical Reaction Network Implementations, (2011), California Institute of Technology, Master’s thesis
[37] Soloveichik, David; Seelig, Georg; Winfree, Erik, DNA as a universal substrate for chemical kinetics, Proc. Natl. Acad. Sci., 107, 5393-5398, (2010)
[38] Thachuk, Chris; Condon, Anne, Space and energy efficient computation with DNA strand displacement systems, (Stefanovic, Darko; Turberfield, Andrew, DNA Computing and Molecular Programming. DNA Computing and Molecular Programming, Lecture Notes in Computer Science (LNCS), vol. 7433, (2012), Springer), 135-149 · Zbl 1372.68105
[39] Thorsley, David; Klavins, Eric, Model reduction of stochastic processes using Wasserstein pseudometrics, (American Control Conference, (2008)), 1374-1381
[40] Thorsley, David; Klavins, Eric, Approximating stochastic biochemical processes with Wasserstein pseudometrics, IET Syst. Biol., 4, 193-211, (2010)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.