# Synthesis-guided Adversarial Scenario Generation for Gray-box Feedback
Control Systems with Sensing Imperfections

Liren Yang<EMAIL_ADDRESS>and  Necmiye Ozay<EMAIL_ADDRESS>University
of MichiganAnn ArborMichiganUSA48105

###### Abstract.

In this paper, we study feedback dynamical systems with memoryless controllers
under imperfect information. We develop an algorithm that searches for
“adversarial scenarios”, which can be thought of as the strategy for the
adversary representing the noise and disturbances, that lead to safety
violations. The main challenge is to analyze the closed-loop system’s
vulnerabilities with a potentially complex or even unknown controller in the
loop. As opposed to commonly adopted approaches that treat the system under
test as a black-box, we propose a synthesis-guided approach, which leverages
the knowledge of a plant model at hand. This hence leads to a way to deal with
gray-box systems (i.e., with known plant and unknown controller). Our approach
reveals the role of the imperfect information in the violation. Examples show
that our approach can find non-trivial scenarios that are difficult to expose
by random simulations. This approach is further extended to incorporate model
mismatch and to falsify vision-in-the-loop systems against finite-time reach-
avoid specifications.

adversarial scenarios, imperfect information games, safety

This article appears as part of the ESWEEK-TECS special issue and was
presented in the International Conference on Embedded Software (EMSOFT), 2021.
DOI: https://doi.org/10.1145/3477033

††journal: TECS††ccs: Computer systems organization Embedded systems††ccs:
General and reference Verification

##  1\. Introduction

Figure 1. Block diagram of a closed-loop control system.

Cyber-physical systems (CPS) combine physical processes and computational
(cyber) elements to perform complicated tasks in a dynamic environment. From a
control perspective, a simplified CPS can be described by the block diagram in
Fig. 1, where the plant represents the physical process, and the controller
makes decisions at the cyber layer. The disturbance input $w$ encompasses
environment parameters, external events and other agents’ actions that
directly act on the plant, whereas the input $v$ captures the noise and data
loss, which lead to imperfect information $y$ and affect the controller’s
decision. The controller’s goal is to determine control actions $u$ so that
the plant’s state trajectories satisfy some high-level specifications under
all possible environmental uncertainties.

One key challenge in the CPS research is, given a control design, how to prove
that it achieves desired closed-loop behavior. This question is particularly
important for safety-critical systems. Due to the complexity of the
specification and the environment, the controller may be complicated even if
the plant has modest complexity and may include optimization, learning and
vision based components. The formal verification of the closed-loop system is
hence a difficult task. Instead of verification, one alternative is to start
with the plant model and close the loop by directly synthesizing a correct-by-
construction controller, which achieves the specification provably. However,
the synthesis problem is also challenging, especially when the controller does
not have perfect information of the state of the world (De Wulf et al., 2006),
(Majumdar et al., 2020), (Yang and Ozay, 2020). For the cases where a vision-
based solution must be used, such task is even harder. Other than synthesis, a
more practical alternative is to quickly find scenarios under which the system
trajectory violates the specification, i.e., to falsify the system. These
adversarial scenarios are valuable for understanding the shortcomings of the
controller at early design stages, which may be hard to expose by random
simulations. Moreover, once found, these adversarial scenarios can be used to
improve the design, e.g., see (Fremont et al., 2020), (Ghosh et al., 2019),
(Wang et al., 2020).

The problem of finding adversarial scenarios (a.k.a. falsification) for CPS
has attracted much attention in the past two decades. Many approaches and
tools are developed using stochastic search and optimization techniques, e.g.,
random tree search (Bhatia and Frazzoli, 2004), (Ernst et al., 2019), (Kim et
al., 2005), (Nahhal and Dang, 2007), (Plaku et al., 2009), specification-
guided stochastic sampling (Annpureddy et al., 2011), Tabu search (Deshmukh et
al., 2015), Bayesian optimization (Deshmukh et al., 2017), (Ghosh et al.,
2018), nonlinear simplex optimization (Donzé, 2010). These works all treat the
system under test as a black-box to avoid its high complexity, and search for
a specification violation at the system level. Notably, some recent works
(Dreossi et al., 2019a), (Dreossi et al., 2019b), (Tuncali et al., 2018) study
systems with vision/learning-based controllers in the loop. In particular,
(Tuncali et al., 2018) searches for a physical environment configuration
(encoded by $w$) at the system level, whereas (Dreossi et al., 2019a) uses a
decomposition idea and focuses on the impact of imperfect information (encoded
by $v$) to the learning component in the cyber layer, which is equivalently
important.

One closely related domain is adversarial learning, which includes a line of
research that analyzes the vulnerability and robustness of machined learning
algorithms against malicious agents. It is shown that inputs carefully crafted
by adding small perturbations unnoticeable to human eyes can fool well-trained
neural network classifiers (Dalvi et al., 2004), (Goodfellow et al., 2015),
(Moosavi-Dezfooli et al., 2016), (Szegedy et al., 2014) or policies obtained
by reinforcement learning (Huang et al., 2017), (Kos and Song, 2017), and may
harm the performance of practical CPS (e.g., autonomous cars) with deep neural
networks in the loop (Pei et al., 2017). In the context of CPS falsification,
these works focus on shifting the output of the learning-based controller by
twisting the noise $v$ adversarially. As pointed out in (Tuncali et al.,
2018), such attacks are at component level and do not necessarily lead to
specification violations at the system level. This is because i) the
effectiveness of the attack relies on the learning module being well-trained,
and ii) a deviation in the learning algorithm’s output does not necessarily
lead to bad behaviors (e.g., to avoid an obstacle in the front, it is
sometimes equivalently good to turn left or right). Adversarial learning
methods usually require the component under analysis to be a white-box, and
the black-box attacks are usually based on the principle of transferability
(Bose et al., 2020), (Huang et al., 2017). More recently, a slightly different
work (Gleave et al., 2019) presents a way to falsify reinforcement learning
policies at the system level using the disturbance $w$, which captures the
move of an adversarial agent. However, the form of the entire closed-loop
system must be known.

In this paper, we ask the following question: when there is a control-oriented
plant model with modest complexity at hand, yet the closed-loop system is
still hard to formally analyze due to highly complex controllers, is there a
way to leverage the knowledge of this simple plant model and quickly identify
non-trivial safety violations at the system level, where both the disturbance
$w$ and the noise $v$ are essential for the violations to occur? Here, by a
“simple plant”, we mean any open-loop system (e.g., switched-affine systems)
for which a two-player safety game can be solved relatively efficiently. By a
“complex controller”, we mean any controller (e.g., hybrid MPC, neural network
controllers or black-box controllers) that makes it challenging to compute the
backward reachable set for the closed-loop system. This problem is motivated
by systems such as autonomous cars, which have relatively simple motion
dynamics but complex controllers and imperfect sensors (e.g., a camera). We
refer to such systems with known plant models and unknown controllers as gray-
box systems. Despite the same terminology, our setting is different from that
in (Yaghoubi and Fainekos, 2019), where the term “gray-box system” refers to
an unknown system whose closed-loop model can be approximated with a local
linear model constructed on the fly in the falsification process. Another
related work is (Waga, 2020), where a finite abstraction (Mealy machine) is
learned from a CPS, and adversarial scenarios of the CPS is searched via model
checking on the abstraction. The main difference of our setting is the
separation of the plant and the controller. Table 1 compares our setting and
the aforementioned works.

We focus on safety specifications and static output-feedback controllers, and
propose a synthesis-guided falsification approach to find adversarial
scenarios111The term “falsification” and “adversarial scenario generation” are
used interchangeably from now on.. The key idea is to inner-approximate the
closed-loop system’s backward reachable set under the guidance of a local two-
player game’s solution, whose complexity is independent of the controller. We
further approach the falsification of vision-in-the-loop systems from such
imperfect information game standpoint and show that a semantic space search
reduction similar to (Dreossi et al., 2019a), (Tuncali et al., 2018) can be
used in our framework.

Table 1. Adversarial Learning vs. Falsification Comparison | White-box | Falsifying | Falsification
---|---|---|---
| Components | Input | Level
Adversarial | controller | $v$ | component
Learning |  (Gleave et al., 2019): plant & controller | $w$ | system
Falsification | $-$ |  $w$ & $v$ | system
This Paper | plant |  $w$ & $v$ | system

In the rest of the paper, we first review the problems of falsification and
synthesis under full information in Section 2, and discuss the falsification
problem under imperfect information in Section 3. Then we present the
following main contributions of our work.

  * •

In Section 4, we propose a synthesis-guided falsification framework to find
adversarial scenarios under our gray-box settings. In this framework,
different backward reachability analysis techniques can be applied (depending
on the structural properties the plant has). We provide two implementations of
our approach for plants with switched affine dynamics, one uses MPT3 toolbox
(Herceg et al., 2013) (works for systems up to 4D), and the other is based on
zonotope computation techniques developed in (Sadraddini and Tedrake, 2019)
(works for systems of 10D or even higher).

  * •

In Section 5, we extend our approach to incorporate model mismatch (Section
5.1) and to falsify vision-in-the-loop systems (Section 5.2) against finite-
time reach and avoid specifications (Section 5.3).

  * •

In Section 6, we evaluate our approach and its extensions with several
examples. We show that the approach can falsify black-box controllers,
including hybrid model predictive controllers (MPC) and feedforward neural
network controllers, by running the same algorithm blindly. To demonstrate the
scalability and effectiveness, we also test our approach against randomly
generated problem instances. Experiments show that the obtained scenarios are
nontrivial.

##  2\. Preliminaries

Notations. Let $S$ be a set, we use $S^{\ast}$ and $S^{\omega}$ to denote the
set of finite and infinite sequences of elements in $S$, respectively. The set
of finite sequences in $S^{\ast}$ of length $T$ is denoted by $S^{T}$, and the
empty sequence of length zero is denoted by $\varepsilon$. Throughout the
paper, we will use bold font letters, e.g., s, to represent infinite
sequences. We denote by $s_{t}$ the $(t+1)^{\rm th}$ element ($t$ starts from
$0$) of a sequence s, and define $\textbf{s}_{t}=s_{0}s_{1}s_{2}\dots s_{t}$
to be the prefix of the sequence s until time $t$. Let $\mathbb{Z}$ be the set
of integers, given $a\in\mathbb{Z}\cup\\{-\infty\\}$ and
$b\in\mathbb{Z}\cup\\{\infty\\}$ such that $a\leq b$, the set
$\\{s\in\mathbb{Z}\mid a\leq s\leq b\\}$ is denoted by $[\\![a,b]\\!]$.

###  2.1. Falsification & Control Synthesis under Perfect Information

Consider a discrete-time time-invariant system
$\overline{\Sigma}:x_{t+1}=f(x_{t},u_{t},w_{t})$ where $x\in X$ is the state,
$u\in U$ is the control input, $w\in W$ is the disturbance input (or process
noise), and $f:X\times U\times W\rightarrow X$ is the transition map. A
sequence $\textbf{x}\in X^{\omega}$ is a trajectory of the system under a
state-feedback controller $\overline{\pi}:X\rightarrow U$ if and only if (iff)
there exists a control sequence $\textbf{u}\in U^{\omega}$ and a disturbance
sequence $\textbf{w}\in W^{\omega}$ such that for all
$t\in[\\![0,\infty]\\!]$: i) $x_{t+1}=f(x_{t},u_{t},w_{t})$, and ii)
$u_{t}=\overline{\pi}(x_{t})$. With a slight abuse of terminology, we will
also call the finite prefix $\textbf{x}_{T}$ a trajectory for any natural
number $T$. Since the state-feedback controller $\overline{\pi}$ makes its
decision based on the exact state $x_{t}$, it is said to have perfect
information. Also note that, due to the disturbance $w$, the closed-loop
system’s trajectory is not uniquely determined by the initial condition and
the controller.

The following two safety problems under perfect information have been studied
in the literature:

  * •

Falsification: given a set $X_{\rm safe}$ of safe states, a set $X_{\rm init}$
of initial states and a state-feedback controller $\overline{\pi}:X\rightarrow
U$, find a trajectory $\textbf{x}_{T}$ of the closed-loop system that starts
at some initial state $x_{0}\in X_{\rm init}$ such that $x_{T}\notin X_{\rm
safe}$ (proving that such $\textbf{x}_{T}$ does not exist is called safety
verification).

  * •

Synthesis: given a set $X_{\rm safe}$ of safe states, find a set of winning
initial states and a state-feedback controller $\overline{\pi}:X\rightarrow U$
such that all the closed-loop trajectories x under controller $\overline{\pi}$
starting from an arbitrary winning state will stay in the safe set for all
time, i.e. $\textbf{x}\in X_{\rm safe}^{\omega}$.

###  2.2. Game Theoretical Interpretation of Verification/Falsification and
Synthesis

The above problems can be analyzed and solved with a game theoretical
interpretation. The game is between the controller and the environment. The
controller’s goal is to keep the states within the safe set $X_{\rm safe}$,
while the environment aims to force the state out of $X_{\rm safe}$. At time
$t$, the controller first picks a control input $u_{t}$ based on the current
state $x_{t}$, and then the environment picks a disturbance input $w_{t}$. At
time $t+1$, the system will evolve to the new state
$x_{t+1}=f(x_{t},u_{t},w_{t})$, from where the game will proceed to the next
round.

Verification/falsification: one-player game. The verification (or
falsification) problem is a one-player game (because the control policy
$\overline{\pi}$ is given) where we play the environment’s role. This one-
player game can be solved by performing the following iteration until
$X_{k}^{\overline{\pi}}\cap X_{\rm init}\neq\emptyset$,

(1) $\displaystyle X_{0}^{\overline{\pi}}$ $\displaystyle=X_{\rm
unsafe}:=X\setminus X_{\rm safe},$ (2) $\displaystyle
X_{k+1}^{\overline{\pi}}$
$\displaystyle=\textbf{Pre}^{\overline{\pi}}(X_{k}^{\overline{\pi}}):=\big{\\{}x\in
X\,\big{|}\,\exists w\in W:f\big{(}x,{\overline{\pi}}(x),w\big{)}\in
X_{k}^{\overline{\pi}}\big{\\}}.$

Once the sets $\\{X_{k}^{\overline{\pi}}\\}_{k=1}^{T}$ are computed, the
falsifying run $\textbf{x}_{T}$ can be easily derived:

(3) $\displaystyle x_{0}$ $\displaystyle\in X_{T}^{\overline{\pi}}\cap X_{\rm
init}$ (4) $\displaystyle x_{t+1}$
$\displaystyle\in\big{\\{}f\big{(}x_{t},{\overline{\pi}}(x_{t}),w\big{)}\mid
w\in W\big{\\}}\cap X_{T-t-1}^{\overline{\pi}}\text{ for
}t\in[\\![0,T-1]\\!].$

###### Remark 1.

The above procedure can be split into two phases: the backward expansion
phase, during which we compute sets
$\\{X_{k}^{\overline{\pi}}\\}_{k=0}^{\infty}$ by Eq. (1), (2), and the forward
expansion phase where the falsifying trajectory $\textbf{x}_{T}$ is computed
via Eq. (3), (4). The computational effort is mainly spent on the backward
expansion phase that involves manipulating sets, whereas the forward expansion
phase is much cheaper because one only needs to find one state per step. In
the backward expansion phase, the biggest challenge is to compute (or even to
under approximate) the predecessors $\textbf{Pre}^{\overline{\pi}}$ of a set
of states because the closed-loop dynamics is potentially complicated. Even
when the open-loop dynamics $f$ is simple, this challenge may arise due of the
complexity of the controller $\overline{\pi}$. $\Diamond$

Falsification by synthesis: two-player game. In the synthesis problem, we play
the controller’s role and refer to the game that we solve as the safety game.
The safety game is a two-player game because the environment’s policy is not
given a priori. If we play the role of the environment assuming that the
controller $\overline{\pi}$ is unknown, the resulting two-player game is
called the dual game (Chou et al., 2018) and can be used for falsification. We
briefly describe the solutions to the safety game and the dual game and their
connection below.

In the perfect information setting, there exists a maximal winning set of the
safety game, i.e., the maximal robust controlled invariant set $R\subseteq
X_{\rm safe}$. This maximal winning set can be achieved by a state-feedback
controller $\overline{\pi}_{\rm best}$ such that
$f\big{(}x,\overline{\pi}_{\rm best}(x),w\big{)}\subseteq R$ for all $x\in R$
and $w\in W$. The set $R$ can be computed at the limit by iteratively removing
set $D_{k}$ from $X_{\rm safe}$, where $D_{k}$ is the set of states that can
be forced into the unsafe set $X_{\rm unsafe}:=X\setminus X_{\rm safe}$ in $k$
steps by the uncertainties. Formally,

(5) $\displaystyle D_{0}$ $\displaystyle=X_{\rm unsafe},$ (6) $\displaystyle
D_{k+1}$ $\displaystyle=\textbf{EPre}(D_{k}):=D_{k}\cup\big{\\{}x\in
X\,\big{|}\,\forall u\in U:\exists w\in W:f(x,u,w)\cap
D_{k}\neq\emptyset\big{\\}}.$

where $\textbf{EPre}(D_{k})$ contains the environment-controllable predecessor
of set $D_{k}$. It is shown in (Bertsekas, 1972) that under mild compactness
conditions,

(7) $\displaystyle R=X\setminus D\text{ \ \ where \ \
}D:=\cup_{k=1}^{\infty}D_{k}.$

The set $D$ is called the dual game winning set under perfect information,
from where falsification is guaranteed regardless of the controller.
Throughout this paper, we assume that Eq. (7) holds. Once we obtain sets
$\\{D_{k}\\}_{k=0}^{\infty}$ by solving the dual game, an environmental
strategy can be derived to pick the disturbance $w_{t}$, in a way to falsify a
specific controller $\overline{\pi}$. Let $x_{0}\in
D=\cup_{k=1}^{\infty}D_{k}$, define

(8) $\displaystyle x_{0}$ $\displaystyle\in D_{T},\text{ for some }T$ (9)
$\displaystyle w_{t}$ $\displaystyle\text{ is s.t.
}x_{t+1}=f\big{(}x_{t},\overline{\pi}(x_{t}),w_{t}\big{)}\in D_{T-t-1}\text{
for }t\in[\\![0,T-1]\\!].$

It can be easily shown inductively that $x_{t}$ exists for all
$t\in[\\![1,T]\\!]$ and $x_{T}\in D_{0}=X_{\rm unsafe}$. Hence
$\textbf{x}_{T}$ is a trajectory falsifying the controller $\overline{\pi}$.
Note that we need the above dual strategy for falsification because even if
initiated in $D$, a safety violation is not guaranteed unless the environment
picks the uncertainties adversarially against the given controller
$\overline{\pi}$.

###### Remark 2.

The dual-game-based falsification procedure also consists of a backward
expansion phase and a forward expansion phase. Notably, the complexity of the
backward expansion only depends on the open-loop system’s transition map $f$
and is independent of the controller $\overline{\pi}$. Via such falsification
approach we only get generic adversarial scenarios, in which case no
controller can ensure safety starting from the falsifying initial condition
$x_{0}$. $\Diamond$

##  3\. Adversarial Scenarios under Imperfect Information

In this section, we describe the problem of finding adversarial scenarios
under imperfect information. We first introduce systems with imperfect
information, then use an example to motivate finding “controller-specific
adversarial scenarios”, and finally give the formal problem statement.

###  3.1. Systems with Imperfect Information

In this paper, we consider the safety control problem for systems with
imperfect state information in the following form:

(10) $\displaystyle\Sigma\ :\ x_{t+1}$ $\displaystyle=f(x_{t},u_{t},w_{t}),\ \
y_{t}=g(x_{t},v_{t}),$

where the state $x$, the control $u$, the disturbance $w$ and the transition
map $f$ are defined exactly the same as the perfect information case, $y\in Y$
is the output (observation), $v\in V$ is the measurement noise and $g:X\times
V\rightarrow Y$ is the measurement map. We denote $x\sim y$ if there exists
$v\in V$ such that $y=g(x,v)$. The control input $u$ can be determined by an
output-feedback control policy (controller) $\pi:(Y\times U)^{\ast}\times
Y\rightarrow U$. We call a controller $\pi$ static (aka, memoryless) if its
decision at a time instant $t$ only depends on the latest observation $y_{t}$.

Given a controller $\pi$ and an initial state $x$, the closed-loop system’s
trajectory is not unique due to the system’s uncertainties. Hence
falsifications, if possible, may not be achieved unless the environment
adversarially picks the disturbance (i.e., process noise) $w_{t}$ and the
sensor noise $v_{t}$. We introduce the following notion of falsifiability to
capture the existence of an adversarial scenario.

###### Definition 1.

Let $\Sigma$ be a system described by Eq. (10) and $\pi:(Y\times
U)^{\ast}\times Y\rightarrow U$ be a controller. Given a state $x$, the
closed-loop system starting from state $x$, denoted by $\Sigma_{\pi}(x)$, is
called falsifiable w.r.t. a safe set $X_{\rm safe}$ if there exists
$T\in\mathbb{Z}$, $\textbf{x}_{T}\in X^{T+1}$, $\textbf{v}_{T-1}\in V^{T}$,
$\textbf{y}_{T-1}\in Y^{T}$, $\textbf{u}_{T-1}\in U^{T}$, $\textbf{w}_{T-1}\in
W^{T}$, such that

  * 1)

$x_{0}=x$, $x_{T}\in X\setminus X_{\rm safe}$,

  * 2)

$\forall
t\in[\\![0,T-1]\\!]:x_{t+1}=f(x_{t},u_{t},w_{t}),y_{t}=g(x_{t},v_{t})$,
$u_{t}=\pi(\textbf{y}_{t},\textbf{u}_{t-1})$, where $\textbf{u}_{-1}$ is
defined to be the empty sequence $\varepsilon$.

Since the sequences $\textbf{x}_{T}$, $\textbf{y}_{T-1}$ and
$\textbf{u}_{T-1}$ can be determined from $x_{0}=x$, $\textbf{v}_{T-1}$ and
$\textbf{w}_{T-1}$ given $f$, $g$ and $\pi$, we will say that
$\Sigma_{\pi}(x)$ is falsifiable under
$(x,\textbf{w}_{T-1},\textbf{v}_{T-1})$. The safety game winning set of a
controller $\pi$, denoted by $Win^{\pi}$, is defined to be $\\{x\in
X\mid\Sigma_{\pi}(x)\text{ is not falsifiable}\\}$.

###  3.2. A Motivating Example

We now present a toy example to motivate the problem of finding “controller-
specific” adversarial scenarios under imperfect information. Consider the
system in Figure. 2, where the circles represent states $x\in[\\![1,6]\\!]$,
the blue and red arrows represent the transitions under two control actions
$u\in\\{blue,red\\}$, and the numbers in quotation marks near a state $x$
represent the possible observations $y$ at state $x$. The safe set $X_{\rm
safe}=[\\![1,5]\\!]$. It can be verified that the maximal robust controlled
invariant set $R=\\{1,2,3,4\\}$ and the dual winning set $D=\\{5,6\\}$ with
perfect information. The best state-feedback controller $\overline{\pi}_{\rm
best}$ is such that $\overline{\pi}_{\rm best}(3)=blue$ and
$\overline{\pi}_{\rm best}(4)=red$.

In the imperfect information case, let $\pi_{1}$ and $\pi_{2}$ be two output-
feedback controllers. Define $\pi_{1}$ to be such that
$\pi_{1}(\textbf{y}_{t},\textbf{u}_{t-1})=blue$ if $y_{0}\in\\{1,3,4\\}$, and
$\pi_{1}(\textbf{y}_{t},\textbf{u}_{t-1})=red$ if $y_{0}=2$. Define $\pi_{2}$
to be such that $\pi_{2}(\textbf{y}_{t},\textbf{u}_{t-1})=blue$ if $y_{0}=1$,
and $\pi_{2}(\textbf{y}_{t},\textbf{u}_{t-1})=red$ if $y_{0}\in\\{2,3,4\\}$.
Clearly, $Win^{\pi_{1}}=\\{1,2,3\\}$ and $Win^{\pi_{2}}=\\{1,2,4\\}$, and
these two winning sets are not comparable. More importantly, no other
controller has a winning set larger than $Win^{\pi_{1}}$ or $Win^{\pi_{2}}$.

Figure 2. Left: motivating example. Right: illustration of controller-specific
falsifications.

By the above argument, any output-feedback controller $\pi$ is guaranteed to
be falsified either starting from state $3$ or from state $4$. Note, however,
that falsification at states $\\{1,2\\}$ can be avoided by some controller
(e.g., $\pi_{1}$ and $\pi_{2}$) although visiting state $3$ and state $4$ is
inevitable from state $1$ and state $2$, respectively. This is because the two
controllers have memory and can distinguish state $3$ from state $4$ if the
system starts from either state $1$ or state $2$ and if the initial state is
remembered. This is not the case, however, if we restrict the controllers to
be static. This suggests that a backward expansion algorithm will not work
unless the controllers to falsify are static.

The situation is illustrated by Figure 2 (right). An adversarial scenario for
controller $\pi_{2}$ can be found from the star, but can be avoided by
controller $\pi_{1}$. Moreover, no controller is better than $\pi_{2}$
($\pi_{1}$ is no better because its winning set is incomparable with that of
$\pi_{2}$). We will refer to such falsifications as controller-specific
adversarial scenarios, to distinguish them from the generic adversarial
scenarios obtained by solving the dual game under full information (see Remark
2). $\dagger$

###  3.3. Problem Statement

Motivated by the above discussions, we will focus on falsifying a closed-loop
system running an output-feedback controller. Our goal is to find a
controller-specific adversarial scenario under imperfect information. The
controllers under consideration in this work are static controllers. Such
static controllers are common in feedback control (e.g., MPC, neural network
controller). The formal problem statement is given below.

###### Problem 1.

Consider a white-box system in Eq. (10), and a black-box static output-
feedback controller $\pi:Y\rightarrow U$ that can be queried at any given
point $y\in Y$, (i.e., $u=\pi(y)$ can be obtained by querying). Given a set
$X_{\rm init}$ of initial states, and a set $X_{\rm safe}$ of safe states,
find an adversarial test case $(x,\textbf{w}_{T-1},\textbf{v}_{T-1})$ such
that $x\in X_{\rm init}\setminus D$, and $\Sigma_{\pi}(x)$ is falsifiable
under $(x,\textbf{w}_{T-1},\textbf{v}_{T-1})$.

In the above problem formulation, requiring $x\in X_{\rm init}\setminus D$
allows the information imperfection (i.e., sensor noise) to play an important
role in the falsification (if $x\in D$, the adversarial disturbance by itself
can lead to safety violation). The initial set $X_{\rm init}$ is usually far
enough from the unsafe set so that trivial falsifying trajectories that start
too “close” to the unsafe set do not exist.

##  4\. Synthesis-guided Adversarial Scenario Generation

We first discuss the challenge of solving Problem 1. Now that our goal is to
find controller-specific falsifying scenarios, we must use the knowledge of
the given controller $\pi$. The dual-game-based falsification approach does
not apply directly because it only searches for generic adversarial scenarios,
as discussed in Remark 2. Theoretically, similar to Eq. (1), (2), one can
search for controller-specific scenarios by solving a one-player game:

(11) $\displaystyle X_{0}^{\pi}$ $\displaystyle=D,$ (12) $\displaystyle
X_{k+1}^{\pi}$ $\displaystyle=\textbf{Pre}^{\pi}(X_{k}^{\pi}):=\big{\\{}x\in
X\,\big{|}\,\exists y\sim x,w\in W:f\big{(}x,\pi(y),w\big{)}\in
X_{k}^{\pi}\big{\\}}.$

We stop iterating when $(X_{N}^{\pi}\setminus D)\cap X_{\rm
init}\neq\emptyset$, and a falsifying trajectory can be extracted by forward
expansion. However, computing $\textbf{Pre}^{\pi}(\cdot)$ is possible only
when the explicit expression of the given controller $\pi$ is fully known and
also simple enough. In practice, it is more common that the given static
output-feedback controller is complicated and even unknown. For example, this
given controller can be a rule-based controller (i.e., look-up table) obtained
by calibration or learning methods, an MPC controller, or even a black-box
controller whose expression is unavailable to the test engineers. The backward
reachable sets of the closed-loop systems under such controllers are difficult
to compute in general. Instead, we are only allowed to simulate or query the
given static controller at certain observation points, and this provides us
with limited knowledge of the controller’s behavior. The key challenge is to
generate careful queries at critical points and avoid sampling the entire
space exhaustively.

The rest of this section is devoted to tackling the above challenge. The key
idea is to use synthesis, which does not require any knowledge of the given
controller $\pi$, to guide where to query $\pi$. In particular, the controller
is only queried at observation points carefully selected by solving a local
dual game, so that exhaustive sampling of the output space is avoided. Based
on the controller’s decision at the selected points, we can under-approximate
$\textbf{Pre}^{\pi}(\cdot)$. This leads to an inner approximation of the
backward reachable set $X_{k}^{\pi}$, which would be sufficient for the
purpose of falsification because we only aim at finding one falsifying
trajectory.

In what follows, we will introduce different ingredients in this procedure and
conclude the section with a pseudocode that integrate all these ingredients.

###  4.1. Under-approximate $\textbf{Pre}^{\pi}(\cdot)$ with Local Dual Game
and Query

First, the inner approximation of $X_{k}^{\pi}$ can be constructed by an
iterative process that alternatingly solves a local dual game under imperfect
information (13) and queries the given controller (15).

(13) $\displaystyle\underline{X}_{0}^{\pi}$ $\displaystyle\subseteq D,$ (14)
$\displaystyle\underline{Y}_{k+1}$
$\displaystyle=\textbf{EPre}_{y}(\underline{X}_{k}^{\pi}\mid U):=\\{y\in
Y\,|\,\forall u\in U:\exists x\sim y,w\in
W:f(x,u,w)\in\underline{X}_{k}^{\pi}\\},$ (15)
$\displaystyle\underline{y}_{k+1}$ $\displaystyle\in\underline{Y}_{k+1},$ (16)
$\displaystyle\underline{X}_{k+1}^{\pi}$
$\displaystyle=\textbf{Pre}_{\underline{y}_{k+1}}^{\pi}(\underline{X}_{k}^{\pi}):=\big{\\{}x\in
X\big{|}x\sim\underline{y}_{k+1},\exists w\in
W:f\big{(}x,\pi(\underline{y}_{k+1}),w\big{)}\in\underline{X}_{k}^{\pi}\big{\\}}.$

In Eq. (13)-(16), we start from the dual game winning set $D$ with perfect
information and expand backwards. Set $\underline{Y}_{k+1}$ is computed as the
solution of a local dual game with imperfect information, consisting of the
output points $y$ for which no matter what control input $u$ is picked at $y$,
a violation will occur starting from some $x\sim y$ ($x$ depends on $u$). The
operation $\textbf{EPre}_{y}(\cdot)$ is similar to the environment-controller
predecessor but in the observation space (indicated by subscript $y$). In the
motivating example, $\underline{X}_{0}=\\{5,6\\}$ and
$\underline{Y}_{1}=\\{3,4\\}$. The significance of step (14) is that it does
not require any knowledge of $\pi$ to compute $\textbf{EPre}_{y}(\cdot)$, and
hence the computational complexity is independent of the complexity of $\pi$.
We then pick an output point $\underline{y}_{k+1}$ from $\underline{Y}_{k+1}$
and simulate the closed-loop system under $\pi(\underline{y}_{k+1})$. This
allows us to compute $\underline{X}_{k+1}^{\pi}$, the set of states from which
visiting $\underline{X}_{k}^{\pi}$ can be enforced by the environment. Note
that, to compute the set $\underline{X}_{k+1}^{\pi}$, we only need to know the
decision of $\pi$ at one point $\underline{y}_{k+1}$. This makes sure that,
again, the complexity of the computation does not depend on the complexity of
$\pi$.

As promised at the beginning of this section, for the alternating iteration
process to be correct, the set $\underline{X}_{k}^{\pi}$ should be an inner
approximation of $X_{k}^{\pi}$. This is stated and proved below.

###### Theorem 1.

Let $\underline{X}_{k}^{\pi}$ and $X_{k}^{\pi}$ be the sets computed by
iterations (13)-(16), and iterations (11), (12) respectively, then
$\underline{X}_{k}^{\pi}\subseteq X_{k}^{\pi}$.

###### Proof.

We prove this by induction.

  1. $1^{\circ}$

Base case: by (11) and (13), $\underline{X}_{0}^{\pi}\subseteq D=X_{0}^{\pi}$.

  2. $2^{\circ}$

Assume $\underline{X}_{k}^{\pi}\subseteq X_{k}^{\pi}$, we prove
$\underline{X}_{k+1}^{\pi}\subseteq X_{k+1}^{\pi}$. Define

(17) $\displaystyle XY_{k+1}^{\pi}$ $\displaystyle:=\big{\\{}(x,y)\in X\times
Y\mid x\sim y,\exists w\in W:f\big{(}x,\pi(y),w\big{)}\in
X_{k}^{\pi}\big{\\}},$ (18) $\displaystyle Y_{k+1}^{\pi}$
$\displaystyle:=\big{\\{}y\in Y\mid\exists x\sim y,w\in
W:f\big{(}x,\pi(y),w\big{)}\in X_{k}^{\pi}\big{\\}},$ (19)
$\displaystyle\widetilde{X}_{k+1}^{\pi}$ $\displaystyle:=\big{\\{}x\in
X\,\,\big{|}\,x\sim\underline{y}_{k+1},\exists w\in
W:f\big{(}x,\pi(\underline{y}_{k+1}),w\big{)}\in X_{k}^{\pi}\big{\\}}.$

By definition, $X_{k+1}^{\pi}$ is the projection of $XY_{k+1}^{\pi}$ onto $X$
space, $Y_{k+1}^{\pi}$ is the projection of $XY_{k+1}^{\pi}$ onto $Y$ space,
and $\widetilde{X}_{k+1}^{\pi}$ is the slice of $XY_{k+1}^{\pi}$ at
$y=\underline{y}_{k+1}$ (see Fig. 3). Clearly, we have
$\underline{y}_{k+1}\in\underline{Y}_{k+1}\subseteq Y_{k+1}^{\pi}$, and this
implies $\widetilde{X}_{k+1}^{\pi}\subseteq X_{k+1}^{\pi}$. Note that we also
have $\underline{X}_{k+1}^{\pi}\subseteq\widetilde{X}_{k+1}^{\pi}$ by the
induction hypothesis $\underline{X}_{k}^{\pi}\subseteq X_{k}^{\pi}$. Thus
$\underline{X}_{k+1}^{\pi}\subseteq\widetilde{X}_{k+1}^{\pi}\subseteq
X_{k+1}^{\pi}$, which completes the induction step and the entire proof.

∎

Once the sets $\underline{X}_{k}^{\pi}$ and the observations
$\underline{y}_{k+1}$ are computed, an adversarial scenario
$(x_{0},\textbf{w}_{N-1},\textbf{v}_{N-1})$ can be derived using a forward
expansion procedure:

(20) $\displaystyle x_{0}$ $\displaystyle\in\underline{X}_{N}^{\pi}\cap X_{\rm
init},$ (21) $\displaystyle y_{t}$ $\displaystyle=\underline{y}_{N-t},\ \
v_{t}\text{ is s.t. }g(x_{t},v_{t})=y_{t}\text{ for }t\in[\\![0,N-1]\\!],$
(22) $\displaystyle w_{t}$ $\displaystyle\text{ is s.t.
}f\big{(}x_{t},\pi(y_{t}),w_{t}\big{)}\in\underline{X}_{N-t-1}^{\pi},\ \
x_{t+1}=f\big{(}x_{t},\pi(y_{t}),w_{t}\big{)}\text{ for }t\in[\\![0,N-1]\\!].$

Clearly, $x_{N}\in\underline{X}_{0}^{\pi}\subseteq D$. The full scenario
$(x_{0},\textbf{w}_{T-1},\textbf{v}_{T-1})$ can be completed by Eq. (8), (9)
so that $x_{T}\in X_{\rm unsafe}$, with $v_{N},\dots,v_{T}$ being arbitrarily
picked.

Figure 3. Illustration: proof of Theorem 1.

Note that the proposed algorithm is not complete in that it does not guarantee
to find a falsification scenario even if one exists. Otherwise it will be
equivalent to verification in the sense that a system is verified whenever no
falsifying scenario is found. Such a complete procedure, however, is
computationally hard (e.g., most verification problems with continuous state-
spaces are undecidable (Henzinger and Raskin, 2000)) and is not the point of
the falsification problem. Moreover, it is not clear how to do verification
with unknown components without resorting to statistical techniques.

###  4.2. Computing $\underline{X}_{k}^{\pi}$ and $\underline{y}_{k}$ for
Switched Affine Systems

As pointed out earlier, the complexity of the set computation in the
alternating iteration (13)-(16) is independent of the controller’s complexity.
Hence it is applicable to systems whose open-loop dynamical model $f$ and the
sensor model $g$ have modest complexity. For such systems, sets
$\underline{X}_{k}^{\pi}$, $\underline{Y}_{k}$ can be described and computed
efficiently using e.g., HJB methods (Mitchell et al., 2005), optimization-
based approaches (Lasserre, 2015), interval analysis (Li and Liu, 2017), just
to mention a few. In what follows, we show, for switched affine systems with
linear constraints, how to do the set computations by leveraging the existing
polytope/zonotope computation techniques. Our implementation includes both of
these options. While the polytope-based implementation is faster for 2D and 3D
plant models, the zonotope-based implementation scales better with the
dimension of the state space.

###### Proposition 1.

Let $\Sigma$ be the following switched affine system,

(23) $\displaystyle x_{t+1}$
$\displaystyle=A_{s_{t}}x_{t}+B_{s_{t}}u_{t}+K_{s_{t}}+E_{s_{t}}w_{t},$ (24)
$\displaystyle y_{t}$ $\displaystyle=Cx_{t}+Du_{t}+Fv_{t},$

where $s_{t}$ is a switching control input from a finite set $S$. Suppose that
set $\underline{X}_{k}^{\pi}$ and the continuous control input set $U$ are
polyhedrons, i.e., $\underline{X}_{k}^{\pi}=\\{x\in\mathbb{R}^{n_{x}}\mid
Hx\leq h\\}$, and $U=\text{cvxh}(\mathcal{V}_{u})$ where cvxh denotes the
convex hull and $\mathcal{V}_{u}\subseteq\mathbb{R}^{n_{u}}$ is a finite set
of vertices. Also assume that, at a given state $x$, the (potentially state-
dependent) process noise $w\in W(x):=\\{w\in\mathbb{R}^{n_{w}}\mid
H_{x}x+H_{w}w\leq h_{w}\\}$, and the sensor noise $v\in
V(x):=\\{v\in\mathbb{R}^{n_{v}}\mid G_{x}x+G_{v}v\leq g_{v}\\}$. Then
$\underline{y}_{k+1}\in\underline{Y}_{k+1}$ can be found by solving the linear
program in (29), and the set $\underline{X}_{k+1}^{\pi}$ is the polyhedron in
(36).

(29) $\displaystyle\begin{array}[]{rl}\text{ find
}&\underline{y}_{k+1}\in\mathbb{R}^{n_{y}},\ \ \\{x_{s,u},\ w_{s,u},\
v_{s,u}\\}_{s\in S,u\in\mathcal{V}_{u}}\\\ \text{ s.t. }&\forall s\in
S,u\in\mathcal{V}_{u}:\\\ &H(A_{s}x_{s,u}+B_{s}u+K_{s}+E_{s}w_{s,u})\leq h,\ \
Cx_{s,u}+Du+Fv_{s,u}=\underline{y}_{k+1},\\\ &H_{x}x_{s,u}+H_{w}w_{s,u}\leq
h_{w},\ \ G_{x}x_{s,u}+G_{v}v_{s,u}\leq g_{v}\end{array},$ (36)
$\displaystyle\underline{X}_{k+1}^{\pi}=\textbf{Proj}_{x}\left(\left\\{\left.\begin{array}[]{l}x\in\mathbb{R}^{n_{x}}\\\
w\in\mathbb{R}^{n_{w}}\\\
v\in\mathbb{R}^{n_{v}}\end{array}\right|\begin{array}[]{l}H(A_{s_{k+1}}x+B_{s_{k+1}}u+K_{s_{k+1}}+E_{s_{k+1}}w)\leq
h\\\ Cx+Du_{k+1}+Fv=\underline{y}_{k+1}\\\ H_{x}x+H_{w}w\leq h_{w},\
G_{x}x+G_{v}v\leq g_{v}\\\ \end{array}\right\\}\right).$

In (36), $(s_{k+1},u_{k+1})=\pi(\underline{y}_{k+1})$ and
$\textbf{Proj}_{x}(\mathcal{X})=\\{x\mid\exists z:(x,z)\in\mathcal{X}\\}$ is
the polytope projection from some high-dimensional polytope $\mathcal{X}$.

We implement (29), (36) with MPT3 toolbox (Herceg et al., 2013). Due to the
complexity of the projection operation in (36), we are restricted to plants
with low-dimensional state spaces (i.e., $n_{x}\leq 4$). To handle the cases
where $n_{x}>4$, we use zonotopes to under-approximate the polytopic set
$\underline{X}_{k+1}^{\pi}$.

###### Proposition 2.

Consider a switched affine system $\Sigma$ in (23), (24). Assume that $C=I$,
$A_{s}$ is invertible222This assumption holds when the discrete-time model is
obtained by sampling a continuous-time linear system.  for all $s\in S$, and
that $U=\langle G_{u},c_{u}\rangle$, $W=\langle G_{w},c_{w}\rangle$,
$V=\langle G_{v},c_{v}\rangle$ and $\underline{X}_{k}^{\pi}=\langle
G_{x},c_{x}\rangle$ are zonotopes333$\langle G,c\rangle$ is the generator-
representation of the zonotope $\\{G\theta+c\mid\theta\in[-1,1]^{N}\\}$, where
$G\in\mathbb{R}^{n\times N}$, $c\in\mathbb{R}^{n}$.. Then
$\underline{y}_{k+1}$ is a feasible solution of the linear program in (41),
and $\underline{X}_{k+1}^{\pi}$ is the intersection of two zonotopes in (42).

(41) $\displaystyle\begin{array}[]{rl}\text{ find
}&\underline{y}_{k+1}\in\mathbb{R}^{n_{y}},\ \ \\{x_{s,u},\ \xi_{s,u},\
w_{s,u},\ \omega_{s,u},\ v_{s,u},\nu_{s,u},\ \\}_{s\in
S,u\in\mathcal{V}_{u}}\\\ \text{ s.t. }&\forall s\in S,u\in\mathcal{V}_{u}:\\\
&A_{s}x_{s,u}+B_{s}u+K_{s}+E_{s}w_{s,u}=G_{x}\xi_{s,u}+c_{x},\ \
Cx_{s,u}+Du+Fv_{s,u}=\underline{y}_{k+1},\\\
&w_{s,u}=G_{w}\omega_{s,u}+c_{w},\ \ v_{s,u}=G_{v}\nu_{s,u}+c_{v}\end{array},$
(42)
$\displaystyle\underline{X}_{k+1}^{\pi}=A_{s_{k+1}}^{-1}(\underline{X}_{k}^{\pi}\oplus-
E_{s_{k+1}}W-B_{s_{k+1}}u_{k+1}-K_{s_{k+1}})\cap(\underline{y}_{k+1}\oplus-FV-
Du_{k+1}).$

In (42), $(s_{k+1},u_{k+1})=\pi(\underline{y}_{k+1})$, $\langle
G_{1},c_{1}\rangle\oplus\langle
G_{1},c_{1}\rangle:=\langle[G_{1},G_{2}],c_{1}+c_{2}\rangle$ and $H\langle
G,c\rangle:=\langle HG,Hc\rangle$.

The main challenge in computing the set $\underline{X}_{k+1}^{\pi}$ using
Proposition 2 is the intersection operation in (42). In fact, the intersection
of two zonotopes is not necessarily a zonotope. However, we can find a
zonotopic under-approximation of the intersection by solving a linear program.
That is, the intersection of two zonotopes $\langle G_{1},c_{1}\rangle$,
$\langle G_{2},c_{2}\rangle$ can be under-estimated by
$\langle\Lambda[G_{1},G_{2}],c\rangle$, where the diagonal matrix
$\Lambda=\textbf{diag}(\\{\lambda_{i}\\}_{i})$ is the solution of the
following optimization problem:

(47) $\displaystyle\begin{array}[]{rl}\max_{\lambda}&\sum_{i}\lambda_{i}\\\
\text{s.t. }&\langle\Lambda[G_{1},G_{2}],c\rangle\subseteq\langle
G_{1},c_{1}\rangle\\\ &\langle\Lambda[G_{1},G_{2}],c\rangle\subseteq\langle
G_{2},c_{2}\rangle\\\ &\lambda_{i}\geq 0,\forall i\end{array}.$

The zonotope containment constraints in (47) can be reformulated into a set of
linear constraints using the technique developed in (Sadraddini and Tedrake,
2019). Therefore (47) is equivalent to a linear program. The obtained zonotope
$\langle\Lambda[G_{1},G_{2}],c\rangle$ is an inner approximation of
$\underline{X}_{k+1}^{\pi}$. Moreover, for low dimensional systems (i.e.,
$n_{x}=2$ or $3$), solving the above optimization problem is slower than
computing the polytopic $\underline{X}_{k+1}^{\pi}$ as in Proposition 1.
However, the zonotope implementation scales better with $n_{x}$ and can easily
go beyond what can be solve via the off-the-shelf polytope computation tools.
For example, the zonotope-based implementation can handle systems with
$n_{x}=10$.

###  4.3. Improving Completeness

We provide a heuristic and a refinement technique to improve the completeness
of the proposed alternating backward expansion (13)-(16).

Selection of the queried point $\underline{y}_{k+1}$. The completeness of our
approach can be improved by a better selection of the observation point
$\underline{y}_{k+1}$ in Eq. (14). One natural heuristic is to pick
$\underline{y}_{k+1}\in\underline{Y}_{k+1}$ that minimizes the distance from
the set $\\{x\mid x\sim\underline{y}_{k+1}\\}$ to the initial set $X_{\rm
init}$. However, this usually leads to set $\underline{X}_{k+1}^{\pi}$ having
zero measure and $\underline{Y}_{k+2}=\emptyset$. If such situation occurs
before $\underline{X}_{k}^{\pi}$ reaches $X_{\rm init}$, we may end up with an
unsatisfactory falsifying trajectory that starts too close to the unsafe set,
and the alternating backward expansion is said incomplete if falsifying
trajectories starting from $X_{\rm init}$ exist but the algorithm does not
find one due to a bad selection of $\underline{y}_{k+1}$. Hence there is a
trade-off between picking a $\underline{y}_{k+1}$ that leads to a state closer
to the initial set $X_{\rm init}$, and picking a $\underline{y}_{k+1}$ that
leads to a larger set $\underline{X}_{k+1}^{\pi}$. Here we use the following
simple heuristic

(48) $\displaystyle\underline{y}_{k+1}=\beta y_{\rm close}+(1-\beta)y_{\rm
center},$

where $y_{\rm close}$ minimizes the Euclidean distance between set $\\{x\mid
x\sim y_{\rm close}\\}$ and $X_{\rm init}$, $y_{\rm center}$ is an
approximated center of the polytopic set $\underline{Y}_{k+1}$, and
$\beta\in[0,1]$ is a tuning factor. In this paper, we use $\beta=0.6$ for all
continuous-state systems.

Refining the control set $U$. Another reason for set $\underline{Y}_{k+1}$
becoming empty before the falsifying trajectory reaches $X_{\rm init}$ during
backward expansion is the control input set $U$ being too large. In this case,
it is hard for an output $y$ to satisfy the condition in the definition of
$\underline{Y}_{k+1}$ (see Eq. (14)) for all $u\in U$. However, for the
alternating backward expansion to be valid, it is sufficient for $y$ to
satisfy the condition only for $u=\pi(y)$ (though this requires the knowledge
of $\pi$ and is undesired). One way to mitigate this problem is to refine the
control input space $U$ into finitely many smaller sets
$\\{U_{i}\\}_{i=1}^{n}$ and replace $\underline{Y}_{k+1}$ by
$\underline{Y}_{k+1,i}:=\textbf{EPre}_{y}(\underline{X}_{k}^{\pi}\mid
U_{i})=\\{y\in Y\mid\forall u\in U_{i}:\exists x\sim y,w\in
W:f\big{(}x,\pi(y),w\big{)}\in\underline{X}_{k}^{\pi}\\}$. The following
proposition can be easily proved under some continuity assumptions and
suggests that a nonempty $\underline{Y}_{k+1,i}$ can be always found if the
partition of $U$ is fine enough.

###### Proposition 3.

Suppose that $X,U$ are normed spaces and the mapping $f$ is continuous in $u$,
and that there exists $y\in Y$, $x\sim y$ and $w\in W$ such that
$f\big{(}x,\pi(y),w\big{)}$ is in the interior of $\underline{X}_{k}^{\pi}$.
There exists $\delta>0$ such that any $\delta$-fine partition
$\\{U_{i}\\}_{i=1}^{n}$ of set $U$ (i.e., $U=\bigcup_{i=1}^{n}U_{i}$ and for
any $u,u^{\prime}\in U_{i}:\|u-u^{\prime}\|\leq\delta$) contains a piece
$U_{i^{\prime}}$ s.t.
$\underline{Y}_{k+1,i^{\prime}}=\textbf{EPre}_{y}(\underline{X}_{k}^{\pi}\mid
U_{i^{\prime}})\neq\emptyset$.

###### Proof.

Let $y\in Y$, $x\sim y$ and $w\in W$ such that $f\big{(}x,\pi(y),w\big{)}$ is
in the interior of $\underline{X}_{k}^{\pi}$, i.e.,
$\\{x^{\prime}\mid\|x^{\prime}-f(x,\pi(y),w)\|\leq\epsilon\\}\subseteq\underline{X}_{k}^{\pi}$
for some $\epsilon>0$. Since $f$ is continuous in $u$, there exists $\delta$
s.t.
$\|u-\pi(y)\|\leq\delta\Rightarrow\|f(x,u,w)-f\big{(}x,\pi(y),w\big{)}\|\leq\epsilon$.
Hence for all $u$ such that $\|u-\pi(y)\|\leq\delta$,
$f(x,u,w)\in\underline{X}_{k}^{\pi}$. Let $\\{U_{i}\\}_{i=1}^{n}$ be any
$\delta$-fine partition of set $U$ and let $\pi(y)\in U_{i^{\prime}}$. One
have $\|u-\pi(y)\|\leq\delta$ for all $u\in U_{i^{\prime}}$. This implies that
$y\in\underline{Y}_{k+1,i^{\prime}}$ and thus
$\underline{Y}_{k+1,i^{\prime}}\neq\emptyset$. ∎

###  4.4. Overall Algorithm

Algorithm 1 summarizes our falsification procedure, integrating the
alternating iteration process, the query heuristic and the control space
refinement.

Algorithm 1
$(x_{0},\textbf{w}_{T-1},\textbf{v}_{T-1})={\textbf{FindAdversarialScenario}}(\Sigma,\pi,X_{\rm
init},X_{\rm safe},k_{\rm max},{\color[rgb]{0,0,0}\delta})$

1: Perform iteration (5), (6) to get $\\{\underline{D}_{k}\\}_{k=0}^{K}$,
where $\underline{D}_{k}\subseteq D_{k}$ ($\underline{D}_{k}\neq D_{k}$
because e.g., the union operation in Eq. (6) is dropped to simplify the
computation)

2: Pick $\underline{X}_{0}^{\pi}\subseteq\bigcup_{k=1}^{K}\underline{D}_{k}$,
set $k=0$

3: while $\underline{X}_{k}^{\pi}\cap X_{\rm init}=\emptyset$ and $k\leq
k_{\rm max}$ do

4: $\mathcal{U}=\\{U\\}$

5: do pick $U^{\prime}\in\mathcal{U}$ , and
$\underline{y}_{k+1}\in\textbf{EPre}_{y}(\underline{X}_{k}^{\pi}\mid
U^{\prime})$ using the heuristic in Eq. (48)

6: if $\exists u,u^{\prime}\in U^{\prime}:\|u-u^{\prime}\|>\delta$

7: split $U^{\prime}$ into $U_{1}$ and $U_{2}$,
$\mathcal{U}=(\mathcal{U}\setminus\\{U^{\prime}\\})\cap\\{U_{1},U_{2}\\}$

8: endif

9: while ($\underline{y}_{k+1}$ does not exist or
$\pi(\underline{y}_{k+1})\notin U^{\prime}$) and $\mathcal{U}\neq\emptyset$

10:
$\underline{X}_{k+1}^{\pi}=\textbf{Pre}^{\pi}_{\underline{y}_{k+1}}(\underline{X}_{k}^{\pi})$

11: update $k=k+1$

12: end while

13: Set $N=k$, generate $\textbf{x}_{N},\textbf{w}_{N-1},\textbf{v}_{N-1}$
using Eq. (20)-(22)

14: From $x_{N}$, complete $\textbf{x}_{T},\textbf{w}_{T-1},\textbf{v}_{T-1}$
using Eq. (8), (9), with “$\overline{\pi}(x_{t})$” replaced by
$\pi\big{(}g(x_{t},v_{t})\big{)}$ where $v_{N},\dots,v_{T-1}$ are picked
randomly.

15: return $x_{0},\textbf{w}_{T-1},\textbf{v}_{T-1}$

We briefly explain Algorithm 1. Line 4-9 corresponds to the refinement
technique introduced in Section 4.3. While in some applications, the control
set $U$ may be physically constrained and it is possible to find
$\underline{y}_{k+1}\in\textbf{EPre}_{y}(\underline{X}_{k}^{\pi}\mid U)$, the
refinement is important when $U$ is large (or even unconstrained). Algorithm 1
handles the latter case by splitting the control set $U$, saving different
pieces in a queue $\mathcal{U}$ and finding
$\underline{y}_{k+1}\in\textbf{EPre}_{y}(\underline{X}_{k}^{\pi}\mid
U^{\prime})$ for each $U^{\prime}\in\mathcal{U}$. By Proposition 3, under some
continuity assumptions on $f$, it is possible to find $\underline{y}_{k+1}$
when the partition of $U$ is fine enough (quantified by the input parameter
$\delta$). An example where the refinement is necessary to find a satisfying
adversarial scenario (i.e., $x_{0}\in X_{\rm init}$) can be found in Section 6
(Example 2). Note that, after splitting $U$, there might be multiple
$\underline{y}_{k+1}$ induced from different parts of $U$, from where the
expansion can proceed. In that case, it is possible to introduce a
backtracking mechanism into our framework to manage the branching. This
increases the computational complexity but can improve the completeness of the
algorithm, especially when the “greedy” heuristic in (48) does not lead the
search towards initial set $X_{\rm init}$ globally.

In Algorithm 1, the input parameters $k_{\rm max}$, $\delta$ can be adapted to
different problems. In our examples, $k^{\rm max}$ is never reached and
$\delta$ is only used in Example 2. There are also several places where
different heuristics can be used. One is the choice of
$\underline{X}_{0}^{\pi}$ where the backward expansion starts. The set
$\underline{X}_{0}^{\pi}$ should be large enough and closer to the initial
set. In all of our examples, we pick
$\underline{X}_{0}^{\pi}=\underline{D}_{K}$. However, in most of our examples,
we find comparable results by picking $\underline{X}_{0}^{\pi}=X_{\rm
unsafe}$. One can also adopt different heuristics for picking multiple
$\underline{y}_{k+1}$’s. This will lead to branching in the backward expansion
and the backtracking like ideas can be used to trace different branches.

##  5\. Extensions

The main development so far is an approach to falsify systems with relatively
simple open-loop dynamics $f$, sensor model $g$, but with potentially
complicated or even unknown static controller $\pi$, against invariance
requirements. Here, we further show that our approach is extensible to i)
systems whose dynamic model $f$ is complex but can be approximated by an
abstraction with a simpler expression, ii) vision-based control systems, whose
dynamics model $f$ is also simple but the sensor model $g$ and the controller
$\pi$ are both complicated/unknown; and iii) against certain safety
requirements expressed in a fragment of temporal logic. Each extension is
illustrated with an example in Section 6.

###  5.1. Incorporating Model Mismatch

Since a simple plant model is assumed in our setting, it is important to
incorporate the mismatch between our simple model and a high fidelity model,
or even the real system. Our goal is to generate an adversarial scenario for
the real system by falsifying the simple model, which serves as an abstraction
of the real system. To this end, we consider simple models parametrized by
model uncertainties $p$ and $q$ (their distinction will be discussed later).
These model uncertainties $p$, $q$ are different from the disturbance $w$ and
the noise $v$ that are picked adversarially in the falsification. Instead, $p$
and $q$ need to be picked in a way to respect the physics. This suggests
another player called the neutral player selecting $p$, $q$ against the
adversarial environment and independently of the controller. Let
$x_{t+1}=f(x_{t},u_{t},w_{t})$ be the concrete dynamics and let
$x_{t+1}=\widehat{f}_{p_{t},q_{t}}(x_{t},u_{t},w_{t})$, where $p_{t}\in P$ and
$q_{t}\in Q$, be an abstraction that has a simpler expression than $f$. The
variable $p_{t}$ captures the terms in $f$ that can be determined after
$x_{t}$ and $u_{t}$ are given, and these terms are known but hard to
incorporate in backward reachable set computation. Whereas $q_{t}$ captures
the terms in $f$ that can be determined only after $w_{t}$ is given. For
example,
$f(x_{t},u_{t},w_{t})=x_{t}+u_{t}+w_{t}+\log(x_{t})+u_{t}^{2}+u_{t}\cos(w_{t})$
and
$\widehat{f}_{p_{t},q_{t}}(x_{t},u_{t},w_{t})=x_{t}+w_{t}+u_{t}+p_{t}+q_{t}$
with $p_{t}\in P:=\\{\log(x)+u^{2}\mid x\in X,u\in U\\}$ and $q_{t}\in
Q:=\\{u\cos(w)\mid w\in W,u\in U\\}$. To construct an adversarial scenario for
the concrete system by falsifying the abstraction, we require the following
condition to hold for $f$ and $\widehat{f}_{p,q}$:

(49) $\displaystyle\forall x\in X,u\in U:\exists p\in P:\forall w\in W:\exists
q\in Q:f(x,u,w)=\widehat{f}_{p,q}(x,u,w).$

The reason for treating $p$ and $q$ differently roots in the order of play in
the game, i.e., the adversarial environment plays after the controller. When
the adversarial environment is choosing $w$, the value of $p$ is already
determined by $x$ and $u$, whereas the value of $q$ remains undetermined.
Therefore the choice of $w$ may depend on $p$ but not $q$. For instance, $p$
can represent known nonlinearities that are abstracted out in backward
reachability but whose value can be easily computed given $x$ and $u$, whereas
$q$ represents unknown but bounded model uncertainties. In each round of the
game, the state is at $x_{t}$ and the adversarial environment picks $v_{t}$
that leads to $y_{t}=g(x_{t},v_{t})$ and $u_{t}=\pi(y_{t})$. Next the neutral
player picks $p_{t}$ so that

(50) $\displaystyle\forall w\in W:\exists q\in
Q:f(x_{t},u_{t},w)=\widehat{f}_{p_{t},q}(x_{t},u_{t},w).$

We know such $p_{t}$ exists by (49). In the above example, the neutral player
picks $p_{t}=\log(x_{t})+u_{t}^{2}$. Then the adversarial environment picks
$w_{t}$ according to the value of $x_{t}$, $u_{t}$ and $p_{t}$. Finally the
neutral player picks $q_{t}$ so that
$f(x_{t},u_{t},w_{t})=\widehat{f}_{p_{t},q_{t}}(x_{t},u_{t},w_{t})$. In the
above example, the neutral player picks $q_{t}=u_{t}\cos(w_{t})$. The
alternating iteration is modified by replacing (14), (16) by

(51) $\displaystyle\underline{Y}_{k+1}$ $\displaystyle=\\{y\in Y\,|\,\forall
u\in U:\exists x\sim y:\forall p\in P:\exists w\in W:\forall q\in
Q:\widehat{f}_{p,q}(x,u,w)\in\underline{X}_{k}^{\pi}\\},$ (52)
$\displaystyle\underline{X}_{k+1}^{\pi}$ $\displaystyle=\big{\\{}x\in
X\big{|}x\sim\underline{y}_{k+1},\forall p\in P:\exists w\in W:\forall q\in
Q:\widehat{f}_{p,q}\big{(}x,\pi(\underline{y}_{k+1}),w\big{)}\in\underline{X}_{k}^{\pi}\big{\\}}.$

The following proposition says that an adversarial scenario for the
abstraction also falsifies the concrete system.

###### Proposition 4.

Replace (14) by (51), and (16) by (52), and let $X_{k}^{\pi}$ be defined by
(12) with the concrete dynamics. We have $\underline{X}_{k}^{\pi}\subseteq
X_{k}^{\pi}$.

To prove Proposition 4, we first introduce a useful lemma.

###### Lemma 1.

Let $x^{\prime}\in X$, $u^{\prime}\in U$ and $X^{\prime}\subseteq X$ be
arbitrary. Suppose that (49) holds, i.e.,

(53) $\displaystyle\exists p^{\prime}\in P:\forall w\in W:\exists q\in
Q:f(x^{\prime},u^{\prime},w)=\widehat{f}_{p^{\prime},q}(x^{\prime},u^{\prime},w),$

and that

(54) $\displaystyle\forall p\in P:\exists w\in W:\forall q\in
Q:\widehat{f}_{p,q}(x^{\prime},u^{\prime},w)\in X^{\prime}.$

Then there exists $w^{\prime}\in W:f(x^{\prime},u^{\prime},w^{\prime})\in
X^{\prime}$.

###### Proof.

Let $p=p^{\prime}$ in (54), we have

(55) $\displaystyle\exists w^{\prime}\in W:\forall q\in
Q:\widehat{f}_{p^{\prime},q}(x^{\prime},u^{\prime},w^{\prime})\in X^{\prime}.$

Combining (53) with (55) yields

(56) $\displaystyle\exists q^{\prime}\in
Q:f(x^{\prime},u^{\prime},w^{\prime})=\widehat{f}_{p^{\prime},q^{\prime}}(x^{\prime},u^{\prime},w^{\prime}).$

Eq. (55) gives
$\widehat{f}_{p^{\prime},q^{\prime}}(x^{\prime},u^{\prime},w^{\prime})\in
X^{\prime}$, which implies that $f(x^{\prime},u^{\prime},w^{\prime})\in
X^{\prime}$ by (56). ∎

Proposition 4 is proved below.

###### Proof.

We will define $XY_{k+1}^{\pi}$, $Y_{k+1}^{\pi}$ and
$\widetilde{X}_{k+1}^{\pi}$ by (17)-(19). It remains to show that, given
$\underline{X}_{k}^{\pi}\subseteq X_{k}^{\pi}$, i) the newly defined
$\underline{Y}_{k+1}\subseteq Y_{k+1}^{\pi}$ and ii) the newly defined
$\underline{X}_{k+1}^{\pi}\subseteq\widetilde{X}_{k+1}^{\pi}$. Then
Proposition 4 follows from the same induction that proves Theorem 1. To prove
i), let $y^{\prime}\in\underline{Y}_{k+1}$ and $u^{\prime}=\pi(y^{\prime})$.
By the new definition of $\underline{Y}_{k+1}$, we know that there exists
$x^{\prime}\sim y^{\prime}$ such that Eq. (54) holds with
$X^{\prime}=\underline{X}_{k}^{\pi}$. By Lemma 1, there exists $w^{\prime}\in
W$ such that $f(x^{\prime},u^{\prime},w^{\prime})\in
X^{\prime}=\underline{X}_{k}^{\pi}\subseteq X_{k}^{\pi}$, which implies that
$y^{\prime}\in Y_{k+1}^{\pi}$. To prove ii), let
$x^{\prime}\in\underline{X}_{k+1}^{\pi}$ be arbitrary and let
$u^{\prime}=\pi(\underline{y}_{k+1})$. By the new definition of
$\underline{X}_{k+1}^{\pi}$, we know that $x^{\prime}\sim\underline{y}_{k+1}$
and (54) holds with $X^{\prime}=\underline{X}_{k}^{\pi}$. Again, by Lemma 1,
there exists $w^{\prime}$ such that $f(x^{\prime},u^{\prime},w^{\prime})\in
X^{\prime}=\underline{X}_{k}^{\pi}\subseteq X_{k}^{\pi}$. That is,
$x^{\prime}\in\widetilde{X}_{k+1}^{\pi}$. ∎

For switched affine systems in Eq. (23), (24) whose $B_{s}$ and $K_{s}$
matrices are linear in $p\in P=\text{cvxh}(\mathcal{V}_{P})$ and $q\in
Q=\text{cvxh}(\mathcal{V}_{Q})$, the updated iteration (51), (51) still lead
to polytopic computations similar to Eq. (29), (36). Then, in the forward
expansion phase (Eq. (22)), $p_{t}$ is picked so that Eq. (49) holds, and then
$w_{t}$ is picked so that
$\widehat{f}_{p_{t},q}\big{(}x_{t},\pi(y_{t}),w_{t}\big{)}\in\underline{X}^{\pi}_{N-t-1}$
for all $q\in Q$, which is feasible by (51), (52). Finally, the system evolves
to the new state $x_{t+1}=f(x_{t},u_{t},w_{t})$.

###  5.2. Falsifying Vision-Based Controllers

Figure 4. Block diagram of vision-in-the-loop systems with noisy images
(left), and with perturbation in a low dimensional semantic space (right).

The block diagram of a typical vision-in-the-loop system is shown in Figure 4
(left). The main challenge of falsifying such systems is twofold. First, since
$y$ represents an image, the dimension of the output space is too high
(Balakrishnan et al., 2019), (Dreossi et al., 2019a). Second, the camera is
hard to model formally and hence it is impossible to perform the proposed
alternating iteration (particularly Eq. (26), (28)). To tackle these two
challenges, we proceed as in (Dreossi et al., 2019a) and restrict the search
to a low dimensional semantic space. To this end, we consider the system shown
in Figure 4 (right) instead, where the complicated vision-based controller and
the camera model are viewed as one block (i.e., the $\pi$-block), while the
sensor noise is captured by a simple $\widehat{g}$-block that perturbs the
real state $x$ (e.g., $y\in\widehat{g}(x)=x+\widehat{v}$, where
$\widehat{v}\in\widehat{V}$ is the admissible perturbation). Here, the output
$y$ has the same dimension as $x$ and the map $g$ is simple, and is hence
amiable to our approach. The scheme can be interpreted as “attacking” the
system in Figure 4 (left) by replacing the true image by an imitating one that
is taken at a perturbed state, and the perturbation can found by falsifying
the system in Figure 4 (right).

The following proposition validates our approach by showing that, under
certain Lipschiz assumption on the camera model444The real cameras are rarely
Lipschiz continuous in the state, but such assumptions are used in analysis of
perception-based controllers, e.g., see (Dean et al., 2020). , the falsifying
images obtained by semantic space perturbation (i.e., falsify the system with
$\widehat{g}$) can be generated by the real camera model $g$. This means we
can find an adversarial scenario for the real vision-in-the-loop system by
falsifying $\widehat{g}$ in the loop instead.

###### Proposition 5.

Let the state space $X$ be a normed space and $g(x,v)=c(x)+v$, where
$c:X\rightarrow\mathbb{R}^{n_{\rm img}}$ models a camera that maps a state to
an image and $V\subseteq\mathbb{R}^{n_{\rm img}}$ is a set of additive noise
in the image space. Assume that $c$ is globally Lipschiz (i.e., $\exists L\geq
0:\forall x,x^{\prime}\in X:\|c(x)-c(x^{\prime})\|\leq L\|x-x^{\prime}\|$) and
that the origin is in the interior of $V$. Define
$\widehat{g}(x,\widehat{v}):=x+\widehat{v}$. There exists
$\widehat{V}\subseteq X$ such that for all $x$, any image generated by
$\widehat{g}$ can be also generated by $g$ under some noise $v$, i.e.,
$\big{\\{}c\big{(}\widehat{g}(x,\widehat{v})\big{)}\mid\widehat{v}\in\widehat{V}\big{\\}}\subseteq\\{g(x,v)\mid
v\in V\\}$.

###### Proof.

Since $V$ contains the origin, there exists $\epsilon$ such that
$\\{v\in\mathbb{R}^{n_{\rm img}}\mid\|v\|\leq\epsilon\\}\subseteq V$. Define
$\widehat{V}=\\{\widehat{v}\in
X\mid\|\widehat{v}\|\leq\tfrac{\epsilon}{L}\\}$, and let $x\in X$ be
arbitrary. We have

$\displaystyle\big{\\{}c\big{(}\widehat{g}(x,\widehat{v})\big{)}\mid\widehat{v}\in\widehat{V}\big{\\}}=\\{c(x+\widehat{v})\mid\|\widehat{v}\|\leq\tfrac{\epsilon}{L}\\}=\\{c(x^{\prime})\mid\|x^{\prime}-x\|\leq\tfrac{\epsilon}{L}\\}$
(57) $\displaystyle\subseteq$
$\displaystyle\\{c(x^{\prime})\mid\|c(x^{\prime})-c(x)\|\leq\epsilon\\}=\\{c(x)+v\mid\|v\|\leq\epsilon\\}\subseteq\\{g(x,v)\mid
v\in V\\}.$

∎

An example with an end-to-end controller can be found in Section 6 (Example
5).

###  5.3. Falsification against Finite-Time Reach-Avoid Specification

Our approach can be extended to falsify systems against finite-time reach-
avoid specifications defined by the following signal temporal logic (STL)
formula

(58) $\displaystyle\Box(x\in X_{\rm safe})\wedge\Diamond_{[\\![0,t_{\rm
max}]\\!]}(x\in X_{\rm target}),$

where $\Box$ and $\Diamond$ are temporal operators “always” and “eventually”,
and $X_{\rm target}$ is a set of target states that we wish to reach at some
time $t\in[\\![0,t_{\rm max}]\\!]$. For the detailed semantics of STL, we
refer the readers to (Donzé and Maler, 2010). Eq. (58) specifies a safety
property, i.e., any violation of the property occurs in finite time. To
falsify a system against specification (58), we construct the following system
with an augmenting state $z$ that captures the timing dynamics:

(59) $\displaystyle x_{t+1}=f(x_{t},u_{t},w_{t}),\ \ z_{t+1}=z_{t}+1.$

The falsification problem can be converted to the one that has already been
solved in Section 4 in the $(x,z)$-space, with the initial set $\Xi_{\rm
init}:=X_{\rm init}\times\\{0\\}$ and unsafe set $\Xi_{\rm unsafe}=\Xi_{\rm
unsafe}^{1}\cup\Xi_{\rm unsafe}^{2}$, where $\Xi_{\rm unsafe}^{1}:=X_{\rm
unsafe}\times[\\![0,\infty]\\!]$ corresponds to violation of state invariance,
and $\Xi_{\rm unsafe}^{2}:=(X\setminus X_{\rm target})\times[\\![t_{\rm
max},\infty]\\!]$ corresponds to missing the deadline of reaching the target
set. To apply the proposed alternating backward expansion algorithm, we start
from $\Xi_{\rm unsafe}^{1}$ and $\Xi_{\rm unsafe}^{2}$ separately. In
particular, when expanding from $\Xi_{\rm unsafe}^{2}$ backwards, we also
restrict $x\in X\setminus X_{\rm target}$ so that, in the falsifying
trajectory, the target set is never visited before $z=t_{\rm max}$. An example
can be found in Section 6 (Example 6).

##  6\. Examples and Evaluations

We present multiple examples to illustrate the efficacy of our approach and
its extensions. The computation time for these examples are reported. We also
evaluate the approach against randomly generated problem instances.

###### Example 1.

Consider a 2D discrete-time linear system in the form of Eq. (23), (24) (no
switching input $s$), with $A=E=C=F=I_{2}$, $B=[1\ 0]^{\top}$, $D=[0\
0]^{\top}$ and $K=[0\ -1]^{\top}$. The control set $U=[-1.2,1.2]$, the noise
set $V=[-1,1]\times[-0.1,0.1]$ and the disturbance set
$W=\\{w\in\mathbb{R}^{2}\mid\|w\|_{1}\leq 0.2\\}$. The state moves downwards
and the goal is to avoid the unsafe set $X_{\rm unsafe}=[3,17]\times[0,3]$
from the initial set $X_{\rm init}=[0,20]\times[17,20]$. We falsify the
following four controllers whose expressions are unknown to the algorithm:

$\displaystyle\pi_{1}(y)$ $\displaystyle=\begin{cases}-1.2&\text{ if
}y\in[0,10]\times[0,20]\\\ 1.2&\text{ if }y\in(10,20]\times[0,20]\end{cases},\
\ \ \ \ \ \pi_{2}(y)=\begin{cases}-1.2&\text{ if }y^{2}>y^{1}\\\ 1.2&\text{
otherwise }\end{cases},$ (63) $\displaystyle\pi_{3}(y)$
$\displaystyle=\begin{cases}-1.2&\text{ if }(y^{2}\leq 15-y^{1}\wedge
y^{2}\geq y^{1})\vee y^{1}\leq 10\\\ 1.2&\text{ otherwise }\end{cases},\ \
\begin{array}[]{c}\pi_{\rm NN}:\\\ \text{feedforward }\\\ \text{neural
net}\end{array}.$

where $y^{1}$, $y^{2}$ are the horizontal and vertical coordinates of $y$
respectively. The perfect information dual winning set is inner approximated
by $\bigcup_{k=1}\underline{D}_{k}$ (purple) where $\underline{D}_{k}$ is the
polytopic set computed by the backward expansion algorithm in Eq. (5), (6) by
ignoring the union operation. We then start the alternating backward expansion
with $\underline{X}_{0}^{\pi}=\underline{D}_{M}\subseteq D$ where
$M=\max\\{k\mid\underline{D}_{k}\neq\emptyset\\}$. Fig. 5 shows the obtained
sets (upper) and the induced falsification runs (lower). The sets
$\underline{X}_{k}^{\pi}$ (gray solid), $\underline{Y}_{k}^{\pi}$ (blue
transparent) are polytopes. We obtain different falsification trajectories
$\textbf{x}_{T}$ (black solid) and output sequences $\textbf{y}_{T}$ (blue
dotted), specific to each controller by running the same algorithm blindly.
The controllers are only sampled along the output sequences $\textbf{y}_{T}$.
$\dagger$

Figure 5. Example 1, falsification under controller $\pi_{1}$ (1st column),
$\pi_{2}$ (2nd column), $\pi_{3}$ (3rd column) and $\pi_{\rm NN}$ (4th
column).

One notable and interesting phenomenon is that the controller-specific
adversarial scenarios where the imperfect information plays a key role usually
occur near the “decision boundary” of the controller, where a discontinuous
decision is made. In Example 1, to cross the obstacle $X_{\rm unsafe}$, a
controller needs to decide to go either left or right. In a typical
adversarial scenario, the true state is on one side but is also very close to
the decision boundary, while the sensor noise makes the controller mistakenly
believe that the state is on the other side and the “opposite” control action
should be taken. This results in chattering behavior along the decision
boundary until the state hits the dual winning set $D$, from where safety
violation is assured by the adversarial process noise only. To summarize, such
scenarios can be found at places where the closed-loop system’s vector field
is discontinuous and these scenarios are hence controller-specific. Our
approach provides a way to detect such critical cases without knowing the
explicit expression of the controllers.

Note that such decision boundary is in general inevitable given static
controllers and an operational domain that is not simply connected. For
example, it is pointed out in (Sontag, 1999) that the region of attraction of
an asymptotically stable equilibrium cannot have holes if the closed-loop
system’s vector field is continuous. Therefore, the operational domain of a
stabilizing controller having holes (i.e., $X_{\rm unsafe}$) will imply
discontinuous closed-loop dynamics, and hence the existence of a “decision
boundary”.

###### Example 2.

(Section 4.3) We provide an example where the control space refinement is
necessary to falsify the system. The system is in the form of Eq. (23), (24)
(no switching input $s$), with

(70) $\displaystyle A=\left[\begin{array}[]{cc}0.9745&0.2132\\\
0.002547&1.151\\\ \end{array}\right],\ \ B=\left[\begin{array}[]{c}0.01959\\\
0.1961\end{array}\right],\ \ E=\left[\begin{array}[]{c}0.01959\\\
-0.04509\end{array}\right],$

$C=F=I_{2}$, $D=K=[0\ 0]^{\top}$. The control set $U=[-1.5,1.5]$, the noise
set $V=[-0.1,0.1]\times[-0.1,0.1]$ and the disturbance set $W=[-0.2,0.2]$. The
unsafe set $X_{\rm unsafe}=[1,2]\times[-0.5,0.5]$ and the initial set $X_{\rm
init}=[-0.15,0.15]\times[-0.15,0.15]$. The system is stabilized by an LQR
controller with saturation $\pi_{\rm LQR}=\min\\{\max\\{[-1\
-1]x,-1.5\\},1.5\\}$ (unknown to the falsification algorithm). Fig. 6 shows
the falsifying trajectory (left) found by Algorithm 1. This falsifying
scenario is nontrivial because the uncertainty profiles (right) need to follow
a special periodic-pattern. If the control space refinement were not used, the
alternating iteration would terminate prematurely before reaching the initial
set backwardly. Essentially, $\pi_{\rm LQR}$ is falsified because it is not
using the full capability allowed by the control set $U=[-1.5,1.5]$. $\dagger$

Figure 6. Example 2: falsifying trajectory (left), disturbance and noise
profiles (right).

###### Example 3.

We apply our approach to the following buck converter system (adopted from
(Yang et al., 2019)).

Figure 7. Example 3.

The system’s states are the current and the voltage of the converter. The
system has two discrete inputs only, i.e., $s\in\\{1,2\\}$, corresponding to
the converter’s dynamics regularized with two different on-off sequences.
Particularly,

(79) $\displaystyle A_{1}=\left[\begin{array}[]{cc}0.9999&-0.04980\\\
0.003984&0.9919\\\ \end{array}\right],K_{1}=\left[\begin{array}[]{c}1.250\\\
0.002618\end{array}\right],A_{2}=\left[\begin{array}[]{cc}0.9992&-0.1360\\\
0.01088&0.9775\\\ \end{array}\right],K_{2}=\left[\begin{array}[]{c}1.250\\\
0.006948\end{array}\right],$

and $E_{1}=E_{2}=C=F=I_{2}$, $B=[0\ 0]^{\top}$. The noise set
$V=[-1,1]\times[-1,1]$ and the disturbance set $W=[-0.2,0.2]\times[-0.2,0.2]$.
The initial set $X_{\rm init}=[0,2]\times[0,1]$. The unsafe set $X_{\rm
unsafe}=[30,50]\times[28,30]$ corresponds to the overshoot in the converter’s
voltage. The control objective is to reach a target voltage level ($25$ V) and
stay close indefinitely. To this end, the following rule-based switching
controller is used:

(80) $\displaystyle\pi(y)=\begin{cases}2&\text{ if
}\big{(}(\widehat{y}^{2}\leq
23.5)\wedge(-23\widehat{y}^{1}+14\widehat{y}^{2}\leq-989)\big{)}\vee\big{(}(\widehat{y}^{2}>23.5)\wedge(\widehat{y}^{1}\geq
54)\big{)}\\\ 1&\text{ otherwise }\\\ \end{cases}$

where $\widehat{y}=\min\big{\\{}\max\\{y,[0\ 0]^{\top}\\},[60\
25]^{\top}\big{\\}}$. The switching rule is depicted in Fig. 7: $s=1$ is used
in the light gray area whereas $s=2$ is used in the dark gray area. There is a
decision boundary along which the closed-loop dynamics is discontinuous.
However, different from Example 1, the vector field points towards this
decision boundary. Fig. 7 shows ten closed-loop trajectories (green solid)
under random disturbance and noise. These trajectories tend to first reach the
decision boundary, chatter and slide along it until the target voltage level
is achieved, and eventually leave the decision boundary and stay close to the
target state. Particularly, the unsafe region is avoided in all the ten
simulations. Due to the chattering behavior along the switching surface, it is
in general difficult to use verification tools (e.g., flow* (Chen et al.,
2013)) based on reachable set over-approximation. We are able to find a
falsifying trajectory (black solid) using our approach, which has only query
access to $\pi$. Unlike Example 1, this falsifying trajectory tends to avoid
the switching surface. $\dagger$

###### Example 4.

(Section 5.1) We illustrate our approach’s capability to deal with model
mismatch by an intersection management problem with two autonomous cars. The
considered scenario is illustrated with Fig. 8. Two identical autonomous cars
approach an uncontrolled intersection at the same time, and coordinate with
each other to cross the intersection safely (i.e., without collision) and
optimally (i.e., minimizing the time of crossing) by solving the same hybrid
MPC problem on their own computational platform. A rough model of the other
car is known to each car so that they can predict the other’s behavior and
react accordingly. The states $[h_{1},d_{1},h_{2},d_{2}]^{\top}$, where
$h_{i}$ is the $i^{\rm th}$ car’s position relative to the center of the
intersection and $d_{i}$ is its speed, evolve with the following dynamics
(Nilsson et al., 2015):

(81) $\displaystyle\dot{h}_{i}=d_{i}+\delta d_{i},\ \
\dot{d}_{i}=\tfrac{1}{m}(F_{i}-f_{0}-f_{1}d_{i}-f_{2}d_{i}^{2}+\delta F_{i}).$

The control inputs $[F_{1},F_{2}]^{\top}$ are the forces acting on the two
cars. The disturbances $[\delta d_{1},\delta F_{1},\delta d_{2},\delta
F_{2}]^{\top}$ are state dependent because they cannot move the car backwards.
The above continuous-time dynamics is discretized with $0.2$s and linearized.
The nonlinear term $f_{2}d_{i}^{2}$ is captured with an additive model
uncertainty $p$, whereas $q$ is not needed in this example. The detailed
parameters can be found in Table. 2. The unsafe set $X_{\rm
unsafe}=[-2,2]\times[5,20]\times[-2,2]\times[5,20]$ corresponds to both cars
being within $2$m to the intersection center but the speeds being both larger
than $5$m/s. The initial set $X_{\rm
init}=[-50,-40]\times[0,20]\times[-50,-40]\times[0,20]$. The observation $y$
consists of an estimate of the two cars’ states. Here, the two cars do not
communicate, so they have a better estimation of their own states but a
coarser estimate of the other car’s state. Hence $y\in\mathbb{R}^{8}$ and
$y=[y^{1},y^{2}]$ where
$y^{i}=[\widehat{h}^{i}_{1},\widehat{d}^{i}_{1},\widehat{h}^{i}_{2},\widehat{d}^{i}_{1}]^{\top}=x+v^{i}$
is the observation of car $i$. We assume that $v^{1}\in
V^{1}=[-0.25,0.25]\times[-0.25,0.25]\times[-1,1]\times[-0.5,0.5]$ and
$v^{2}\in V^{2}=[-1,1]\times[-0.5,0.5]\times[-0.25,0.25]\times[-0.25,0.25]$.
The MPC controller $\pi_{\rm MPC}$ to falsify essentially contains two
identical MPC formulations, one is solved on car 1 with observation $y^{1}$,
and the other solved on car 2 with observation $y^{2}$. To minimize the
crossing time, $\pi_{\rm MPC}$ will assign priority to the car that may cross
the intersection sooner and ask the other car to slow down to avoid collision.
Under randomly generated process and measurement noise, the controller
experiences no safety violation in dozens of simulations. Our approach finds a
falsification trajectory where a collision occurs. Fig. 8 plots the true and
observed position of the two cars. The falsification scenario is interpreted
as follows: the positions and the velocities of two cars are identical, but
the observation makes each car believe that it is the one with priority. Thus
both cars accelerate to the intersection and collide.

Table 2. Parameter values of the model in Examples 5 Parameter | Description | Value
---|---|---
$m$ | mass of cars | 1462 (kg)
$f_{0}$ | friction/drag term | 51 (N)
$f_{1}$ | friction/drag term | 1.2567 (Ns/m)
$f_{2}$ | friction/drag term |  0.4342(N$\text{r}^{2}$/$\text{m}^{2}$)

$\dagger$

Figure 8. Intersection management: two autonomous cars.

###### Example 5.

(Section 5.2) Consider a self-driving car with linear lateral and longitudinal
dynamics in the form of Eq. (23), (24) (no switching input $s$), with

(90) $\displaystyle A$ $\displaystyle=\left[\begin{array}[]{cc}1&0\\\ 0&1\\\
\end{array}\right],B=\left[\begin{array}[]{c}0.1\\\ 0\\\
\end{array}\right],E=\left[\begin{array}[]{ccc}0.1&0\\\ 0&0.1\\\
\end{array}\right],K=\left[\begin{array}[]{c}0\\\ 1.5\\\ \end{array}\right].$

The control set $U=[-1.8,1.8]$ and the disturbance set
$W=[-0.1,0.1]\times[-0.1,0.1]\times[-0.05,0.05]$. The observation is a camera
image that is generated by Carla (Dosovitskiy et al., 2017). An end-to-end
controller $\pi_{\rm NN}$ is implemented by a feedforward neural network,
whose input is a low resolution image and output is the control $u$. The
approximated noise set $\widehat{V}=[-0.17,0.17]\times[-0.05,0.05]$. The
controller’s objective is to avoid a steady red truck ($X_{\rm
unsafe}=[-1.5,1.5]\times[0,5]$) from the initial set $X_{\rm
init}=[-2,2]\times[-30,-29]$ without deceleration. The neural network is
trained with a set of demonstrations (i.e., image-control input pairs)
generated by a hybrid MPC controller (Levine et al., 2016). The obtained
falsifying scenario is shown in Figure 9 (left). The green solid line
represents a typical closed-loop trajectory under random noise and
disturbance. In this case the truck (red box) is avoided. However, a
falsifying trajectory can be found in the middle of the domain. Since the
neural network tries to interpolate the behavior of the demonstrating MPC

Figure 9. Example 5. Left: falsifying trajectory. Right: a typical image
generated by Carla along the trajectory.

controller, it tends to choose a positive lateral speed if it is more likely
to cross the obstacle from the right, and choose a negative lateral speed
otherwise. Therefore, although $\pi_{\rm NN}$ is continuous, it has a sharp
change of decision in the middle of the domain, and small noise can cause
undesired behavior (see the zoomed-in plot). A video can be found at
https://youtu.be/QeBoqsdmCU4. $\dagger$

###### Example 6.

(Section 5.3) Consider a 2D linear system in the form of Eq. (23), (24).

Figure 10. Example 6.

where $A=I$, $B=E=0.25I$ and $K=[0\ 0]^{\top}$. The control set
$U=[-1,-1]\times[-2,2]$, the disturbance set $W=[-0.1,0.1]\times[-0.3,0.3]$,
and the noise set $V=[-1,1]\times[-1,1]$. The initial set $X_{\rm
init}=[0,20]\times[17,20]$, the unsafe set $X_{\rm unsafe}=[3,17]\times[0,3]$
and the target set $X_{\rm target}=[0,20]\times[0,3]$. The settings are
similar to Example 1 except that now there is i) a target set and ii) a
“braking” action, which allows the state to stay away from the unsafe set.
However, braking will prevent the state moving towards the target set, and the
deadline $t_{\rm max}$ for reaching the target may be missed. We use a hybrid
MPC controller $\pi_{\rm MPC}$ that minimizes the sum of distance from the
predicted states to the target set while enforcing $x_{t}\notin X_{\rm
unsafe}$ and $x_{t^{\star}}\in X_{\rm target}$ for some
$t^{\star}\in[\\![0,t_{\rm max}]\\!]$. The controller is static and decides to
go left/right and accelerate/decelerate at each point. A falsification
scenario is found via backward expansion from set $\Xi_{\rm unsafe}^{2}$.
Figure 10 shows the results. The green solid line represents a typical
trajectory under random noise and disturbance, which satisfies the finite
reach-avoid specification. The first half of the falsifying trajectory (black
solid) “chatters” in the middle of the state space under the adversarial
observation sequence (blue dotted), until the state is too close to $X_{\rm
unsafe}$ to cross it. The controller then decides to brake and cannot reach
the target set by the deadline $t_{\rm max}$. This corresponds to the second
half of the falsifying trajectory hitting $\Xi_{\rm unsafe}^{2}$. $\dagger$

###  6.1. Computation Time for the Examples 1-6

In this short section, we report the computation time to find a satisfying
adversarial scenario for Examples 1-6 in the paper. All the experiments are
run on a 1.80 GHz machine with 16 GB RAM. Table 3 summarizes the result for
each example. The second column (Dim $x$) is the dimension of the state space
$X$, the third column (Dim $y$) is the dimension of the observation space $Y$,
and the fourth column $T$ is the length of the obtained safety-violating
trajectory. The computation time grows with the dimension of the state space
and observation space, and also the length of the falsifying trajectory. We
also apply the falsification tool s-taliro to some examples. Except for
Example 1 with controller $\pi_{2}$, s-taliro could not find any falsifying
trajectories after running for hours (e.g., $10^{5}$ iterations for Example
2). The results for s-taliro is given in the last column, where $l$ is the
number of iterations, $t$ is the time and $r$ is the robustness value ($r<0$
means that the system is falsified). For Example 4 and 6, simulations with the
hybrid MPC controller in the loop are very time-consuming, hence we could only
run small number of iterations.

We note that a comparison with s-taliro is not fair in that s-taliro works
with black-box dynamics, hence aims to solve a harder problem. Our purpose
with this comparison is to show that the obtained adversarial examples are
nontrivial to find and to demonstrate the importance of using the plant model
whenever it is available.

Table 3. Evaluation of Algorithm 1 against Examples 1-6 Example |  Dim $x$ |  Dim $y$ | $T$ | Controller type | CPU | time (s) | s-taliro
---|---|---|---|---|---|---|---
index |  |  | (# steps) |  | Backward | Forward |  ($l$, $t$, $r$)
|  |  | 15 |  Rule-based $\pi_{1}$ | 18.56 | 5.09 |  ($10^{4}$,4226, 5.1)
1 | $2$ | $2$ | 15 |  Rule-based $\pi_{2}$ | 17.95 | 5.06 |  ($10^{4}$,1098,-3e-3)
|  |  | 15 |  Rule-based $\pi_{3}$ | 17.41 | 4.56 |  ($10^{4}$,3085,5.2)
|  |  | 14 |  Neural net $\pi_{\rm NN}$ | 17.08 | 4.30 |  ($10^{3}$,5768,0.11)
2 | $2$ | $2$ | 115 |  LQR $\pi_{\rm LQR}$ | 4096.28 | 38.85 |  ($10^{5}$,1.9e4,0.8)
3 | $2$ | $2$ | 132 | Rule-based | 263.15 | 46.63 |  ($10^{4}$,1e4,4.1)
4 | $4$ | $8$ | 27 |  Hybrid MPC $\pi_{\rm MPC}$ | 1640.45 | 83.12 | (50, 4.6e4, 29.4)
5 | $2$ |  image: $3072$ | 28 |  Neural net $\pi_{\rm NN}$ | 39.41 | 1.44 | -
|  |  semantic: $2$ |  | (end-to-end) |  |  |
6 | $3$ | $2$ | 50 |  Hybrid MPC $\pi_{\rm MPC}$ | 182.41 | 67.25 |  ($10^{2}$,4.4e4,0.75)

###  6.2. Evaluation with Randomly Generated Instances

We generate random problem instances and test the efficacy and scalability of
our approach. We consider integrator-like dynamics of different dimension with
small model mismatch. The output map is assumed to be $y=x+v$. The tested 2D
systems are single integrators on a plane, with small randomly generated model
mismatch. The mismatch is in the form of an additive quadratic term in the
state $x$, which is bounded by a small number. The 6D systems are double
integrators in a 3D space, and the 10D systems are double integrators in a 3D
space with a 4D stable but uncontrollable subspace. In all problem instances,
the objective is to reach a polytopic target set from a randomly generated
rectangular initial set $X_{\rm init}$, while avoiding multiple random
rectangular sets ($X_{\rm unsafe}$ is the union of these rectangles). Since
the safe domain is nonconvex, we use hybrid MPC controllers.

Table 4 shows the results. In the obtained adversarial scenarios, since the
trajectories hit $X_{\rm unsafe}$ by construction, the falsification is
considered successful (marked as “✓”) if the safety-violating trajectory
starts from $X_{\rm init}$, whereas the “$\times$” mark indicates that the
obtained safety-violating trajectory is from $x_{0}\notin X_{\rm init}$. For
each problem instance, we also run ten simulations from the same initial state
$x_{0}$ under random noise and disturbance profiles. The number of violations
among these ten random simulations is reported in the fifth column of Table 4.
While the initial state $x_{0}$ is not always in $X_{\rm init}$, random
simulations therefrom still tend to be safe in many cases (e.g., 2D case,
instances 4, 6, 8-10, 10D case, instance 2). This suggests that the scenarios
we found, though not from $X_{\rm init}$, are still nontrivial. Moreover, the
time of finding an adversarial scenario is small comparing to the time of
random simulations. One reason is because the hybrid MPC controller solves a
sequence of MILPs, which is time consuming. In fact, a considerable portion of
the falsification time is devoted to the query step. While the time for set
manipulation grows with the plant’s dimension $n_{x}$, the overall
falsification time also depends on the length of the falsifying trajectory and
the time for controller query. Our zonotope-based implementation works for 10D
dynamics, while the polytope-based implementation (using MPT3) can hardly go
beyond 4D.

Table 4. Evaluation of Algorithm 1 against Random Instances Dim $x$ | Instance | success | falsification | # violations | CPU time of
---|---|---|---|---|---
($n_{x}$) | index |  (from $X_{\rm init}$) | CPU time |  under random $v,w$ | 10 simulations
|  |  | (s) | (out of 10) | (s)
2 | 1 | ✓ | 874 | 1 | 6799
(polytope) | 2 | ✓ | 1018 | 0 | 8571
| 3 | ✓ | 719 | 0 | 9275
| 4 | $\times$ | 650 | 0 | 4917
| 5 | ✓ | 1278 | 0 | 10970
| 6 | $\times$ | 663 | 0 | 7628
| 7 | ✓ | 695 | 0 | 19470
| 8 | $\times$ | 639 | 0 | 17164
| 9 | $\times$ | 766 | 0 | 16329
| 10 | $\times$ | 1716 | 0 | 23420
| 11 | ✓ | 1991 | 3 | 14952
6 | 1 | ✓ | 1860 | 0 | 80283
(zonotope) | 2 | ✓ | 1602 | 0 | 21957
| 3 | ✓ | 281 | 0 | 26205
| 4 | $\times$ | 745 | 2 | 8281
| 5 | ✓ | 2841 | 0 | 17920
10 | 1 | ✓ | 542 | 0 | 22026
(zonotope) | 2 | $\times$ | 1045 | 0 | 10147

##  7\. Conclusion and Future Work

We considered the problem of falsifying safety properties for systems with
static controllers that do not have access to perfect state information. A
synthesis-guided falsification approach was proposed to find a class of
“interesting” falsifying scenarios specific to the given controller. The
approach was shown to be applicable to systems with relatively simple dynamics
but complicated or even unknown controllers, including MPC and neural network
controllers. We presented extensions of our approach to falsify vision-in-the-
loop systems against finite-time reach-avoid specifications. Some
computational aspects of the proposed approach were also discussed. We believe
that our approach nicely complements the black-box approaches from
falsification and white-box approaches from adversarial learning. For future
work, we will explore the falsification problem i) against more complicated
specifications and ii) for other classes of dynamics, either using
abstraction-based techniques or nonlinear backward reachable set computations.

###### Acknowledgements.

This work is supported in part by ONR grant # N00014-18-1-2501.

## References

  * (1)
  * Annpureddy et al. (2011) Yashwanth Annpureddy, Che Liu, Georgios Fainekos, and Sriram Sankaranarayanan. 2011.  S-taliro: A tool for temporal logic falsification for hybrid systems. In _Intl. Conf. on TACAS_. Springer, 254–257.
  * Balakrishnan et al. (2019) Anand Balakrishnan, Aniruddh G Puranic, Xin Qin, Adel Dokhanchi, Jyotirmoy V Deshmukh, Heni Ben Amor, and Georgios Fainekos. 2019\.  Specifying and evaluating quality metrics for vision-based perception systems. In _2019 DATE Conf._ IEEE, 1433–1438.
  * Bertsekas (1972) Dimitri Bertsekas. 1972\.  Infinite time reachability of state-space regions by using feedback control.  _IEEE TAC_ 17, 5 (1972), 604–613.
  * Bhatia and Frazzoli (2004) Amit Bhatia and Emilio Frazzoli. 2004.  Incremental search methods for reachability analysis of continuous and hybrid systems. In _Intl. Workshop on HSCC_. Springer, 142–156.
  * Bose et al. (2020) Avishek Joey Bose, Gauthier Gidel, Hugo Berrard, Andre Cianflone, Pascal Vincent, Simon Lacoste-Julien, and William L Hamilton. 2020.  Adversarial Example Games.  _arXiv preprint arXiv:2007.00720_ (2020).
  * Chen et al. (2013) Xin Chen, Erika Ábrahám, and Sriram Sankaranarayanan. 2013\.  Flow*: An analyzer for non-linear hybrid systems. In _Intl. Conf. on CAV_. Springer, 258–263.
  * Chou et al. (2018) Glen Chou, Yunus Emre Sahin, Liren Yang, Kwesi J Rutledge, Petter Nilsson, and Necmiye Ozay. 2018\.  Using control synthesis to generate corner cases: A case study on autonomous driving.  _IEEE TCAD_ 37, 11 (2018), 2906–2917.
  * Dalvi et al. (2004) Nilesh Dalvi, Pedro Domingos, Sumit Sanghai, and Deepak Verma. 2004.  Adversarial classification. In _Prod. of the tenth ACM SIGKDD Intl. Conf. on KDD_. 99–108.
  * De Wulf et al. (2006) Martin De Wulf, Laurent Doyen, and Jean-François Raskin. 2006\.  A lattice theory for solving games of imperfect information. In _Intl. Workshop on HSCC_. Springer, 153–168.
  * Dean et al. (2020) Sarah Dean, Andrew J Taylor, Ryan K Cosner, Benjamin Recht, and Aaron D Ames. 2020.  Guaranteeing Safety of Learned Perception Modules via Measurement-Robust Control Barrier Functions.  _arXiv preprint arXiv:2010.16001_ (2020).
  * Deshmukh et al. (2017) Jyotirmoy Deshmukh, Marko Horvat, Xiaoqing Jin, Rupak Majumdar, and Vinayak S Prabhu. 2017.  Testing cyber-physical systems through bayesian optimization.  _ACM TECS_ 16, 5s (2017), 1–18.
  * Deshmukh et al. (2015) Jyotirmoy Deshmukh, Xiaoqing Jin, James Kapinski, and Oded Maler. 2015.  Stochastic local search for falsification of hybrid systems. In _Intl. Symp. on ATVA_. Springer, 500–517.
  * Donzé (2010) Alexandre Donzé. 2010\.  Breach, a toolbox for verification and parameter synthesis of hybrid systems. In _Intl. Conf. on CAV_. Springer, 167–170.
  * Donzé and Maler (2010) Alexandre Donzé and Oded Maler. 2010.  Robust satisfaction of temporal logic over real-valued signals. In _Intl. Conf. on FORMATS_. Springer, 92–106.
  * Dosovitskiy et al. (2017) Alexey Dosovitskiy, German Ros, Felipe Codevilla, Antonio Lopez, and Vladlen Koltun. 2017.  CARLA: An Open Urban Driving Simulator. In _Prod. of the 1st ACRL_. 1–16.
  * Dreossi et al. (2019a) Tommaso Dreossi, Alexandre Donzé, and Sanjit A Seshia. 2019a.  Compositional falsification of cyber-physical systems with machine learning components.  _Journal of Automated Reasoning_ 63, 4 (2019), 1031–1053.
  * Dreossi et al. (2019b) Tommaso Dreossi, Daniel J Fremont, Shromona Ghosh, Edward Kim, Hadi Ravanbakhsh, Marcell Vazquez-Chanlatte, and Sanjit A Seshia. 2019b.  Verifai: A toolkit for the formal design and analysis of artificial intelligence-based systems. In _Intl. Conf. on CAV_. Springer, 432–442.
  * Ernst et al. (2019) Gidon Ernst, Sean Sedwards, Zhenya Zhang, and Ichiro Hasuo. 2019.  Fast falsification of hybrid systems using probabilistically adaptive input. In _Intl. Conf. on QEST_. Springer, 165–181.
  * Fremont et al. (2020) Daniel J Fremont, Johnathan Chiu, Dragos D Margineantu, Denis Osipychev, and Sanjit A Seshia. 2020\.  Formal Analysis and Redesign of a Neural Network-Based Aircraft Taxiing System with VerifAI. In _32nd International Conference on CAV_.
  * Ghosh et al. (2018) Shromona Ghosh, Felix Berkenkamp, Gireeja Ranade, Shaz Qadeer, and Ashish Kapoor. 2018.  Verifying controllers against adversarial examples with bayesian optimization. In _2018 IEEE ICRA_. IEEE, 7306–7313.
  * Ghosh et al. (2019) Shromona Ghosh, Hadi Ravanbakhsh, and Sanjit A Seshia. 2019\.  Counterexample-Guided Synthesis of Perception Models and Control.  _arXiv preprint arXiv:1911.01523_ (2019).
  * Gleave et al. (2019) Adam Gleave, Michael Dennis, Cody Wild, Neel Kant, Sergey Levine, and Stuart Russell. 2019\.  Adversarial policies: Attacking deep reinforcement learning.  _arXiv preprint arXiv:1905.10615_ (2019).
  * Goodfellow et al. (2015) Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy. 2015\.  Explaining and harnessing adversarial examples. In _Prod. of the 3rd ICLR_.
  * Henzinger and Raskin (2000) Thomas A Henzinger and Jean-François Raskin. 2000\.  Robust undecidability of timed and hybrid systems. In _Intl. Workshop on HSCC_. Springer, 145–159.
  * Herceg et al. (2013) Martin Herceg, Michal Kvasnica, Jones Colin N., and Manfred Morari. 2013.  Multi-Parametric Toolbox 3.0. In _Proc. of the European Control Conference_. Zürich, Switzerland, 502–510.  http://control.ee.ethz.ch/~mpt.
  * Huang et al. (2017) Sandy Huang, Nicolas Papernot, Ian Goodfellow, Yan Duan, and Pieter Abbeel. 2017.  Adversarial attacks on neural network policies. In _Prod. of 5th ICLR_.
  * Kim et al. (2005) Jongwoo Kim, Joel M Esposito, and Vijay Kumar. 2005\.  An RRT-based algorithm for testing and validating multi-robot controllers. In _Robotics: Science and Systems_. 249–256.
  * Kos and Song (2017) Jernej Kos and Dawn Song. 2017.  Delving into adversarial attacks on deep policies. In _Prod. of 5th ICLR_.
  * Lasserre (2015) Jean B Lasserre. 2015\.  Tractable approximations of sets defined with quantifiers.  _Mathematical Programming_ 151, 2 (2015), 507–527.
  * Levine et al. (2016) Sergey Levine, Chelsea Finn, Trevor Darrell, and Pieter Abbeel. 2016.  End-to-end training of deep visuomotor policies.  _The Journal of Machine Learning Research_ 17, 1 (2016), 1334–1373.
  * Li and Liu (2017) Yinan Li and Jun Liu. 2017\.  Invariance control synthesis for switched nonlinear systems: An interval analysis approach.  _IEEE TAC_ 63, 7 (2017), 2206–2211.
  * Majumdar et al. (2020) Rupak Majumdar, Necmiye Ozay, and Anne-Kathrin Schmuck. 2020\.  On abstraction-based controller design with output feedback. In _Prod. of the 23rd Intl. Conf. on HSCC_. 1–11.
  * Mitchell et al. (2005) Ian M Mitchell, Alexandre M Bayen, and Claire J Tomlin. 2005.  A time-dependent Hamilton-Jacobi formulation of reachable sets for continuous dynamic games.  _IEEE TAC_ 50, 7 (2005), 947–957.
  * Moosavi-Dezfooli et al. (2016) Seyed-Mohsen Moosavi-Dezfooli, Alhussein Fawzi, and Pascal Frossard. 2016\.  Deepfool: a simple and accurate method to fool deep neural networks. In _Prod. of the IEEE CVPR_. 2574–2582.
  * Nahhal and Dang (2007) Tarik Nahhal and Thao Dang. 2007.  Test coverage for continuous and hybrid systems. In _Intl. Conf. on CAV_. Springer, 449–462.
  * Nilsson et al. (2015) Petter Nilsson, Omar Hussien, Ayca Balkan, Yuxiao Chen, Aaron D Ames, Jessy W Grizzle, Necmiye Ozay, Huei Peng, and Paulo Tabuada. 2015.  Correct-by-construction adaptive cruise control: Two approaches.  _IEEE TCST_ 24, 4 (2015), 1294–1307.
  * Pei et al. (2017) Kexin Pei, Yinzhi Cao, Junfeng Yang, and Suman Jana. 2017\.  Deepxplore: Automated whitebox testing of deep learning systems. In _Prod. of the 26th SOSP_. 1–18.
  * Plaku et al. (2009) Erion Plaku, Lydia E Kavraki, and Moshe Y Vardi. 2009\.  Falsification of LTL safety properties in hybrid systems. In _Intl. Conf. on TACAS_. Springer, 368–382.
  * Sadraddini and Tedrake (2019) Sadra Sadraddini and Russ Tedrake. 2019.  Linear encodings for polytope containment problems. In _2019 CDC_. IEEE, 4367–4372.
  * Sontag (1999) Eduardo D Sontag. 1999\.  Stability and stabilization: discontinuities and the effect of disturbances.  In _Nonlinear analysis, differential equations and control_. Springer, 551–598.
  * Szegedy et al. (2014) Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. 2014\.  Intriguing properties of neural networks. In _Prod. of the 2nd ICLR_.
  * Tuncali et al. (2018) Cumhur Erkan Tuncali, Georgios Fainekos, Hisahiro Ito, and James Kapinski. 2018.  Simulation-based adversarial test generation for autonomous vehicles with machine learning components. In _2018 IEEE IV Symp._ IEEE, 1555–1562.
  * Waga (2020) Masaki Waga. 2020\.  Falsification of cyber-physical systems with robustness-guided black-box checking. In _Prod. of the 23rd Intl. Conf. on HSCC_. 1–13.
  * Wang et al. (2020) Xiao Wang, Saasha Nair, and Matthias Althoff. 2020.  Falsification-Based Robust Adversarial Reinforcement Learning.  _arXiv preprint arXiv:2007.00691_ (2020).
  * Yaghoubi and Fainekos (2019) Shakiba Yaghoubi and Georgios Fainekos. 2019.  Gray-box adversarial testing for control systems with machine learning components. In _Prod. of the 22nd Intl. Conf. on HSCC_. 179–184.
  * Yang et al. (2019) Liren Yang, Xiaofan Cui, Al-Thaddeus Avestruz, and Necmiye Ozay. 2019.  Correct-by-construction control synthesis for buck converters with event-triggered state measurement. In _2019 ACC_. 1056–1063.
  * Yang and Ozay (2020) Liren Yang and Necmiye Ozay. 2020.  Efficient safety control synthesis with imperfect state information. In _2020 CDC_. IEEE, 874–880.