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

TL;DR

The paper introduces Synchronous Signal Temporal Logic (SSTL), a decidable subset of STL, enabling static safety and liveness verification of cyber-physical systems by translating SSTL to LTL_P for model checking.

Contribution

It defines SSTL with a fixed sampling assumption, proves its equivalence to STL under the Signal Invariance Hypothesis, and demonstrates decidable verification via translation to LTL_P.

Findings

SSTL is a decidable fragment of STL for safety and liveness properties.

Translation of SSTL to LTL_P enables model checking with SPIN.

Application to a 33-node human heart model validates the approach.

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.