Abstraction-Free Control Synthesis to Satisfy Temporal Logic Constraints under Sensor Faults and Attacks

In this subsection, we first give the notations that we will use throughout this paper. We next present the system model.

Notations. We use $\mathbb{R}^{n}$ to denote the $n$-dimensional Euclidean space. Given a vector $a\in\mathbb{R}^{n}$, we use $supp(a)$ and $[a]_{i}$ to denote its support and $i$-th entry, respectively. For any matrix $A$, we denote its trace as $tr(A)$. The set of positive semi-definite matrices of dimension $n\times n$ is represented as $\mathbb{S}^{n\times n}$. We denote the set of non-negative real numbers as $\mathbb{R}_{\geq 0}$. A function $\alpha:\mathbb{R}_{\geq 0}\rightarrow\mathbb{R}_{\geq 0}$ belongs to class $\mathcal{K}$ if it is continuous, strictly increasing, and $\alpha(0)=0$. A class $\mathcal{K}$ function belongs to class $\mathcal{K}_{\infty}$ if $\alpha(x)\rightarrow\infty$ when $x\rightarrow\infty$. We use $\mathbb{P}(\cdot)$ to represent the probability of an event.

Consider a nonlinear dynamical system defined as

where $x_{t}\in\mathbb{R}^{n}$ is the system state, $u_{t}\in\mathbb{R}^{p}$ is the control input at time $t$, $\sigma_{t}\in\mathbb{R}^{n\times n}$, and $W_{t}$ is an $n$-dimensional Brownian motion. Functions $f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n}$ and $g:\mathbb{R}^{n}\rightarrow\mathbb{R}^{n\times p}$ are locally Lipschitz continuous.

We denote the system output at time $t$ as $y_{t}\in\mathbb{R}^{q}$. The output $y_{t}$ follows an observation process [31] given as:

where $c\in\mathbb{R}^{q\times n}$, $\nu_{t}\in\mathbb{R}^{q\times q}$, and $V_{t}$ is a $q$-dimensional Brownian motion. We assume that the system operates in the presence of a malicious adversary. The adversary can inject a signal $a_{t}\in\mathbb{R}^{q}$ to manipulate the output $y_{t}$ with $supp(a_{t})\subseteq\{1,\ldots,q\}$. We assume that once the adversary determines the set of sensors to attack, it cannot adjust the support of the attack signal, i.e., the adversary cannot change its target after the attack starts. We assume that there are finitely many choices for the support of $a_{t}$, denoted as $\mathcal{F}=\{r_{1},\ldots,r_{m}\}$, which is also known to the system. In the remainder of this paper, we refer to $r_{i}$ as a fault pattern. However, the choice $supp(a_{t})$ made by the adversary is not known to the system.

In this subsection, we introduce background on finite time stability of stochastic nonlinear systems. Consider a stochastic nonlinear system with complete state information given by Eqn. (1). We then give the definition of finite time stability in probability.

Let $V$ be a twice continuously differentiable function. Finite time stability in probability is then certified by the following stochastic Lyapunov theorem.

The system given in Eqn. (1) and (2) employs a set of EKFs [33] to estimate the system state. Each EKF corresponds to a potential fault pattern $r_{i}\in\mathcal{F}$. We briefly review the background on EKF in the following.

We denote the state estimate at time $t$ as $\hat{x}_{t,i}$ when fault pattern $r_{i}$ is chosen by the adversary. Then the dynamics of $\hat{x}_{t,i}$ can be represented as

where $K_{t,i}=P_{t,i}c_{i}^{\top}R_{t,i}^{-1}$, $R_{t,i}=\nu_{t,i}\nu_{t,i}^{\top}$, and $c_{i}$ as well as $y_{t,i}$ are obtained from matrix $c$ and vector $y_{t}$ by removing the corresponding rows indexed by $r_{i}$. Matrix $\nu_{t,i}$ is obtained from $\nu_{t}$ by removing the rows and columns indexed by $r_{i}$. The covariance of $x_{t,i}$, denoted as $P_{t,i}$, is the solution to

where $Q_{t}=\sigma_{t}\sigma_{t}^{\top}$ and $A_{t,i}=\frac{\partial\bar{f}}{\partial x}(\hat{x}_{t},u)$ with $\bar{f}(\hat{x}_{t,i},u)=f(\hat{x}_{t,i})+g(\hat{x}_{t,i})u$. A belief state $b_{t,i}\in\mathbb{R}^{n}\times\mathbb{S}^{n\times n}\triangleq\mathbb{B}$ corresponding to fault pattern $r_{i}$ is defined as $b_{t,i}=(\hat{x}_{t,i},P_{t,i})$. The evolution of the belief state is described by Eqn. (5) and (6). We make the following assumptions on Eqn. (1) and (2).

Given Assumption 1, we have the following result.

In this subsection, we introduce GDTL [2, 3], which will be used to model the task that needs to be satisfied by system (1)-(2). We then formulate the problem studied in this paper.

The syntax of GDTL is defined as follows:

where $l:\mathbb{B}\rightarrow\mathbb{R}$, and $l\leq 0$ is a predicate.

Let $\mathbf{b}=b^{0}b^{1}\ldots$ be an infinite sequence of belief states with each $b^{i}\in\mathbb{B}$. We denote the suffix $b^{t}b^{t+1}\ldots$ of $\mathbf{b}$ as $\mathbf{b}^{t}$. Then a GDTL formula is interpreted as follows:

• •

  $\mathbf{b}^{t}\models True$

• •

  $\mathbf{b}^{t}\models l\leq 0$ iff $l(b^{t})\leq 0$

• •

  $\mathbf{b}^{t}\models\neg\varphi$ iff $\neg(\mathbf{b}^{t}\models\varphi)$

• •

  $\mathbf{b}^{t}\models\varphi_{1}\land\varphi_{2}$ iff $(\mathbf{b}^{t}\models\varphi_{1})\land(\mathbf{b}^{t}\models\varphi_{2})$

• •

  $\mathbf{b}^{t}\models\varphi_{1}\mathcal{U}\varphi_{2}$ iff $\exists t^{\prime}\geq t$ s.t. $(\mathbf{b}^{t^{\prime}}\models\varphi_{2})\land(\mathbf{b}^{t^{\prime\prime}}\models\varphi_{1})$ for all $t^{\prime\prime}<t^{\prime}$

Let $\mathbb{B}_{l}=\{b:l(b)\leq 0\}$ be the set of belief states such that predicate $l$ is true and $\mathcal{L}_{\varphi}$ be the set of predicates that appear in a GDTL formula $\varphi$. We present the following proposition [3] so as to construct an equivalent deterministic Rabin automaton (DRA) representing GDTL formula $\varphi$.

Leveraging Proposition 1, we can represent a GDTL formula using an equivalent DRA defined as follows:

We consider that the system given by Eqn. (1) and (2) needs to satisfy a GDTL specification $\varphi$. We define a labeling function $L:\mathbb{B}\rightarrow 2^{\tilde{\Pi}}$, where $\tilde{\Pi}$ is the set of atomic propositions generated by Proposition 1. For any $\pi\in\tilde{\Pi}$, we define $\llbracket\pi\rrbracket$ as $\llbracket\pi\rrbracket=\{b:\pi\in L(b)\}$. Consider $Z\in 2^{\tilde{\Pi}}$. We define $\llbracket Z\rrbracket$ as

We let $\mathbf{b}$ be a trajectory of belief state of infinite length. We now define the trace of $\mathbf{b}$ to establish the connection between the satisfaction of $\varphi$ to trajectory $\mathbf{b}$.

Using the trace of system trajectory, we have that GDTL specification $\varphi$ is satisfied if $Trace(\mathbf{b})\models\varphi$. The problem investigated in this paper is then formulated as follows:

This subsection derives fault-tolerant stochastic finite time convergence CBF. We first define stochastic finite time convergence CBF under complete information in the absence of an adversary. Then we extend it to the incomplete information setting. We finally propose the fault-tolerant stochastic finite time convergence CBF to address the presence of the adversary.

Stochastic finite time convergence CBF provides the finite time stability in probability guarantee as given by Definition 1. We formally state this result as follows:

In the following, we extend Definition 4 and Lemma 2 to the incomplete information setting where the system state is estimated via an EKF. Define

as the supremum of $h(x)$ for all $x$ belonging to the $\varepsilon$-neighborhood of the boundary of $\mathcal{C}$. We then present the following preliminary result [35].

We define $\hat{h}(x)=h(x)-\bar{h}_{\varepsilon}$. Provided Lemma 3, we are now ready to develop stochastic finite time convergence CBF under incomplete information setting for the system described by (1) and (2) employing EKF for state estimation, assuming that $a_{t}=\mathbf{0}$ for all $t\geq 0$.

We are now ready to present fault-tolerant stochastic finite time convergence CBF for the system given by (1)-(2) as follows. The system utilizes $m$ EKFs, with each associated with one attack pattern $r_{i}\in\mathcal{F}$, where $i=1,\ldots,m$.

The proof of Lemma 4 is omitted due to space constraint. Functions $h_{1},\ldots,h_{m}$ satisfying conditions 1) and 2) in Lemma 4 are fault tolerant stochastic finite time convergence CBFs.

Given the GDTL formula, we construct the DRA representing it, as defined in Definition 2. We then pick an accepting run of the automaton $\mathcal{A}$, denoted as $\eta$. We rewrite $\eta$ into the prefix suffix form $\eta=q_{1},\ldots,q_{n},(\eta_{suff})^{\omega}$. We next decompose the accepting run $\eta$ into a sequence of sub-formulae, denoted as $\psi_{1},\ldots,\psi_{N}$. Here

where $\Phi_{j}$ is the input word for self-loop transition $\delta(q_{j},\Phi_{j})=q_{j}$, and $\phi_{j}$ is the input word corresponding to the transition from state $q_{j}$ to $q_{j+1}$. That is, sub-formula $\psi_{j}$ models a one-step transition from state $q_{j}$ to $q_{j+1}$ along accepting run $\eta$.

We next synthesize the control policy to satisfy each sub-formula leveraging fault-tolerant finite time convergence control barrier functions in Section IV-A and fault-tolerant zeroing control barrier functions proposed in [36]. We then derive the satisfaction probability of each sub-formula, which is used to bound the probability of satisfying $\varphi$.

We let functions $h^{j}$ and $d^{j}$ be given as

Then sub-formula $\psi_{j}$ indicates that the system trajectory needs to guarantee $h^{j}(b)\geq 0$ for all $[t_{j},t_{j+1}]$ and $d^{j}(b)\geq 0$ for some $t^{\prime}\in[t_{j},t_{j+1}]$, where $t_{j}$ and $t_{j+1}$ are some time instants satisfying $t_{j+1}\geq t_{j}\geq 0$. We now define

We next present an algorithm for synthesizing the control policy so that the probability of satisfying sub-formula $\psi_{j}$ is lower bounded in Algorithm 1. In line 3, we compute $X_{t}(\varrho)=\{i:\hat{h}_{i}^{j}(b_{t,i})<\varrho_{1},\hat{d}_{i}^{j}(b_{t,i})<\varrho_{2}\}$, where $\varrho=[\varrho_{1},\varrho_{2}]^{\top}$ and $\varrho_{1},\varrho_{2}>0$ are constants. In line 4, we first compute the set of control inputs $\Omega_{i}$ and $\Gamma_{i}$, where $\Omega_{i}$ ensures that $h^{j}(b_{t,i})\geq 0$ for all $t\in[t_{j},t_{j+1}]$, and $\Gamma_{i}$ ensures that there exists $t^{\prime}\in[t_{j},t_{j+1}]$ such that $d^{j}(x)\geq 0$, provided that the fault pattern is $r_{i}$. If $\cap_{i\in X_{t}(\varrho)}(\Omega_{i}\cap\Gamma_{i})\neq\emptyset$, then any control input $u\in\cap_{i\in X_{t}(\varrho)}(\Omega_{i}\cap\Gamma_{i})$ guarantees the satisfaction of sub-formula $\psi_{j}$ regardless of the fault pattern. If such $u$ does not exist, then line 5-11 aims to identify the fault pattern by comparing the state estimate when fault pattern $r_{i}$ is removed. Line 17 computes the control input by solving a quadratic program. If no feasible control input can be found, we will repeat the procedure for another accepting run $\eta^{\prime}\neq\eta$.