A spatio-temporal specification language and its completeness & decidability

In the past few years, significant progress has been made on spatio-temporal cyber-physical systems in achieving spatio-temporal properties on several long-standing tasks. With the broader specification of spatio-temporal properties on various applications, the concerns over their spatio-temporal logics have been raised in public, especially after the widely reported safety-critical systems involving self-driving cars, intelligent transportation system, image processing. In this paper, we present a spatio-temporal specification language, STSL _PC, by combining Signal Temporal Logic (STL) with a spatial logic S4 _u, to characterize spatio-temporal dynamic behaviors of cyber-physical systems. This language is highly expressive: it allows the description of quantitative signals, by expressing spatio-temporal traces over real valued signals in dense time, and Boolean signals, by constraining values of spatial objects across threshold predicates. STSL _PC combines the power of temporal modalities and spatial operators, and enjoys important properties such as finite model property. We provide a Hilbert-style axiomatization for the proposed STSL _PC and prove the soundness and completeness by the spatio-temporal extension of maximal consistent set and canonical model. Further, we demonstrate the decidability of STSL _PC and analyze the complexity of STSL _PC. Besides, we generalize STSL to the evolution of spatial objects over time, called STSL _OC, and provide the proof of its axiomatization system and decidability.