Formal Verification of Chemical Reaction Network Equivalence: A Bisimulation Approach

The Chemical Reaction Network (CRN) model is a language designed to describe the behavior of chemical or biological molecules. Determining whether, in a given semantics, two CRNs have the same behavior is an interesting problem both in itself and for its uses in practice. Such practical uses that have been demonstrated include understanding biological systems by comparison to simple, well-understood CRNs, and verifying that physical implementations of abstract CRNs correctly implement their intended specifications. We defined a concept of CRN equivalence based on bisimulation as explored in concurrent systems, and explored its implications for CRNs in the low-copy-number semantics. We then explored algorithms to check whether two CRNs satisfy this concept of equivalence, and the computational complexity of that task. I will present this definition and our results, and place them in context with other concepts and methods to check CRN equivalence. I will also touch on the uses of this area of theory in practical molecular programming.Non UBCUnreviewedAuthor affiliation: California Institute of TechnologyGraduat