TY - GEN
T1 - A sound and complete axiomatisation for spatio-temporal specification language
AU - Li, Tengfei
AU - Liu, Jing
AU - An, Dongdong
AU - Sun, Haiying
N1 - Publisher Copyright:
© 2019 Knowledge Systems Institute Graduate School. All rights reserved.
PY - 2019
Y1 - 2019
N2 - 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 real-values spatial entities in dense time. The combined language is divided into two formalisms, STSLPC and STSLOC, 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.
AB - 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 real-values spatial entities in dense time. The combined language is divided into two formalisms, STSLPC and STSLOC, 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.
KW - S4
KW - STSLSTSL
KW - Signal temporal logic (STL)
KW - Soundness completeness axiomatization system
KW - SpatioTemporal specification language (STSL)
UR - https://www.scopus.com/pages/publications/85071377591
U2 - 10.18293/SEKE2019-222
DO - 10.18293/SEKE2019-222
M3 - 会议稿件
AN - SCOPUS:85071377591
T3 - Proceedings of the International Conference on Software Engineering and Knowledge Engineering, SEKE
SP - 153
EP - 158
BT - Proceedings - SEKE 2019
PB - Knowledge Systems Institute Graduate School
T2 - 31st International Conference on Software Engineering and Knowledge Engineering, SEKE 2019
Y2 - 10 July 2019 through 12 July 2019
ER -