Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems

Partha Roop; Sobhan Chatterjee; Avinash Malik; Nathan Allen; Logan Kenwright

cs.FLMar 26, 2026

Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems

Authors: Partha Roop, Sobhan Chatterjee, Avinash Malik, Nathan Allen, Logan Kenwright

Organizations: University of Auckland, Auckland, New Zealand · Auckland University of Technology, Auckland, New Zealand

Abstract

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 ) )

Panel of Figure 2 — 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

\Delta t=0.5

seconds

System	Property	SSTL Formula	Result	Time
Traffic Light	$[\varphi_{mutex}]$	$\square\neg(NS_{green}=1\land EW_{green}=1)$	Satisfied	1.713s
	$[\varphi_{NS\_safe}]$	$\square(NS_{green}=1\rightarrow EW_{red}=1)$	Satisfied	1.502s
	$[\varphi_{EW\_safe}]$	$\square(EW_{green}=1\rightarrow NS_{red}=1)$	Satisfied	1.624s
	$[\varphi_{fairness}]$	$\square\lozenge(NS_{green}=1)$	Not Satisfied	1.559s
	$[\varphi_{liveness\_NS}]$	$\lozenge(NS_{green}=1)$	Satisfied	1.475s
	$[\varphi_{response\_NS\_yellow}]$	$\square(NS_{green}=1\rightarrow\lozenge(NS_{yellow}=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 $\mathbb{N}_{\geq 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)

Work	Core idea	Strength	Limitation vs. SSTL
Roehm et al. ( Roehm et al., 2016 )	Reach-set abstraction	Sound/complete for samples	Requires reachability; costly abstractions
Bae&Lee ( Bae and Lee, 2019a )	Syntactic separation + SMT	Refutational completeness (bounded)	Complex SMT over reals; bounded scope
Yu et al. ( Yu et al., 2022 )	$\epsilon$ -strengthening + SMT	Robust model checking	Guarantees up to thresholds only
Lercher&Althoff ( Lercher and Althoff, 2024 )	Four-valued STL on sets	Incremental verification	Depends on set refinement strategy
Belta&Sadraddini ( Belta and Sadraddini, 2019 )	DC programming (robustness trees)	Convex subproblems	Restrictive dynamics/spec classes

Table 3. STL verification approaches vs. our SSTL

Explore similar work

ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning
May 7, 2026Bowen Ye, Zhijian Li, Junyue Huang +2Signal Temporal Logic LLM Tool Use
Shanghai Jiao Tong University · Alibaba Group, Hangzhou, China
Large Language Models as Falsifiers for Cyber-Physical Systems
Sep 17, 2026Ali ArjomandBigdeli, Jiawei Zhou, Stanley BakCyber-Physical Systems Large Language Model-Guided Optimization
Stony Brook University, Stony Brook, New York, USA
Fast Constraint Extraction for Corrective Control under STL Specifications via Logical Dependency Tracking
Sep 8, 2026Antoine Besset, Joris Tillet, Chuchu Fan +1Signal Temporal Logic Robust Control
u2IS, ENSTA, Institut Polytechnique de Paris, France · Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, France · REALM, AeroAstro, Massachusetts Institute of Technology, Cambridge, USA

May 7, 2026J/K move · Enter open · S save

ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning

Bowen Ye, Zhijian Li, Junyue Huang, Junkai Ma+1

Shanghai Jiao Tong University · Alibaba Group, Hangzhou, China

Signal Temporal Logic LLM Tool Use

Open paper AskPDF arXiv

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.

Abstract

Explore similar work

ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning

Large Language Models as Falsifiers for Cyber-Physical Systems

Fast Constraint Extraction for Corrective Control under STL Specifications via Logical Dependency Tracking