Finite-Horizon Optimal Spatio-Temporal Pattern Control under Spatio-Temporal Logic Specifications

In spatially distributed systems such as smart buildings and intelligent transportation systems, control of spatio-temporal patterns is an important issue. In this paper, we consider a finite-horizon optimal spatio-temporal pattern control problem where the pattern is specified by a signal spatio-temporal logic formula over finite traces, which will be called an SSTL f formula. We give the syntax and Boolean semantics of SSTL f. Then, we show linear encodings of the temporal and spatial operators used in SSTLf and we convert the problem into a mixed integer programming problem. We illustrate the effectiveness of this proposed approach through an example of a heat system in a room.