Att konstruera korrekta, robusta DNA-enheter är svårt på grund av de många möjligheterna till oönskade störningar mellan molekyler i systemet. DNA-strängsförskjutning har föreslagits som ett designparadigm för DNA-enheter, och programmeringsspråket för DNA-strängsförskjutning (DSD) har utvecklats som ett sätt att formellt programmera och analysera dessa enheter för att kontrollera oönskade störningar. Vi demonstrerar för första gången användningen av probabilistiska verifieringstekniker för att analysera DNA-enheters korrekthet, tillförlitlighet och prestanda under konstruktionsfasen. Vi använder den probabilistiska modellkontrollen PRISM, i kombination med DSD-språket, för att designa och felsöka DNA-strängsförskjutningskomponenter och för att undersöka deras kinetik. Vi visar hur våra tekniker kan användas för att identifiera konstruktionsfel och för att utvärdera fördelarna med kontrasterande designbeslut, även på apparater som innehåller relativt få ingångar. Vi demonstrerar sedan användningen av dessa komponenter för att konstruera en DNA-strängsförskjutningsanordning för ungefärlig majoritetsomröstning. Slutligen diskuterar vi några av utmaningarna och möjliga anvisningar för att tillämpa dessa metoder på mer komplexa konstruktioner.
De har nyligen använt DSD strand deplacement specifikation språk och den probabilistiska modellkontroll PRISM för att verifiera egenskaper på enkla DNA-reaktion grindar och sedan komponera dem till ett större DNA-system som implementerar den ungefärliga majoriteten protokollet REF.
Design and analysis of DNA strand displacement devices using probabilistic model checking
{'venue': 'Journal of The Royal Society Interface', 'journal': 'Journal of The Royal Society Interface', 'mag_field_of_study': ['Computer Science', 'Medicine']}