一句话：提出基于句法分离的 STL 有界模型检测算法，将验证归约为 SMT 可满足性，实现有界反驳完备。
信号时序逻辑（STL）广泛用于规约信息物理系统（CPS）中连续信号的性质，但已有分析方法即使对有界信号也不完备，无法保证 CPS 程序的正确性。本文针对具有连续时间无限状态空间的 CPS 程序，提出一种新的符号有界模型检测算法。核心是 STL 的句法分离：将公式分解为依赖信号不相交片段的等价子公式，从而把 STL 模型检测归约为 first-order logic 公式的可满足性；对具有多项式动态的 CPS 程序，该问题可用 SMT 判定。基于此，算法对一般 STL 性质在有界信号上具有反驳完备性，能够验证给定界内 CPS 程序的正确性。
Signal temporal logic (STL) is a temporal logic formalism for specifying properties of continuous signals. STL is widely used for analyzing programs in cyber-physical systems (CPS) that interact with physical entities. However, existing methods for analyzing STL properties are incomplete even for bounded signals, and thus cannot guarantee the correctness of CPS programs. This paper presents a new symbolic model checking algorithm for CPS programs that is refutationally complete for general STL properties of bounded signals. To address the difficulties of dealing with an infinite state space over a continuous time domain, we first propose a syntactic separation of STL, which decomposes an STL formula into an equivalent formula so that each subformula depends only on one of the disjoint segments of a signal. Using the syntactic separation, an STL model checking problem can be reduced to the satisfiability of a first-order logic formula, which is decidable for CPS programs with polynomial dynamics using satisfiability modulo theories (SMT). Unlike the previous methods, our method can verify the correctness of CPS programs for STL properties up to given bounds.
@article{paperbot663,
title = {Bounded model checking of signal temporal logic properties using syntactic separation},
author = {Kyungmin Bae and Jia Lee},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290364}
}