Koopman-Model Predictive Control with Signal Temporal Logic Specifications for Temperature Regulation of a Warm-Water Supply System

Control of warm-water supply for dialysis treatment in a hospital environment is typical of safety-critical control problems. In order to guarantee the continuity of warm-water supply satisfying physical specifications for a wide range of operating conditions, it is inevitable to consider the nonlinearity involved in a dynamic model of a warm-water supply system for the control design. In this paper, we propose to incorporate control specifications described by signal temporal logic, which is a temporal logic with semantics over finite-time signals in formal methods, into the so-called Koopman-Model Predictive Control (MPC) as a novel technique of nonlinear MPC based on the Koopman operator framework for nonlinear systems. This enables us to generate a sequence of optimal inputs such that the controlled state of a nonlinear system can satisfy the specifications. The proposal is applied to the temperature regulation of warm-water supply, and its effectiveness is established numerically.