Two-Domain DNA Strand Displacement
Luca Cardelli
Microsoft Research
Cambridge, UK

luca@microsoft.com

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

Among the many techniques being developed for molecular computing [5], DNA strand displacement has
been proposed as mechanism for performing computation with DNA strands [8, 3]. In most schemes,
single-stranded DNA acts as signals and double-stranded (or more complex) DNA structures act as gates.
Various circuits have been demonstrated experimentally [10]. The strand displacement mechanism is
appealing because it is autonomous [4]: once signals and gates are mixed together, computation proceeds
on its own without further intervention until the gates or signals are depleted (output is often read by
fluorescence). The energy for computation is provided by the gate structures themselves, which are
turned into inactive waste in the process. Moreover, the mechanism requires only DNA molecules: no
organic sources, enzymes, or transcription/translation ingredients are required, and the whole apparatus
can be chemically synthesized and run in basic wet labs.
The main aims of this approach are to harness computational mechanisms that can operate at the
molecular level and produce nano-scale structures under program control, and somewhat separately that
can intrinsically interface to biological entities [2]. The computational structures that one may easily
implement this way (without some form of unbounded storage) vary from Boolean networks, to state
machines, to Petri nets. The last two are particularly interesting because they take advantage of DNA’s
ability to encode symbolic information: they operate on DNA strands that represent abstract signals.
The fundamental mechanism in many of these schemes is toehold mediated branch migration and
strand displacement [10], which implements a basic step of computation. It operates as shown in Figure
1, where each letter and corresponding segment represents a DNA domain (a sequence of nucleotides,
C,G,T ,A) and each DNA strand is seen as the concatenation of multiple domains. Single strands have
an orientation; double strands are composed of two single strands with opposite orientation, where the
bottom strand is the Watson-Crick, C − G, T − A, complement of the top strand. The ‘short’ domains
hybridize (bind) reversibly to their complements, while the ‘long’ domains hybridize irreversibly; the
exact critical length depends on physical condition. Distinct letters indicate domains that do not hybridize
with each other.
In the first reaction of Figure 1, a short toehold domain t initiates binding between a double strand and
a single strand. After the (reversible) binding of the toehold, the x domain of the single strand gradually
replaces the top x strand of the double strand by branch migration. The branching point between the
S. B. Cooper, E. Kashefi, P. Panangaden (Eds.): Developments in
Computational Models (DCM 2010)
EPTCS 26, 2010, pp. 47–61, doi:10.4204/EPTCS.26.5

48

Two-Domain DNA Strand Displacement

Figure 1: Toehold-mediated DNA branch migration and strand displacement

=
Figure 2: Examples of allowable single and double strands: t † x†t † x†t,tx, xt, x
two top x domains performs a random walk that eventually leads to displacing the x strand. The final
detachment of the top x strand makes the whole process essentially irreversible, because there is no
toehold for the reverse reaction. The second reaction illustrates the case where the top domains do not
match: then the toehold binds reversibly and no displacement occurs. The third reaction illustrates the
more detailed situation where the top domains matches only initially: the branch migration can proceed
only up to a certain point and then must revert back to the toehold: hence no displacement occurs and
the whole reaction reverts.
The fourth reaction illustrates a toehold exchange, where a branch migration (of strand tx) leads to a
displacement (of strand xt), but where the whole process is reversible via a reverse toehold binding and
branch migration. The first (irreversible) and fourth (reversible) reactions are the fundamental steps that
can be composed to achieve computation by strand displacement.

2

Two-domain Signals and Gates

We now describe some DNA strand displacement structures that emulate, depending on the point of view,
either chemical reactions or Petri net transitions. Their function is to join input signals and fork output
signals. To achieve compositionality, so that gates can be composed arbitrarily into larger circuits, it
is necessary to first fix the structure of the signals. Any given choice of signal structure requires a
different gate architecture, for example for 4-domain signals [9] (signals composed of 4 segments of
different function), and 3-domain signals [1]. Here we present a new, streamlined, architecture based on
2-domain signals, where the gates can be combined into arbitrary circuits (including loops), and where
the waste products do not interfere with the active gates.

Luca Cardelli

49

Figure 3: Transducer Txy | tx → ty: initial state plus input tx.
Top-nicked double strands.
Double-stranded DNA (dsDNA) can have interruptions (nicks) on one strand while remaining connected
if the opposite strand has enough hold on the area around the nick. We called such structures nicked
double-stranded DNA (ndsDNA). This excludes any long overhangs or any protrusions from the doublestrand. In particular, we work with top-nicked double-strands, where all the nicks are on one strand
(the top one by convention). A deviation from this simple structure happens fleetingly during branch
migration, but all the initial and final species we use are ndsDNA.
We use t for short domains, x,y,z for long domains, and a,b,c for long domains that are meant to
be privately used by some construction. We write, e.g., tx for a single-stranded DNA (ssDNA) strand
consisting of a toehold t followed by a domain x, and similarly for xt. We write, e.g., txy for a fully
complemented double strand consisting of a continuous strand txy at the top and its Watson-Crick complement at the bottom. Finally, we write tx† y to indicate the same double strand but with a nick at the top
between x and y. In the figures, a nick is indicated by an arrowhead and a discontinuity.
Examples of allowable single and double strands are shown in Figure 2. We assume that domains
indicated by different letters are distinct, so that, e.g., x does not hybridize with y, zy, yz, ty, or yt. To
simplify our notation, we use an implicit equivalence illustrated in the bottom part of the figure. Suppose
we start with a regular double strand, and we nick it at the top (bottom left). Long segments between
nicks remain attached to the bottom strand, while short toehold segments can detach and reattach (bottom
right). We regard these reversible states as equivalent; the notation x†t † y then indicates two equivalent
situations, where the top t is either present or absent, and where t is implicitly exchanged with the
environment. Hence, we can use x†t † y to indicate an open toehold between x and y, because the toehold
is available (sometime). This way, we do not need to use separate notations for temporarily occluded
and temporarily open toeholds, which we would have to regard as equivalent anyway (up to some kinetic
occlusion effects).
Two-domain strand displacement gates.
All our gates are top-nicked dsDNA and our signals are two-domain ssDNA. This simple setup is more
expressive than it might appear at first. For example (Figure 3), let us consider a single strands tx as
encoding a signal, with the strand xt as its cosignal, and consider the problem of constructing a signal transducer Txy from a signal tx to a signal ty, with the reduction Txy | tx → ty, where | is parallel
composition of components, and final waste is discarded. All signals share the same toehold t, and
are distinguished by the long domains x,y,z, etc. As shown in Figure 4, the input tx can initiate a signal/cosignal cascade of strand displacements in the left double-strand that after two toehold exchanges
releases a private cosignal at (the segment a is privately used by the Txy transducer, with a distinct a for
each xy pair). The at cosignal then initiates a backward cascade in the right double strand that releases
the desired output signal ty at the fourth reaction. The release of ty is reversible, but the gate is then

50

Two-Domain DNA Strand Displacement

Figure 4: Transducer Txy | tx → ty reactions.

Figure 5: Fork Fxyz | tx → ty | tz: initial state plus input tx.
locked down by the last two reactions. The locking down of the gate is also used to reabsorb the xt and
ta strands, by exploiting the x end of the right structure and the a end of the left structure. In the end,
only unreactive (no exposed toeholds) dsDNA and ssDNA is left. In Figure 4, the initial structures from
Figure 3 are shown inside rounded rectangles, and the final structures inside squared rectangles. The
reaction rules are described abstractly in Figure 10.
The structures in Figure 3 can be written in the notation described above as Txy = t † xt † at † a | ta |
x†ty†ta†t | yt. The auxiliary signal ta contains the private segment a, uniquely joining the two halves
of Txy transducers, and we can therefore assume that it will not interfere with other gates. The auxiliary
cosignal yt however contains a public segment y, which is necessary to release the output signal. It is
therefore important to maintain an invariant that no other gate in the whole system spontaneously absorbs
yt, or in general any public cosignal, although it may do so in a proper response to inputs. For example,
a Tzy transducer and a Txy transducer may use “each other’s” yt cosignal without problem.
The transducer Txy can be extended easily to a fork gate Fxyz such that Fxyz | tx → ty | tz, releasing two
outputs from one input. This is shown in Figure 5, where the left half of the structure is the same as in
Txy . The fork gate can be extended to a catalytic gate Cxyz such that Cxyz | tx | ty → ty | tz (Figure 6). The
right half of Cxyz is unchanged from Fxyz , except that yt is not required because it is produced by the left
half. This gate, like the more general join gate discussed next, takes two inputs, but absorbs them only if

Figure 6: Catalyst Cxyz | tx | ty → ty | tz: initial state plus inputs tx and ty.

Luca Cardelli

51

Figure 7: Join Jxyz | tx | ty → tz: initial state plus inputs tx, ty.

Figure 8: Join Jxyz | tx | ty → tz: final state plus output tz.
both inputs are present [9]. If only the first input is present, it is returned to the soup by reversibility of
strand displacement between tx and xt.
Let us now consider, in Figures 7 and 8, a binary join gate Jxyz such that Jxyz | tx | ty → tz (the
generalization to additional outputs works as in the fork gate). Each distinct combination of xyz requires
choosing a distinct private domain connecting the two halves of the gate; this private domain can however
be shared among a population of gates with the same input and output signals. The main new feature
in this gate is the additional t † by†t structure that absorbs a signal and a cosignal together, or neither
separately. Without it, and without the bt, tb components, the join gate would leave behind a yt residual
(all the other single strands, xt, zt, ta, are reclaimed). Hence t † by†t is a ‘garbage collector’ turning
undesired active residuals to waste. It is triggered only after the release of a private strand tb, so that
the collector does not reclaim an extraneous cosignal yt before the join gate has committed to its inputs.
Such an extraneous yt could come from a transducer Txy , or from another join Juvy (before any input) or
Jyuv (after the first input) causing cross-gate interference, or even from within the same join, as in Jxyy .
Removing garbage is important because accumulated garbage slows down future reactions by imposing a
growing reverse pressure on the desired direction of the reactions. We have designed all gates to remove
all active garbage, but until now garbage removal did not require additional double strands. The Join
structure is easily generalized to any number of inputs; for example, Figure 9 shows a 3-input Join with
collectors.
Discussion: The double strand restrictions.
The restriction of allowing only ndsDNA structures has a number of potential advantages. The absence of any branching seems inherently more trouble-free than complex structures that can interact
in unexpected ways through their protruding single-stranded parts. Here all double-stranded structures
are quiescent (except for receptive toeholds on the bottom strand) and only single-stranded components
have hybridization potential, eliminating the possibility that the gate themselves may polymerize, or may

52

Two-Domain DNA Strand Displacement

Figure 9: 3-Join Jwxyz | tw | tx | ty → tz: initial state plus inputs tw, tx, ty.
self-interact. These structures also have a simple syntactical representation and simple reduction rules,
which simplify formal verification. Nothing prevents us from devising precise syntax and reductions for
more general structures [7], and there is no good reason in principle to avoid more complex structures if
they work well. However, we have shown that our simplified structures already cover a surprising range
of computation (fork and join gates in populations are equivalent to Petri Nets [1]), and hence one can
restrict the use of more complex structures to the situations where they are actually needed, or where
they somehow perform better.
Discussion: The single strand restrictions.
Our hybridized structures start as ndsDNA, but we have to ensure that they remain ndsDNA through
computation. (Except for transients, i.e., during branch migrations that either revert harmlessly or lead to
strand displacements.) This invariant puts constraints on the allowable single strands. First of all, single
strands consisting only of long segments are inert because all the double strands are fully complemented
(except for toeholds), and hence they can be ignored. A single strand of the form xty could bind to a
double strand of the form x†t † z, leading to a configuration that is stable and is not ndsDNA. Therefore
our single strands cannot contain substrands of the form xty, and we are left with single strands of the
form, xnt m or t n xm or t n xmt p . The third class could lead to stable configurations with two overlapping
competing toeholds (t † x†t † y†t with txt and tyt) and hence are ruled out too. Multiple toeholds in sequence
bind as stably as a long domain, so e.g. xttt would be as bad as the former xty, and they can lead to
competing toeholds: x†t †t † y with xtt and tty. Hence we do not allow consecutive toeholds in the top
strands. Similarly, strands with consecutive long segments can lead to stable competition: txy and yzt
over t † xyz†t. In the end, we are left only with xt or tx, and the only remaining competition is between
tx and xt over t † x†t, where the stable structures are ndsDNA. A final case to consider is tx and yt over
t † xy†t: if a single strand is present it binds only reversibly, and if both are present they both bind stably
and release xy, so the stable structures are always ndsDNA. In fact, t † xy†t is an important configuration
that seems to add some power: without it we can still implement garbage-collecting join gates, but
apparently only by using more than one distinct toehold.
Discussion: The double strand restrictions, revisited.
We finally have to make sure that no reactive single strands other than t, tx, xt, plus the unreactive x and
xy, are ever released from double strands during computation. This imposes another restriction on double
strands: nicks should break the top strand into segments of two domains or less. Otherwise, the double
strand t † xty†t could release a forbidden single strand xty in presence of tx and yt. (We could still allow
t † xyz†t, but it would be unreactive.) Hence, we are left with allowable double strands that are nicked
concatenations of the double-stranded elements t, x, tx, xt, xy.

Luca Cardelli

53

Figure 10: The basic reactions (D1,D2 are arbitrary or empty double strands).

3

Nick Algebra

In this section we provided a formal framework where we can perform calculations about the evolution
of systems of top-nicked double strands. Domains are taken either from a finite set of short domains
(toeholds) or from an unbounded set of long domains ranged over by x,y,z and a,b,c. The set of toeholds
must be finite (and in practice quite small) because of its reversible-binding assumption that limits length
and hence cardinality. Designs based on a single toehold can be easily adapted to multiple toeholds to
increase binding discrimination and efficiency, but the converse is problematic: designs based on distinct
toeholds may fail if the toeholds are then identified. Here we require only a single distinguished toehold,
always indicated by the constant t, but it would be easy to generalize to multiple toeholds.
An infix operator ‘.’ may be used to concatenate domains into single strands; this is often omitted,
particularly because all our single-strands have the form t.x or x.t, which are then usually written tx
and xt (unless we wish to use long identifiers for domains). Single strands t, x, and x.y remain implicit
‘waste’, and are not used in the syntax.
Double strands are written underlined. We use an infix operator ‘† ’ to represent a ‘nick’ on the
top strand of a double-stranded sequence, an infix operator ‘.’ (often omitted) to represent the unbroken
concatenation of top and bottom strands, and /o for the empty double strand. The segments between nicks
are only single or pair combinations of toeholds and domains.
A soup U is a finite multiset of single and double strands, with multiset union indicated by ‘ | ’, and
with a notation (νx)U for domain isolation. The latter indicates that x is not used outside of U: this
allows us to declare private domains locally, and to combine constructions compositionally. In practice,
it means simply that all the domains indicated by ν must be chosen distinct when a global system is fixed
for execution: the algebraic laws for (νx)U encode such a guarantee. We also use U n as an abbreviation
for n copies of U in parallel ( | ). The resulting algebra is our nick algebra, which is strictly a subset of
the DSD (DNA Strand Displacement) language [7].
Definition: Term Syntax
S ::= t.x | x.t
D ::= /o | t | x | t.x | x.t | x.x | D† D
U ::= S | D | U|U | (νx)U

Single strand
Double strand
Soup

The set of public domains pd(U) is the inductively defined set of those domains not bound by ν
in U; in particular pd(t.x) = pd(x.t) = pd(x) = pd(t.x) = pd(x.t) = {x}, pd(x.y) = {x, y}, pd(t) =
pd(/o) = {}, and pd((νx)U) = pd(U) − {x}. Then, U{y/x} is the substitution of y for x in U, with

54

Two-Domain DNA Strand Displacement

the representative cases t{y/x} = t, x{y/x} = y, z{y/x} = z for z 6= x, ((νz)U){y/x} = (νz)U{y/x} for
z∈
/ {x, y}, ((νx)U){y/x} = (νx)U, and ((νy)U){y/x} = (νz)U{z/y}{y/x} for a z ∈
/ pd(U) ∪ {x, y}.
Algebraic equality (a binary congruence relation over the term syntax) is indicated just by = and
is axiomatized below with the monoid laws of (/o, † ), the commutative monoid laws of (/o, | ), and the
scoping laws of (νx)U [6].
Definition: Algebraic Equality
= is an equivalence relation
D1 = D2 , D3 = D4 ⇒ D1 † D3 = D2 † D4
U1 = U2 , U3 = U4 ⇒ U1 | U3 = U2 | U4
U1 = U2 ⇒ (νx)U1 = (νx)U2
D1 † (D2 † D3 ) = (D1 † D2 )† D3
o=D
/o† D = D† /
U1 | (U2 | U3 ) = (U1 | U2 ) | U3
U1 | U2 = U2 | U1
o=U
/o | U = U | /
(νx)U = (νy)(U{y/x})
if y ∈
/ pd(U)
(νx)/o = /
o
(νx)(U1 | U2 ) = U1 | (νx)U2
if x ∈
/ pd(U1 )
(νx)(νy)U = (νy)(νx)U
Note that (νx)(νx)U = (νx)U is derivable. As an example of use of the isolation operation, consider
that it is always possible to bring all the ν prefixes to the top level by making all the private domains
distinct: (νx)tx | (νx)tx = (νx)tx | (νy)ty = (νx)(νy)(tx | ty). This means that conflicts between local
definitions can be resolved globally, while allowing local definition to be combined without consideration
of global conflicts.
The reduction relation U1 → U2 describes a single step of system evolution; it is the smallest binary
relation on U satisfying the rules below, where ↔ stands for two reduction rules in opposite directions. Its
symmetric and transitive closure U1 →∗ U2 describes multi-step system evolution. In the reduction rules,
the single-stranded waste (t, x, xy) is automatically removed because it can be immediately identified as
waste (as a consequence, the single strands t, x, xy need not be included in the syntax). Alternatively,
we could have made the single-stranded waste explicit and introduced separate rules to remove it. The
double-stranded waste instead has a special degradation rule because it requires a check over the whole
double strand. The four basic reactions (exchange, coverage, cooperation) are depicted in Figure 10.
Definition: Reduction
D1 †t † xt † D2 | tx ↔ D1 †tx†t † D2 | xt
D1 †t † x† D2 | tx → D1 †tx† D2
D1 † x†t † D2 | xt → D1 † xt † D2
D1 †t † xy†t † D2 | tx | yt → D1 †tx† yt † D2
D→/
o
if D not reactive
U1 → U2 ⇒ U1 | U → U2 | U
U1 → U2 ⇒ (νx)U1 → (νx)U2
U1 = U2 ,U2 → U3 ,U3 = U4 ⇒ U1 → U4

Exchange
Left coverage
Right coverage
Cooperation
Waste
Dilution
Isolation
Well-mixing

Luca Cardelli

55

A double strand D is reactive if it can react in some context; that is, by the first four rules. Hence
it must be of the form D1 †t † xt † D2 , D1 †tx†t † D2 , D1 †t † x† D2 , D1 † x†t † D2 , or D1 †t † xy†t † D2 . Among the
unreactive (waste) double strands are thus t, x, xt, tx, xy, t †t, t †tx, xt †t, xt †ty, xt †t †ty, etc. The waste rule
is really a convenience to simplify results of calculations; more generally, as commonly done in process
algebra, one would instead eliminate unreactive components via an observational equivalence [6].

4

Correctness

If U1 →∗ U2 then U1 may reduce to U2 , but it may also reduce to something else since →∗ is a relation.
When U1 →∗ U2 is used to state a correctness property of system reduction, we say that this is a maycorrectness property: the system starting from U1 may reduce to U2 , but it may also wander in a different
section of state space and never be able to get to U2 from there. A stronger property is will-correctness,
indicated by U1 →∀ U2 , and defined as ∀U, U1 →∗ U ⇒ U →∗ U2 . This means that although U1 may
wander to some U in some part of the state space, it will always find a path to U2 from there (it cannot
avoid finding a path to U2 ). If U1 →∀ U2 and U2 is the only terminal state, then we can say that U1 must
reduce to U2 . But will-correctness does not imply that reduction necessarily terminates, and in particular
if U →∀ U we can say that U is reversible. Since U1 →∗ U1 holds by reflexivity, will-correctness implies
may-correctness. (All these properties are really examples of a large class of reachability properties that
could be expressed in a temporal logic.)
It is convenient in the next examples and proofs to use a more pictographic notation for nick algebra
expressions, to highlight the positions of the toeholds. We use the following abbreviations († is still
needed in for x† y):
Definition: Two-Domain Pictograms
px

xq
Dp x
xq D
D^ D’

for tx
for xt
for D†tx (including D = /
o)
for xt † D (including D = /
o)
†
†
for D t D’ (including D = /
o or D’ = /o)

Signal
Cosignal
Bound signal
Bound cosignal
Bottom toehold

For example, the transducer from Figure 3 can be written as:
t † xt † at † a | ta | x†ty†ta†t | yt
^ xq aq a | p a | xp yp a^ | yq

explicit notation
pictogram notation

We now show that the transducer may work correctly. Because of their chemical origin, all components come in populations of identical molecules, and any private domain can only be private to a
population, and not to an individual molecule. Hence we need to show that a populations of transducers,
all sharing the same private domain, may map an input population to a desired output population.
Proposition 1: Transducer Txyn May-Correctness
Let Txyn = (νa)((^ xq aq a | p a | xp yp a^ | yq )n ),
then Txyn | p xn →∗ p yn .

56

Two-Domain DNA Strand Displacement

Proof
Let T xay = ^ xq aq a | p a | xp yp a^ | yq for a 6= x, y, so that Txyn = (νa)((T xay )n ). We first show that T xay | p x →∗
p y.
T xay | p x
= ^ xq aq a | p a | xp yp a^ | yq | p x
↔ p x^ aq a | p a | xp yp a^ | yq | xq
↔ p xp a^ a | xp yp a^ | yq | xq | aq
↔ p xp a^ a | xp y^ aq | yq | xq | p a
→ p xp ap a | xp y^ aq | yq | xq
→ xp y^ aq | yq | xq
↔ x^ yq aq | xq | p y
→ xq yq aq | p y
→ py
Hence (T xay | p x)n →∗ p yn by induction, (T xay )n | p xn →∗ p yn by associativity, (νa)((T xay )n | p xn )
→∗ (νa)p yn by isolation, and Txyn | p xn →∗ p yn by ν-equivalence and by Txyn definition. End proof.
We can similarly check the may-correctness of fork and join gates:
n May-Correctness
Proposition 2: Fork Fxyz
n = (νa)(( x a a | a | x z y a | z | y )n ),
Let Fxyz
^ q q
p
p p p ^
q
q
n
n
∗
n
n
then Fxyz | p x → p y | p z .

n May-Correctness
Proposition 3: Join Jxyz
n = (νa)(νb)(( x y a a | a | x b z a | b | z | b† y )n ),
Let Jxyz
^
^ q q q
p
p p p ^
q
q ^
n | xn | yn →∗ zn .
then Jxyz
p
p
p

Consider now the difficulties involved in proving more interesting properties. We would like a transducer, for example, to work correctly in ‘all possible contexts’. Unfortunately that is just not true, because
some context could absorb the yq strand, which is public, and interfere with the transducer. One would
have to consider instead ‘all possible contexts that do not interfere with yq ’. This is a rather awkward
notion: for compositionality one would have, for each component, to keep track of all the elements in
the context that the component might be interfering with. Moreover, the transducer interferes with yq ,
and hence it interferes with (another copy or another population of) itself.
Let us consider a simpler ‘progress’ property: that the transducer does not deadlock with itself. This
can be expressed as a will-correctness property, that for any intermediate state U, if Txyn | txn →∗ U then
U →∗ tyn . This appears to require an induction on all possible intermediate configurations U for any
n. Even for a fixed small n, the state space U can grow very large, which suggests that automated
state exploration tools should be useful. Note also that an induction on the length of →∗ is problematic
because of the reversible exchange rule: infinite sequences of reductions exist in almost all systems. In
a stochastic interpretation of reduction, actual convergence can often be achieved (with measure 1), and
this is another challenging property to prove.
We now illustrate how to check a will-correctness property, for a single copy of a transducer:

Luca Cardelli

57

Proposition 4: Txy1 Will-Correctness
Txy1 | p x →∀ p y.

Moreover, p y is the only reachable terminal state.

Proof
We show that if Txy1 | p x →∗ U then U →∗ p y. We enumerate all distinct states U, up to algebraic equality,
arising from Txy1 | tx by all possible traces, and then we check that each state can lead to p y. Assume
x 6= y; indentation means a branch in the derivation:
01. (νa) ^ xq aq a | p a | xp yp a^ | yq | p x
02. ↔ (νa) p x^ aq a | p a | xp yp a^ | yq | xq
03. ↔ (νa) p xp a^ a | xp yp a^ | yq | xq | aq
04. ↔ (νa) p xp a^ a | xp y^ aq | yq | xq | p a
05.
↔ (νa) p xp ap a | xp y^ aq | yq | xq
06.
→ (νa) xp y^ aq | yq | xq
07.
↔ (νa) x^ yq aq | xq | p y
08.
↔ (νa) xq yq aq | p y
09.
→ py
10.
↔ (νa) p xp ap a | x^ yq aq | xq | p y → 07
→ 08
11.
↔ (νa) p xp ap a | xq yq aq | p y
12.
↔ (νa) p xp ap a | p y → 09
13. ↔ (νa) p xp a^ a | x^ yq aq | xq | p a | p y
↔ 10
14. ↔ (νa) p xp a^ a | xq yq aq | p a | p y ↔ 11
15. ↔ (νa) p xp a^ a | p a | p y ↔ 12
All other states (up to algebraic equality) can be reduced to these states by well-mixing. We can then
check that all these states have a path to state 9. The case for x = y is similar: the state graphs is the same
because, as can be seen above, there is never both an x redex and a different y redex in the same state, and
when two x signals or cosignals can be chosen, it does not matter which one is chosen, by well-mixing.
End proof.
For transducer composition, the may-correctness property Txyn | Tyzn | p xn →∗ p zn follows simply from
Proposition 1, but even just the will-correctness property Txy1 | Tyz1 | p x →∀ p z (including x = z and y = z
and x = y = z) does not follow from Proposition 4, and requires the analysis of a product state space.
For example, Txy1 | Tyx1 can absorb the inputs p x | p y sequentially (converting p x to a second p y and then
p y to p x) or in parallel (each transducer starting to process an input before producing an output). In fact,
consider the following transducer that uses a public ‘a’ domain instead of a private one:
Txay = ^ xq aq a | p a | xp yp a^ | yq
Txay by itself satisfies may and will-correctness as shown above for Txy1 , and so does Tyax . But the
two together do not satisfy the will-correctness property of just producing p x on input p x, because the
following ‘crosstalk’ derivation is possible, where in the third step aq goes to the ‘wrong’ gate:
Txay | Tyax | p x
= ^ xq aq a | p a | xp yp a^ | yq | ^ yq aq a | p a | yp xp a^ | xq | p x
↔ p x^ aq a | p a | xp yp a^ | yq | ^ yq aq a | p a | yp xp a^ | xq | xq
↔ p xp a^ a | xp yp a^ | yq | ^ yq aq a | p a | yp xp a^ | xq | xq | aq
↔ p xp a^ a | xp yp a^ | yq | ^ yq aq a | p a | yp x^ aq | xq | xq | p a
→ p xp ap a | xp yp a^ | yq | ^ yq aq a | p a | yp x^ aq | xq | xq

58

Two-Domain DNA Strand Displacement
→ xp yp a^ | yq | ^ yq aq a | p a | yp x^ aq | xq | xq
↔ xp yp a^ | yq | ^ yq aq a | p a | y^ xq aq | xq | p x
→ xp yp a^ | ^ yq aq a | p a | yq xq aq | xq | p x
→ xp yp a^ | ^ yq aq a | p a | xq | p x

The last state is final (no further progress can be made), and is not just the expected p x (which can
be obtained by a different derivation). Moreover, no p y is ever produced. The system is deadlocked
in a state where the output p x has been produced, but many other active components have been left to
interfere with future operation. However, that last state, if supplied with an additional p y, then unblocks
and reduces just to p y | p x. Hence, although Txay | Tyax | p x 9∀ p x, we have that Txay | Tyax | p x | p y →∀
p x | p y. That means that a large population of such gates in practice does not deadlock easily over an
input population of p x: each pair of stuck gates can be unblocked by another gate correctly producing
a p y, and it is very unlikely that a large fraction of gates ends up being blocked. This can be seen in
stochastic simulations of large populations, and also in Ordinary Differential Equation simulations with
unit concentration of Txay | Tyax , where the concentration of the residual p a tends asymptotically to zero.
Hence, another interesting property of these system is that, even though small populations may deadlock,
large populations may converge to an almost-correct solution with high probability.

5

Testing

Gate and circuits designs have been tested with the DSD tool [7]. We give a simple example here, testing
a combination of two fork and four join gates in the following configuration, where yv, yw, zv, zw are
four output domains (i.e., yv does not mean y.v in this section).
n |
Fx,y,z
n
Fu,v,w |
n
Jy,v,yv
|
n
Jy,w,yw |
n
Jz,v,zv
|
n
Jz,w,zw |
m
m
p x | p u (input, m ≤ n)

x

u

F

F

y
J

z
J

yv

yw

v
J

w
J

zv

zw

Since fork and join gates accept inputs and produce outputs in a specific order, one should not expect
identical rates of production of yv,yw,zv,zw. (If desired, one can mix populations of symmetric gates, to
achieve symmetric behavior.) In Figure 11 we see an Ordinary Differential Equations simulation with
unit rates for toehold binding and unbinding, and with concentrations of 1.0 for the input signals and
10.0 for the gates; hence 10% of each gates is consumed during the computation. The system has a total
of 54 single strand species, 108 double strand species, and 172 reactions, and therefore 162 ODEs. At
time 3 (left), yv is ahead out of the gates, with zw trailing last. At time 30 (middle left) yv and yw are
closer, and zv and zw are closer. At time 300 (middle right) the computation has reached 90% completion
with similar output quantities approaching the expected 0.5 concentration. The higher curve of the fourth
graph shows the total accumulation of the four p D† D’q garbage species for the join gates, indicating that
all the gates are being converted to waste. One can further examine the trajectories of all the species in
the system to check that no deadlock occurs, and that all the structures are turned to output or to waste.

Luca Cardelli

59

Figure 11: Testing a fork/join circuit.

6

Conclusions

We have shown how to implement fork and join gates via simple two-domain structures, and how to
implement them in a ‘clean’ way that automatically removes all active garbage. In essence, we have
given an implementation of the higher-level strand algebra of [1]. But is this implementation correct?
We have provided a formal framework where we can perform calculations and study such questions,
and we have discussed some simple correctness definitions and some complex behavioral properties. A
formal proof of absence of gate interference under all possible combinations and numbers of gates and
inputs will require an extensive amount of case analysis, which likely needs to be automated, as well
as the identification of appropriate invariants. Alternatively, one may gain confidence in the designs by
simulation testing.

Acknowledgments
Figures were prepared with the DSD tool [7]. I would like to thank the members of the Molecular
Programming Project at Caltech and U.Washington for many tutorials and discussions.

References
[1] L. Cardelli. Strand Algebras for DNA Computing. In DNA Computing and Molecular Programming. LNCS
5877, Springer, October 2009, pp 12-24.
[2] Y. Benenson, T. Paz-Elizur, R. Adar, E. Keinan, Z. Livneh, E. Shapiro. Programmable and Autonomous
Computing Machine made of Biomolecules. Nature, 414(22), November 2001.
[3] W. Fontana. Pulling Strings. Science 314(8), 2006.
[4] S. J. Green, D. Lubrich, A. J. Turberfield. DNA Hairpins: Fuel for Autonomous DNA Devices. Biophysical
Journal 91, October 2006, 2966–2975.
[5] M. Hagiya. Towards Molecular Programming. In G. Ciobanu, G. Rozenberg, (Eds.) Modelling in Molecular
Biology. Springer, 2004.
[6] R. Milner. Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, 1999.
[7] A. Phillips, L. Cardelli. A Programming Language for Composable DNA Circuits. Journal of the Royal
Society Interface, August 2009 6:S419-S436.
[8] G. Seelig, D. Soloveichik, D.Y. Zhang, E. Winfree. Enzyme-Free Nucleic Acid Logic Circuits. Science
314(8), 2006.
[9] D. Soloveichik, G. Seelig, E. Winfree. DNA as a Universal Substrate for Chemical Kinetics. PNAS 107 no.
12, 5393-5398.

60

Two-Domain DNA Strand Displacement

[10] B. Yurke, A.P. Mills Jr. Using DNA to Power Nanostructures. Genetic Programming and Evolvable Machines
archive 4(2), 111 - 122, Kluwer, 2003.
[11] D. Y. Zhang, A. J. Turberfield, B. Yurke, E. Winfree. Engineering Entropy-driven Reactions and Networks
Catalyzed by DNA. Science, 318:1121-1125, 2007.

7

Appendix

7.1

May-Correctness of binary Fork and Join gates

n May-Correctness
Proposition 2: Fxyz
n = (νa)(( x a a | a | x z y a | z | y )n ),
Let Fxyz
^ q q
p
p p p ^
q
q
n | xn →∗ yn | zn .
then Fxyz
p
p
p

Proof
n = (νa)((F
n
Let F xayz = ^ xq aq a | p a | xp zp yp a^ | zq | yq for a 6= x, y, z, so thatFxyz
xayz ) ). We first show
that F xayz | p x →∗ p y | p z.
F xayz | p x
= ^ xq aq a | p a | xp zp yp a^ | zq | yq | xq
↔ p x^ aq a | p a | xp zp yp a^ | zq | yq | xq
↔ p xp a^ a | xp zp yp a^ | zq | yq | xq | aq
↔ p xp a^ a | xp zp y^ aq | zq | yq | xq | p a
→ p xp ap a | xp zp y^ aq | zq | yq | xq
→ xp zp y^ aq | zq | yq | xq
↔ xp z^ yq aq | zq | xq | p y
↔ x^ zq yq aq | xq | p y | p z
→ xq zq yq aq | p y | p z
→ | py | pz
Hence (F xayz | p x)n →∗ (p y | p z)n by induction, (F xayz )n | p xn → p yn | p zn by associativity, (νa)((F xayz )n | p xn )
∗
n | xn →∗ yn | zn by ν-equivalence and by F n definition. End
→ (νa)(p yn | p zn ) by isolation, and Fxyz
p
p
p
xyz
proof.

n May-Correctness
Proposition 3: Jxyz
n = (νa)(νb)(( x y a a | a | x b z a | b | z | b† y )n ),
Let Jxyz
^ q q q
^
p
p p p ^
q
q ^
n | xn | yn →∗ zn .
then Jxyz
p
p
p

Proof
n = (νa)((J
n
Let J xyaz = ^ xq yq aq a | p a | xp bp zp a^ | bq | zq | ^ b† y^ for a 6= x, y, z, so that Jxyz
xyaz ) ). We
∗
first show that J xyaz | p x | p y → p z.
J xyaz | p x | p y
= ^ xq yq aq a | p a | xp bp zp a^ | bq | zq | ^ b† y^ | p x | p y
↔ p x^ yq aq a | p a | xp bp zp a^ | bq | zq | ^ b† y^ | p y | xq
↔ p xp y^ aq a | p a | xp bp zp a^ | bq | zq | ^ b† y^ | xq | yq

Luca Cardelli

61

↔ p xp yp a^ a | xp bp zp a^ | bq | zq | ^ b† y^ | xq | yq | aq
↔ p xp yp a^ a | xp bp z^ aq | bq | zq | ^ b† y^ | xq | yq | p a
→ p xp yp ap a | xp bp z^ aq | bq | zq | ^ b† y^ | xq | yq
→ xp bp z^ aq | bq | zq | ^ b† y^ | xq | yq
↔ xp b^ zq aq | bq | ^ b† y^ | xq | yq | p z
↔ x^ bq zq aq | ^ b† y^ | xq | yq | p z | p b
→ xq bq zq aq | ^ b† y^ | yq | p z | p b
→ ^ b† y^ | yq | p z | p b
→ pz
Hence (J xyaz | p x | p y)n →∗ p zn by induction, (J xyaz )n | p xn | p yn →∗ p zn by associativity, (νa)((J xyaz )n | p xn | p yn ) →∗
n | xn | yn →∗ zn by ν-equivalence and by J n definition. End proof.
(νa)p zn by isolation, and Jxyz
p
p
p
xyz

7.2

DSD Script for Figure 11

This script can be run from a browser in DSD [7] using ‘deterministic’ simulation.
http://research.microsoft.com/en-us/projects/dna/default.aspx
directive sample 300.0 1000
directive plot <t^ yv>; <t^ yw>; <t^ zv>; <t^ zw>; sum([t^ _]:[_ t^])
new t@1.0,1.0
def F(N, x, y, z) =
new a
( N* <t^ a>
| N* <y t^>
| N* <z t^>
| N* t^:[x t^]:[a t^]:[a]
| N* [x]:[t^ z]:[t^ y]:[t^ a]:t^ )
def J(N, x, y, z) =
new a new b
( N* <t^ a>
| N* <b t^>
| N* <z t^>
| N* t^:[x t^]:[y t^]:[a t^]:[a]
| N* [x]:[t^ b]:[t^ z]:[t^ a]:t^
| N* t^:[b y]:t^ )
(
|
|
|
|
|
|

F(10, x, y,
F(10, u, v,
J(10, y, v,
J(10, y, w,
J(10, z, v,
J(10, z, w,
1 * <t^ x>

| 1 * <t^ u> )

z)
w)
yv)
yw)
zv)
zw)

