Sandboxing Controllers for Stochastic Cyber-Physical Systems

Abstract

Current cyber-physical systems (CPS) are expected to accomplish complex tasks. To achieve this goal, high performance, but unverified controllers (e.g. deep neural network, black-box controllers from third parties) are applied, which makes it very challenging to keep the overall CPS safe. By sandboxing these controllers, we are not only able to use them but also to enforce safety properties over the controlled physical systems at the same time. However, current available solutions for sandboxing controllers are just applicable to deterministic (a.k.a. non-stochastic) systems, possibly affected by bounded disturbances. In this paper, for the first time we propose a novel solution for sandboxing unverified complex controllers for CPS operating in noisy environments (a.k.a. stochastic CPS). Moreover, we also provide probabilistic guarantees on their safety. Here, the unverified control input is observed at each time instant and checked whether it violates the maximal tolerable probability of reaching the unsafe set. If this probability exceeds a given threshold, the unverified control input will be rejected, and the advisory input provided by the optimal safety controller will be used to maintain the probabilistic safety guarantee. The proposed approach is illustrated empirically and the results indicate that the expected safety probability is guaranteed.

This work was supported in part by the H2020 ERC Starting Grant AutoCPS (grant agreement No 804639) and German Research Foundation (DFG) through the grants ZA 873/1-1 and ZA 873/4-1. Marco Caccamo was supported by an Alexander von Humboldt Professorship endowed by the German Federal Ministry of Education and Research. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors and do not necessarily reflect the views of the Alexander von Humboldt Foundation.

Appendix: Proof of Theorem 2

The Proof of Theorem 2 is done with the help of the following lemma.

Lemma 1

Given a finite MDP $\mathfrak {M}\,=\,\{\tilde{X},\,\tilde{U},\,\tilde{T}\}$ and a Markov policy $\mu \,=\,(\mu _0, \mu _1,\ldots ,\mu _{H-1})$ in a finite time horizon $\overline{0,H}$, we have

$$\begin{aligned} 1-\tilde{V}_{n+1}(\tilde{x}) = \sum _{\tilde{y}\in \tilde{X}\backslash \{\phi \}}(1-\tilde{V}_{n}(\tilde{y}))\tilde{T}(\tilde{y}|\tilde{x},\mu _{H-n-1}(\tilde{x})) \end{aligned}$$

where $\tilde{V}_{n}(\tilde{x})$ is the value function for the reach-avoid problem and $\tilde{x}\in \tilde{X}$.

The proof can be readily derived based on Theorem 1 and the definition of $\tilde{T}$. Let $\mu '$ be the Markov policy used to control the system when the unverified controller is accepted at some states at some time instants. Here, we use $\tilde{X}_s$ to represent $\tilde{X}\backslash \{\phi \}$. Let’s define:

$$\begin{aligned} f(\tilde{x}(k),\mu '_{k}(\tilde{x}(k))) = 1-\sum _{\tilde{x}(k+1)\in \tilde{X}_s}\tilde{V}_{*,H-k-1}(\tilde{x}(k+1))\tilde{T}(\tilde{x}(k+1)|\tilde{x}(k),\mu '_{k}(\tilde{x}(k))), \end{aligned}$$

and

$$\begin{aligned} g(\tilde{x}(k-1),\mu '_{k-1}(\tilde{x}(k-1)))=\tilde{T}(\tilde{x}(k)|\tilde{x}(k-1),\mu '_{k-1}(\tilde{x}(k-1))). \end{aligned}$$

Given initial state $s_0\in \tilde{X}_s$, at each time instant $t=k$ where $k\in \overline{0,H-1}$, we have

$$\begin{aligned} \begin{aligned}&1-\tilde{V}^{\mu '}_{H}(s_0)\\ =&\sum _{\tilde{x}(1)\in \tilde{X}_s}\left( \sum _{\tilde{x}(2)\in \tilde{X}_s}\left( \ldots \left( \sum _{\tilde{x}(k)\in \tilde{X}_s}f(\tilde{x}(k),\mu '_{k}(\tilde{x}(k)))g(\tilde{x}(k-1),\mu '_{k-1}(\tilde{x}(k-1)))\right) \right. \right. \\&\left. \left. \ldots \right) g(\tilde{x}(1),\mu '_{1}(\tilde{x}(1)))\right) g(s_0,\mu '_{0}(s_0))\\ \end{aligned} \end{aligned}$$

$$\begin{aligned} \begin{aligned} \ge&\sum _{\tilde{x}(1)\in \tilde{X}_s}\left( \sum _{\tilde{x}(2)\in \tilde{X}_s}\left( \ldots \left( f(\underline{\tilde{x}(k)},\underline{\mu '_{k}(\tilde{x}(k))})\sum _{\tilde{x}(k)\in \tilde{X}_s}g(\tilde{x}(k-1),\mu '_{k-1}(\tilde{x}(k-1)))\right) \right. \right. \\&\left. \left. \ldots \right) g(\tilde{x}(1),\mu '_{1}(\tilde{x}(1)))\right) g(s_0,\mu '_{0}(s_0))\\ \ge&\sum _{\tilde{x}(1)\in \tilde{X}_s}\left( \sum _{\tilde{x}(2)\in \tilde{X}_s}\left( \ldots \left( \left( \sum _{\tilde{x}(k)\in \tilde{X}_s}g(\underline{\tilde{x}(k-1)},\underline{\mu '_{k-1}(\tilde{x}(k-1))}))\right) f(\underline{\tilde{x}(k)},\underline{\mu '_{k}(\tilde{x}(k))})\right. \right. \right. \\&\left. \left. \left. \sum _{\tilde{x}(k-1)\in \tilde{X}_s}g(\tilde{x}(k-2),\mu '_{k-2}(\tilde{x}(k-2)))\right) \ldots \right) g(\tilde{x}(1),\mu '_{1}(\tilde{x}(1)))\right) g(s_0,\mu '_{0}(s_0))\\ \ge&\sum _{\tilde{x}(1)\in \tilde{X}_s}\left( \sum _{\tilde{x}(2)\in \tilde{X}_s}\left( \ldots \left( \left( \sum _{\tilde{x}(k-1)\in \tilde{X}_s}g(\underline{\tilde{x}(k-2)},\underline{\mu '_{k-2}(\tilde{x}(k-2))})\right) \right. \right. \right. \\&\left( \sum _{\tilde{x}(k)\in \tilde{X}_s}g(\underline{\tilde{x}(k-1)},\underline{\mu '_{k-1}(\tilde{x}(k-1))})\right) f(\underline{\tilde{x}(k)},\underline{\mu '_{k}(\tilde{x}(k))})\\&\left. \left. \left. \sum _{\tilde{x}(k-2)\in \tilde{X}_s}g(\tilde{x}(k-3),\mu '_{k-3}(\tilde{x}(k-3)))\right) \ldots \right) g(\tilde{x}(1),\mu '_{1}(\tilde{x}(1)))\right) g(s_0,\mu '_{0}(s_0))\\&\ldots \\ \ge&\prod _{t=1}^{k}\sum _{\tilde{x}(t)\in \tilde{X}_s}g(\underline{\tilde{x}(t-1)}, \underline{\mu _{t-1}(\tilde{x}(t-1))}) (f(\underline{\tilde{x}(k)},\underline{\mu '_{k}(\tilde{x}(k))}) \end{aligned} \end{aligned}$$

where

$$\begin{aligned} (\underline{\tilde{x}(t-1)},\,\underline{\mu _{t-1}(\tilde{x}(t-1))}) = \mathop {\arg \min }_{\begin{array}{c} \tilde{x}(t-1)\in \tilde{X}_s\\ \mu _{t-1}(\tilde{x}(t-1)) \end{array}}\sum _{\tilde{x}(t)\in \tilde{X}_s}g(\tilde{x}(t-1), \mu _{t-1}(\tilde{x}(t-1))) \end{aligned}$$

for all $t\in \overline{0,k}$, and

$$\begin{aligned} (\underline{\tilde{x}(k)},\,\underline{\mu _{k}(\tilde{x}(k))}) = \mathop {\arg \min }_{\begin{array}{c} \tilde{x}(k)\in \tilde{X}_s\\ \mu _{k}(\tilde{x}(k)) \end{array}}f(\tilde{x}(k),\mu '_{k}(\tilde{x}(k))). \end{aligned}$$

Noted that $\omega = (\underline{\tilde{x}(0)}, \underline{\mu _0(\tilde{x}(0))},\underline{\tilde{x}(1)}, \underline{\mu _1(\tilde{x}(1))}\ldots \,\underline{\tilde{x}(k)})$ is one of the paths up to time instant k which can be generated by the system controlled by the Markov policy $\mu '$, and the History-based Supervisor ensures that for all paths $\omega$ up to arbitrary time instant $k\in \overline{0,H}$,

$$\begin{aligned} \prod _{t=1}^{k}\sum _{\tilde{x}\in \tilde{X}_s}g(\omega _x(t-1), \omega _u(t-1))\left( f(\omega _x(k),u_{uc}(\omega _x(k),k))\right) \ge 1-\rho . \end{aligned}$$

Note that we have $1-\tilde{V}^{\mu '}_{H}(s_0)\ge 1-\rho$, i.e. $p^{\mu '}_{s_0}(\diamond ^{\le H}\mathcal {A}^c) =\tilde{V}^{\mu '}_{H}(s_0) \le \rho$.