合成基因逻辑电路在随机时间契约下的证明携带架构
A proof-carrying architecture for synthetic genetic logic circuits under stochastic temporal contracts
- Faculty of Computer Science, University of Vienna（维也纳大学计算机科学学院）
- Faculty of Informatics, TU Wien（维也纳工业大学信息学院）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出证明携带合成生物学（PCS-Bio）架构，通过连接布尔等价、随机契约等义务，为无环基因逻辑电路提供时间精化保证，实验显示切片可降低风险与延迟。
AI中文摘要：
基因设计自动化将布尔规范映射为调控网络和DNA序列，但成功的映射并不能确立每个输出随时间保持正确的概率。本文提出证明携带合成生物学（PCS-Bio），一种用于在固定输入下运行的无环基因逻辑电路的形式化架构。一个理想校验器连接布尔等价性、序列与模型来源、局部随机契约以及任何替代到目标的差异界限。在明确的语义和校验器假设下，这些义务蕴含联合时间精化保证，无需假设分子事件之间的独立性。赋值特定的充分立方体选择证明每个输出值所需的分支。这可以在保留的局部契约在物理存在但逻辑屏蔽的输入上保持一致的条件下，降低风险和延迟核算。报告的评估涉及三个独立接口：一个存档的Cello执行与序列重建，一个受限的精确有理校验器用于合成有限状态实例，以及诊断性IEEE 754 binary64重放。在60个确定性布尔公式图中，切片在55个案例中减少了最坏赋值风险费用总和，并在54个案例中减少了最大核算延迟。这些结果涉及证明核算和选定的实现组件。它们并未确立一个集成的序列绑定时间证书或物理验证。
英文摘要：
Genetic design automation maps Boolean specifications to regulatory networks and DNA sequences, but a successful mapping does not establish the probability that every output remains correct over time. This paper presents Proof-Carrying Synthetic Biology (PCS-Bio), a formal architecture for acyclic genetic logic circuits operated under fixed inputs. An ideal checker connects Boolean equivalence, sequence and model provenance, local stochastic contracts, and any surrogate-to-target discrepancy bounds. Under explicit semantic and checker assumptions, these obligations imply a joint temporal refinement guarantee without assuming independence among molecular events. Assignment-specific sufficient cubes select the branches needed to prove each output value. This can reduce risk and delay accounting provided that the retained local contracts remain uniform over the physically present but logically masked inputs. The reported evaluation exercises three separate interfaces: an archived Cello execution with sequence reconstruction, a restricted exact rational checker for a synthetic finite-state instance, and diagnostic IEEE~754 binary64 replay. Across 60 deterministic Boolean formula graphs, slicing reduced the worst-assignment risk-charge sum in 55 cases and the maximum accounting delay in 54. These results concern proof accounting and selected implementation components. They do not establish an integrated sequence-bound temporal certificate or physical validation.
