Conference Abstract in DNA Computing and Molecular Programming

Automated Design an Verification of Localized DNA Computation Circuits

Michael Boemo, Andrew Turberfield, Luca Cardelli

In Andrew Phillips & Peng Yin, ed., 2015, ‘DNA’,  Springer doi: 10.1007/978-3-319-21999-8_11

Presented at DNA2

  • Department of Physics, Clarendon Laboratory, University of Oxford, Parks Road, Oxford OX1 3PU, UK
  • Department of Computer Science, Wolfs Building, University of Oxford, Parks Road, Oxford OX1 3QD, UK
  • Microsoft Research Cambridge, Station Road, Cambridge CB1 2FB, UK


Simple computations can be performed using the interactions between single-stranded molecules of DNA. These interactions are typically toehold-mediated strand displacement reactions in a well-mixed solution. We demonstrate that a DNA circuit with tethered reactants is a distributed system and show how it can be described as a stochastic Petri net. The system can be verified by mapping the Petri net onto a continuous time Markov chain, which can also be used to find an optimal design for the circuit. This theoretical machinery can be applied to create software that automatically designs a DNA circuit, linking an abstract propositional formula to a physical DNA computation system that is capable of evaluating it.