Probabilistic Analysis of Localized DNA Hybridization Circuits.

Molecular devices made of nucleic acids can perform complex information processing tasks at the nanoscale, with potential applications in biofabrication and smart therapeutics. However, limitations in the speed and scalability of such devices in a well-mixed setting can significantly affect their performance. In this article, we propose designs for localized circuits involving DNA molecules that are arranged on addressable substrates and interact via hybridization reactions. We propose designs for localized elementary logic circuits, which we compose to produce more complex devices, including a circuit for computing the square root of a four bit number. We develop an efficient method for probabilistic model checking of localized circuits, which we implement within the Visual DSD design tool. We use this method to prove the correctness of our circuits with respect to their functional specifications and to analyze their performance over a broad range of local rate parameters. Specifically, we analyze the ex...