基于信号时序逻辑的CPS运行时强制执行
系统与控制
2025-02-18 v1 系统与控制
摘要
网络-物理系统（CPS），尤其是涉及自主性的系统，需要其安全性的保证。运行时强制执行（RE）是一种轻量级方法，用于形式确保在系统执行期间满足某些指定属性。因此，近期存在对CPS的RE兴趣。然而，现有方法并非为适合CPS混合动力学的规范而设计。鉴于此，我们开发了使用信号时序逻辑（STL）定义的属性来实现CPS的运行时强制执行。在本工作中，我们旨在为给定的STL公式构建运行时强制器，以最小方式修改信号以满足该公式。为此，首先将要强制执行的STL公式翻译为timed transducer，同时将要纠正的信号编码为timed words。我们提供了时序算子\emph{until}和\emph{release}的时序转换器，注意到其他时序算子可使用这两个算子表示。我们的做法使能够有效地为CPS执行STL属性。提供了一个案例研究，以说明该方法并生成其适用于CPS的实证证据。
引用
@article{arxiv.2502.11584,
title = {Runtime Enforcement of CPS against Signal Temporal Logic},
author = {Han Su and Saumya Shankar and Srinivas Pinisetty and Partha S. Roop and Naijun Zhan},
journal= {arXiv preprint arXiv:2502.11584},
year = {2025}
}