VEMDP 2014 CONTRIBUTED PAPERS: PAPERS WITH ABSTRACTS

ABSTRACT. In this paper, we illustrate the use of the Infobiotics Workbench platform, designed to model and analyse stochastic P systems, by modeling basic synthetic Boolean gates and analysing them using some computational techniques: simulation, verification and biocompilation.

ABSTRACT. DNA strand displacement systems have proven themselves to be a fertile substrate for the design of programmable molecular machinery and circuitry. Domain-level reaction enumerators provide the foundations for molecular programming languages by formalizing DNA strand displacement mechanisms and modeling interactions at the “domain” level – one level of abstraction above models that explicitly describe DNA strand sequences. Unfortunately, the most-developed models currently only treat pseudo-linear DNA structures, while many systems being experimentally and theoretically pursued exploit a much broader range of secondary structure configurations. Here, we describe a new domain-level reaction enumerator that can handle arbitrary non-psuedoknotted secondary structures and reaction mechanisms including association and dissociation, 3-way and 4-way branch migration, and direct as well as remote toehold activation. To avoid polymerization that is inherent when considering general structures, we employ a time-scale separation technique that holds in the limit of low concentrations. This also allows us to “condense” the detailed reactions by eliminating fast transients, with provable guarantees of correctness for the set of reactions and their kinetics. We hope that the new reaction enumerator will be used in new molecular programming languages, compilers, and tools for analysis and verification that treat a wider variety of mechanisms of interest to experimental and theoretical work.

ABSTRACT. The emerging fields of genetic engineering, synthetic biology, DNA computing, DNA nanotechnology, and molecular programming herald the birth of a new information technology that acquires information by directly sensing molecules within a chemical environment, stores information in molecules such as DNA, RNA, and proteins, processes that information by means of chemical and biochemical transformations, and uses that information to direct the manipulation of matter at the nanometer scale. To scale up beyond current proof-of-principle demonstrations, new methods for managing the complexity of designed molecular systems will need to be developed. Here we focus on the challenge of verifying the correctness of molecular implementations of abstract chemical reaction networks, where operation in a well-mixed "soup" of molecules is stochastic, asynchronous, concurrent, and often involves multiple intermediate steps in the implementation, parallel pathways, and side reactions. This problem relates to the verification of Petri Nets, but existing approaches are not sufficient for certain situations that commonly arise in molecular implementations, such as what we call "delayed choice." We formulate a new theory of pathway decomposition that provides an elegant formal basis for comparing chemical reaction network implementations, and we present an algorithm that computes this basis. We further show how pathway decomposition can be combined with bisimulation to handle a wider class that includes all currently known enzyme-free DNA implementation techniques. We anticipate that our notion of logical equivalence between chemical reaction network implementations will be valuable for other molecular implementations such as biochemical enzyme systems, and perhaps even more broadly in concurrency theory.

ABSTRACT. 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 proposed, as have meth- ods 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 no 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 Re- action Network model covers the DNA stack machine, as well as copy-tolerant Turing machines and some examples from biochemistry. We adapt the bisimula- tion 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 Π2-complete, and thus undecidable in the general case. We hope that the ability to model and verify implementations of polymer reaction networks will aid in the rational design of molecular systems.