Verifying Chemical Reaction Networks with the Isabelle Theorem Prover
Verifying Chemical Reaction Networks with the Isabelle Theorem Prover
复制标题
DOI：
10.1109/allerton58177.2023.10313474
复制
发表时间：
2023-09
期刊：
影响因子：
--
通讯作者：
James I. Lathrop;Peter-Michael Osera;Addison W. Schmidt;Jesse Slater
中科院分区：
文献类型：
--
作者：
James I. Lathrop;Peter-Michael Osera;Addison W. Schmidt;Jesse Slater
分子编程涉及通过算法控制纳米级设备来计算功能，创建结构，并操纵分子以执行各种任务。许多可编程的纳米器件已经在实验室物理实验中得到了成功的演示。这些设备的一些应用是安全关键的，因此需要对其正确性进行广泛的验证。不幸的是，这些应用的实验和部署需要大约10的18次方的分子器件计数，使得通过模型检查和模拟进行验证不可行。因此，这些系统的验证必须通过独立于系统中设备数量的证明技术来完成。在本文中，我们开发了一个子类的分子程序，计算半线性函数建模的随机化学反应网络的一般证明结构。这些证明技术是在Isabelle中开发的，Isabelle是一个自动定理证明器，所产生的理论文件被打包，以便可以重复使用。
Molecular programming involves algorithmically controlling nanoscale devices to compute functions, create structures, and manipulate molecules to perform various tasks. Many programmed nanoscale devices have been successfully demonstrated in the laboratory with physical experiments. Some of the applications for these devices are safety critical, and thus require extensive verification for their correctness. Unfortunately, experiments and deployment of these applications require molecular device counts on the order of ten to the eighteenth power, making verification via model checking and simulation infeasible. Verification of these systems must therefore be accomplished through proof techniques independent of the number of devices in the system.Developing these proofs can be tedious and time-consuming. In this paper, we develop general proof constructs for a subclass of molecular programs that compute semilinear functions modeled by a stochastic chemical reaction network. These proof techniques are developed in Isabelle, an automated theorem prover, with resulting theory files packaged so that they can be reused.