11institutetext: Trinity College Dublin, Dublin, Ireland

# ReCCoVER: Detecting Causal Confusion for Explainable Reinforcement Learning

Jasmina Gajcin 11 0000-0002-8731-1236  Ivana Dusparic 11 0000-0003-0621-5400

###### Abstract

Despite notable results in various fields over the recent years, deep
reinforcement learning (DRL) algorithms lack transparency, affecting user
trust and hindering their deployment to high-risk tasks. Causal confusion
refers to a phenomenon where an agent learns spurious correlations between
features which might not hold across the entire state space, preventing safe
deployment to real tasks where such correlations might be broken. In this
work, we examine whether an agent relies on spurious correlations in critical
states, and propose an alternative subset of features on which it should base
its decisions instead, to make it less susceptible to causal confusion. Our
goal is to increase transparency of DRL agents by exposing the influence of
learned spurious correlations on its decisions, and offering advice to
developers about feature selection in different parts of state space, to avoid
causal confusion. We propose ReCCoVER, an algorithm which detects causal
confusion in agent’s reasoning before deployment, by executing its policy in
alternative environments where certain correlations between features do not
hold. We demonstrate our approach in the taxi and grid world environments,
where ReCCoVER detects states in which an agent relies on spurious
correlations and offers a set of features that should be considered instead.

###### Keywords:

Reinforcement Learning Explainability Intepretablity Feature Attribution
Causal Explanations Causal Confusion

##  1 Introduction

Understanding decisions of RL agents can increase users’ trust and encourage
collaboration with the system, prevent discrimination or uncover surprising
behavior [18]. One of the main tasks of explainability in RL is, however, to
ensure that agent’s behavior is correct and not prone to mistakes. This is a
necessary step before agent can be deployed to a real-life task.

In this work, we focus on one specific obstacle to successful deployment of RL
agents – causal confusion. Causal confusion is a phenomenon which occurs when
agent learns to rely on spurious correlations between the features which might
not hold over the entire state space. For illustration, we refer to an example
of a medical decision-making system for assigning urgent care to patients
[12], which learns to rely on the correlation between arm pain and heart
attacks, resulting in system suggesting emergency care for a patient with a
minor arm injury. In other words, the system failed to learn the causal
structure of the task – that heart attack is the true reason for administering
urgent care and arm pain is just a side effect that is highly correlated, but
should not affect the decision (Figure 1). Reliance on spurious correlations
becomes an issue when agent is confronted with a situation in which the
correlation does not hold. For this reason, it is necessary to verify that
agent’s behavior does not depend on any spurious correlations before
deployment to a real-life task, even if agent performs optimally in
experimental setting. Causal confusion was first detected in imitation
learning (IL), where RL agent can learn to rely on spurious correlations in
expert’s observations which do not hold in the RL environment [10]. Causal
confusion was further examined in RL and, to mitigate its effects, a method
for targeted exploration was proposed [12], forcing the agent to visit states
that challenge potential learned spurious correlations.

Figure 1: Different causal structures in different situations for a medical
decision system. Agent uses features $Condition$ and $Armpain$ to decide on
$Treatment$. Dotted lines represent causal relationships between features,
while full lines show whether agent should rely on the feature for its
decision. Left: if $Condition=HeartAttack$, arm pain should be disregarded.
Right: If $Condition=ArmInjury$, arm pain is an important factor in
determining treatment.

In this work, we address the problem of causal confusion in RL from the
perspective of explainability, and aim to increase understanding of agent’s
behavior in critical states, by examining whether agent relies on spurious
correlations to make a decision. To achieve the above, we propose ReCCoVER
(Recognizing Causal Confusion for Verifiable and Explainable RL), an approach
for detecting and correcting situations in which an agent relies on damaging
spurious correlations. If spurious correlation is uncovered, we identify the
area of state space in which relying on such correlation is damaging and
ReCCoVER generates an alternative subset of features that the agent should
instead focus on in that state subspace, to avoid causal confusion. It is
important to note that the subset of features agent should rely on can differ
between states – a feature can be useful in one state, but might need to be
ignored in another (Figure 1). To make our explanations concise, we verify
agent’s reasoning only in critical states. Specifically, we focus on states in
which agent reaches local maximum in terms of state-value function. Since
agent has an opportunity to achieve a large reward or complete a subtask in
local maxima states [20], these decisions are some of the most important in
agent’s execution. To uncover the possibility of spurious correlation in state
$s$, we make use of the fact that a policy relying on such correlation will
fail to generalize to situations where the correlation is broken. To that end,
we create alternative environments by performing causal interventions on
features and explore the behavior of the policy in different settings. Taking
the example of the medical system described above, we explore what makes it
decide on urgent care for a patient with heart attack by forcing arm pain to
be absent and observing how well agent performs in the alternative situation.
To find out whether a policy relying on a different set of features would
generalize better in the alternative environment, we propose a method for
training a feature-parametrized policy, which simultaneously learns a separate
policy for each possible subset of features. Performance of this policy in
alternative environments is used to detect whether ignoring certain features
during training could prevent spurious correlations from being learned and
produce correct behavior in an alternative environment in which agent’s
original policy fails. This way we can make sure that agents make decisions in
critical states based on the correct features (e.g. suggesting urgent care
because of the heart-attack and not arm pain), and do not rely on damaging
correlations.

Current work in causal confusion focuses on learning a robust policy that does
not rely on spurious correlations [12]. However, current approaches can only
detect spurious correlations in agent’s reasoning after recording a drop in
performance when the agent is deployed to an environment where such
correlations do not hold. In contrast, we focus on verifying the behavior of a
trained policy before deployment, to ensure that it does not rely on damaging
spurious correlations, and propose improvements to make policy less prone to
causal confusion and thus safer for deployment. Most similar to our work is
the original work on causal confusion, which proposes a method for uncovering
the true causes of expert’s actions when an RL policy is learned using IL
[10]. However, the work assumes that the true causes are constant throughout
the episode, and that the same set of features should be considered and same
features should be ignored in each state. Additionally, the work detects
causal confusion which originates as a consequence of distributional shift
between expert’s observations and agent’s environment. In contrast, we observe
that a single feature can be both useful and confusing, depending on the
situation – arm pain should not be a cause of a decision if a patient has a
heart attack, but should be considered if they suffer from an arm injury.
Moreover, we focus on a RL setting where causal confusion stems from agent
learning spurious correlations throughout its experience in the environment,
and create alternative environments in which such correlations do not hold to
verify agent’s reasoning.

By proposing ReCCoVER, the main contributions of this paper are:

  1. 1.

A method for extracting critical states in which agent’s behavior needs to be
verified. For each critical state, ReCCoVER generates a set of alternative
environments in which certain correlations between features are broken, to
simulate conditions that the agent did not observe often during training.

  2. 2.

An approach for detecting spurious correlations in agent’s policy by examining
agent’s performance in alternative environments where learned correlations do
not hold. If spurious correlation is detected, we identify the area of state
space in which relying on that correlation is damaging and ReCCoVER proposes a
subset of features that agent should rely on in that area instead.

We test and evaluate ReCCoVER in the taxi and minigrid traffic environments,
where we uncover parts of the state space where causal confusion is damaging
and propose a different subset of features agent should rely on, to avoid
learning spurious correlations. Full ReCCoVER code and evaluation environments
are available at https://github.com/anonymous902109/reccover.

##  2 Related Work

In this section we present a short description of structural causal models,
along with a brief overview of current methods in explainable RL.

###  2.1 Structural Causal Models (SCM)

Structural causal models [16] represent causal relationships between variables
and consist of two main parts: a directed acyclic graph (DAG), and a set of
structural equations. Each node in the DAG is associated with either an
observable $(\\{X_{i}\\}^{n}_{i=1})$ or an unobservable variable
$(\\{U_{i}\\}^{m}_{i=1})$, and presence of a directed edge between two nodes
implies a causal relationship. Structural equations can be assigned to edges
in order to describe the strength of the causal effect:

$X_{i}=f_{i}(PA_{i},U_{i})$ (1)

In other words, value of each observable variable $X_{i}$ is directed by the
values of its parent variables $PA_{i}$ and unobserved variables through some
function $f_{i}$.

Causal interventions are operations on the SCM that help us detect a cause-
effect relationship between two variables. Intervention on variable $A$ is
usually denoted by the do-operator: $do(A=v)$, and represents setting value of
$A$ to $v$ [17]. Intervening on a variable removes any incoming causal arcs to
that variable, because it forcibly sets the value of the variable, regardless
of the other variables that might be causing it. Outgoing causal relationships
will, however, remain intact. When intervening on features of an RL state, we
use the $do(f\rightarrow v;s)$ notation to describe forcibly setting feature
$f$ to $v$ in state $s$.

###  2.2 Explainable Reinforcement Learning (XRL)

Recent years have seen a rise in developing methods for explaining RL agents
[18]. According to their scope, XRL approaches can be divided into local and
global. While local XRL methods explain one decision [15, 13, 24], the aim of
global explanations is to understand the behavior of a policy as a whole [1,
6, 20, 23, 8]. Within this classification, ReCCoVER can be considered a hybrid
method – while we aim to verify policy behavior locally, in specific, critical
states, we also provide a way to extract critical states automatically,
enabling global explanations to be generated without the need for user input.

Feature attribution is a local method for explaining a decision by assigning
importance to input features, depending on their contribution to the output
[3]. Feature attribution is often referred to as feature importance [4]. In
supervised learning, feature attribution is commonly used for explaining and
verifying behavior of black-box models. For example, LIME [11] generates an
intrinsically interpretable local model which approximates behavior of the
black-box system around the instance in question. Feature importance can be
then extracted from the interpretable model, for example as feature weights in
case of linear LIME. Similarly, saliency maps are used in image-based
supervised learning tasks to highlight parts of the image which contributed
the most to the decision [21].

In XRL, feature attribution methods such as saliency maps and LIME have been
adopted from supervised learning to explain decisions of RL agents [9, 19, 7].
Similarly, the aim of this work is to explain agent’s behavior by examining
the influence of individual features on the decision. However, instead of only
showing which features contributed to the decision, we explore whether an
agent is relying on spurious correlations in that state, and if so, offer an
alternative set of features that agent should instead be considering. This
enables the developer to not only detect errors in agent’s reasoning, but also
correct them.

##  3 ReCCoVER

In this section, we posit a method for examining critical states and detecting
potential spurious correlations in agent’s decision-making process, which we
call ReCCoVER :Recovering Causal Confusion for Verifiable and Explainable
Reinforcement Learning. As input, ReCCoVER requires agent’s learnt policy
$\pi$, state-value function $V_{\pi}(s)$, feature set $\mathcal{F}$ and a set
of possible feature subsets $\mathcal{G}$. If the entire feature space is
searched, $\mathcal{G}$ is the power set of $\mathcal{F}$,
$\mathcal{G}=\mathcal{P}(\mathcal{F})$.

We start by describing an approach for gathering critical states in agent’s
execution (Section 3.1). Since actions in these states can bring large reward,
we focus on verifying agent’s behavior in these states. We then describe the
process of simultaneously learning a separate policy for each subset of
features in $\mathcal{G}$ (Section 3.2). We propose a method for generating
alternative environments by performing interventions on state features
(Section 3.3). Since setting a value of a feature can break its correlation
with other features, we use policy performance in alternative environments to
observe how policies depending on different features handle different
correlation settings. Finally, we describe how causal confusion can be
detected in alternative environments by executing a feature-parametrized
policy and observing whether ignoring specific features during training
prevents the agent from learning spurious correlations (Section 3.4). An
overview of the ReCCoVER approach is shown in Figure 2 and Algorithm 2.

Input: Policy $\pi$, state-value function $V_{\pi}$, feature set
$\mathcal{F}$, feature subsets $\mathcal{G}$
Parameters: $\alpha$, $k$
Output: Feature subset $\mathcal{F}(S^{*})$

1: Extract critical states $S_{c}$

2: Train a feature-parametrized policy $\pi_{G}$

3: for $s_{c}\in S_{c}$ do

4: Generate alternative environments $\mathcal{A}(s_{c})$ by intervening on
each feature in $\mathcal{F}$

5: Filter $\mathcal{A}(s_{c})$ based on state novelty

6: for $A\in\mathcal{A}(s_{c})$ do

7: Evaluate policy $\pi$ in $A$ for $k$ steps and record return $R_{\pi}$

8: for $G_{i}\in\mathcal{G}$ do

9: Evaluate policy $\pi_{G}(G_{i})$ in $A$ for $k$ steps and record return
$R(G_{i})$

10: end for

11: if $R_{\pi}\ll R(G_{j})$ for some $G_{j}\in\mathcal{G}$ then

12: Identify subspace $S^{*}\subseteq S$ where detected spurious correlation
is damaging

13: Propose feature subset $G_{j}$ to be used in states in $S^{*}$

14: end if

15: end for

16: end for

Algorithm 1 ReCCoVER algorithm Figure 2: Overview of ReCCoVER: to explain
decisions of policy $\pi$, a set of critical states $S_{c}$ is extracted.
Feature-parametrized policy $\pi_{G}$ is trained to simultaneously learn a
separate policy for each subset of features in $\mathcal{G}$. For each
critical state $s_{c}^{(i)}$, a set of alternative environments
$\mathcal{A}(s_{c}^{(i)})$ is generated, and performance of policy $\pi$ and
policies corresponding to different feature subsets in $\pi_{G}$ are evaluated
in $\mathcal{A}(s_{c}^{(i)})$. Alternative environments in which causal
confusion is detected are manually examined to extract an area of subspace
$S^{*}$ where relying on causal confusion damages performance of $\pi$ and a
different subset of features $\mathcal{F}(S^{*})$ is proposed to be used in
states in $S^{*}$.

###  3.1 Extracting Critical States

Naturally, agent’s behavior must be verified as a whole before deployment to a
real-life task. However, it can be costly to explain agent’s behavior in each
state. Additionally, making a sub-optimal action is riskier in certain states
than in others. For example, taking a slightly longer route is less dangerous
for a self-driving car than incorrectly reacting in a near-collision
situation. Thus, we focus on ensuring that agent behaves correctly in
selected, critical states.

Inspired by the idea of interesting states [20], we consider critical states
to be those in which an agent reaches a local maximum. Formally, given policy
$\pi$ and its state-value function $V_{\pi}(s)$, a set of local maxima states
$S_{c}$ is defined as:

$S_{c}=\\{s\in S|V_{\pi}(s)\geq V_{\pi}(s^{\prime}),\forall s^{\prime}\in
T_{s}\\}$ (2)

where $T_{s}$ is a set of states that agent can transition to from $s$ by
taking any available action $a\in\mathcal{A}$. Local maxima states represent
situations that are preferable for the agent, and often correspond to a larger
reward, due to achieving a sub goal or finishing the task. Since making the
right decision in these states can yield a large reward, it is important to
ensure agent’s reasoning is correct and does not rely on spurious correlations
in these states. The output of this part of the method is a set of critical
states $S_{c}$.

###  3.2 Training Feature-Parametrized Policy

Figure 3: Feature-parametrized policy training: each episode $i$, a random
feature subset $G_{i}$ is generated and used to mask agent states. At the same
time, $G_{i}$ is used as a parameter for the sampling function, to ensure that
only policy relying on $G_{i}$ is updated.

Knowing a separate policy for each feature subset helps us understand how
agent’s behavior changes when its access to certain features is denied during
training. To train a separate policy for each subset of features, we adapt the
approach proposed by [10] from the IL to an RL setting. To uncover the subset
of features an agent should rely on in order to avoid causal confusion,
authors in [10] propose an approach for training a feature-parametrized neural
network to simultaneously learn a separate policy for each possible subset of
features. Each feature subset is encoded as a binary vector, with each
coordinate indicating whether the specific feature is present. During
training, feature subsets are iteratively sampled and only policy relying on
the chosen subset of features is updated.

We adapt this approach from IL to DRL setting. We also represent each feature
subset as a binary vector, where each coordinate denotes presence of a
feature. However, instead of supervised methods used in the original work, we
use DQN [14] to learn a policy. In every iteration of the algorithm, a binary
vector is sampled at random and the feature-parametrized policy is updated
based only on features present in the chosen vector. In this way, multiple
policies that rely only on features available in their corresponding vectors
are learned simultaneously. High-level overview of the training process for
the feature-parametrized DRL policy is shown in Figure 3 and further laid out
in Algorithm 1. The output of this stage of ReCCoVER is a feature-parametrized
policy $\pi_{G}$.

Input: Set of feature subsets $\mathcal{G}$
Output: Feature-parametrized policy $\pi_{G}$

1: Randomly initialize appropriate network(s)

2: Initialize replay memory buffer $\mathcal{D}$

3: while loss not converged do

4: Receive initial observation $s_{0}$

5: Sample random feature subset $G_{i}\in\mathcal{G}$

6: while episode not over do

7: Mask current state $s_{t}^{*}=[s_{t}\odot G_{i};G_{i}]$

8: Select action $a_{t}$ based on policy network

9: Execute $a_{t}$, receive reward $r_{t+1}$ and new state $s_{t+1}$

10: Update state $s_{t}=s_{t+1}$

11: Mask new state $s_{t+1}^{*}=[s_{t+1}\odot G_{i};G_{i}]$

12: Store $(s_{t}^{*},a_{t},r_{t+1},s_{t+1}^{*},G_{i})$ in $\mathcal{D}$

13: Sample batch from $\mathcal{D}$ with feauture subset $G_{i}$

14: Calculate the loss specific to the DRL algorithm

15: Perform gradient descent update based on the loss

16: end while

17: end while

Algorithm 2 Training a feature-parametrized policy $\pi_{G}$

###  3.3 Generating Alternative Environments

A policy that relies on a damaging spurious correlation will fail to
generalize to an environment where such correlation does not hold. To test
whether agent learned such correlations, we generate alternative environments
in which specific correlations between features do not hold and evaluate the
policy in them. To break correlation between two features we use causal
interventions. Specifically, for two features $A$ and $B$, where $A$ causes
$B$ ($A\rightarrow B$), performing an intervention on $B$ and setting it to a
fixed value cancels any correlation between the two.

To examine how well a policy handles a change in correlations between features
in a critical state $s_{c}$, we generate a set of alternative environments
$\mathcal{A}(s_{c})$ by intervening on specific state features of $s_{c}$.
Environment $A(f\rightarrow v;s_{c})$ denotes an environment with starting
state $s_{c}$, in which feature $f$ is forcibly set to value $v$. By setting a
feature to a specific value, we break any correlation between that feature and
features that are causing it.

For a task with $N$ features, where each feature can take $M$ different
values, there are $N\cdot M$ possible alternative environments. Seeing how
generating such large number of environments might be unfeasible, we evaluate
the policy in the selected subset of alternative environments. Since we wish
to test agent’s behavior in unexpected situations, where learned correlations
might be broken, we adopt the idea of state novelty [22]. Intuitively, to
explain agent’s action in state $s_{c}$, we only perform intervention
$do(f\rightarrow v;s_{c})$ on state $s_{c}$ if it leads to a highly novel
state $s^{\prime}$. We generate a data set of agent’s transitions
$\mathcal{D}$ by unrolling the policy in the environment and calculate novelty
of a state $s$ as:

$\mathcal{N}(s)=\begin{cases}\frac{1}{\sqrt{n(s)}},&\text{if }n(s)\geq 1\\\
1,&\text{otherwise}\end{cases}$ (3)

where $n(s)$ is the number of occurrences in agent’s experience $\mathcal{D}$.

For a critical state $s_{c}$ we generate a set of alternative environments by
performing interventions on $s_{c}$ that lead to highly novel states:

$\mathcal{A}(s_{c})=\\{A(f\rightarrow
v;s_{c})|\mathcal{N}(s^{\prime})>\alpha,s^{\prime}=do(f\rightarrow
v;s_{c})\\}$ (4)

where $\alpha$ is a threshold value, denoting how novel a state must be to be
considered. The output from this stage of ReCCoVER is a set of alternative
environments $\mathcal{A}(s_{c})$ for each critical state $s_{c}\in S_{c}$.

###  3.4 Detecting Causal Confusion

Given a set of alternative environments $\mathcal{A}(s_{c})$ for a state
$s_{c}$ being explained, we can execute policy $\pi$ to test its robustness in
each of them. If $\pi$ fails in environment $A(s_{c})$, one explanation for
that could be that agent’s reliance on a spurious correlation has lead to poor
generalization to an alternative environment where such correlation is broken.
However, it is also possible that by intervening on a feature, we made the
task much more difficult or impossible to complete in the alternative
environment (e.g., changed the goal position to a far away or unreachable
position). The difference is that, if reliance on a spurious correlation is
the cause of failure, then a policy which ignores features that contribute to
spurious correlation in that state would perform well, as it would not be able
to learn the damaging correlation. On the other hand, if environment
$A(s_{c})$ is indeed unsolvable, any policy relying on any subset of features
will fail as well.

To examine whether agent’s policy $\pi$ relies on spurious correlations in a
specific critical state, we compare its performance in alternative
environments with the performance of feature-parametrized policy $\pi_{G}$. By
evaluating individual policies of $\pi_{G}$, we can see how policies relying
on different subsets of features differ in behavior in a critical state. Given
a set of alternative environments $\mathcal{A}(s_{c})$ in critical state
$s_{c}$, agent’s policy $\pi$ is executed in each of them for a fixed number
of steps $k$. Similarly, individual policies corresponding to different
feature subsets from $\pi_{G}$ are executed in each alternative environment
for the same number of steps. In each alternative environment $A(s_{c})$, we
compare the returns of agent’s policy $\pi$, with returns of individual
policies in $\pi_{G}$.

Causal confusion is detected in an alternative environment $A(s_{c})$ if
agent’s policy $\pi$ fails to generalize to $A(s_{c})$, but policy
$\pi_{G}(G^{\prime})$ corresponding to subset of features $G^{\prime}$ shows
good performance. This means that $\pi$ learned to rely on a spurious
correlation in $s_{c}$ which $\pi_{G}(G^{\prime})$ did not learn, as it did
not consider certain features. Formally, for feature-parametrized policy
$\pi_{G}$, agent’s policy $\pi$ and an alternative environment $A(f\rightarrow
v;s_{c})$, ReCCoVER detects causal confusion if there exists a policy
$\pi_{G}(G^{\prime})$ trained on a subset of features $G^{\prime}$, that
performs significantly better than $\pi$ in $A(f\rightarrow v;s_{c})$:

$\mathcal{R}^{k}(A(f,v;s_{c}),\pi)\ll\mathcal{R}^{k}(A(f,v;s_{c}),\pi_{G}(G^{\prime}))$
(5)

where $\mathcal{R}^{k}(A,\pi)$ is a return achieved in environment $A$ after
following policy $\pi$ for $k$ steps. Defining what is considered a
“significantly better performance” can depend on the task. In this work, we
assume RL tasks in which failure is met with a large negative reward, thus
allowing for more straightforward identification of poor generalization
performance. On the contrary, if $\pi$ is at least as successful as other
policies in $\pi_{G}$ in all alternative environments, we assume that its
behavior is satisfactory and not reliant on spurious correlations.

An environment $A(s_{c})$ where causal confusion is detected uncovers a part
of the state space in which reliance on spurious correlations damages agent’s
performance. We expect that alternative environments in which causal confusion
is detected will offer an insight into which parts of the environment agent
cannot conquer due to its reliance on spurious correlations. As our work is
preliminary and of exploratory nature, we manually examine the alternative
environments where causal confusion is detected, to extract parts of the state
space in which an agent should rely on a modified subset of features. Ideally,
this process should be automated, and problematic state subspaces directly
extracted. If causal confusion is detected in an alternative environment
$A(s_{c})$, where $\pi_{G}(G^{\prime})$ outperforms $\pi$, and a human expert
manually extracts a subset of problematic states $S^{*}\subseteq S$, we
propose that the agent should rely on features from $G^{\prime}$ in states
from $S^{*}$.

##  4 Evaluation Scenarios and Settings

In this section, we describe two environments in which we evaluate ReCCoVER.

#### Taxi Environment

is modelled after the OpenAI [2] taxi environment. Agent’s goal in this task
is to navigate a $5\times 5$ grid world, pick up a passenger from a designated
location and drop them off at their destination. Each step in the environment
yields a $-1$ penalty, picking up the passenger wins $+10$ reward and for
successfully completing the task the agent receives $+20$ reward. Episodes
terminate upon task completion, or after $200$ time steps.

In the original environment, the agent has information about the taxi’s
position, passenger’s location and destination. We augment the state space
with another feature – a passenger descriptor, which has a high influence on
passenger’s choice of destination, in order to create potential for spurious
correlations to be learned in the environment. Using the passenger descriptor
as a proxy for destination will have no negative consequences as long as the
two features are highly correlated. However, if the agent that relies on the
descriptor encounters a situation in which the descriptor is not indicative of
the destination, it will fail to drop off the passenger. It is imperative from
the perspective of generalization and explainability, for the agent to
recognize that, despite this correlation, destination is ultimately the
important feature as it will always indicate the correct drop-off coordinates,
regardless of the descriptor value. In each state, agents should rely only on
the original features, and ignore the passenger descriptor.

Figure 4: MiniGridworld traffic environment: Agent (red) needs to reach the
goal (green), avoid collision with the other vehicle (blue) and obey the
traffic light (outlined red).

#### MiniGrid Traffic Environment

is based on grid world environment [5]. We extend it into a traffic
environment by setting up a traffic light, and another vehicle in the
environment in front of the agent. Reaching the goal requires obeying the
traffic light and avoiding collision with the other vehicle. The vehicle in
front of the agent drives ahead whenever possible, while obeying the traffic
light. The agent has access to its own location, location of the goal,
location and the current action of the other vehicle, traffic light location
and light color. The agent can decide at each step whether to move forward or
remain in place. Each step has a living $-1$ penalty, while crashing into the
other vehicle or violating the red light costs $-10$ and terminates the
episode. Successfully navigating to the goal brings $+10$ reward, and
correctly crossing the traffic light is awarded with $+10$. Episodes are
limited to $200$ time steps.

Unlike the taxi environment, different situations in this environment require
different subsets of features. For example, consider the situation where the
agent is at the traffic light, behind another vehicle (Figure 4). If the
traffic light is red, the agent only needs to rely on this feature to know
that it needs to stay in place. If the light is green, the agent needs to
observe both the light and the position of the car in front. Under the
assumption that the car in front of the agent follows traffic rules, it is
likely that the action of the vehicle in front of the agent and agent’s action
will be highly correlated. However, if the agent relies on this correlation,
and only observes the action of the car in front of it to decide whether it
should move forward, then its policy will fail in a situation where the car in
front stops behaving as expected (e.g., stops even though the traffic light is
green or drives despite the red light). This means that the subset of
necessary features is not constant throughout the episode, as the action of
the vehicle in front needs to be considered in specific states, but can be
confusing in other.

Table 1: Training parameters for policies $\pi_{correct}$ and $\pi_{confused}$
in taxi and minigrid environments. The same parameters are used for
$\pi_{correct}$ and $\pi_{confused}$ within one task.

Task Algorithm Architecture Learning Rate Gamma Memory Capacity Exploration
Start Epsilon End Epsilon Epsilon Decay Taxi DQN Linear(5, 256) Linear(256, 6)
$1\mathrm{e}{-4}$ 0.99 10000 0.9 0.01 100000 Minigrid traffic DQN Linear(6,
512) Linear(512, 2) $1\mathrm{e}{-4}$ 0.99 80000 0.9 0.1 50000

Table 2: Training parameters for feature-parametrized policy $\pi_{G}$ in taxi
and minigrid environments as a part of ReCCoVER algorithm.

Task Algorithm Architecture Learning Rate Gamma Memory Capacity Exploration
Start Epsilon End Epsilon Epsilon Decay Taxi DQN Linear(10, 512) Linear(512,
6) $1\mathrm{e}{-4}$ 0.99 320000 0.9 0.01 100000 Minigrid traffic DQN
Linear(12, 512) Linear(512, 2) $1\mathrm{e}{-4}$ 0.99 80000 0.9 0.1 50000

##  5 Evaluating ReCCoVER

To demonstrate detection and correction of causal confusion in RL using
ReCCoVER, we set up three evaluation goals to examine:

  1. 1.

Goal 1 (Critical states): Verify that extracted critical states correspond to
local maxima states in terms of state-value function.

  2. 2.

Goal 2 (Recognizing causal confusion): Verify that, for a policy which relies
on a spurious correlation to make a decision in a critical state, ReCCoVER
flags the state.

  3. 3.

Goal 3 (Proposing correct feature subset): Verify that relying on the feature
subset proposed by ReCCoVER during training produces a policy less prone to
causal confusion.

To verify that correct critical states have been extracted, we manually
examine them, with a view to automate this process in the future. In the taxi
environment, local maxima states in terms of the state-value function should
correspond to situations in which the agent reaches the passenger location or
destination and should perform a pick-up or drop-off action, to complete a
sub-goal and collect a reward. In the minigrid traffic environment, local
maximum is reached when the agent is at the traffic light, or a step away from
the goal, as successfully crossing the traffic light or reaching the goal
brings large rewards.

To evaluate the second goal, we train a policy $\pi_{confused}$ which relies
on spurious correlations in the environment, and apply ReCCoVER to detect
causal confusion in critical states. To train $\pi_{confused}$ in the taxi
environment, we purposefully randomize the destination feature during
training, forcing $\pi_{confused}$ to rely on the passenger descriptor. As
long as the passenger descriptor correlates with the destination, the agent
can safely ignore the destination and use the descriptor as its proxy.
However, we expect to see a drop in performance in alternative environments in
which the destination is intervened on, breaking the descriptor and
destination correlation. Additionally, we expect causal confusion to occur
only in states in which the destination is important for the policy, such as
situations where an agent has picked up the passenger and is trying to drop
them off. In the minigrid traffic environment, we randomize the feature
denoting the traffic light, in order to learn a policy $\pi_{confused}$ which
relies solely on the actions of the vehicle in front of the agent. As long as
the vehicle in front of the agent follows the traffic rules (i.e., correctly
stops at the traffic light), an agent can safely ignore the traffic light and
follow the vehicle. We expect to see causal confusion occur in a situations
where vehicle in front does not follow traffic rules.

To evaluate the third goal, we start by examining the alternative environments
in which ReCCoVER detected spurious correlations. We manually extract a set of
states $S^{*}$ where causal confusion damaged the performance of
$\pi_{confused}$ and propose a different feature subset $\mathcal{F}(S^{*})$
to be used in states in $S^{*}$, to prevent learning spurious correlations.
$\mathcal{F}(S^{*})$ equals the feature subset $G^{\prime}$ of policy
$\pi_{G}(G^{\prime})$ which outperformed $\pi_{confused}$ in alternative
environments. We then train a new policy $\pi_{correct}$, ensuring that it
focuses only on features from $\mathcal{F}(S^{*})$ in states in $S^{*}$. We do
this by purposefully randomizing all features not present in
$\mathcal{F}(S^{*})$, in states from $S^{*}$ during training. Finally, we
apply ReCCoVER to $\pi_{correct}$, to examine whether adjusting which features
policy relies on in certain areas of the state space makes it less prone to
learning spurious correlations.

Training parameters for policies $\pi_{correct}$ and $\pi_{confused}$ in both
environments are shown in Table 1. ReCCoVER also requires parameters $k$ and
$\alpha$, denoting the number of steps that policies are evaluated in
alternative environments and novelty sensitivity when choosing novel
alternative environments respectively. We evaluate policies in alternative
environments for $k=3$ steps in taxi, and $k=1$ steps in minigrid traffic
environment, and use $\alpha=0.9$ in both tasks. Additionally, training
parameters for feature-parametrized policy $\pi_{G}$ in ReCCoVER are given in
Table 2. We limit the training of $\pi_{G}$ by including in $\mathcal{G}$ only
those feature subsets which enable learning at least a part of the task. In
the taxi environment, agent’s state consists of its x location, y location,
passenger descriptor, passenger location and destination. We consider $4$
feature subsets corresponding to binary vectors
$\begin{bmatrix}1&1&1&1&1\end{bmatrix}$,
$\begin{bmatrix}1&1&0&1&1\end{bmatrix}$,
$\begin{bmatrix}1&1&1&1&0\end{bmatrix}$ and
$\begin{bmatrix}1&1&0&1&0\end{bmatrix}$. First three feature subsets can be
used to learn the complete task in the environment where descriptor and
destination features are highly correlate, as they contain all necessary
information. The last subset can help the agent achieve the first subtask of
picking up the passenger, but lacks information about destination, necessary
for completing the task. In minigrid traffic environment, agent’s state
consists of its location, goal location, other vehicle’s action and location,
traffic light location and color. We limit $\mathcal{G}$ to $3$ feature
subsets: $\begin{bmatrix}1&1&1&1&1&1\end{bmatrix}$,
$\begin{bmatrix}1&1&1&1&1&0\end{bmatrix}$ and
$\begin{bmatrix}1&1&0&1&1&1\end{bmatrix}$. All three subsets can learn the
task fully in the environment in which the vehicle in front of the agent is
following traffic rules.

##  6 Results

In this section, we present our results of evaluating ReCCoVER in two RL
environments against the three evaluation goals (Section 5).

###  6.1 Taxi Environment

#### Goal 1 (Extracting Critical States):

ReCCoVER extracts 16 critical states (Table 3). $S_{c}$ contains states in
which the agent is at the passenger location and should perform the pick up
action, and states in which the agent should perform a drop off action, after
successfully picking up the passenger and reaching the destination. Both
situations correspond to local maxima, as they represent states in which agent
has potential to receive a large reward in the next step.

#### Goal 2 (Recognizing Causal Confusion):

We apply ReCCoVER to examine the $\pi_{confused}$, policy which relies on the
passenger descriptor, but ignores the destination feature. For each critical
state, ReCCoVER generated on average $8.81$ alternative environments (Table
3), and examined behavior of $\pi_{confused}$ and $\pi_{G}$ in them. ReCCoVER
detected causal confusion in $4$ critical states (Table 3), corresponding to
$4$ possible destination positions. In these states, the agent is at the
destination, about to drop off the passenger. Intervening on the destination
feature in these states breaks the correlation between descriptor and
destination, and leads to poor performance for $\pi_{confused}$. For that
reason, we discover that performance of $\pi_{confused}$ drops in alternative
environments obtained by intervening on the destination feature. However, in
the same alternative environments, policy
$\pi_{G}(\begin{bmatrix}1&1&0&1&1\end{bmatrix})$ performed significantly
better than $\pi_{confused}$. Policy
$\pi_{G}(\begin{bmatrix}1&1&0&1&1\end{bmatrix})$ relied on destination and
ignored the passenger descriptor, making it robust to changes in correlation
between the two features. In critical states where the agent should pick up
the passenger, ReCCoVER does not detect causal confusion, because information
about destination is not necessary for this part of the task and ignoring it
does not damage immediate performance.

#### Goal 3 (Proposing Correct Feature Subset):

All alternative environments in which ReCCoVER detected causal confusion for
policy $\pi_{confused}$ have been obtained by intervening on destination, in
situations where the agent already picked up the passenger. For this reason,
we propose that the subset of features that the agent relies on be altered
only in parts of the state space in which the agent has completed the subtask
of picking up the passenger. Policy $\pi_{confused}$ was outperformed in each
such alternative environment by
$\pi_{G}(\begin{bmatrix}1&1&0&1&1\end{bmatrix})$. For this reason, train
$\pi_{correct}$ to rely on feature subset
$\begin{bmatrix}1&1&0&1&1\end{bmatrix}$ in parts of the state space where the
passenger has been picked up. In other areas of the environment,
$\pi_{correct}$ relies on the same features as $\pi_{confused}$, denoted by
$\begin{bmatrix}1&1&1&1&0\end{bmatrix}$. As above, we randomize the features
that the agent should not rely on in specific states during training. Finally,
we apply ReCCoVER algorithm to uncover whether altered feature subset helped
$\pi_{correct}$ become less susceptible to causal confusion. ReCCoVER does not
detect causal confusion in any critical state for policy $\pi_{correct}$,
indicating that it does not rely on spurious correlations (Table 3).

Table 3: Output of each stage of the ReCCoVER algorithm in taxi environment.

Policy Number of episodes Number of collected transitions Number of critical
states Average number of alternative worlds per critical state Number of
states where causal confusion detected $\pi_{confused}$ $\pi_{correct}$ 100
100 920 916 16 16 8.81 8.43 4 0

###  6.2 Minigrid Traffic Environment

#### Goal 1 (Extracting Critical States):

ReCCoVER extracts $2$ critical states (Table 4). The first represents the
situation where the agent is at the traffic light, while in the second, the
agent is one step away from the goal. Both states show to situations in which
the agent is about to complete a sub task or reach the goal and receive a
large reward, making them plausable local maxima states.

#### Goal 2 (Recognizing Causal Confusion):

We apply ReCCoVER to examine behavior of policy $\pi_{confused}$, which fully
relies on the actions of the vehicle in front of the agent to make decisions,
ignoring the traffic light. On average, $14$ alternative environments are
generated for each critical state (Table 4). ReCCoVER detects causal confusion
in alternative environment where the agent is at the red light, but the
vehicle in front of it continues driving (Table 4). Policy $\pi_{confused}$,
relying only on the decisions of the vehicle in front, in this situation runs
the red light, and receives a large penalty. However, policy
$\pi_{G}(\begin{bmatrix}1&1&0&1&1&1&1\end{bmatrix})$, which relies on the
traffic light, but ignores the actions of the vehicle in front, acts correctly
in this state and stops at the red light. It is important to note that
$\pi_{G}(\begin{bmatrix}1&1&0&1&1&1&1\end{bmatrix})$ cannot be applied to
entire task, as knowing the current action of the vehicle in front is needed
to avoid collision. In a critical state where the agent is one step away from
the goal, no causal confusion is detected, since the traffic light in this
state does not affect the action.

#### Goal 3 (Proposing Correct Feature Subset):

By examining the alternative environment in which ReCCoVER detected causal
confusion for policy $\pi_{confused}$, we propose that the feature subset that
the agent relies on be altered in part of the state space $S^{*}$ where the
agent is at the red traffic light. We train policy $\pi_{correct}$ to rely on
the same feature subset $\begin{bmatrix}1&1&1&1&1&0\end{bmatrix}$ as
$\pi_{confused}$ in all situations except in states from $S^{*}$, where it
should rely on subset $\begin{bmatrix}1&1&0&1&1&1\end{bmatrix}$. We train
$\pi_{correct}$ to ignore the traffic light when agent is not directly at it,
by randomizing the traffic light feature. However, when the agent is at the
red light, we encourage the agent to observe the traffic light and ignore the
vehicle in front, by randomizing the feature corresponding to the action of
the vehicle. This way, we obtain a policy $\pi_{correct}$, which focuses on
the car in front of it in all situations, except when it faces a red light,
where it ignores the vehicle and relies only on the light color. To ensure
that $\pi_{correct}$ can encounter all the necessary situations, we train it
in an environment where the vehicle in front does not always follow the
traffic rules, and might run the red light. ReCCoVER is applied to examine the
behavior of $\pi_{correct}$, and causal confusion is not found in any critical
states, indicating that $\pi_{correct}$ does not rely on any spurious
correlations (Table 4).

Table 4: Output of each stage of the ReCCoVER approach in minigrid
environment.

Policy Number of episodes Number of collected transitions Number of critical
states Average number of alternative worlds per critical state Number of
states where causal confusion detected $\pi_{confused}$ $\pi_{correct}$ 100
100 1500 1500 2 1 14 15 1 0

##  7 Discussion and future work

In this work, we explored the problem of causal confusion in RL and proposed
ReCCoVER, a method for detecting spurious correlations in agent’s reasoning
before deployment. We evaluated our approach in two RL environments, where
ReCCoVER located situations in which reliance on spurious correlations was
damaging agent’s performance, and proposed a different subset of features that
should instead be used in that area of state space. Our work is, however, of
exploratory nature, and its purpose was to perform initial analysis of if and
how detecting causal confusion can aid in developing more transparent RL
agents. As such, certain stages of ReCCoVER algorithm are simplified and
manual – for example, we examine agent’s behavior only in critical states, and
limit the search for causal confusion to a subset of alternative environments.

For ReCCoVER to be applicable beyond benchmark scenarios, it needs to be
extended in two main directions – increasing and verifying its scalability and
automating the verification of ReCCoVER. In future work, we hope to explore
ways for narrowing down the feature subset search space $\mathcal{G}$, while
training the feature-parametrized policy, to make this stage of ReCCoVER more
feasible. Additionally, we hope to automate parts of the process which
currently require manual attention, such as verification of critical states or
extraction of areas of the state space where causal confusion is damaging.
Once fully automated, we will explore applicability of our approach beyond
explainability, due to its focus on correcting mistakes in agent’s reasoning.
Mistake detection and correction is useful in transfer learning, to ensure
that knowledge that is being reused is not prone to causal confusion.
Additionally, it can help improve robustness of RL policies, either through
human-in-the-loop approaches or as auto-correction.

## Acknowledgement

This publication has emanated from research conducted with the financial
support of a grant from Science Foundation Ireland under Grant number
18/CRT/6223. For the purpose of Open Access, the author has applied a CC BY
public copyright licence to any Author Accepted Manuscript version arising
from this submission.

## References

  * [1] Amir, D., Amir, O.: Highlights: Summarizing agent behavior to people. In: Proceedings of the 17th International Conference on Autonomous Agents and MultiAgent Systems. pp. 1168–1176 (2018)
  * [2] Brockman, G., Cheung, V., Pettersson, L., Schneider, J., Schulman, J., Tang, J., Zaremba, W.: Openai gym. arXiv preprint arXiv:1606.01540 (2016)
  * [3] Burkart, N., Huber, M.F.: A survey on the explainability of supervised machine learning. Journal of Artificial Intelligence Research 70, 245–317 (2021)
  * [4] Carvalho, D.V., Pereira, E.M., Cardoso, J.S.: Machine learning interpretability: A survey on methods and metrics. Electronics 8(8), 832 (2019)
  * [5] Chevalier-Boisvert, M., Willems, L., Pal, S.: Minimalistic gridworld environment for openai gym. https://github.com/maximecb/gym-minigrid (2018)
  * [6] Coppens, Y., Efthymiadis, K., Lenaerts, T., Nowé, A., Miller, T., Weber, R., Magazzeni, D.: Distilling deep reinforcement learning policies in soft decision trees. In: Proceedings of the IJCAI 2019 workshop on explainable artificial intelligence. pp. 1–6 (2019)
  * [7] Dethise, A., Canini, M., Kandula, S.: Cracking open the black box: What observations can tell us about reinforcement learning agents. In: Proceedings of the 2019 Workshop on Network Meets AI & ML. pp. 29–36 (2019)
  * [8] Gajcin, J., Nair, R., Pedapati, T., Marinescu, R., Daly, E., Dusparic, I.: Contrastive explanations for comparing preferences of reinforcement learning agents. arXiv preprint arXiv:2112.09462 (2021)
  * [9] Greydanus, S., Koul, A., Dodge, J., Fern, A.: Visualizing and understanding atari agents. In: International conference on machine learning. pp. 1792–1801. PMLR (2018)
  * [10] de Haan, P., Jayaraman, D., Levine, S.: Causal confusion in imitation learning. Advances in Neural Information Processing Systems 32, 11698–11709 (2019)
  * [11] Lundberg, S.M., Lee, S.I.: A unified approach to interpreting model predictions. Advances in neural information processing systems 30 (2017)
  * [12] Lyle, C., Zhang, A., Jiang, M., Pineau, J., Gal, Y.: Resolving causal confusion in reinforcement learning via robust exploration. In: Self-Supervision for Reinforcement Learning Workshop-ICLR 2021 (2021)
  * [13] Madumal, P., Miller, T., Sonenberg, L., Vetere, F.: Explainable reinforcement learning through a causal lens. In: Proceedings of the AAAI conference on artificial intelligence. vol. 34, pp. 2493–2500 (2020)
  * [14] Mnih, V., Kavukcuoglu, K., Silver, D., Graves, A., Antonoglou, I., Wierstra, D., Riedmiller, M.: Playing atari with deep reinforcement learning. arXiv preprint arXiv:1312.5602 (2013)
  * [15] Olson, M.L., Neal, L., Li, F., Wong, W.K.: Counterfactual states for atari agents via generative deep learning. arXiv preprint arXiv:1909.12969 (2019)
  * [16] Pearl, J.: Causality. Cambridge university press (2009)
  * [17] Peters, J., Janzing, D., Schölkopf, B.: Elements of causal inference: foundations and learning algorithms. The MIT Press (2017)
  * [18] Puiutta, E., Veith, E.: Explainable reinforcement learning: A survey. In: International cross-domain conference for machine learning and knowledge extraction. pp. 77–95. Springer (2020)
  * [19] Puri, N., Verma, S., Gupta, P., Kayastha, D., Deshmukh, S., Krishnamurthy, B., Singh, S.: Explain your move: Understanding agent actions using specific and relevant feature attribution. arXiv preprint arXiv:1912.12191 (2019)
  * [20] Sequeira, P., Gervasio, M.: Interestingness elements for explainable reinforcement learning: Understanding agents’ capabilities and limitations. Artificial Intelligence 288, 103367 (2020)
  * [21] Simonyan, K., Vedaldi, A., Zisserman, A.: Deep inside convolutional networks: Visualising image classification models and saliency maps. arXiv preprint arXiv:1312.6034 (2013)
  * [22] Şimşek, Ö., Barto, A.G.: Using relative novelty to identify useful temporal abstractions in reinforcement learning. In: Proceedings of the twenty-first international conference on Machine learning. p. 95 (2004)
  * [23] Verma, A., Murali, V., Singh, R., Kohli, P., Chaudhuri, S.: Programmatically interpretable reinforcement learning. In: International Conference on Machine Learning. pp. 5045–5054. PMLR (2018)
  * [24] van der Waa, J., van Diggelen, J., Bosch, K.v.d., Neerincx, M.: Contrastive explanations for reinforcement learning in terms of expected consequences. arXiv preprint arXiv:1807.08706 (2018)


* Wen et al. (2011) Shuhuan Wen, Wei Zheng, Jinghai Zhu, Xiaoli Li, and Shengyong Chen. 2011.  Elman fuzzy adaptive control for obstacle avoidance of mobile robots using hybrid force/position incorporation.  _IEEE Transactions on Systems, Man, and Cybernetics, Part C (Applications and Reviews)_ 42, 4 (2011), 603–608.
  * Wright and Felleisen (1994) A.K. Wright and M. Felleisen. 1994.  A Syntactic Approach to Type Soundness.  _Information and Computation_ 115, 1 (Nov. 1994), 38–94.  https://doi.org/10.1006/inco.1994.1093

##  Appendix A Collision Avoidance Source Code

⬇

1let vfi:{v: float | v > 0.} = 0.5

2let dt:{v: float | v > 0.} = 0.1

3let b:{v: float | v > 0.} = 0.136

4let xli:{v: float | v > 0.} = 2.

5let xbrake:{v: float | v >= xli} = 4.

6let amax:{v: float | v >= 0.} = 0.06

7

8let need_to_brake (xf, vf, xl, vl) =

9 ((xf +. ((vf*.vf)/.(2.*.b)) +.

10 ((1.+.(amax /. b))*.(2.*.dt*.vf+.((amax*.(4.*.dt*.dt))/. 2.))) +.

11 ((vf*.dt)/. 2.))

12 >=

13 (xl +. (((vl-.(b*.dt))*.(vl-.(b*.dt)))/.(2.*.b)) +.

14 (((vl-.(b*.dt))*.dt)/. 2.)))

15

16let (follower_control (xf, vf, xl, vl)) :

17 {v:float | ((~need_to_brake(xf, vf, xl, vl) && (v = amax)) ||

18 (need_to_brake(xf, vf, xl, vl) && (v = -.b)))} =

19 (if ((xf +. ((vf*.vf)/.(2.*.b)) +.

20 ((1.+.(amax /. b))*.(2.*.dt*.vf+.((amax*.(4.*.dt*.dt))/. 2.))) +.

21 ((vf*.dt)/. 2.)) + 0.5 % key difference here

22 >=

23 (xl +. (((vl-.(b*.dt))*.(vl-.(b*.dt)))/.(2.*.b)) +.

24 (((vl-.(b*.dt))*.dt)/. 2.)))

25 then (-.b)

26 else amax)

27

28% This can be assumed to be built-in

29let max (x,y) : {v:float | v >= x && v >= y} =

30 (if (x < y) then y else x)

31

32let (leader_control xl) : {v:float | ((xl >= xbrake) && (v = -.b)) ||

33 ((xl < xbrake) && (v = 0.))} =

34 (if (xl >= xbrake) then (-.b) else 0.)

35

36let node exec () =

37 let rec ((xf, vf, af, xl, vl, al):

38 {(x:float)*(v:float)*(a:float)*(x2:float)*(v2:float)*(a2:float) |

39 (x2 > x) && (x2 >= xli) && (v2 >= 0.) && (v >= 0.) &&

40 (x >= 0.) && (a >= -.b) &&

41 ((x +. ((v*.v)/.(2.*.b)) +. ((v*.dt)/. 2.)) <

42 (x2 +. ((v2*.v2)/.(2.*.b)) +. ((v2*.dt)/. 2.)))

43 }) =

44 xf = (0. fby (xf +. (vf_next *. dt)))

45 models (robot_get ("follower_x"))

46 and vf = (vfi fby max(vf +. (af*.dt), 0.))

47 models (robot_get ("follower_vel"))

48 and af = (follower_control xf_next, vf_next, xl_next, vl_next)

49 and xl = (xli fby (xl +. (vl_next *. dt)))

50 models (robot_get ("leader_x"))

51 and vl = (vfi fby max(vl +. (al*.dt), 0.))

52 models (robot_get ("leader_vel"))

53 and al = (leader_control xl_next)

54 (0., vfi, amax, xli, vfi, 0.) fby

55 in (() models (robot_str ("accel", af)); (xf, vf, af, xl, vl, al))

We implemented and verified the collision avoidance controller in MARVeLus,
and present the source code of the system here. In particular, we add the
convenience definitions need_to_brake, which ego’s control decision to apply
brakes based on supplied ego and leader positions and velocities (replicating
the conditional of $a^{f}$ in Fig. 12), and max, which takes the maximum of
two values. These would otherwise be directly implemented in the source code,
as function calls within synchronous nodes had not yet been fully implemented
in the compiler. We note that need_to_brake deviates slightly from the
dynamics equations, by causing the ego vehicle to maintain at least a
$0.5\text{\,}\mathrm{m}$ separation from the leader, to prevent any
imprecision encountered in the real experiment from causing the vehicles to
collide.

We assigned concrete values to various system constants (Lines 1-6) in the
discrete model to match the real-world experimental setup and to set the scale
of the experiment. For example, the initial distance of the leader vehicle
($2\text{\,}\mathrm{m}$) and initial velocities
($0.5\text{\,}\mathrm{m}\mathrm{/}\mathrm{s}$) were chosen with the intent of
running the experiment with small wheeled robots much smaller than full-size
vehicles. We set the maximum braking acceleration of both vehicles to
$0.136\text{\,}\mathrm{m}\mathrm{/}\mathrm{s}^{2}$, which was determined in
existing work to approximate a typical automobile’s braking force at the scale
of the wheeled robots used in the experiment (Chen et al., 2022). We
arbitrarily chose a maximum acceleration
($0.06\text{\,}\mathrm{m}\mathrm{/}\mathrm{s}^{2}$) that was somewhat less
than the braking acceleration, to limit the speeds reached by the robots in
the real experiment. Due to space constraints, we intended for the vehicles to
travel no farther than $8\text{\,}\mathrm{m}$ total, and determined that
allowing the leader vehicle to drive $2\text{\,}\mathrm{m}$ before braking
would provide ample distance for both vehicles to stop within the
$8\text{\,}\mathrm{m}$ space.

As with the simplified industrial controller, we define our state variables as
members of a tuple stream (Line 20). The safety property is specified on Line
21 as (x2 > x), along with various other assumptions, such as non-negative
velocities and correct starting order. As with the simplified example, the
safety property is insufficient, as it is not inductive. We add the assumption
that the previous instant has left the system in a recoverable state, i.e. the
ego would be able to avoid a collision if it were to respond immediately with
maximum braking (Lines 23-24). Lines 25-28 allow the verifier to assume that
the ego and leader vehicles’ acceleration decisions were correct in the
previous instant. Line 30 defines the initial condition—the ego begins at the
origin with initial velocity of $0.5\text{\,}\mathrm{m}\mathrm{/}\mathrm{s}$
and immediately begins accelerating, while the leader begins at
$2\text{\,}\mathrm{m}$, traveling at a constant
$0.5\text{\,}\mathrm{m}\mathrm{/}\mathrm{s}$. Lines 31-38 update the system’s
physical parameters, either by simulating the dynamics for simulation and
verification, or collecting the actual parameters if deployed to the real
system. Using these values, the state vector is updated with the ego position
and velocity (Line 39), the ego makes its control decision (Lines 40-41), the
leader’s position and velocity are updated (Line 42), and makes its own
control decision (Line 43). Finally, the ego acceleration command is published
to the shared variable “accel” on the robot.

##  Appendix B Detailed Experimental Methods

As part of MARVeLus, we developed extensions to the Zélus runtime and
additional software components to allow MARVeLus programs to communicate with
real robot sensors and actuators. The robotics stack consists of the user
MARVeLus code and runtime, kinematic models, and low-level sensor and actuator
drivers, which all run locally onboard the robots (Fig. 14). The modular
software architecture of the MARVeLus robotics stack provides flexibility in
testing and development; physical robots can be quickly replaced with their
simulated counterparts, and computationally intensive tasks can be offloaded
to an external computing resources. The trusted base consists of the MARVeLus
compiler, runtime, kinematic models, and sensor and low-level drivers. That
is, we trust that sensor data is always available and valid, communications
between software components is instantaneous and keeps shared states
sufficiently consistent, and that actuators are always able to attain their
commanded values.

We used our robotics extensions to demonstrate the verified collision
avoidance program, with small wheeled robots acting as the follower and leader
vehicles. Our verified control code runs on the follower vehicle, while the
leader vehicle acts independently though consistent with the previously-
defined assumptions. For realism, the robots do not communicate with one
another; the follower vehicle has no knowledge of when the leader will start
braking, only that the two vehicles start in a safe configuration.

###  B.1. Experimental Setup

We tested the MARVeLus collision avoidance implementation using small wheeled
robots on a straight $8\text{\,}\mathrm{m}$ track (Fig. 15). The software on
the robots were synchronized externally via a central server to ensure timing
consistency between the components. In addition to the collision avoidance
scenario in which the leader brakes abruptly and stops, we tested two other
variations: (1) The leader remains stationary throughout, simulating an
obstacle present on the track or roadway. (2) The leader decelerates to a
constant slow speed, but does not fully stop, allowing the ego vehicle to
continue moving forward as long as it maintains safe separation. When both
robots have stopped, or after a predetermined period of time in the case of
the slow-moving leader, the final distance between the two robots is recorded.

###  B.2. Robot Hardware

We selected the M-Bot Mini as our primary development target. The robot is
primarily controlled by a BeagleBone Blue single-board Linux computer
(BeagleBoard, 2018), which is uniquely suited for our application as it gives
userspace applications, such as the MARVeLus program and runtime, direct
access to robot hardware, simplifying our implementation. The robot is driven
by two motorized wheels arranged in a differential-drive configuration, with
quadrature encoders to measure position and wheel speed. Using the encoders
for odometry, the robots are able to estimate their velocity and distance
traveled. With our experimental setup, we determined that inaccuracies that
may potentially arise from wheel slippage and friction were negligible, and
that odometry alone was sufficiently accurate for distance and velocity
measurement.

###  B.3. Simulated Distance Sensing

The ego vehicle periodically receives velocity and position data from the
leader. Since we already assume that the ego vehicle has perfect knowledge of
the leader’s kinematic state, this method avoids potential errors or
inaccuracies arising from direct distance sensing, such as via computer vision
or LiDAR. However, we note that the modularity of the platform allows such
methods to be implemented and accessed within MARVeLus code should they be
necessary for future experiments. Besides sending position and velocity data,
the leader and ego vehicles do not communicate with one another in any other
way.

###  B.4. Communications and Runtime

Communications between the MARVeLus runtime and the other software components
is handled through the Lightweight Communications and Marshalling (LCM)
protocol (LCM Project, [n. d.]), which provides an inter-process link, even
between robots. Each component in the robotics stack maintains a local copy of
relevant system variables as a key-value store, which allows updates from
other components to propagate when available, and enables each component to
operate asynchronously. As a result, sensor and actuator interfacing is
handled as read and write calls, respectively, to the appropriate data store.
We trust that communications is instantaneous and error-free, and that data
stays sufficiently consistent system-wide, though we note that formal
verification of internal robot communications has been explored in other works
(Anand and Knepper, 2015).

The MARVeLus runtime is an extension of the Zélus runtime, allowing it to
control physical robot actuators and to derive stream values from real sensors
via foreign function interfaces that are inserted into the MARVeLus program at
compilation. The primary purpose of the MARVeLus runtime is to interpret
robot_get and robot_str commands from user code, and format them into the
appropriate LCM messages for read and write operations, respectively. The
runtime is assumed to be trusted and as a result is designed to contain only
the minimal necessary functionality.

###  B.5. User Code

Since embedded systems may have limited computational capabilities, the
verification stage of the MARVeLus workflow is not typically performed onboard
the robot itself. Instead, user programs are first verified on an external
system using the MARVeLus verifier and the SMT solver. After successful
verification, the program is translated to its intermediate OCaml
representation, and the result is transmitted to the robots for compilation
into a native executable. We note that we also trust the compilation process,
though there is existing work on formally verifying the compilation of
synchronous languages (Bourke et al., 2017).

###  B.6. Kinematic Models

The kinematic models simulate the discrete dynamics of the robots, and update
their actual speeds to match (Fig. 17). The kinematic model on the leader
vehicle defines the behavior that we assumed in the verified program, causing
it to begin braking after traveling a predetermined distance unknown to the
ego vehicle. The kinematic model on the follower vehicle accepts an
acceleration value from the user code, and incorporates this into its velocity
calculation. This separation of the dynamics from the user code enhances the
realism of the experiment, as it prohibits user code from directly modifying
the robot’s velocity, instead requiring it to do so through modulating the
acceleration, simulating controlling the brakes and throttle of an actual
vehicle. Although we employ discrete-time kinematic models, we note that one
may leverage the hybrid simulation features Zélus already supports (such as
dynamics defined by differential equations) for a higher-fidelity simulation.
We trust that this component has been implemented correctly, and note that the
kinematics are often incorporated into or modeled as invariants used to
augment the specifications of the user’s MARVeLus code.

$\displaystyle v^{f}_{0}$ $\displaystyle=0.5$ $\displaystyle v^{\ell}_{0}$
$\displaystyle=0.5$ $\displaystyle a^{\ell}_{0}$ $\displaystyle=0$
$\displaystyle v^{f}_{n+1}$ $\displaystyle=v^{f}_{n}+a^{f}_{n}\cdot dt$
$\displaystyle v^{\ell}_{n+1}$ $\displaystyle=v^{\ell}_{n}+a^{\ell}_{n}\cdot
dt$ $\displaystyle a^{\ell}_{n+1}$ $\displaystyle=\begin{cases}0&\text{if
}x^{\ell}_{n}<4\\\ -0.136&\text{otherwise}\end{cases}$ Figure 17. Kinematic
Models of the ego ($f$) and leader ($\ell$) vehicles. In the original
collision-avoidance scenario, the leader’s velocity is clamped to zero to
prevent the robot from reversing after stopping. In the slow-moving leader
scenario, it is instead clamped to a low but nonzero value. In the stationary
leader scenario, the leader’s initial velocity is set to zero.

###  B.7. Robot Driver

The C-based low-level driver on the robot manages hardware control of the
motors and encoders, and serves as a MARVeLus-compatible interface for the
Robot Control library (BeagleBoard, [n. d.]). The driver primarily
communicates with the kinematic model and MARVeLus runtime, ensuring that the
actual robot’s behavior is representative of the modeled robot, and reports
the robot’s own velocity derived from encoder measurements. For simplicity, we
chose to implement motor speed control at this level, though we note that this
discrete controller could plausibly be implemented and verified in MARVeLus if
desired. We assume that encoder data is always valid.

##  Appendix C Additional Experimental Data

Figure 18. Relative kinematic plot for actual and simulated experiments in
which the leader remains stationary Figure 19. Relative kinematic plot for
actual and simulated experiments in which the leader decelerates but does not
stop completely

Table 2.  Leader deceleration Trial # | Distance (m)
---|---
1 | 1.6955
2 | 0.7874
3 | 0.7620
4 | 0.7684
5 | 2.1082
6 | 0.7493
7 | 0.7620
8 | 1.0859
9 | 0.7049
10 | 0.7112

Table 3.  Leader stationary Trial # | Distance (m)
---|---
1 | 0.5080
2 | 0.4064
3 | 0.4000
4 | 0.5526
5 | 0.5398
6 | 0.5144
7 | 0.5271
8 | 0.5461
9 | 0.55245
10 | 0.2794

Table 4.  Leader halting Trial # | Distance (m)
---|---
1 | 0.4699
2 | 0.3747
3 | 0.3429
4 | 0.4953
5 | 0.4318
6 | 0.4636
7 | 0.5017
8 | 0.5207
9 | 0.4953
10 | 0.5144