1
|
Konur S, Gheorghe M, Krasnogor N. Verifiable biology. J R Soc Interface 2023; 20:20230019. [PMID: 37160165 PMCID: PMC10169095 DOI: 10.1098/rsif.2023.0019] [Citation(s) in RCA: 0] [Impact Index Per Article: 0] [Reference Citation Analysis] [Abstract] [Key Words] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 05/11/2023] Open
Abstract
The formalization of biological systems using computational modelling approaches as an alternative to mathematical-based methods has recently received much interest because computational models provide a deeper mechanistic understanding of biological systems. In particular, formal verification, complementary approach to standard computational techniques such as simulation, is used to validate the system correctness and obtain critical information about system behaviour. In this study, we survey the most frequently used computational modelling approaches and formal verification techniques for computational biology. We compare a number of verification tools and software suites used to analyse biological systems and biochemical networks, and to verify a wide range of biological properties. For users who have no expertise in formal verification, we present a novel methodology that allows them to easily apply formal verification techniques to analyse their biological or biochemical system of interest.
Collapse
Affiliation(s)
- Savas Konur
- Department of Computer Science, University of Bradford, Richmond Building, Bradford BD7 1DP, UK
| | - Marian Gheorghe
- Department of Computer Science, University of Bradford, Richmond Building, Bradford BD7 1DP, UK
| | - Natalio Krasnogor
- School of Computing Science, Newcastle University, Science Square, Newcastle upon Tyne NE4 5TG, UK
| |
Collapse
|
2
|
Sanjabi M, Jahanian A. Analytical design of multi-threshold and high fan-in DNA-based logical sensors to profile the pattern of MS microRNAs. Biomed Eng Lett 2021; 11:131-145. [PMID: 34150349 PMCID: PMC8155178 DOI: 10.1007/s13534-021-00186-9] [Citation(s) in RCA: 0] [Impact Index Per Article: 0] [Reference Citation Analysis] [Abstract] [Key Words] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Received: 09/05/2020] [Revised: 01/04/2021] [Accepted: 02/10/2021] [Indexed: 11/25/2022] Open
Abstract
Early detection of diseases is very important to increase the life quality and reduce the treatment cost for the patient. MicroRNAs have been introduced in recent years as an efficient class of biomarkers for detecting the risky situation of many diseases such as cancers, Multiple sclerosis (MS), and heart attacks, and other diseases. Now, real-time PCR has been used to profile the microRNA expression, which is expensive, time-consuming, and has low accuracy. Most recently, DNA logic gates are used to detect the MicroRNA expression level that is more accurate and faster than previous methods. In this paper, we improved the design of multi-threshold and multi-input DNA-based logic gates in response to specific microRNA (miRNA) inputs. The proposed design style can simultaneously recognize multiple miRNAs with different rising and falling thresholds. The proposed structure in this paper is used to diagnose Multiple Sclerosis (MS) as a case study. We simulated this system to understand its performance and compare it with other existing methods. The simulation results show the efficiency of the proposed method in terms of accuracy, efficiency, and speed. In this analysis, unwanted reactions, fault positive, and the probability of generating the final output using the formal method are investigated in depth. Finally, the proposed solutions are improved based on the results of these analyses. The analytic approach of this paper helps to design the DNA-based logic gates for real diseases.
Collapse
Affiliation(s)
- Mercedeh Sanjabi
- Faculty of Computer Science and Engineering, Shahid Beheshti University, Tehran, Iran
| | - Ali Jahanian
- Faculty of Computer Science and Engineering, Shahid Beheshti University, Tehran, Iran
| |
Collapse
|
3
|
Henglein F, Shoham S, Vizel Y. Formal Semantics and Verification of Network-Based Biocomputation Circuits. LECTURE NOTES IN COMPUTER SCIENCE 2021. [PMCID: PMC7798404 DOI: 10.1007/978-3-030-67067-2_21] [Citation(s) in RCA: 2] [Impact Index Per Article: 0.7] [Reference Citation Analysis] [Abstract] [Track Full Text] [Download PDF] [Figures] [Subscribe] [Scholar Register] [Indexed: 11/25/2022]
Abstract
Network-Based Biocomputation Circuits (NBCs) offer a new paradigm for solving complex computational problems by utilizing biological agents that operate in parallel to explore manufactured planar devices. The approach can also have future applications in diagnostics and medicine by combining NBCs computational power with the ability to interface with biological material. To realize this potential, devices should be designed in a way that ensures their correctness and robust operation. For this purpose, formal methods and tools can offer significant advantages by allowing investigation of design limitations and detection of errors before manufacturing and experimentation. Here we define a computational model for NBCs by providing formal semantics to NBC circuits. We present a formal verification-based approach and prototype tool that can assist in the design of NBCs by enabling verification of a given design’s correctness. Our tool allows verification of the correctness of NBC designs for several NP-Complete problems, including the Subset Sum, Exact Cover and Satisfiability problems and can be extended to other NBC implementations. Our approach is based on defining transition systems for NBCs and using temporal logic for specifying and proving properties of the design using model checking. Our formal model can also serve as a starting point for computational complexity studies of the power and limitations of NBC systems.
Collapse
|
4
|
Lakin MR, Phillips A. Domain-Specific Programming Languages for Computational Nucleic Acid Systems. ACS Synth Biol 2020; 9:1499-1513. [PMID: 32589838 DOI: 10.1021/acssynbio.0c00050] [Citation(s) in RCA: 5] [Impact Index Per Article: 1.3] [Reference Citation Analysis] [Abstract] [Key Words] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 01/21/2023]
Abstract
The construction of models of system behavior is of great importance throughout science and engineering. In bioengineering and bionanotechnology, these often take the form of dynamic models that specify the evolution of different species over time. To ensure that scientific observations and conclusions are consistent and that systems can be reliably engineered on the basis of model predictions, it is important that models of biomolecular systems can be constructed in a reliable, principled, and efficient manner. This review focuses on efforts to address this need by using domain-specific programming languages as the basis for custom design tools for researchers working on computational nucleic acid devices, where a domain-specific language is simply a programming language tailored to a particular application domain. The underlying thesis of our review is that there is a continuum of practical implementation strategies for computational nucleic acid systems, which can all benefit from appropriate domain-specific languages and software design tools. We emphasize the need for specialized yet flexible tools that can be realized using domain-specific languages that compile to more general-purpose representations.
Collapse
Affiliation(s)
- Matthew R. Lakin
- Department of Computer Science, University of New Mexico, Albuquerque, New Mexico 87131, United States
- Department of Chemical & Biological Engineering, University of New Mexico, Albuquerque, New Mexico 87131, United States
- Center for Biomedical Engineering, University of New Mexico, Albuquerque, New Mexico 87131, United States
| | | |
Collapse
|
5
|
Li X, Sun X, Zhou J, Yao D, Xiao S, Zhou X, Wei B, Li C, Liang H. Enzyme-assisted waste-to-reactant transformation to engineer renewable DNA circuits. Chem Commun (Camb) 2019; 55:11615-11618. [PMID: 31501837 DOI: 10.1039/c9cc05941e] [Citation(s) in RCA: 1] [Impact Index Per Article: 0.2] [Reference Citation Analysis] [Abstract] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 01/16/2023]
Abstract
To date, implementation of renewable DNA circuits remains challenging due to issues including reactant depletion and waste accumulation. Herein we simultaneously addressed both issues through nicking enzyme-assisted waste-to-reactant transformation. As a proof-of-concept, a renewable entropy-driven catalytic DNA circuit was implemented, exhibiting a good renewability when replenishing fuel.
Collapse
Affiliation(s)
- Xiang Li
- CAS Key Laboratory of Soft Matter Chemistry, iChEM (Collaborative Innovation Center of Chemistry for Energy Materials), Department of Polymer Science and Engineering, Hefei National Laboratory for Physical Sciences at the Microscale, University of Science and Technology of China, Hefei, Anhui 230026, P. R. China.
| | - Xianbao Sun
- State Key Laboratory of Bioelectronics, School of Biological Science and Medical Engineering, Southeast University, Nanjing, Jiangsu 210096, P. R. China.
| | - Junxiang Zhou
- CAS Key Laboratory of Soft Matter Chemistry, iChEM (Collaborative Innovation Center of Chemistry for Energy Materials), Department of Polymer Science and Engineering, Hefei National Laboratory for Physical Sciences at the Microscale, University of Science and Technology of China, Hefei, Anhui 230026, P. R. China.
| | - Dongbao Yao
- CAS Key Laboratory of Soft Matter Chemistry, iChEM (Collaborative Innovation Center of Chemistry for Energy Materials), Department of Polymer Science and Engineering, Hefei National Laboratory for Physical Sciences at the Microscale, University of Science and Technology of China, Hefei, Anhui 230026, P. R. China.
| | - Shiyan Xiao
- CAS Key Laboratory of Soft Matter Chemistry, iChEM (Collaborative Innovation Center of Chemistry for Energy Materials), Department of Polymer Science and Engineering, Hefei National Laboratory for Physical Sciences at the Microscale, University of Science and Technology of China, Hefei, Anhui 230026, P. R. China.
| | - Xiang Zhou
- CAS Key Laboratory of Soft Matter Chemistry, iChEM (Collaborative Innovation Center of Chemistry for Energy Materials), Department of Polymer Science and Engineering, Hefei National Laboratory for Physical Sciences at the Microscale, University of Science and Technology of China, Hefei, Anhui 230026, P. R. China.
| | - Bing Wei
- CAS Key Laboratory of Soft Matter Chemistry, iChEM (Collaborative Innovation Center of Chemistry for Energy Materials), Department of Polymer Science and Engineering, Hefei National Laboratory for Physical Sciences at the Microscale, University of Science and Technology of China, Hefei, Anhui 230026, P. R. China.
| | - Chengxu Li
- CAS Key Laboratory of Soft Matter Chemistry, iChEM (Collaborative Innovation Center of Chemistry for Energy Materials), Department of Polymer Science and Engineering, Hefei National Laboratory for Physical Sciences at the Microscale, University of Science and Technology of China, Hefei, Anhui 230026, P. R. China.
| | - Haojun Liang
- CAS Key Laboratory of Soft Matter Chemistry, iChEM (Collaborative Innovation Center of Chemistry for Energy Materials), Department of Polymer Science and Engineering, Hefei National Laboratory for Physical Sciences at the Microscale, University of Science and Technology of China, Hefei, Anhui 230026, P. R. China.
| |
Collapse
|
6
|
Ellis SJ, Klinge TH, Lathrop JI. Robust chemical circuits. Biosystems 2019; 186:103983. [PMID: 31207268 DOI: 10.1016/j.biosystems.2019.103983] [Citation(s) in RCA: 2] [Impact Index Per Article: 0.4] [Reference Citation Analysis] [Abstract] [Key Words] [MESH Headings] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Received: 08/29/2018] [Revised: 06/10/2019] [Accepted: 06/11/2019] [Indexed: 11/18/2022]
Abstract
We introduce a new motif for constructing robust digital logic circuits using input/output chemical reaction networks. These chemical circuits robustly handle adversarial manipulation to their input signals, initial concentrations, rate constants, and measurements. In particular, we show that all Boolean circuits and several sequential circuits enjoy this robustness. Our results complement existing literature in the following three ways: (1) our logic gates read their inputs catalytically which make fanout gates unnecessary; (2) formal requirements and rigorous proofs of satisfaction are provided for each circuit; and (3) robustness of every circuit is closed under modular composition.
Collapse
Affiliation(s)
- Samuel J Ellis
- The Molecular Sciences Software Institute, Blacksburg, VA 24060, USA.
| | - Titus H Klinge
- Department of Mathematics and Computer Science, Drake University, Des Moines, IA 50311, USA.
| | - James I Lathrop
- Department of Computer Science, Iowa State University, Ames, IA 50011, USA.
| |
Collapse
|
7
|
|
8
|
Cardelli L, Kwiatkowska M, Whitby M. Chemical reaction network designs for asynchronous logic circuits. NATURAL COMPUTING 2017; 17:109-130. [PMID: 29576757 PMCID: PMC5856889 DOI: 10.1007/s11047-017-9665-7] [Citation(s) in RCA: 5] [Impact Index Per Article: 0.7] [Reference Citation Analysis] [Abstract] [Key Words] [Grants] [Track Full Text] [Figures] [Subscribe] [Scholar Register] [Indexed: 06/08/2023]
Abstract
Chemical reaction networks (CRNs) are a versatile language for describing the dynamical behaviour of chemical kinetics, capable of modelling a variety of digital and analogue processes. While CRN designs for synchronous sequential logic circuits have been proposed and their implementation in DNA demonstrated, a physical realisation of these devices is difficult because of their reliance on a clock. Asynchronous sequential logic, on the other hand, does not require a clock, and instead relies on handshaking protocols to ensure the temporal ordering of different phases of the computation. This paper provides novel CRN designs for the construction of asynchronous logic, arithmetic and control flow elements based on a bi-molecular reaction motif with catalytic reactions and uniform reaction rates. We model and validate the designs for the deterministic and stochastic semantics using Microsoft's GEC tool and the probabilistic model checker PRISM, demonstrating their ability to emulate the function of asynchronous components under low molecular count.
Collapse
Affiliation(s)
- Luca Cardelli
- Microsoft Research, Cambridge, UK
- Department of Computer science, University of Oxford, Oxford, UK
| | | | - Max Whitby
- Department of Computer science, University of Oxford, Oxford, UK
| |
Collapse
|
9
|
Murayama K, Nagao R, Asanuma H. D-a
TNA Circuit Orthogonal to DNA Can Be Operated by RNA Input via SNA. ChemistrySelect 2017. [DOI: 10.1002/slct.201701126] [Citation(s) in RCA: 7] [Impact Index Per Article: 1.0] [Reference Citation Analysis] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 11/07/2022]
Affiliation(s)
- Keiji Murayama
- Graduate School of Engineering; Nagoya University, Furo-cho, Chikusa-ku; Nagoya 464-8603 Japan
| | - Ryuya Nagao
- Graduate School of Engineering; Nagoya University, Furo-cho, Chikusa-ku; Nagoya 464-8603 Japan
| | - Hiroyuki Asanuma
- Graduate School of Engineering; Nagoya University, Furo-cho, Chikusa-ku; Nagoya 464-8603 Japan
| |
Collapse
|
10
|
|
11
|
Thubagere AJ, Thachuk C, Berleant J, Johnson RF, Ardelean DA, Cherry KM, Qian L. Compiler-aided systematic construction of large-scale DNA strand displacement circuits using unpurified components. Nat Commun 2017; 8:14373. [PMID: 28230154 PMCID: PMC5331218 DOI: 10.1038/ncomms14373] [Citation(s) in RCA: 45] [Impact Index Per Article: 6.4] [Reference Citation Analysis] [Abstract] [MESH Headings] [Track Full Text] [Download PDF] [Figures] [Journal Information] [Subscribe] [Scholar Register] [Received: 08/07/2016] [Accepted: 12/21/2016] [Indexed: 11/09/2022] Open
Abstract
Biochemical circuits made of rationally designed DNA molecules are proofs of concept for embedding control within complex molecular environments. They hold promise for transforming the current technologies in chemistry, biology, medicine and material science by introducing programmable and responsive behaviour to diverse molecular systems. As the transformative power of a technology depends on its accessibility, two main challenges are an automated design process and simple experimental procedures. Here we demonstrate the use of circuit design software, combined with the use of unpurified strands and simplified experimental procedures, for creating a complex DNA strand displacement circuit that consists of 78 distinct species. We develop a systematic procedure for overcoming the challenges involved in using unpurified DNA strands. We also develop a model that takes synthesis errors into consideration and semi-quantitatively reproduces the experimental data. Our methods now enable even novice researchers to successfully design and construct complex DNA strand displacement circuits.
Collapse
Affiliation(s)
- Anupama J. Thubagere
- Bioengineering, California Institute of Technology, 1200 East California Boulevard, Pasadena, California 91125, USA
| | - Chris Thachuk
- Computer Science, California Institute of Technology, 1200 East California Boulevard, Pasadena, California 91125, USA
| | - Joseph Berleant
- Computer Science, California Institute of Technology, 1200 East California Boulevard, Pasadena, California 91125, USA
| | - Robert F. Johnson
- Bioengineering, California Institute of Technology, 1200 East California Boulevard, Pasadena, California 91125, USA
| | - Diana A. Ardelean
- Applied and Computational Mathematics, California Institute of Technology, 1200 East California Boulevard, Pasadena, California 91125, USA
| | - Kevin M. Cherry
- Bioengineering, California Institute of Technology, 1200 East California Boulevard, Pasadena, California 91125, USA
| | - Lulu Qian
- Bioengineering, California Institute of Technology, 1200 East California Boulevard, Pasadena, California 91125, USA
- Computer Science, California Institute of Technology, 1200 East California Boulevard, Pasadena, California 91125, USA
| |
Collapse
|
12
|
|
13
|
Fages F, Le Guludec G, Bournez O, Pouly A. Strong Turing Completeness of Continuous Chemical Reaction Networks and Compilation of Mixed Analog-Digital Programs. COMPUTATIONAL METHODS IN SYSTEMS BIOLOGY 2017. [DOI: 10.1007/978-3-319-67471-1_7] [Citation(s) in RCA: 22] [Impact Index Per Article: 3.1] [Reference Citation Analysis] [Track Full Text] [Subscribe] [Scholar Register] [Indexed: 01/09/2023]
|
14
|
Badelt S, Shin SW, Johnson RF, Dong Q, Thachuk C, Winfree E. A General-Purpose CRN-to-DSD Compiler with Formal Verification, Optimization, and Simulation Capabilities. LECTURE NOTES IN COMPUTER SCIENCE 2017. [DOI: 10.1007/978-3-319-66799-7_15] [Citation(s) in RCA: 17] [Impact Index Per Article: 2.4] [Reference Citation Analysis] [Track Full Text] [Subscribe] [Scholar Register] [Indexed: 12/13/2022]
|
15
|
|
16
|
Petersen RL, Lakin MR, Phillips A. A strand graph semantics for DNA-based computation. THEORETICAL COMPUTER SCIENCE 2016; 632:43-73. [PMID: 27293306 PMCID: PMC4896506 DOI: 10.1016/j.tcs.2015.07.041] [Citation(s) in RCA: 7] [Impact Index Per Article: 0.9] [Reference Citation Analysis] [Abstract] [Key Words] [Grants] [Track Full Text] [Subscribe] [Scholar Register] [Indexed: 06/06/2023]
Abstract
DNA nanotechnology is a promising approach for engineering computation at the nanoscale, with potential applications in biofabrication and intelligent nanomedicine. DNA strand displacement is a general strategy for implementing a broad range of nanoscale computations, including any computation that can be expressed as a chemical reaction network. Modelling and analysis of DNA strand displacement systems is an important part of the design process, prior to experimental realisation. As experimental techniques improve, it is important for modelling languages to keep pace with the complexity of structures that can be realised experimentally. In this paper we present a process calculus for modelling DNA strand displacement computations involving rich secondary structures, including DNA branches and loops. We prove that our calculus is also sufficiently expressive to model previous work on non-branching structures, and propose a mapping from our calculus to a canonical strand graph representation, in which vertices represent DNA strands, ordered sites represent domains, and edges between sites represent bonds between domains. We define interactions between strands by means of strand graph rewriting, and prove the correspondence between the process calculus and strand graph behaviours. Finally, we propose a mapping from strand graphs to an efficient implementation, which we use to perform modelling and simulation of DNA strand displacement systems with rich secondary structure.
Collapse
Affiliation(s)
| | - Matthew R Lakin
- Department of Computer Science, University of New Mexico, Albuquerque, NM, USA
| | | |
Collapse
|
17
|
Lakin MR, Stefanovic D, Phillips A. Modular verification of chemical reaction network encodings via serializability analysis. THEORETICAL COMPUTER SCIENCE 2016; 632:21-42. [PMID: 27325906 PMCID: PMC4911709 DOI: 10.1016/j.tcs.2015.06.033] [Citation(s) in RCA: 6] [Impact Index Per Article: 0.8] [Reference Citation Analysis] [Abstract] [Key Words] [Grants] [Track Full Text] [Subscribe] [Scholar Register] [Indexed: 06/06/2023]
Abstract
Chemical reaction networks are a powerful means of specifying the intended behaviour of synthetic biochemical systems. A high-level formal specification, expressed as a chemical reaction network, may be compiled into a lower-level encoding, which can be directly implemented in wet chemistry and may itself be expressed as a chemical reaction network. Here we present conditions under which a lower-level encoding correctly emulates the sequential dynamics of a high-level chemical reaction network. We require that encodings are transactional, such that their execution is divided by a "commit reaction" that irreversibly separates the reactant-consuming phase of the encoding from the product-generating phase. We also impose restrictions on the sharing of species between reaction encodings, based on a notion of "extra tolerance", which defines species that may be shared between encodings without enabling unwanted reactions. Our notion of correctness is serializability of interleaved reaction encodings, and if all reaction encodings satisfy our correctness properties then we can infer that the global dynamics of the system are correct. This allows us to infer correctness of any system constructed using verified encodings. As an example, we show how this approach may be used to verify two- and four-domain DNA strand displacement encodings of chemical reaction networks, and we generalize our result to the limit where the populations of helper species are unlimited.
Collapse
Affiliation(s)
- Matthew R. Lakin
- Department of Computer Science, University of New Mexico, Albuquerque, NM, USA
| | - Darko Stefanovic
- Department of Computer Science, University of New Mexico, Albuquerque, NM, USA
- Center for Biomedical Engineering, University of New Mexico, Albuquerque, NM, USA
| | | |
Collapse
|
18
|
Lakin MR, Minnich A, Lane T, Stefanovic D. Design of a biochemical circuit motif for learning linear functions. J R Soc Interface 2015; 11:20140902. [PMID: 25401175 DOI: 10.1098/rsif.2014.0902] [Citation(s) in RCA: 9] [Impact Index Per Article: 1.0] [Reference Citation Analysis] [Abstract] [MESH Headings] [Grants] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 12/24/2022] Open
Abstract
Learning and adaptive behaviour are fundamental biological processes. A key goal in the field of bioengineering is to develop biochemical circuit architectures with the ability to adapt to dynamic chemical environments. Here, we present a novel design for a biomolecular circuit capable of supervised learning of linear functions, using a model based on chemical reactions catalysed by DNAzymes. To achieve this, we propose a novel mechanism of maintaining and modifying internal state in biochemical systems, thereby advancing the state of the art in biomolecular circuit architecture. We use simulations to demonstrate that the circuit is capable of learning behaviour and assess its asymptotic learning performance, scalability and robustness to noise. Such circuits show great potential for building autonomous in vivo nanomedical devices. While such a biochemical system can tell us a great deal about the fundamentals of learning in living systems and may have broad applications in biomedicine (e.g. autonomous and adaptive drugs), it also offers some intriguing challenges and surprising behaviours from a machine learning perspective.
Collapse
|
19
|
Li X, Wang X, Song T, Lu W, Chen Z, Shi X. A Novel Computational Method to Reduce Leaky Reaction in DNA Strand Displacement. JOURNAL OF ANALYTICAL METHODS IN CHEMISTRY 2015; 2015:675827. [PMID: 26491602 PMCID: PMC4605363 DOI: 10.1155/2015/675827] [Citation(s) in RCA: 3] [Impact Index Per Article: 0.3] [Reference Citation Analysis] [Abstract] [Track Full Text] [Figures] [Subscribe] [Scholar Register] [Received: 05/06/2015] [Accepted: 07/07/2015] [Indexed: 06/05/2023]
Abstract
DNA strand displacement technique is widely used in DNA programming, DNA biosensors, and gene analysis. In DNA strand displacement, leaky reactions can cause DNA signals decay and detecting DNA signals fails. The mostly used method to avoid leakage is cleaning up after upstream leaky reactions, and it remains a challenge to develop reliable DNA strand displacement technique with low leakage. In this work, we address the challenge by experimentally evaluating the basic factors, including reaction time, ratio of reactants, and ion concentration to the leakage in DNA strand displacement. Specifically, fluorescent probes and a hairpin structure reporting DNA strand are designed to detect the output of DNA strand displacement, and thus can evaluate the leakage of DNA strand displacement reactions with different reaction time, ratios of reactants, and ion concentrations. From the obtained data, mathematical models for evaluating leakage are achieved by curve derivation. As a result, it is obtained that long time incubation, high concentration of fuel strand, and inappropriate amount of ion concentration can weaken leaky reactions. This contributes to a method to set proper reaction conditions to reduce leakage in DNA strand displacement.
Collapse
Affiliation(s)
- Xin Li
- Department of Obstetrics and Gynecology, Renmin Hospital of Wuhan University, Wuhan, Hubei 430060, China
| | - Xun Wang
- College of Mathematics and System Science, Shandong University of Science and Technology, Qingdao, Shandong 266590, China
| | - Tao Song
- College of Computer and Communication Engineering, China University of Petroleum, Qingdao, Shandong 266580, China
- Faculty of Engineering, Computing and Science, Swinburne University of Technology Sarawak Campus, 93350 Kuching, Sarawak, Malaysia
| | - Wei Lu
- Key Laboratory of Image Information Processing and Intelligent Control, School of Automation, Huazhong University of Science and Technology, Wuhan, Hubei 430074, China
| | - Zhihua Chen
- Key Laboratory of Image Information Processing and Intelligent Control, School of Automation, Huazhong University of Science and Technology, Wuhan, Hubei 430074, China
| | - Xiaolong Shi
- Key Laboratory of Image Information Processing and Intelligent Control, School of Automation, Huazhong University of Science and Technology, Wuhan, Hubei 430074, China
| |
Collapse
|
20
|
Chiu TY, Chiang HJK, Huang RY, Jiang JHR, Fages F. Synthesizing Configurable Biochemical Implementation of Linear Systems from Their Transfer Function Specifications. PLoS One 2015; 10:e0137442. [PMID: 26352855 PMCID: PMC4564270 DOI: 10.1371/journal.pone.0137442] [Citation(s) in RCA: 11] [Impact Index Per Article: 1.2] [Reference Citation Analysis] [Abstract] [MESH Headings] [Track Full Text] [Download PDF] [Figures] [Journal Information] [Subscribe] [Scholar Register] [Received: 04/03/2015] [Accepted: 08/16/2015] [Indexed: 11/18/2022] Open
Abstract
The ability to engineer synthetic systems in the biochemical context is constantly being improved and has a profound societal impact. Linear system design is one of the most pervasive methods applied in control tasks, and its biochemical realization has been proposed by Oishi and Klavins and advanced further in recent years. However, several technical issues remain unsolved. Specifically, the design process is not fully automated from specification at the transfer function level, systems once designed often lack dynamic adaptivity to environmental changes, matching rate constants of reactions is not always possible, and implementation may be approximative and greatly deviate from the specifications. Building upon the work of Oishi and Klavins, this paper overcomes these issues by introducing a design flow that transforms a transfer-function specification of a linear system into a set of chemical reactions, whose input-output response precisely conforms to the specification. This system is implementable using the DNA strand displacement technique. The underlying configurability is embedded into primitive components and template modules, and thus the entire system is adaptive. Simulation of DNA strand displacement implementation confirmed the feasibility and superiority of the proposed synthesis flow.
Collapse
Affiliation(s)
- Tai-Yin Chiu
- Department of Physics, National Taiwan University, Taipei, Taiwan
- Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan
| | - Hui-Ju K. Chiang
- Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan
- EPI Lifeware, Inria Paris-Rocquencourt, Rocquencourt, France
| | - Ruei-Yang Huang
- Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan
| | - Jie-Hong R. Jiang
- Graduate Institute of Electronics Engineering, National Taiwan University, Taipei, Taiwan
- Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan
- * E-mail:
| | - François Fages
- EPI Lifeware, Inria Paris-Rocquencourt, Rocquencourt, France
| |
Collapse
|
21
|
Kahramanoğulları O, Cardelli L. Gener: a minimal programming module for chemical controllers based on DNA strand displacement. Bioinformatics 2015; 31:2906-8. [PMID: 25957353 PMCID: PMC4547617 DOI: 10.1093/bioinformatics/btv286] [Citation(s) in RCA: 3] [Impact Index Per Article: 0.3] [Reference Citation Analysis] [Abstract] [Track Full Text] [Download PDF] [Figures] [Journal Information] [Subscribe] [Scholar Register] [Received: 12/04/2014] [Accepted: 04/30/2015] [Indexed: 11/15/2022] Open
Abstract
Summary: Gener is a development module for programming chemical controllers based on DNA strand displacement. Gener is developed with the aim of providing a simple interface that minimizes the opportunities for programming errors: Gener allows the user to test the computations of the DNA programs based on a simple two-domain strand displacement algebra, the minimal available so far. The tool allows the user to perform stepwise computations with respect to the rules of the algebra as well as exhaustive search of the computation space with different options for exploration and visualization. Gener can be used in combination with existing tools, and in particular, its programs can be exported to Microsoft Research’s DSD tool as well as to LaTeX. Availability and implementation: Gener is available for download at the Cosbi website at http://www.cosbi.eu/research/prototypes/gener as a windows executable that can be run on Mac OS X and Linux by using Mono. Contact: ozan@cosbi.eu
Collapse
Affiliation(s)
- Ozan Kahramanoğulları
- Department of Mathematics, University of Trento, Trento, Italy, The Microsoft Research-University of Trento Centre for Computational and Systems Biology
| | - Luca Cardelli
- Microsoft Research Cambridge and Department of Computer Science, University of Oxford
| |
Collapse
|
22
|
Dalchau N, Chandran H, Gopalkrishnan N, Phillips A, Reif J. Probabilistic Analysis of Localized DNA Hybridization Circuits. ACS Synth Biol 2015; 4:898-913. [PMID: 26133087 DOI: 10.1021/acssynbio.5b00044] [Citation(s) in RCA: 24] [Impact Index Per Article: 2.7] [Reference Citation Analysis] [Abstract] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 11/30/2022]
Abstract
Molecular devices made of nucleic acids can perform complex information processing tasks at the nanoscale, with potential applications in biofabrication and smart therapeutics. However, limitations in the speed and scalability of such devices in a well-mixed setting can significantly affect their performance. In this article, we propose designs for localized circuits involving DNA molecules that are arranged on addressable substrates and interact via hybridization reactions. We propose designs for localized elementary logic circuits, which we compose to produce more complex devices, including a circuit for computing the square root of a four bit number. We develop an efficient method for probabilistic model checking of localized circuits, which we implement within the Visual DSD design tool. We use this method to prove the correctness of our circuits with respect to their functional specifications and to analyze their performance over a broad range of local rate parameters. Specifically, we analyze the extent to which our localized designs can overcome the limitations of well-mixed circuits, with respect to speed and scalability. To provide an estimate of local rate parameters, we propose a biophysical model of localized hybridization. Finally, we use our analysis to identify constraints in the rate parameters that enable localized circuits to retain their advantages in the presence of unintended interferences between strands.
Collapse
Affiliation(s)
- Neil Dalchau
- Microsoft Research, Cambridge CB1 2FB, United Kingdom
| | - Harish Chandran
- Department
of Computer Science, Duke University, Durham, North Carolina 27708, United States
| | - Nikhil Gopalkrishnan
- Department
of Computer Science, Duke University, Durham, North Carolina 27708, United States
- Wyss
Institute, Harvard University, Boston, Massachusetts 02115, United States
| | | | - John Reif
- Department
of Computer Science, Duke University, Durham, North Carolina 27708, United States
| |
Collapse
|
23
|
Konur S, Gheorghe M. A Property-Driven Methodology for Formal Analysis of Synthetic Biology Systems. IEEE/ACM TRANSACTIONS ON COMPUTATIONAL BIOLOGY AND BIOINFORMATICS 2015; 12:360-371. [PMID: 26357223 DOI: 10.1109/tcbb.2014.2362531] [Citation(s) in RCA: 6] [Impact Index Per Article: 0.7] [Reference Citation Analysis] [Abstract] [MESH Headings] [Track Full Text] [Subscribe] [Scholar Register] [Indexed: 06/05/2023]
Abstract
This paper proposes a formal methodology to analyse bio-systems, in particular synthetic biology systems. An integrative analysis perspective combining different model checking approaches based on different property categories is provided. The methodology is applied to the synthetic pulse generator system and several verification experiments are carried out to demonstrate the use of our approach to formally analyse various aspects of synthetic biology systems.
Collapse
|
24
|
Zhang T, Shang C, Duan R, Hakeem A, Zhang Z, Lou X, Xia F. Polar organic solvents accelerate the rate of DNA strand replacement reaction. Analyst 2015; 140:2023-8. [DOI: 10.1039/c4an02302a] [Citation(s) in RCA: 8] [Impact Index Per Article: 0.9] [Reference Citation Analysis] [Abstract] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 11/21/2022]
Abstract
Acceleration of the reaction rate by polar organic solvents during both simple and complicated DNA strand replacement reactions is reported.
Collapse
Affiliation(s)
- Tianchi Zhang
- Key Laboratory for Large-Format Battery Materials and System
- Ministry of Education
- School of Chemistry and Chemical Engineering
- Huazhong University of Science and Technology
- Wuhan 430074
| | - Chunli Shang
- Key Laboratory for Large-Format Battery Materials and System
- Ministry of Education
- School of Chemistry and Chemical Engineering
- Huazhong University of Science and Technology
- Wuhan 430074
| | - Ruixue Duan
- Key Laboratory for Large-Format Battery Materials and System
- Ministry of Education
- School of Chemistry and Chemical Engineering
- Huazhong University of Science and Technology
- Wuhan 430074
| | - Abdul Hakeem
- Key Laboratory for Large-Format Battery Materials and System
- Ministry of Education
- School of Chemistry and Chemical Engineering
- Huazhong University of Science and Technology
- Wuhan 430074
| | - Zhenyu Zhang
- Key Laboratory for Large-Format Battery Materials and System
- Ministry of Education
- School of Chemistry and Chemical Engineering
- Huazhong University of Science and Technology
- Wuhan 430074
| | - Xiaoding Lou
- Key Laboratory for Large-Format Battery Materials and System
- Ministry of Education
- School of Chemistry and Chemical Engineering
- Huazhong University of Science and Technology
- Wuhan 430074
| | - Fan Xia
- Key Laboratory for Large-Format Battery Materials and System
- Ministry of Education
- School of Chemistry and Chemical Engineering
- Huazhong University of Science and Technology
- Wuhan 430074
| |
Collapse
|
25
|
kang D, Duan R, Tan Y, Hong F, Wang B, Chen Z, Xu S, Lou X, Wei W, Yurke B, Xia F. Speeding up the self-assembly of a DNA nanodevice using a variety of polar solvents. NANOSCALE 2014; 6:14153-14157. [PMID: 25350569 DOI: 10.1039/c4nr02257b] [Citation(s) in RCA: 7] [Impact Index Per Article: 0.7] [Reference Citation Analysis] [Abstract] [MESH Headings] [Track Full Text] [Subscribe] [Scholar Register] [Indexed: 06/04/2023]
Abstract
The specific recognition and programmable assembly properties make DNA a potential material for nanodevices. However, the more intelligent the nanodevice is, the more complicated the structure of the nanodevice is, which limits the speed of DNA assembly. Herein, to address this problem, we investigate the performance of DNA Strand Displacement Reaction (DSDR) in a mixture of polar organic solvents and aqueous buffer and demonstrate that the organic polar solvent can speed up DNA self-assembly efficiently. Taking DSDR in 20% ethanol as an example, first we have demonstrated that the DSDR is highly accelerated in the beginning of the reaction and it can complete 60% of replacement reactions (160% enhancement compared with aqueous buffer) in the first 300 seconds. Secondly, we calculated that the ΔΔG of the DSDR in 20% ethanol (-18.2 kcal mol(-1)) is lower than that in pure aqueous buffer (-32.6 kcal mol(-1)), while the activation energy is lowered by introducing ethanol. Finally, we proved that the DSDR on the electrode surface can also be accelerated using this simple strategy. More importantly, to test the efficacy of this approach in nanodevices with a complicated and slow DNA self-assembly process, we apply this strategy in the hybridization chain reaction (HCR) and prove the acceleration is fairly obvious in 20% ethanol, which demonstrates the feasibility of the proposed strategy in DNA nanotechnology and DNA-based biosensors.
Collapse
Affiliation(s)
- Di kang
- School of Chemistry and Chemical Engineering, Huazhong University of Science and Technology, Wuhan, China.
| | | | | | | | | | | | | | | | | | | | | |
Collapse
|
26
|
Biophysically inspired rational design of structured chimeric substrates for DNAzyme cascade engineering. PLoS One 2014; 9:e110986. [PMID: 25347066 PMCID: PMC4210168 DOI: 10.1371/journal.pone.0110986] [Citation(s) in RCA: 7] [Impact Index Per Article: 0.7] [Reference Citation Analysis] [Abstract] [Track Full Text] [Download PDF] [Figures] [Journal Information] [Subscribe] [Scholar Register] [Received: 08/18/2014] [Accepted: 09/18/2014] [Indexed: 12/21/2022] Open
Abstract
The development of large-scale molecular computational networks is a promising approach to implementing logical decision making at the nanoscale, analogous to cellular signaling and regulatory cascades. DNA strands with catalytic activity (DNAzymes) are one means of systematically constructing molecular computation networks with inherent signal amplification. Linking multiple DNAzymes into a computational circuit requires the design of substrate molecules that allow a signal to be passed from one DNAzyme to another through programmed biochemical interactions. In this paper, we chronicle an iterative design process guided by biophysical and kinetic constraints on the desired reaction pathways and use the resulting substrate design to implement heterogeneous DNAzyme signaling cascades. A key aspect of our design process is the use of secondary structure in the substrate molecule to sequester a downstream effector sequence prior to cleavage by an upstream DNAzyme. Our goal was to develop a concrete substrate molecule design to achieve efficient signal propagation with maximal activation and minimal leakage. We have previously employed the resulting design to develop high-performance DNAzyme-based signaling systems with applications in pathogen detection and autonomous theranostics.
Collapse
|
27
|
Aubert N, Mosca C, Fujii T, Hagiya M, Rondelez Y. Computer-assisted design for scaling up systems based on DNA reaction networks. J R Soc Interface 2014; 11:20131167. [PMID: 24451393 DOI: 10.1098/rsif.2013.1167] [Citation(s) in RCA: 32] [Impact Index Per Article: 3.2] [Reference Citation Analysis] [Abstract] [Key Words] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 12/16/2022] Open
Abstract
In the past few years, there have been many exciting advances in the field of molecular programming, reaching a point where implementation of non-trivial systems, such as neural networks or switchable bistable networks, is a reality. Such systems require nonlinearity, be it through signal amplification, digitalization or the generation of autonomous dynamics such as oscillations. The biochemistry of DNA systems provides such mechanisms, but assembling them in a constructive manner is still a difficult and sometimes counterintuitive process. Moreover, realistic prediction of the actual evolution of concentrations over time requires a number of side reactions, such as leaks, cross-talks or competitive interactions, to be taken into account. In this case, the design of a system targeting a given function takes much trial and error before the correct architecture can be found. To speed up this process, we have created DNA Artificial Circuits Computer-Assisted Design (DACCAD), a computer-assisted design software that supports the construction of systems for the DNA toolbox. DACCAD is ultimately aimed to design actual in vitro implementations, which is made possible by building on the experimental knowledge available on the DNA toolbox. We illustrate its effectiveness by designing various systems, from Montagne et al.'s Oligator or Padirac et al.'s bistable system to new and complex networks, including a two-bit counter or a frequency divider as well as an example of very large system encoding the game Mastermind. In the process, we highlight a variety of behaviours, such as enzymatic saturation and load effect, which would be hard to handle or even predict with a simpler model. We also show that those mechanisms, while generally seen as detrimental, can be used in a positive way, as functional part of a design. Additionally, the number of parameters included in these simulations can be large, especially in the case of complex systems. For this reason, we included the possibility to use CMA-ES, a state-of-the-art optimization algorithm that will automatically evolve parameters chosen by the user to try to match a specified behaviour. Finally, because all possible functionality cannot be captured by a single software, DACCAD includes the possibility to export a system in the synthetic biology markup language, a widely used language for describing biological reaction systems. DACCAD can be downloaded online at http://www.yannick-rondelez.com/downloads/.
Collapse
Affiliation(s)
- Nathanaël Aubert
- Graduate School of Information Science and Technology, University of Tokyo, , Tokyo, Japan
| | | | | | | | | |
Collapse
|
28
|
Lakin MR, Petersen R, Gray KE, Phillips A. Abstract Modelling of Tethered DNA Circuits. ACTA ACUST UNITED AC 2014. [DOI: 10.1007/978-3-319-11295-4_9] [Citation(s) in RCA: 18] [Impact Index Per Article: 1.8] [Reference Citation Analysis] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 11/24/2022]
|
29
|
Affiliation(s)
- Ehud Shapiro
- Department of Computer Science and Applied Mathematics, and the Department of Biological Chemistry, Weizmann Institute of Science, Rehovot 76100, Israel
| | | |
Collapse
|
30
|
Genot AJ, Fujii T, Rondelez Y. Scaling down DNA circuits with competitive neural networks. J R Soc Interface 2013; 10:20130212. [PMID: 23760296 DOI: 10.1098/rsif.2013.0212] [Citation(s) in RCA: 40] [Impact Index Per Article: 3.6] [Reference Citation Analysis] [Abstract] [Key Words] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 01/21/2023] Open
Abstract
DNA has proved to be an exquisite substrate to compute at the molecular scale. However, nonlinear computations (such as amplification, comparison or restoration of signals) remain costly in term of strands and are prone to leak. Kim et al. showed how competition for an enzymatic resource could be exploited in hybrid DNA/enzyme circuits to compute a powerful nonlinear primitive: the winner-take-all (WTA) effect. Here, we first show theoretically how the nonlinearity of the WTA effect allows the robust and compact classification of four patterns with only 16 strands and three enzymes. We then generalize this WTA effect to DNA-only circuits and demonstrate similar classification capabilities with only 23 strands.
Collapse
|
31
|
Functional Analysis of Large-Scale DNA Strand Displacement Circuits. LECTURE NOTES IN COMPUTER SCIENCE 2013. [DOI: 10.1007/978-3-319-01928-4_14] [Citation(s) in RCA: 7] [Impact Index Per Article: 0.6] [Reference Citation Analysis] [Track Full Text] [Subscribe] [Scholar Register] [Indexed: 01/02/2023]
|
32
|
Modular Verification of DNA Strand Displacement Networks via Serializability Analysis. LECTURE NOTES IN COMPUTER SCIENCE 2013. [DOI: 10.1007/978-3-319-01928-4_10] [Citation(s) in RCA: 9] [Impact Index Per Article: 0.8] [Reference Citation Analysis] [Track Full Text] [Subscribe] [Scholar Register] [Indexed: 01/09/2023]
|
33
|
Hockenberry AJ, Jewett MC. Synthetic in vitro circuits. Curr Opin Chem Biol 2012; 16:253-9. [PMID: 22676890 PMCID: PMC3424401 DOI: 10.1016/j.cbpa.2012.05.179] [Citation(s) in RCA: 49] [Impact Index Per Article: 4.1] [Reference Citation Analysis] [Abstract] [MESH Headings] [Grants] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Received: 03/20/2012] [Revised: 04/17/2012] [Accepted: 05/04/2012] [Indexed: 11/19/2022]
Abstract
Inspired by advances in the ability to construct programmable circuits in living organisms, in vitro circuits are emerging as a viable platform for designing, understanding, and exploiting dynamic biochemical circuitry. In vitro systems allow researchers to directly access and manipulate biomolecular parts without the unwieldy complexity and intertwined dependencies that often exist in vivo. Experimental and computational foundations in DNA, DNA/RNA, and DNA/RNA/protein based circuitry have given rise to systems with more than 100 programmed molecular constituents. Functionally, they have diverse capabilities including: complex mathematical calculations, associative memory tasks, and sensing of small molecules. Progress in this field is showing that cell-free synthetic biology is a versatile testing ground for understanding native biological circuits and engineering novel functionality.
Collapse
Affiliation(s)
- Adam J. Hockenberry
- Interdepartmental Biological Sciences Graduate Program, Northwestern University, 2205 Tech Drive, Evanston, IL 60208, USA
- Chemistry of Life Processes Institute, Northwestern University, 2170 Campus Drive, Evanston, IL 60208, USA
| | - Michael C. Jewett
- Interdepartmental Biological Sciences Graduate Program, Northwestern University, 2205 Tech Drive, Evanston, IL 60208, USA
- Chemistry of Life Processes Institute, Northwestern University, 2170 Campus Drive, Evanston, IL 60208, USA
- Department of Chemical and Biological Engineering, Northwestern University, 2145 Sheridan Road, Evanston, IL 60208, USA
- Member, Robert H. Lurie Comprehensive Cancer Center, Northwestern University, Feinberg School of Medicine, Northwestern University, 303 E. Superior, Chicago, IL 60611, USA
| |
Collapse
|
34
|
Thachuk C, Condon A. Space and Energy Efficient Computation with DNA Strand Displacement Systems. ACTA ACUST UNITED AC 2012. [DOI: 10.1007/978-3-642-32208-2_11] [Citation(s) in RCA: 3] [Impact Index Per Article: 0.3] [Reference Citation Analysis] [Track Full Text] [Journal Information] [Subscribe] [Scholar Register] [Indexed: 03/28/2023]
|