Secure Control for Autonomous Cyber-Physical Systems Under Temporal Logic Constraints

Niu, Luyao

Etd

Secure Control for Autonomous Cyber-Physical Systems Under Temporal Logic Constraints

Public

Modern cyber-physical systems are expected to perform increasingly complex tasks. Synthesizing controllers to satisfy the assigned complex tasks with provable guarantees has received extensive research attention. The prior works assume that the cyber-physical systems are operated in benign environments where no adversary perturbs the system behaviors. Cyber-physical systems, however, have been demonstrated to be attractive targets of malicious attacks in a large variety of applications. To this end, the controllers designed for cyber-physical systems need to be capable of satisfying the complex specifications in the presence of malicious adversaries. In this thesis, we consider cyber-physical systems operated in adversarial environments. The systems aim at synthesizing controllers so as to satisfy some complex specifications modeled using temporal logic formulas. We identify a sequence of important problem settings, and propose a solution to each of them. We first study the problem of maximizing the probability of satisfying a linear temporal logic specification, i.e., maximizing the satisfaction probability. There exists an adversary that tampers with the input of the actuator, aiming to minimize the satisfaction probability. We formulate the interaction between the system and adversary as a stochastic game, and develop a value iteration algorithm to synthesize the controller. We then extend the problem to the scenarios where the systems are given multiple temporal logic specifications that may not be satisfied simultaneously. We develop efficient algorithms to synthesize controllers that yield minimum violations of the specifications. Next, we study the problem of control synthesis for cyber-physical systems with partial observabilities under linear temporal logic constraints. We formulate the interaction between the system and adversary as a partially observable stochastic game. We synthesize a controller equipped with finite memory for the system. We further investigate the problem of satisfying time sensitive specifications modeled using metric interval temporal logic for cyber-physical systems in the presence of attack. Incorporating the notion of time provides the adversary an additional attack surface, i.e., timing attack. We propose a durational stochastic game to capture the interaction between the system and the adversary that launches actuator attacks as well as timing attacks. We synthesize a controller for the system to maximize the satisfaction probability. Computing the aforementioned stochastic games is computationally demanding. In addition, synthesizing controllers using the stochastic games suffers from the curse of dimensionality for systems of large scales. To mitigate the computations, we study the problem of abstraction-free control synthesis for cyber-physical systems under linear temporal logic specifications. The abstraction-free synthesis eliminates the procedure of abstracting the cyber-physical system as a discrete finite abstraction. We decompose the linear temporal logic specification into a sequence of sub-formulas, and use a set of control barrier function based constraints to guarantee the satisfaction of each sub-formula.

Creator