Verifying Chemical Reaction Network Implementations: A Pathway Decomposition Approach

TL;DR

This paper introduces a new pathway decomposition theory and algorithm to verify the correctness of chemical reaction network implementations, addressing challenges of infinite state spaces and complex reaction pathways.

Contribution

It develops a formal pathway decomposition framework and algorithm for verifying chemical reaction networks, including handling delayed choices and combining with weak bisimulation.

Findings

Provides a formal basis for comparing implementations

Handles delayed choice scenarios in molecular systems

Enables verification of enzyme-free DNA implementation techniques

Abstract

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 providing a single guarantee covering an infinite set of possible initial states (molecule counts) and an infinite state space potentially explored by the system given any initial state. We address these issues by formulating 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. Our theory naturally handles certain situations that commonly arise in molecular implementations, such as what we call "delayed choice," that are not easily accommodated by other approaches. We further show how pathway decomposition can be combined with weak bisimulation to handle a wider class that includes most 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.