A Sound and Complete Axiomatisation for Spatio-Temporal Specification Language
Tengfei Li, Jing Liu, Dongdong An, Haiying Sun · Proceedings/Proceedings of the ... International Conference on Software Engineering and Knowledge Engineering · 2019
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 S4u to deal with the changes of realvalues spatial entities in dense time.The combined language is divided into two formalisms, ST SLP C and ST SLOC , 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.