AI RESEARCH
Synchronous Signal Temporal Logic for Decidable Verification of Cyber-Physical Systems
arXiv CS.CL
•
ArXi:2603.25531v1 Announce Type: cross 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.