Runtime Verification of Spatio-Temporal Specification Language

Combining spatial and temporal primitives together is quite useful to specify dynamic behaviors of cyber-physical systems. The ability to represent spatio-temporal properties by means of formulas in spatio-temporal logics has recently found important applications in various fields, such as runtime verification, parameter synthesis, and falsification. In this paper, we present a spatio-temporal specification language, STSL, 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 combines the power of temporal modalities and spatial operators and enjoys important properties such as safety and liveness. We provide the falsification problem through extending Lemire’s algorithm and a parameter synthesis procedure by calling the simulated annealing algorithm. We demonstrate the proposed approach on the adaptive cruise control system and path planning of quadrotors.