Formal Design Theory for Partially Observable Systems with Uncertainties

My research aims to derive a formal design theory on provably-correct high-level task planning for partially observable dynamical systems with uncertainties. For this, we propose a learning-based framework by combining methods from machine learning, formal methods, optimal control, decision theory, and game theory.

Our first research thrust is motivated by cooperative tasking between human and robots, and therefore focuses on the sequential decision-making problems in a collaborative scenario. To apply formal methods in sequential decision-making, it is of critical importance to obtain an expressive and meanwhile tractable mathematical model to characterize the dynamics of the system. The majority of existing work assumed a given system model or the structure of the model is fixed. However, it could be tedious and difficult to obtain such a model in practice. The first question we ask is how to build a system model. Due to the uncertainty and partial observability, we choose the partially observable Markov decision process (POMDP) as our system model. In particular, a POMDP model with continuous observations, called vector auto-regressive POMDP (VAR-POMDP), is proposed and the Bayesian non-parametric learning is adopted so we do not need to assume any knowledge of the model structure or its state space. After obtaining a VAR-POMDP model from data, the next question we ask is how to achieve performance guarantees in task planning. To automate the task planning process, we choose the probabilistic computation tree logic (PCTL) as formal specifications because it is very close to the natural English language, specifies branching-time properties, and also allows us to specify probabilistic bounds on the achievement of certain tasks. The high-level task planning problem can be converted into a finite-horizon planning problem or an infinite-horizon planning problem. The main barrier for the planning problem comes from the continuous observation space and the temporal correlation. To deal with this issue, we extend the point-based approximation algorithm and the heuristic search value iteration algorithm to approximate the exact value function by a piece-wise linear function and prove that the approximation error is bounded. The proposed VAR-POMDP model learning and its associated PCTL planning provide a formal design theoretical framework for partially observable systems with uncertainties such as human-robot collaboration.

Our second research thrust is mainly motivated by cyber attack and defense security-related applications, and therefore focuses on decision-making problems in an adversary scenario. In addition to uncertainties in the transition and observation in the POMDP model, the main concern induced by the adversary scenario is the uncertainty of the behavior of the opponent. For this, a partial observable stochastic game theoretical framework is pursued. In particular, we propose to investigate the one-sided partially observable stochastic games in which the state is hidden for one player but directly observed by the other player. Our observation is that, although it is beneficial for the informed player to take advantage of the asymmetrical information, the player has to balance the potential information leakage issue, which is the main challenge of the problem. To solve this issue, we adopt the concept of $\epsilon$-sacrifice policy and a two-step belief update strategy respectively. The asymmetrical information game can be solved by dynamic programming and a Stackelberg equilibrium can be achieved if players are rational. This game theoretical approach provides a systematic way for analyzing the interaction between two players in adversary scenarios and for defense policy synthesis in partially observable systems with uncertainties.

My research will pave the way toward a formal design theory that can handle uncertain, partially observable, and dynamic environments in a variety of applications including human-robot collaboration (HRC) and cyber-security.