Efficient SMT-Based Model Checking for Signal Temporal Logic
- Title
- Efficient SMT-Based Model Checking for Signal Temporal Logic
- Authors
- LEE, JIA; Yu, Geunyeol; BAE, KYUNGMIN
- Date Issued
- 2021-11-17
- Publisher
- IEEE/ACM
- Abstract
- 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.
- URI
- https://oasis.postech.ac.kr/handle/2014.oak/108189
- Article Type
- Conference
- Citation
- 36th IEEE/ACM International Conference on Automated Software Engineering, 2021-11-17
- Files in This Item:
- There are no files associated with this item.
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.