Correct-By-Construction Fault-Tolerant Control

Abstract

Correct-by-construction control synthesis methods refer to a collection of model-based techniques to algorithmically generate controllers/strategies that make the systems satisfy some formal specifications. Such techniques attract much attention as they provide formal guarantees on the correctness of cyber-physical systems, where corner cases may arise due to the interaction among different modules. The controllers synthesized through such methods, however, may still malfunction due to faults, such as physical component failures and unexpected operating conditions, which lead to a sudden change of the system model. In these cases, we want to guarantee that the performance of the faulty system degrades gracefully, and hence achieve fault tolerance.

This thesis is about 1) incorporating fault detection and detectability analysis algorithms in correct-by-construction control synthesis, 2) formalizing the graceful degradation specification for fault tolerant systems with temporal logic, and 3) developing algorithms to synthesize correct-by-construction controllers that achieve such graceful degradation, with possible delay in the fault detection. In particular, two sets of approaches from the temporal logic planning domain, i.e., abstraction-based synthesis and optimization-based path planning, are considered.

First, for abstraction-based approaches, we propose a recursive algorithm to reduce the fault tolerant controller synthesis problem into multiple small synthesis problems with simpler specifications. Such recursive reduction leverages the structure of the fault propagation and hence avoids the high complexity of solving the problem monolithically as one general temporal logic game. Furthermore, by exploring the structural properties in the specifications, we show that, even when the fault is detected with delay, the problem can be solved by a similar recursive algorithm without constructing the belief space.

Secondly, optimization-based path planning is considered. The proposed approach leverages the recently developed temporal logic encodings and state-of-art mixed integer programming (MIP) solvers. The novelty of this work is to enhance the open-loop strategy obtained through solving the MIP so that it can react contingently to faults and disturbance.

Finally, the control synthesis techniques developed for discrete state systems is shown to be applicable to continuous states systems. This is demonstrated by fuel cell thermal management application. Particularly, to apply the abstraction-based synthesis methods to complex systems such as the fuel cell thermal management system, structural properties (e.g., mixed monotonicity) of the system are explored and leveraged to ease abstraction computation, and techniques are developed to improve the scalability of synthesis process whenever the system has a large number of control actions.