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

• URL: http://arxiv.org/abs/2603.25531v1
• Date: Thu, 26 Mar 2026 15:06:17 GMT
• Title: Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems
• Abstract summary: Many Cyber Physical System (CPS) work in a safety-critical environment, where correct execution, reliability and trustworthiness are essential.<n>Signal Temporal Logic (STL) provides a formal framework for checking safety-critical CPS.<n>We propose Synchronous Signal Temporal Logic (SSTL), a decidable fragment of STL, which admits static safety and liveness property verification.
• Score: 1.0895848625126727
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Fast Constraint Extraction for Corrective Control under STL Specifications via Logical Dependency Tracking [13.336304771873214]
  Key difficulty is identifying which uncertain components actually affect global satisfaction, especially for nested formulas.<n>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.
  arXiv  Detail & Related papers  (2026-09-08T20:44:28Z)
• Correct-by-Construction Behavior Tree Synthesis from Signal Temporal Logic Specifications with Application to Robotic Missions [5.524204636266904]
  Behavior Trees (BTs) are widely adopted for complex task execution in robotics.<n>This letter synthesizes correct-by-construction BTs from Signal Temporal Logic (STL) specifications.
  arXiv  Detail & Related papers  (2026-07-21T05:43:19Z)
• pdSTL: Probabilistic Differentiable Signal Temporal Logic for Stochastic Systems [0.0]
  We introduce pdSTL (probabilistic differentiable Signal Temporal Logic), a framework that unifies probabilistic semantics with differentiable robustness over belief trajectories.<n>Results demonstrate that pdSTL efficient optimization with formal probabilistic guarantees, significantly outperforming deterministic differentiable STL in maintaining safety margins under real-world uncertainty.
  arXiv  Detail & Related papers  (2026-06-17T20:01:56Z)
• Systematic Integration of Digital Twins and Constrained LLMs for Interpretable Cyber-Physical Anomaly Detection [0.0]
  Cyber attacks targeting Industrial Control Systems (ICS) have become increasingly sophisticated and hard to identify.<n>Detecting such attacks requires integrating low-level behavioral cues with high-level semantic interpretation.<n>This paper presents a Digital Twin (DT)-driven hybrid detection approach.
  arXiv  Detail & Related papers  (2026-04-04T16:38:12Z)
• Conformalized Signal Temporal Logic Inference under Covariate Shift [13.843989967082031]
  Signal Temporal Logic (STL) inference learns interpretable logical rules for temporal behaviors in dynamical systems.<n>The proposed framework preserves the interpretability of STL formulas while significantly improving symbolic learning reliability at deployment time.
  arXiv  Detail & Related papers  (2026-03-28T00:38:01Z)
• Feasibility Restoration under Conflicting STL Specifications with Pareto-Optimal Refinement [18.383508411056944]
  Signal Temporal Logic (STL) is expressive language that specifies expressive requirements in robotics.<n>STL specifications may become conflicting in real-world applications, where safety rules, traffic regulations, task and objectives can be cannot be satisfied together.<n>We propose a unified two-stage framework that first restores feasibility via minimal relaxation, then refine the feasible solution by formulating it as a value-aware multi-objective optimization problem.
  arXiv  Detail & Related papers  (2026-03-06T23:41:01Z)
• STLCG++: A Masking Approach for Differentiable Signal Temporal Logic Specification [9.039665244779185]
  We present STLCG++, a masking-based approach that parallelizes STL computation and backpropagation across timesteps.<n>We also introduce a smoothing technique to enable the differentiation of time interval bounds, thereby expanding STL's applicability in gradient-based optimization tasks.
  arXiv  Detail & Related papers  (2025-01-08T00:06:43Z)
• Retrieval-Augmented Mining of Temporal Logic Specifications from Data [0.46040036610482665]
  This work addresses the task of learning STL requirements from observed behaviors in a data-driven manner. We present a novel framework that combines Bayesian Optimization (BO) and Information Retrieval (IR) techniques to simultaneously learn both the structure and the parameters of STL formulae.
  arXiv  Detail & Related papers  (2024-05-23T09:29:00Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  We present a novel controller synthesis method that does not rely on any explicit representation of the noise distributions. First, we abstract the continuous control system into a finite-state model that captures noise by probabilistic transitions between discrete states. We use state-of-the-art verification techniques to provide guarantees on the interval Markov decision process and compute a controller for which these guarantees carry over to the original control system.
  arXiv  Detail & Related papers  (2023-01-04T10:40:30Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  We propose a method for synthesising controllers for Markov jump linear systems. Our method is based on a finite-state abstraction that captures both the discrete (mode-jumping) and continuous (stochastic linear) behaviour of the MJLS. We apply our method to multiple realistic benchmark problems, in particular, a temperature control and an aerial vehicle delivery problem.
  arXiv  Detail & Related papers  (2022-12-01T17:36:30Z)
• Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty [68.00748155945047]
  Capturing uncertainty in models of complex dynamical systems is crucial to designing safe controllers. Several approaches use formal abstractions to synthesize policies that satisfy temporal specifications related to safety and reachability. Our contribution is a novel abstraction-based controller method for continuous-state models with noise, uncertain parameters, and external disturbances.
  arXiv  Detail & Related papers  (2022-10-12T07:57:03Z)
• SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version) [71.12474112166767]
  We introduce a variant of one of the most investigated models in this spectrum, namely simple artifact systems (SASs) This DL, enjoying suitable model-theoretic properties, allows us to define SASs to which backward reachability can still be applied, leading to decidability in PSPACE of the corresponding safety problems.
  arXiv  Detail & Related papers  (2021-08-27T15:04:11Z)
• Stability and Identification of Random Asynchronous Linear Time-Invariant Systems [81.02274958043883]
  We show the additional benefits of randomization and asynchrony on the stability of linear dynamical systems. For unknown randomized LTI systems, we propose a systematic identification method to recover the underlying dynamics.
  arXiv  Detail & Related papers  (2020-12-08T02:00:04Z)
• SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
  We study the verification of parameterised multi-agent systems (MASs) In particular, we study whether unwanted states, characterised as a given state formula, are reachable in a given MAS.
  arXiv  Detail & Related papers  (2020-08-11T15:24:05Z)
• Backpropagation through Signal Temporal Logic Specifications: Infusing Logical Structure into Gradient-Based Methods [28.72161643908351]
  This paper presents a technique, named STLCG, to compute the quantitative semantics of Signal Temporal Logic (STL) formulas using computation graphs. STL is a powerful and expressive formal language that can specify spatial and temporal properties of signals generated by both continuous and hybrid systems.
  arXiv  Detail & Related papers  (2020-07-31T22:01:39Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.