Design and analysis of DNA strand displacement devices using probabilistic model checking

Area of Science:

• Synthetic Biology
• Computational Biology
• Molecular Engineering

Background:

• Designing complex DNA devices is challenging due to potential molecular interference.
• DNA strand displacement (DSD) offers a design paradigm, with a formal language for analysis.
• Existing methods struggle to guarantee device correctness and reliability.

Purpose of the Study:

• To introduce probabilistic verification for analyzing DNA device design.
• To assess the correctness, reliability, and performance of DNA devices early in the design phase.
• To demonstrate the application of these techniques in designing a functional DNA device.

Main Methods:

• Utilizing the probabilistic model checker PRISM.
• Integrating PRISM with the DNA strand displacement (DSD) programming language.
• Applying probabilistic verification to debug DSD components and analyze kinetics.

Main Results:

• Probabilistic verification successfully identified design flaws in DNA devices.
• The methods allowed for evaluation of different design choices and their impact on performance.
• Demonstrated the construction of a DNA strand displacement device for approximate majority voting.

Conclusions:

• Probabilistic verification is a powerful tool for designing reliable DNA devices.
• This approach enhances the formal analysis and debugging of DNA strand displacement systems.
• Future work can extend these methods to more intricate DNA-based computational designs.