Spatio-Temporal Specification Language for Cyber-Physical Systems.

Specifying spatio-temporal aspects with changes of spatial entities in dense time is one of the important areas in cyber-physical systems. The major problem is the complexity and verifiability of dense time and real-valued variables of the spatio-temporal properties of cyber-physical systems. We propose a spatio-temporal specification language, named STSL, which integrates Signal Temporal Logic (STL) with a spatial logic S4\(_u\) to deal with the changes of real values spatial entities in dense time. We present a Hilbert-style axiomatization for the proposed STSL and provide the soundness and completeness result. Further, we provide the satisfiable relation of spatio-temporal formulas and the corresponding complexity and a decision procedure is present to check the satisfiability problem of the decidable fragment of STSL. Besides, spatio-temporal model is monitored at runtime for the changes of spatial signals over time using MATLAB.