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

Takuma KINUGAWA; Toshimitsu USHIO

doi:10.1587/transinf.2021FOP0003

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

Takuma KINUGAWA, Toshimitsu USHIO

Full Text Views

0

Cite this

Summary :

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 SSTL_f 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.

Publication: IEICE TRANSACTIONS on Information Vol.E105-D No.10 pp.1658-1664

Publication Date: 2022/10/01

Publicized: 2022/04/08

Online ISSN: 1745-1361

DOI: 10.1587/transinf.2021FOP0003

Type of Manuscript: Special Section PAPER (Special Section on Formal Approaches)

Category

Authors

Takuma KINUGAWA
Osaka University
Toshimitsu USHIO
Osaka University

Keyword

optimal control, spatio-temporal logic, spatially distributed system

Cite this

Copy

Takuma KINUGAWA, Toshimitsu USHIO, "Finite-Horizon Optimal Spatio-Temporal Pattern Control under Spatio-Temporal Logic Specifications" in IEICE TRANSACTIONS on Information, vol. E105-D, no. 10, pp. 1658-1664, October 2022, doi: 10.1587/transinf.2021FOP0003.
Abstract: 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 SSTL_f 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2021FOP0003/_p

Copy

@ARTICLE{e105-d_10_1658,
author={Takuma KINUGAWA, Toshimitsu USHIO, },
journal={IEICE TRANSACTIONS on Information},
title={Finite-Horizon Optimal Spatio-Temporal Pattern Control under Spatio-Temporal Logic Specifications},
year={2022},
volume={E105-D},
number={10},
pages={1658-1664},
abstract={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 SSTL_f 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.},
keywords={},
doi={10.1587/transinf.2021FOP0003},
ISSN={1745-1361},
month={October},}

Copy

TY - JOUR
TI - Finite-Horizon Optimal Spatio-Temporal Pattern Control under Spatio-Temporal Logic Specifications
T2 - IEICE TRANSACTIONS on Information
SP - 1658
EP - 1664
AU - Takuma KINUGAWA
AU - Toshimitsu USHIO
PY - 2022
DO - 10.1587/transinf.2021FOP0003
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E105-D
IS - 10
JA - IEICE TRANSACTIONS on Information
Y1 - October 2022
AB - 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 SSTL_f 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.
ER -