Verifying chemical reaction network implementations: A pathway decomposition approach
Verifying chemical reaction network implementations: A pathway decomposition approach
复制标题
验证化学反应网络的实现：路径分解方法
DOI：
10.1016/j.tcs.2017.10.011
复制
发表时间：
2017
影响因子：
1.1
通讯作者：
Winfree, Erik
中科院分区：
文献类型：
--
作者：
Shin, Seung Woo;Thachuk, Chris;Winfree, Erik
基因工程、合成生物学、DNA计算、DNA纳米技术和分子编程等新兴领域预示着一种新信息技术的诞生，这种技术通过直接感知化学环境中的分子来获取信息，将信息存储在DNA、RNA和蛋白质等分子中，通过化学和生化转化来处理这些信息，并利用这些信息来指导纳米尺度上的物质操纵。为了扩大目前的原理验证演示范围，需要开发管理设计分子系统复杂性的新方法。在这里，我们重点关注验证抽象化学反应网络的分子实现的正确性的挑战，其中充分混合的分子“汤”中的操作是随机的、异步的、并发的，并且通常涉及实现中的多个中间步骤、并行路径和副反应。该问题与 Petri 网的验证有关，但现有方法不足以提供单一保证，涵盖无限组可能的初始状态（分子计数）以及给定任何初始状态的系统可能探索的无限状态空间。我们通过制定一种新的路径分解理论来解决这些问题，该理论为比较化学反应网络实现提供了优雅的形式基础，并且我们提出了一种计算该基础的算法。我们的理论自然地处理分子实现中常见的某些情况，例如我们所说的“延迟选择”，其他方法不易适应。我们进一步展示了如何将通路分解与弱互模拟相结合，以处理更广泛的类别，其中包括大多数当前已知的无酶 DNA 实现技术。我们预计化学反应网络实现之间的逻辑等价概念对于其他分子实现（例如生化酶系统）甚至在并发理论中可能更有价值。
The emerging fields of genetic engineering, synthetic biology, DNA computing, DNA nanotechnology, and molecular programming herald the birth of a new information technology that acquires information by directly sensing molecules within a chemical environment, stores information in molecules such as DNA, RNA, and proteins, processes that information by means of chemical and biochemical transformations, and uses that information to direct the manipulation of matter at the nanometer scale. To scale up beyond current proof-of-principle demonstrations, new methods for managing the complexity of designed molecular systems will need to be developed. 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.