Verifying Chemical Reaction Network Implementations: A Bisimulation Approach

Efforts in programming DNA and other biological molecules have recently focused on general schemes to physically implement arbitrary Chemical Reaction Networks. Errors in some of the proposed schemes have driven a desire for formal verification methods. We show that by interpreting each implementation species as a set of formal species, the concept of weak bisimulation can be adapted to CRNs in a way that agrees with an intuitive notion of a correct implementation. We give examples of how to use bisimulation to prove the correctness of an implementation or detect subtle problems. We examine the complexity of finding a valid interpretation between two CRNs if one exists, and that of checking whether an interpretation is valid. We show that both are PSPACE-complete in the general case, but are NP-complete and polynomial-time respectively under an assumption that holds in many practical cases. We give algorithms for both of those problems.