Modelling, simulating and verifying Turing-powerful strand displacement systems

We demonstrate how the DSD programming language can be used to design a DNA stack machine and to analyse its behaviour. Stack machines are of interest because they can efficiently simulate a Turing machine. We extend the semantics of the DSD language to support operations on DNA polymers and use our stack machine design to implement a non-trivial example: a ripple carry adder which can sum two binary numbers of arbitrary size. We use model checking to verify that the ripple carry adder executes correctly on a range of inputs. This provides the first opportunity to assess the correctness and kinetic properties of DNA strand displacement systems performing Turing-powerful symbolic computation.

Lakin...Phillips - DNA 2011 - Modelling, Simulating and Verifying Turing-Powerful Strand Displacement Systems.pdf
PDF file

In  International Conference on DNA Computing and Molecular Programming

Publisher  Springer Verlag

Details

TypeArticle
URLLocalized Hybridization Circuits
Pages130-144
Volume6937
> Publications > Modelling, simulating and verifying Turing-powerful strand displacement systems