A Caltech Library Service

Verifying polymer reaction networks using bisimulation

Johnson, Robert F. and Winfree, Erik (2020) Verifying polymer reaction networks using bisimulation. Theoretical Computer Science, 843 . pp. 84-114. ISSN 0304-3975.

[img] PDF - Published Version
Creative Commons Attribution.


Use this Persistent URL to link to this item:


The Chemical Reaction Network model has been proposed as a programming language for molecular programming. Methods to implement arbitrary CRNs using DNA strand displacement circuits have been investigated, as have methods to prove the correctness of those or other implementations. However, the stochastic Chemical Reaction Network model is provably not deterministically Turing-universal, that is, it is impossible to create a stochastic CRN where a given output molecule is produced if and only if an arbitrary Turing machine accepts. A DNA stack machine that can simulate arbitrary Turing machines with minimal slowdown deterministically has been proposed, but it uses unbounded polymers that cannot be modeled as a Chemical Reaction Network. We propose an extended version of a Chemical Reaction Network that models unbounded linear polymers made from a finite number of monomers. This Polymer Reaction Network model covers the DNA stack machine, as well as copy-tolerant Turing machines and some examples from biochemistry. We adapt the bisimulation method of verifying DNA implementations of Chemical Reaction Networks to our model, and use it to prove the correctness of the DNA stack machine implementation. We define a subclass of single-locus Polymer Reaction Networks and show that any member of that class can be bisimulated by a network using only four primitives, suggesting a method of DNA implementation. Finally, we prove that deciding whether an implementation is a bisimulation is Π⁰₂-complete, and thus undecidable in the general case, although it is tractable in many special cases of interest. We hope that the ability to model and verify implementations of Polymer Reaction Networks will aid in the rational design of molecular systems.

Item Type:Article
Related URLs:
URLURL TypeDescription
Johnson, Robert F.0000-0002-5340-8347
Winfree, Erik0000-0002-5899-7523
Additional Information:© 2020 The Author(s). Published by Elsevier B.V. This is an open access article under the CC BY license ( Received 8 January 2020, Revised 6 August 2020, Accepted 10 August 2020, Available online 1 September 2020. The authors would like to thank Chris Thachuk, Damien Woods, Dave Doty, Seung Woo Shin, and Lulu Qian for helpful discussions. RFJ and EW were supported by NSF grants 1317694, 1213127, and 0832824. RFJ was also supported by Caltech's Summer Undergraduate Research Fellowship and an NSF graduate fellowship. The authors declare that they have no known competing financial interests or personal relationships that could have appeared to influence the work reported in this paper.
Funding AgencyGrant Number
Caltech Summer Undergraduate Research Fellowship (SURF)UNSPECIFIED
Subject Keywords:Verification; Molecular computing; Bisimulation; Chemical Reaction Networks; Polymer Reaction Networks; DNA strand displacement
Record Number:CaltechAUTHORS:20201029-152451680
Persistent URL:
Official Citation:Robert F. Johnson, Erik Winfree, Verifying polymer reaction networks using bisimulation, Theoretical Computer Science, Volume 843, 2020, Pages 84-114, ISSN 0304-3975, (
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:106345
Deposited By: Tony Diaz
Deposited On:29 Oct 2020 23:31
Last Modified:29 Oct 2020 23:31

Repository Staff Only: item control page