The Formal Language and Design Principles of Autonomous DNA Walker Circuits

Verifiable biology

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.

Design and Simulation of an Autonomous Molecular Mechanism Using Spatially Localized DNA Computation

As a well-established technique, DNA synthesis offers interesting possibilities for designing multifunctional nanodevices. The micro-processing system of modern semiconductor circuits is dependent on strategies organized on silicon chips to achieve the speedy transmission of substances or information. Similarly, spatially localized structures allow for fixed DNA molecules in close proximity to each other during the synthesis of molecular circuits, thus providing a different strategy that of opening up a remarkable new area of inquiry for researchers. Herein, the Visual DSD (DNA strand displacement) modeling language was used to design and analyze the spatially organized DNA reaction network. The execution rules depend on the hybridization reaction caused by directional complementary nucleotide sequences. A series of DNA strand displacement calculations were organized on the locally coded travel track, and autonomous movement and addressing operations are gradually realized. The DNA nanodevice operates in this manner follows the embedded "molecular program", which improves the reusability and scalability of the same sequence domain in different contexts. Through the communication between various building blocks, the DNA device-carrying the target molecule moves in a controlled manner along the programmed track. In this way, a variety of molecular functional group transport and specific partition storage can be realized. The simulation results of the visual DSD tool provide qualitative and quantitative proof for the operation of the system.

Acceleration of DNA Hybridization Chain Reactions on 3D Nanointerfaces of Magnetic Particles and Their Direct Application in the Enzyme-Free Amplified Detection of microRNA

Accelerated DNA hybridization chain reactions (HCRs) using DNA origami as a scaffold have received considerable attention in dynamic DNA nanotechnology. However, tailor-made designs are essential for DNA origami scaffolds, hampering the practical application of accelerated HCRs. Here, we constructed the semilocalized HCR and localized HCR systems using magnetic beads (MBs) as a simple scaffold to explore them for the enzyme-free miR-21 detection. The semilocalized HCR system relied on free diffusing one hairpin DNA and MBs immobilized with another hairpin DNA, and the localized HCR system relied on MBs coimmobilized with two hairpin DNAs. We demonstrated that the DNA density on MBs plays a critical role in HCR kinetics and limit of detection (LOD). Among semilocalized HCR systems, MBs with a medium DNA density showed a faster HCR and lower LOD (10 pM) than the diffusive (conventional) HCR system (LOD: 86 pM). In contrast, the HCR further accelerated for the localized HCR systems as the DNA density increased. The localized HCR system with the highest DNA density showed the fastest HCR and the lowest LOD (533 fM). These findings are of great importance for the rational design of accelerated HCRs using simple scaffolds for practical applications.

Flap Endonuclease 1-Assisted DNA Walkers for Sensitively and Specifically Sensing ctDNAs

DNA walkers have shown superior performance in biosensing due to their programmability to design molecular walking behaviors with specific responses to different biological targets. However, it is still challenging to make DNA walkers capable of distinguishing DNA targets with single-base differences, so that DNA walkers that can be used for circulating tumor DNA sensing are rarely reported. Herein, a flap endonuclease 1 (FEN 1)-assisted DNA walker has been proposed to achieve mutant biosensing. The target DNA is captured on a gold nanoparticle (AuNP) as a walking strand to walk by hybridizing to the track strands on the surface of the AuNP. FEN 1 is employed to report the walking events by cleaving the track strands that must form a three-base overlapping structure recognized by FEN 1 after hybridizing with the captured target DNA. Owing to the high specificity of FEN 1 for structure recognition, the one-base mutant DNA target can be discriminated from wild-type DNA. By constructing a sensitivity-enhanced DNA walker system, as low as 1 fM DNA targets and 0.1% mutation abundance can be sensed, and the theoretical detection limits for detecting the DNA target and mutation abundance achieve 0.22 fM and 0.01%, respectively. The results of epidermal growth factor receptor (EGFR) L858R mutation detection on cell-free DNA samples from 15 patients with nonsmall cell lung cancer were completely consistent with that of next-generation sequencing, indicating that our DNA walker has potential for liquid biopsy.

Formal Semantics and Verification of Network-Based Biocomputation Circuits

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.

Regeneration of Burnt Bridges on a DNA Catenane Walker

DNA walkers are molecular machines that can move with high precision onthe nanoscale due to their structural and functional programmability. Despite recent advances in the field that allow exploring different energy sources, stimuli, and mechanisms of action for these nanomachines, the continuous operation and reusability of DNA walkers remains challenging because in most cases the steps, once taken by the walker, cannot be taken again. Herein we report the path regeneration of a burnt-bridges DNA catenane walker using RNase A. This walker uses a T7RNA polymerase that produces long RNA transcripts to hybridize to the path and move forward while the RNA remains hybridized to the path and blocks it for an additional walking cycle. We show that RNA degradation triggered by RNase A restores the path and returns the walker to the initial position. RNase inhibition restarts the function of the walker.

Simple Single-Legged DNA Walkers at Diffusion-Limited Nanointerfaces of Gold Nanoparticles Driven by a DNA Circuit Mechanism

We designed and prepared a single-legged DNA walker that relies on the creation of a simple diffusion-limited nanointerface on a gold nanoparticle (DNA/PEG⁽⁺⁾-GNP) track co-modified with fluorescence-labeled hairpin DNA and poly(ethylene glycol) (PEG) containing a positively charged amino group at one end. The movement of our single-legged DNA walker is driven by an enzyme-free DNA circuit mechanism through cascading toehold mediated DNA displacement reactions (TMDRs) using fuel hairpin DNAs. The acceleration of TMDRs was observed for the DNA/PEG⁽⁺⁾-GNP track through electrostatic interaction between the positively charged track and negatively charged DNAs, resulting in the acceleration of the DNA circuit and amplification of the fluorescence signal. Furthermore, the DNA/PEG⁽⁺⁾-GNP track allowed autonomous and persistent movement of a walker DNA strand on the same GNP track, because the intraparticle DNA circuit occurred preferentially by preventing diffusion of the negatively charged free walker DNA strand from near the positively charged tracks into solution through electrostatic interaction. Based on comparative study of kinetics of TMDRs and DNA walking behaviors, it is to be noted that the DNA/PEG⁽⁺⁾-GNP track showed the fastest DNA circuit reaction (walking rate) and the largest number of steps taken by the walker DNA strand compared to other GNP tracks with varying nanointerfaces that differ in terms of their type of charges (no and negative charges), density of positive charges, and number of hairpin DNAs per GNP track. These facts reveal that the positive charges on the GNP track play an important role in the acceleration of the DNA circuit, as well as the successful walking motion of the single-legged DNA strand. By using the fluorescence signal amplification functions, our single-legged DNA walker could be applied directly and successfully to enzyme-free miRNA-detection systems. The miRNA-detection system provided higher discrimination of other mismatched miRNAs and higher sensitivity (the lowest LOD: 4.0 pM) when compared to other miRNA-detection systems based on other GNP tracks without positive charges. Unlike existing single-legged DNA walkers, our single-legged DNA walkers do not require complex processes, such as immobilization of the walker DNA strand on the tracks and precise adjustment of the sequence of walker DNA. Therefore, our strategy, based on the creation of diffusion-limited nanointerfaces, has enormous potential for the applications of single-legged DNA walkers to biosensors, bioimaging, and computing.

Programming Motions of DNA Origami Nanomachines

DNA nanotechnology enables the precise fabrication of DNA-based machines with nanoscale dimensions. A wide range of DNA nanomachines are designed, which can be activated by specific inputs to perform various movement and functions. The excellent rigidity and unprecedented addressability of DNA origami have made it an excellent platform for manipulating and investigating the motion behaviors of DNA machines at single-molecule level. In this Concept, power supply, machine actuation, and motion behavior of DNA machines on origami platforms are summarized and classified. The strategies utilized for programming motion behavior of DNA machines on DNA origami are also discussed with representative examples. The challenges and outlook for future development of manipulating DNA nanomachines at the single molecule level are presented and discussed.

Solving mazes with single-molecule DNA navigators

Molecular devices with information-processing capabilities hold great promise for developing intelligent nanorobotics. Here we demonstrate a DNA navigator system that can perform single-molecule parallel depth-first search on a ten-vertex rooted tree defined on a two-dimensional DNA origami platform. Pathfinding by the DNA navigators exploits a localized strand exchange cascade, which is initiated at a unique trigger site on the origami with subsequent automatic progression along paths defined by DNA hairpins containing a universal traversal sequence. Each single-molecule navigator autonomously explores one of the possible paths through the tree. A specific solution path connecting a given pair of start and end vertices can then be easily extracted from the set of all paths taken by the navigators collectively. The solution path laid out on origami is illustrated with single-molecule imaging. Our approach points towards the realization of molecular materials with embedded computational functions operating at the single-molecule level.

Petri-net-based 2D design of DNA walker circuits

We consider localised DNA computation, where a DNA strand walks along a binary decision graph to compute a binary function. One of the challenges for the design of reliable walker circuits consists in leakage transitions, which occur when a walker jumps into another branch of the decision graph. We automatically identify leakage transitions, which allows for a detailed qualitative and quantitative assessment of circuit designs, design comparison, and design optimisation. The ability to identify leakage transitions is an important step in the process of optimising DNA circuit layouts where the aim is to minimise the computational error inherent in a circuit while minimising the area of the circuit. Our 2D modelling approach of DNA walker circuits relies on coloured stochastic Petri nets which enable functionality, topology and dimensionality all to be integrated in one two-dimensional model. Our modelling and analysis approach can be easily extended to 3-dimensional walker systems.

A spatially localized architecture for fast and modular DNA computing

Cells use spatial constraints to control and accelerate the flow of information in enzyme cascades and signalling networks. Synthetic silicon-based circuitry similarly relies on spatial constraints to process information. Here, we show that spatial organization can be a similarly powerful design principle for overcoming limitations of speed and modularity in engineered molecular circuits. We create logic gates and signal transmission lines by spatially arranging reactive DNA hairpins on a DNA origami. Signal propagation is demonstrated across transmission lines of different lengths and orientations and logic gates are modularly combined into circuits that establish the universality of our approach. Because reactions preferentially occur between neighbours, identical DNA hairpins can be reused across circuits. Co-localization of circuit elements decreases computation time from hours to minutes compared to circuits with diffusible components. Detailed computational models enable predictive circuit design. We anticipate our approach will motivate using spatial constraints for future molecular control circuit designs.