Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Design and Analysis of DNA Strand Displacement Devices using Probabilistic Model Checking

Matthew Lakin, David Parker, Luca Cardelli, Marta Kwiatkowska, and Andrew Phillips

Abstract

Designing correct, robust DNA devices is difficult because of the many possibilities for unwanted interference between molecules in the system. DNA strand displacement has been proposed as a design paradigm for DNA devices, and the DSD programming language has been developed as a means of formally programming and analysing these devices to check for unwanted interference. We demonstrate, for the first time, the use of probabilistic verification techniques to analyse the correctness, reliability and performance of DNA devices during the design phase. We use the probabilistic model checker PRISM, in combination with the DSD language, to design and debug DNA strand displacement components and to investigate their kinetics. We show how our techniques can be used to identify design flaws and to evaluate the merits of contrasting design decisions, even on devices comprising relatively few inputs. We then demonstrate the use of these components to construct a DNA strand displacement device for approximate majority voting. Finally, we discuss some of the challenges and possible directions for applying these methods to more complex designs.

Details

Publication typeArticle
Published inJournal of the Royal Society Interface
URLhttp://dx.doi.org/10.1098/rsif.2011.0800
Pages1470-1485
Volume9
Number72
PublisherThe Royal Society
> Publications > Design and Analysis of DNA Strand Displacement Devices using Probabilistic Model Checking