Verifying chemical reaction network implementations: A bisimulation approach
Verifying chemical reaction network implementations: A bisimulation approach
复制标题
验证化学反应网络的实现：互模拟方法
DOI：
10.1016/j.tcs.2018.01.002
复制
发表时间：
2018
影响因子：
1.1
通讯作者：
Winfree, Erik
中科院分区：
文献类型：
--
作者：
Johnson, Robert;Dong, Qing;Winfree, Erik
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. By interpreting each implementation species as a multiset 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. The theory of CRN bisimulation can be used to prove the correctness of a general implementation scheme or to detect subtle problems. Given a specific formal CRN and a specific implementation CRN, the complexity of finding a valid interpretation between the two CRNs if one exists, and that of checking whether an interpretation is valid are both PSPACE-complete in the general case, but are NP-complete and polynomial-time respectively under an assumption that holds in many cases of interest. We present effective algorithms for both of those problems. We further discuss features of CRN bisimulation including a transitivity property and a modularity condition, the precise connection to the general theory of bisimulation, and an extension that takes into account spurious catalysts.
