基于可达性分析的线性时不变系统针对信号时序逻辑规约的全自动验证

尽管可达性分析是动态系统形式化验证最有前景的方法之一，但其阻碍更广泛应用的一个主要缺点是需手动调节算法参数（如时间步长）。若旨在验证系统满足由信号时序逻辑公式描述的复杂规约，手动调节尤为成问题，因为可达集的紧致程度对规约满足性的影响往往对人类而言非平凡可见。我们针对线性系统提出一个全自动验证器来解决此问题，它自动细化可达性分析的所有参数，直至能证明或证伪系统对所有初始状态和所有不确定输入满足某信号时序逻辑公式。我们的验证器将可达集时序逻辑与依赖保持相结合，得到一种模型检测方法，其过近似误差在参数调节适当时收敛于零。尽管本工作为简洁起见聚焦于线性系统，我们所提出的通用概念可等价地应用于非线性和混合系统。