.png){kind=icon}
返回
Closure certificates
.png){kind=icon}
PRE
AI
DOI：10.1016/j.nahs.2025.101630.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
屏障证书，定义为动态系统状态的一个实值函数，其零水平集表征一个归纳可验证的状态不变量，将可达状态与不安全状态分离。当与强大的决策过程（如和积规划（SOS）或理论模可满足性求解器（SMT））结合时，屏障证书能够实现安全的自动化演绎验证方法。屏障证书方法已被扩展以反驳LTL和ω-正则规范，通过分离对应ω自动机的连续转换，以期否定所有接受运行。不出所料，此类策略注定是保守的，因为反驳循环属性也需要通过推理排序函数来证明活性。本文介绍了闭包证书的概念，作为从状态不变量到转换不变量的屏障证书的自然扩展。我们展示了如何使用此类证书上的排序函数论证来验证离散时间动态系统是否符合线性时态逻辑公式。我们用基于SOS和SMT的表征增强了这些定义，以自动化闭包证书的搜索，并通过一些案例研究展示了其有效性。
