A sound and complete axiomatisation for spatio-temporal specification language

Specifying spatio-temporal aspects is one of the important areas in cyber-physical systems. Spatio-temporal logic with changes of truth value in discrete time and dense time has been researched, but a combination of spatial and temporal components with changes of spatial entities in dense time hasn't been well-done. The major problem is dense time and real-valued variables of the spatio-temporal properties of cyber-physical systems. In this paper, 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. The combined language is divided into two formalisms, STSL_PC and STSL_OC, which is applied to interpret the Boolean semantics and quantitative semantics, respectively. The syntax of the two formalism and the corresponding semantics are provided. Besides, we present a Hilbert-style axiomatization for the proposed STSL and provide the soundness and completeness result by the spatio-temporal extension of maximal consistent set and canonical model.