SMT-Based Model Checking for Signal Temporal Logic


Introduction

Signal temporal logic (STL) is a temporal logic used to specify properties of continuous signals. STL has been widely applied in specifying, monitoring, and testing properties of hybrid systems that exhibit both discrete and continuous behavior. However, model checking techniques for hybrid systems have primarily been limited to invariant and reachability properties. In this work, we present a novel logical foundation for STL, introduce bounded model checking algorithms and a tool for general STL properties of hybrid systems. With this new foundation, the robust STL model checking problem can be reduced to the satisfiability of a first-order logic formula. This allows us to develop the first model checking algorithm for STL that can guarantee the correctness of STL up to given bounds. We demonstrate the effectiveness of STLmc on various hybrid system case studies.

Logical Foundations and Algorithms

We have developed a novel logical foundation for STL and SMT-based bounded robust model checking algorithms on this foundation [1,2,3]. Our logical foundation includes: (i) syntactic separation, decomposing an STL formula into components, with each component depending exclusively on separate segments of a signal; (ii) signal discretization, ensuring a complete abstraction of a signal through a set of discrete elements; and (iii) ε-strengthening, reducing robust STL model checking to Boolean STL model checking. We combine these foundational techniques to develop the algorithms, which are refutation-complete, meaning that they can guarantee correctness up to given bounds. Based on these algorithms, we implement a framework shown in Figure 1, called STLmc.

An SMT-based robust bounded STL model checking framework.
Figure 1. An SMT-based robust bounded STL model checking framework.

Logical foundations. A temporal logic formula 𝜑 is called syntactically separated if 𝜑 is a Boolean combination of formulas, each of which depends only on a disjoint part of the underlying time domain (such as the past, present, or future). This decomposition is well-known for LTL. However, it becomes more challenging for logics with temporal operators constrained by time intervals, such as MTL and STL; no generic method has been proposed for separating such formulas into disjoint parts. In [1], we address this problem and generalize the STL syntax by adding extra time constraints, called STL with global time (STL-GT), and propose a syntactic separation procedure based on the Boolean semantics of STL.

For bounded signals with finite variable points (excluding Zeno behaviors), the satisfaction of a temporal logic formula must depend on a finite number of sampled time points. Intuitively, a discretization of a signal is a finite set of time points that equivalently captures the meaning of a temporal logic formula. Although signal discretization methods have been proposed for various temporal logics, they cannot be directly applicable to STL. The main difficulty arises from the timed until operator, which often results in overly “fine” discretized signals, hindering efficient model checking of hybrid systems. In [2], we propose a novel technique to build a complete yet reasonably coarse discretization for STL.

Algorithms. We combine the these two foundational techniques to develop SMT-based bounded model checking algorithms for STL [1,2]. The core of our algorithms involves translating an STL formula into a decidable fragment of first-order logic for a signal with a finite number of variable points, where the satisfaction of each subformula can change finitely, while the value of the signal may continuously change over time. By leveraging syntactic separation, it becomes obvious to translate an STL formula into a quantifier-free first-order formula in linear real arithmetic.

Despite these advances, the underlying Boolean semantics limits the applicability of these techniques to hybrid systems because small perturbations in signals can cause the system to violate properties verified by Boolean STL model checking. To address this, in [3], we propose robust STL model checking, which verifies whether the robustness degree of an STL formula exceeds a robustness threshold ε > 0 for all possible system behaviors. We reduce the robust STL model checking problem to Boolean model checking using ε-strengthening (making the problem harder to be true by ε). We can then apply the refutation-complete Boolean model checking algorithms to solve this problem.

Experiments

We conducted two experiments: one evaluates the results of robust STL model checking, and the other compares the performance of STLmc for invariant properties with existing reachability analysis tools for hybrid automata.

Robust STL model checking. We consider the following hybrid automata models: load management of batteries (Bat), network of water tanks (Wat), autonomous driving of cars (Car), railroad gate controller (Rail), network of thermostats (Thm), filtered oscillator (Oscil-N), spacecraft rendezvous (Space-N), and navigation system (Nav-N). We consider three variants with different continuous dynamics (e.g., Bat-L has linear dynamics, Bat-P has polynomial dynamics, and Bat-N has ODE dynamics). For each model, we use three STL formulas. For the discrete bound, we set 𝑁 = 20 for linear models, 𝑁 = 10 for polynomial models, and 𝑁 = 5 for ODE models. We use different time bounds 𝜏 and robustness thresholds ε depending on the model’s characteristics. As the underlying SMT solver, we use Yices for linear and polynomial models, and dReal for ODE models. We set a timeout of 60 minutes.

The experimental results are summarized in Table 1, where 𝜏 denotes the time bound, 𝑁 denoted the discrete bound, and |Ψ| denotes the size of the SMT encoding Ψ (in thousands). For the model checking results, ⊤ indicates that no counterexample was found up to bound 𝑁, and ⊥ indicates that a counterexample was found at some 𝑘 ≤ 𝑁. As shown in the table, our tool can perform robust model checking of nontrivial STL formulas for hybrid systems with various continuous dynamics. ODE models generally require more time than linear and polynomial models due to the high computational costs of handling nonlinear constraints.

Table 1. Experimental results for robust STL model checking.
Experimental results for robust STL model checking.

Comparison with reachability analysis tools. We compare the performance of STLmc in verifying invariant properties against four hybrid automata reachability analysis tools: HyComp, SpaceEx, Flow*, and dReach. For each model, we consider a true invariant property so that reachability analysis explores all possible behaviors up to given bounds. We measure the execution times (in seconds) for analyzing the invariant properties up to a given bound with a timeout of 60 minutes. Since each tool has a different notion of bounds, we use the number of discrete jumps 𝑁 and the maximum time horizon 𝜏 as the common bound parameters, which are “encoded” in the models if needed. We use the same settings for the discrete bound 𝑁 and time horizon 𝜏 as in the previous experiment.

The experimental results are summarized in Table 2, with execution times in seconds. T/O denotes a timeout. Because HyComp only supports linear models, it is not included in the results for polynomial and ODE models. Similarly, SpaceEx supports only linear ODEs and is therefore not applicable (N/A) for models with nonlinear ODEs (Car, Rail, and Wat). As shown in the table, our tool has comparable performance to the other tools for the invariant properties. For example, for the autonomous car system with ODE dynamics (Car-N), both STLmc and dReach verify the invariant property within 1 minute, whereas Flow* times out. This is because the systems’s dynamics are complex, involving trigonometric dynamic. For linear models, dReach cannot solve some problems in time. This problem is because dReach enumerate all possible paths and there are too many scenarios with a larger discrete bound 𝑁. STLmc can solve all the problems in time, including linear models with large discrete bounds.

Table 2. Execution time for analyzing invariant properties (in seconds).
Execution time for analyzing invariant properties (in seconds).

References

  1. K. Bae, J. Lee, Bounded model checking of signal temporal logic properties using syntactic separation, Proc. ACM Program. Lang. 3 (POPL) (2019) 51:1–51:30, https://doi.org/10.1145/3290364.
  2. J. Lee, G. Yu, K. Bae, Efficient SMT-based model checking for signal temporal logic, in: IEEE/ACM International Conference on Automated Software Engineering, IEEE, 2021, pp. 343–354, https://ieeexplore.ieee.org/document/9678719.
  3. G Yu., J. Lee, K. Bae. STLmc: Robust STL model checking of hybrid systems using SMT, in: International Conference on Computer Aided Verification, Springer, 2022, Volume 13371, https://doi.org/10.1007/978-3-031-13185-1_26.
  4. J. Lee, G Yu., K. Bae. SMT-based robust model checking for signal temporal logic, Science of Computer Programming, 2025, Volume 246, https://doi.org/10.1016/j.scico.2025.103332.