Before revision:  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.
After revision:  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.