一句话：提出基于SMT的STL有界模型检测算法，通过离散化连续信号并翻译为一阶实数公式，实现可靠且可扩展的验证。
信号时序逻辑（STL）广泛用于信息物理系统的连续行为规约与分析，但现有STL模型检测方法要么不完备，要么效率很低。本文提出一种新的基于SMT的STL模型检测算法。作者设计翻译技术，将有界STL模型检测问题归约为实数上一阶逻辑公式的可满足性问题，并交由先进SMT求解器判定。其核心是一个新的理论结果：构造连续信号的“小而完备”离散化，同时保持STL的有界可满足性。该翻译使算法对有界信号具有反驳完备性，且比先前的反驳完备算法具有更好的可扩展性。
Signal temporal logic (STL) is widely used to specify and analyze properties of cyber-physical systems with continuous behaviors. However, STL model checking is still quite limited, as existing STL model checking methods are either incomplete or very inefficient. This paper presents a new SMT-based model checking algorithm for verifying STL properties of cyber-physical systems. We propose a novel translation technique to reduce the STL bounded model checking problem to the satisfiability of a first-order logic formula over reals, which can be solved using state-of-the-art SMT solvers. Our algorithm is based on a new theoretical result, presented in this paper, to build a small but complete discretization of continuous signals, which preserves the bounded satisfiability of STL. Our translation method allows an efficient STL model checking algorithm that is refutationally complete for bounded signals, and that is much more scalable than the previous refutationally complete algorithm.
DOI 原文 ·
@inproceedings{paperbot6605,
title = {Efficient SMT-Based Model Checking for Signal Temporal Logic},
author = {Jia Lee and Geunyeol Yu and Kyungmin Bae},
booktitle = {ASE},
year = {2021},
doi = {10.1109/ase51524.2021.9678719}
}