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

TL;DR

This paper introduces a novel nonlinear model predictive control method using Koopman operator theory combined with signal temporal logic to ensure temperature regulation in warm-water supply systems, addressing safety-critical requirements.

Contribution

It integrates signal temporal logic specifications into Koopman-based MPC, enabling effective control of nonlinear systems with formal safety guarantees.

Findings

Successfully applied to temperature regulation in warm-water systems

Demonstrated effectiveness through numerical simulations

Ensures safety-critical specifications are met

Abstract

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.