Many Cyber Physical System (CPS) work in a safety-critical environment, where correct execution, reliability and trustworthiness are essential. Signal Temporal Logic (STL) provides a formal framework for checking safety-critical CPS. However, static verification of STL is undecidable in general, except when we want to verify using run-time-based methods, which have limitations. We propose Synchronous Signal Temporal Logic (SSTL), a decidable fragment of STL, which admits static safety and liveness property verification. In SSTL, we assume that a signal is sampled at fixed discrete steps, called ticks, and then propose a hypothesis, called the Signal Invariance Hypothesis (SIH), which is inspired by a similar hypothesis for synchronous programs. We define the syntax and semantics of SSTL and show that SIH is a necessary and sufficient condition for equivalence between an STL formula and its SSTL counterpart. By translating SSTL to LTL_P (LTL defined over predicates), we enable decidable model checking using the SPIN model checker. We demonstrate the approach on a 33-node human heart model and other case studies.
Figures & tables
Figure 1. The 33-node heart model. (Adapted from ( Yip et al., 2018 ) )
Figure 2. Comparison of STL and SSTL for the heart model scenario.
Figure 3. Illustration of the mapping between the continuous time and the discrete time assuming that the signal is sampled at a fixed interval Δt=0.5 seconds
System
Property
SSTL Formula
Result
Time
Traffic Light
[φmutex]
□¬(NSgreen=1∧EWgreen=1)
Satisfied
1.713s
[φNS_safe]
□(NSgreen=1→EWred=1)
Satisfied
1.502s
[φEW_safe]
□(EWgreen=1→NSred=1)
Satisfied
1.624s
[φfairness]
□◊(NSgreen=1)
Not Satisfied
1.559s
[φliveness_NS]
◊(NSgreen=1)
Satisfied
1.475s
[φresponse_NS_yellow]
□(NSgreen=1→◊(NSyellow=1))
Satisfied
1.539s
Table 1. SSTL properties verified across three case studies. Properties were verified using SPIN with verification times shown.
Work
Time handling
Key assumption/tool
Limitation vs. SSTL
Fainekos&Pappas ( Fainekos and Pappas, 2009 )
Discrete check of CTL/MTL
Robustness, bounded sampling
Needs robustness margins; extra assumptions
Deshmukh et al. ( Bartocci et al., 2018 )
Piecewise-constant interp.
RoSI, partial traces
Interp. choice affects semantics
Chen&Francis ( Chen and Francis, 1995 )
Uniform discrete-time STL
Fixed sampling over N≥0
Breaks explicit link to dense-time STL
Donzé et al. ( Donzé et al., 2013 )
Mixed-time with interfaces
@cd / @dc operators
Interface discipline adds complexity
Yang et al. ( Yang et al., 2020 )
Uniform discretisation for planning
Robust semantics, MIQP
Optimization-oriented; not equivalence
Table 2. Discretisation methods vs. our SSTL (concise view)
Signal Temporal Logic (STL) is an expressive formal language for specifying spatio-temporal requirements over real-valued, real-time signals. It has been widely used for the verification and synthesis of autonomous systems and cyber-physical systems. In practice, however, users often express their requirements in natural language rather than in structured STL formulas, making natural-language-to-STL translation a critical yet challenging task. Manual specification requires temporal-logic expertise and cannot scale, while prompting commercial LLM APIs incurs substantial token costs and may expose sensitive system requirements to third-party services, raising privacy concerns for industrial deployment. To address these challenges, we present ReasonSTL, a tool-augmented framework that adapts local open-source language models for natural-language-to-STL generation. ReasonSTL decomposes the translation process into explicit reasoning, deterministic tool calls, and structured formula construction. We further introduce process-rewarded training to supervise both tool-use trajectories and final formulas, together with STL-Bench, a bilingual, computation-aware benchmark grounded in real-world signals. Experiments show that a 4B model trained with ReasonSTL achieves state-of-the-art performance in both automatic metrics and human evaluations, demonstrating that ReasonSTL provides a transparent, low-cost, and privacy-preserving alternative for formal specification drafting.
Bowen Ye, Zhijian Li, Junyue Huang +2
Shanghai Jiao Tong University · Alibaba Group, Hangzhou, China
Falsification searches for counterexamples to formal specifications in cyber-physical systems (CPS). With specifications written in Signal Temporal Logic (STL), falsification can be formulated as a robustness optimization problem, traditionally tackled with black-box search algorithms. In parallel, large language models (LLMs) have recently emerged as surprisingly effective optimizers when coupled with iterative prompting. In this work, we connect these ideas and introduce LLM-Falsifier, an LLM-based approach that falsifies specifications by minimizing the STL robustness degree. Beyond generic prompt-based optimization, our key idea is to expose the LLM to semantic information that is natural for language models but absent from standard numerical optimizers, including natural-language input and output names, output trajectories, and critical-time witnesses for the minimum robustness value. These additions enable smarter and more sample-efficient robustness search. On the ARCH-COMP falsification benchmarks, LLM-Falsifier is shown to outperform existing falsification tools based on a range of optimization paradigms, from surrogate-based and Bayesian optimization to search-based testing, on 14 of 21 specifications when measured by the average number of simulations required to find a counterexample.
Ali ArjomandBigdeli, Jiawei Zhou, Stanley Bak
Stony Brook University, Stony Brook, New York, USA
Ensuring the satisfaction of Signal Temporal Logic (STL) specifications under uncertainty is challenging, as reachability-based monitoring provides guarantees but does not indicate how to restore satisfaction when it becomes indeterminate. A key difficulty is identifying which uncertain components actually affect global satisfaction, especially for nested formulas. This paper introduces a logical dependency tracking framework that propagates uncertainty through the STL structure and captures the causal contribution of reachable sets to satisfaction. By associating markers to uncertain predicates and propagating them via three-valued semantics, we extract in milliseconds a compact Disjunctive Normal Form (DNF) of sufficient constraints, avoiding combinatorial enumeration. As an application, we formulate control correction as a minimum-effort optimization problem. Using zonotopic reachability, the derived constraints are enforced via linear programming, yielding corrections that guarantee STL satisfaction under bounded uncertainty and provide certified probabilistic bounds in the stochastic case. We demonstrate the approach on a nonlinear system with nested STL specifications, showing that dependency tracking enables efficient and formally guaranteed correction. The tracking implementation is available at https://github.com/Antoine-Bst/STL-Three-Valued-Clause-Filtering/.
Antoine Besset, Joris Tillet, Chuchu Fan +1
u2IS, ENSTA, Institut Polytechnique de Paris, France · Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, France · REALM, AeroAstro, Massachusetts Institute of Technology, Cambridge, USA