等温化学反应器的形式化验证
计算机科学中的逻辑
2025-09-03 v1
摘要
化学反应器是可以用常微分方程（ODE）系统描述的动态系统。反应器的安全性、法规遵从性和经济性取决于反应器能否达到某些状态，并且通常通过数值模拟进行评估。在本工作中，我们展示了如何利用在自动定理证明器KeYmaera X中实现的微分动态逻辑（dL），来符号化地确定等温化学反应器的可达性，从而提供某些条件得到满足的数学保证（例如，出口浓度永远不会超过法规阈值）。首先，我们将dL应用于其动力学可以闭式求解的系统，例如间歇反应器中的一级反应，证明了此类反应器不能超过指定的浓度限值。我们将此方法扩展到复杂如Michaelis-Menten动力学的反应模型，其动力学需要近似或数值解。在所有情况下，证明都通过识别不变量来促进；我们发现质量守恒既是从描述质量作用动力学的ODE中证明的原理，也是证明其他性质的有用关系。未能找到连续搅拌釜式反应器（CSTR）的有用不变量，这限制了可以用dL证明的反应网络的复杂性。虽然dL为化学反应中的可达性提供了一种有趣的符号逻辑方法，但我们获得的边界相对于通常通过数值可达性分析获得的边界而言相当宽泛。
引用
@article{arxiv.2509.01130,
title = {Formal Verification of Isothermal Chemical Reactors},
author = {Parivash Feyzishendi and Sophia Hamer and Jinyu Huang and Tyler R. Josephson},
journal= {arXiv preprint arXiv:2509.01130},
year = {2025}
}