用于信息物理系统可判定验证的同步信号时序逻辑
形式语言与自动机理论
2026-03-27 v1 计算与语言
摘要
许多信息物理系统 (CPS) 在安全关键环境中工作，正确执行、可靠性与可信性至关重要。信号时序逻辑 (STL) 为检查安全关键 CPS 提供了形式化框架。然而，STL 的静态验证一般是不可判定的，除非使用基于运行时的方法，而后者存在局限性。我们提出同步信号时序逻辑 (SSTL)，一种 STL 的可判定片段，允许静态安全性与活性属性验证。在 SSTL 中，我们假设信号在固定离散步（称为节拍）上采样，然后提出一个假设——信号不变性假设 (SIH)，其灵感来自同步程序的类似假设。我们定义 SSTL 的语法与语义，并证明 SIH 是 STL 公式与其 SSTL 对应物等价的充要条件。通过将 SSTL 翻译为 LTL_P（基于谓词的 LTL），我们实现了使用 SPIN 模型检测器的可判定模型检测。我们在 33 节点人体心脏模型及其他案例研究上展示了该方法。
引用
@article{arxiv.2603.25531,
title = {Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems},
author = {Partha Roop and Sobhan Chatterjee and Avinash Malik and Nathan Allen and Logan Kenwright},
journal= {arXiv preprint arXiv:2603.25531},
year = {2026}
}