PaperlayerView exact revision on arXiv

Source-linked AI summary

Two-Domain DNA Strand Displacement

Luca Cardelli

arXiv:1006.2993v1cs.LOcs.PL

TL;DR

Composable DNA strand-displacement gates require a fixed signal structure, and each choice entails a different gate architecture. This paper develops two-domain structures for fork and join gates and formalizes their behavior; the structures cover a range of computation, including Petri nets, while interference across contexts remains a correctness challenge.

  • Problem

    Composable strand-displacement gates require a fixed signal structure, and each signal choice entails a different gate architecture.

    Source: §2 · p. 2

  • Method

    The paper develops two-domain, top-nicked DNA structures for fork and join gates and provides syntax and reduction rules for formalizing them.

    Source: §2 · p. 2, Two-domain strand displacement gates · pp. 4–5, Discussion: The double strand… · p. 6

  • Results

    Fork and join gates in populations are equivalent to Petri nets, and the simplified structures have syntactical representations and reduction rules that simplify formal verification.

    Source: Discussion: The double strand… · p. 6

  • Takeaways & Limitations

    The formal framework supports calculations of correctness and behavioral properties, though proving absence of gate interference across all combinations requires extensive case analysis and likely automation.

    Source: §6 · p. 13

    A transducer is not correct in all possible contexts because a context can absorb its public output strand and interfere with it.

    Source: Proof · p. 10

Abstract

from arXiv · show

We investigate the computing power of a restricted class of DNA strand displacement structures: those that are made of double strands with nicks (interruptions) in the top strand. To preserve this structural invariant, we impose restrictions on the single strands they interact with: we consider only two-domain single strands consisting of one toehold domain and one recognition domain. We study fork and join signal-processing gates based on these structures, and we show that these systems are amenable to formalization and to mechanical verification.

1 Introduction

DNA strand displacement offers an autonomous way to compute with molecular signals and gates. Its basic operations use toehold binding and branch migration, with matched displacement irreversible and toehold exchange reversible.

1 Introduction

  • DNA strand displacement computation proceeds autonomously after signals and gates are mixed, using gate structures as energy and converting them to inactive waste.The apparatus requires only DNA molecules and can be chemically synthesized and run in basic wet labs.Source: §1 · p. 1
  • Molecular computing aims include program-controlled nanoscale structure production and interfaces to biological entities, with Petri nets and state machines representing abstract signals on DNA strands.Source: §1 · p. 1
  • A short toehold initiates binding, after which the incoming x domain replaces the top x strand through branch migration.Source: §1 · p. 1, Figure 1 · p. 2
  • Matched domains can complete strand displacement irreversibly, whereas mismatched or only initially matching domains fail to displace and revert.The matching case becomes essentially irreversible when the displaced top strand detaches without a reverse-reaction toehold.Source: §1 · p. 2
  • Toehold exchange can displace one strand while remaining reversible, and these reversible and irreversible reactions are fundamental steps for composing computations.Source: §1 · p. 2

2 Two-domain Signals and Gates

The section presents a streamlined architecture using two-domain signals and top-nicked DNA structures, then develops transducer, fork, catalyst, and join gates. Strand restrictions preserve the structural invariant while supporting composable circuits.

Two-domain strand displacement gates.

  • The transducer Txy converts input tx into ty through two displacement cascades linked by a privately used auxiliary cosignal.The output release is reversible, but subsequent reactions lock down the gate and reabsorb xt and ta.Source: Two-domain strand displacement gates · pp. 3–4
  • The fork Fxyz releases ty and tz from tx, while catalyst Cxyz uses inputs tx and ty to produce ty and tz.The catalyst’s right half is unchanged from the fork; its left half produces the yt cosignal used there.Source: Two-domain strand displacement gates · pp. 4–5
  • The binary join Jxyz combines tx and ty to release tz, and its garbage collector converts active yt residuals to waste.The collector is triggered only after release of a private strand, avoiding premature reclamation of an extraneous yt cosignal.Source: Two-domain strand displacement gates · p. 5

Discussion: The double strand restrictions.

  • Populations of the simplified structures’ fork and join gates are equivalent to Petri Nets.The structures also have simple syntax and reduction rules that simplify formal verification.Source: Discussion: The double strand… · p. 6

Discussion: The single strand restrictions.

  • To preserve ndsDNA, allowable single strands exclude forms that could create stable non-ndsDNA configurations or competing toeholds.The discussion narrows the remaining signals to tx and xt, with a further reversible interaction between tx and yt over t†xy†t.Source: Discussion: The single strand… · p. 6

Discussion: The double strand restrictions, revisited.

3 Nick Algebra

Nick algebra formalizes systems of top-nicked double strands using restricted strand syntax and compositional soups. It defines system evolution through reaction rules, with waste handled explicitly or implicitly.

3 Nick Algebra

  • The formalism uses one distinguished toehold t from a finite set of short domains and an unbounded set of long domains, while multi-toehold generalization is possible.Designs using distinct toeholds may fail if those toeholds are later identified.Source: §3 · p. 7
  • Double strands use † for top-strand nicks, and the segments between nicks are restricted to single or paired toeholds and domains.Single strands have the form t.x or x.t, usually written tx or xt; standalone t, x, and x.y strands remain implicit waste.Source: §3 · p. 7
  • The nick algebra models soups as finite multisets of single and double strands, supports private-domain isolation, and forms a strict subset of the DSD language.Isolation allows locally defined domains to be combined compositionally, with private domains kept distinct in a global system.Source: §3 · p. 7
  • Algebraic equality captures concatenation, parallel-soup, and isolation laws, allowing private domain definitions to be renamed and combined without global conflicts.The laws include commutativity of parallel composition and scope rules for isolation.Source: Definition: Term Syntax · p. 8, Definition: Algebraic Equality · p. 8
  • System evolution is the smallest reduction relation generated by exchange, coverage, and cooperation reactions, closed under soup composition, isolation, and algebraic equality.The reflexive, symmetric, and transitive closure describes multi-step evolution.Source: Definition: Algebraic Equality · p. 8, Definition: Reduction · p. 8
  • Single-stranded waste is omitted from the syntax, while double-stranded waste has a degradation rule and reactive strands are those matching one of five specified forms.Eliminating unreactive components by an observational equivalence is offered as an alternative to the waste rule.Source: §3 · p. 7, Definition: Algebraic Equality · p. 8, Definition: Reduction · p. 9

4 Correctness

The section establishes may-correctness for transducer populations and fork and join gates, then examines stronger will-correctness and how interference complicates composition. A single transducer’s will-correctness is checked by enumerating reachable states, while composed gates can exhibit cross-talk and small-population deadlock.

4 Correctness

  • Will-correctness requires every reachable intermediate state to retain a path to the output, and the single-transducer case is checked by enumerating states up to algebraic equality.The enumerated states are each checked for a path to the desired output.Source: §4 · p. 9, Proof · p. 11
  • For n transducers sharing a private domain, the proof lifts a single-transducer input-to-output reduction to a population-level may-correctness result.The proof uses induction, associativity, and isolation of the private domain.Source: Definition: Two-Domain Pictograms · p. 9, Proof · p. 10
  • The fork and join gates may produce their specified outputs from their respective inputs: x yields y and z at the fork, while x and y yield z at the join.These reductions are stated for n copies of each gate.Source: Proof · p. 10
  • Correctness in all contexts fails when a context can absorb the public output strand, and each transducer can interfere with another copy of itself.Restricting to noninterfering contexts would require tracking which context elements each component may interfere with.Source: Proof · p. 10
  • Composed transducers’ will-correctness does not follow from the single-transducer result and requires analyzing a product state space.The stated composition property includes cases where signal names coincide.Source: Proof · p. 11
  • Two individually correct transducers using a public auxiliary domain can cross-talk, producing a final state that is not the expected output and lacks will-correctness.The crosstalk example leaves the system deadlocked even though another derivation can produce the expected output.Source: Proof · pp. 11–12
  • Although small populations may deadlock, large populations may converge to an almost-correct solution with high probability.This behavior is reported in stochastic and ODE simulations; the residual auxiliary cosignal concentration tends asymptotically to zero in the ODE simulation.Source: Proof · p. 12

5 Testing

An ODE simulation tested a circuit combining two fork and four join gates. The computation reached 90% completion by time 300, with similar output quantities approaching 0.5.

5 Testing

  • 90% completion was reached at time 300, with similar output quantities approaching the expected 0.5 concentration.The four outputs were yv, yw, zv, and zw.Source: §5 · p. 12, Figure 11 · p. 13
  • At time 3, yv led production and zw trailed; by time 30, yv and yw, and zv and zw, were closer.The gates accept inputs and produce outputs in a specific order, so identical production rates were not expected.Source: §5 · p. 12
  • The simulated system contained 54 single-strand species, 108 double-strand species, 172 reactions, and therefore 162 ODEs.Unit rates were used for toehold binding and unbinding, with input concentrations of 1.0 and gate concentrations of 10.0.Source: §5 · p. 12
  • Trajectory inspection indicated no deadlock, and all structures turned into output or waste.The higher curve tracked accumulation of the four join-gate garbage species, indicating conversion of all gates to waste.Source: §5 · p. 12

6 Conclusions

The paper presents simple two-domain fork and join gates that automatically remove active garbage, and a formal framework for studying their behavior. Proving absence of interference across all combinations and numbers of gates and inputs remains a substantial task.

6 Conclusions

  • The proposed fork and join gates use simple two-domain structures and automatically remove all active garbage.The implementation is described as a clean implementation of the higher-level strand algebra of.Source: §6 · p. 13
  • A formal framework is provided for calculations, correctness definitions, and studying complex behavioral properties of the gate designs.Source: §6 · p. 13
  • Proving absence of interference for every combination and number of gates and inputs requires extensive case analysis, likely automation, and appropriate invariants; simulation testing is an alternative way to gain confidence.Source: §6 · p. 13

7 Appendix

The appendix proves may-correctness for binary fork and join gates by deriving their signal transformations. It also provides a DSD script defining gates and a test circuit.

7.1 May-Correctness of binary Fork and Join gates

  • The fork gate is shown to transform input x into outputs y and z through repeated gate copies, using induction and associativity.The proof then applies isolation to the system with private domain a.Source: Proof · p. 14
  • The join gate is shown to transform inputs x and y into output z through repeated gate copies, using induction and associativity.Its construction uses private domains a and b.Source: Proof · pp. 14–15

7.2 DSD Script for Figure 11

  • The script can be run in a browser using DSD's deterministic simulation.Source: §7.2 · p. 15
  • The DSD script defines fork and join gates parameterized by N and constructs a test network with two fork gates, four join gates, and inputs x and u.The supplied definitions use N=10 in that network.Source: §7.2 · p. 15
Loading 1006.2993v1…