Aarhus University Seal

publications item

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.