# Automated Robot Recovery from Assumption Violations
of High-Level Specifications

Qian Meng and Hadas Kress-Gazit The authors are with Cornell University in
Ithaca, NY 14850, USA. Email<EMAIL_ADDRESS>This work is
supported by ONR PERISCOPE MURI award N00014-17-1-2699.

###### Abstract

This paper presents a framework that enables robots to automatically recover
from assumption violations of high-level specifications during task execution.
In contrast to previous methods relying on user intervention to impose
additional assumptions for failure recovery, our approach leverages synthesis-
based repair to suggest new robot skills that, when implemented, repair the
task. Our approach detects violations of environment safety assumptions during
the task execution, relaxes the assumptions to admit observed environment
behaviors, and acquires new robot skills for task completion. We demonstrate
our approach with a Hello Robot Stretch in a factory-like scenario.

##  I Introduction

Formal synthesis – the process of transforming a high-level specification into
a correct-by-construction system – is increasingly being used to create
provably-correct robot behaviors that fulfill complex, high-level tasks [1]. A
common approach to synthesis first creates a discrete abstraction of the
environment and the robot skills (or actions) [2, 3, 4, 5], then generates a
temporal logic [6] specification from the abstraction and the user-provided
tasks. Synthesis algorithms (e.g. [7]) transform the specification into a
symbolic strategy that guides the composition of the robot skills to satisfy
the high-level task. If the synthesis fails, meaning the task cannot be
guaranteed, researchers have leveraged the feedback from synthesis to modify
the abstraction and the specification to make the specification realizable [8,
9, 10, 11, 12].

Synthesis for Generalized Reactivity(1) (GR(1)) specifications has been used
for synthesizing robot control from high-level specifications due to its
relatively-low quadratic time complexity in the size of its state space [7].
GR(1) specifications are a fragment of Linear Temporal Logic (LTL) [6] and are
structured as an implication from assumptions on the environment behaviors to
guarantees on the system behaviors, as described in Section II-C. The
assumptions and guarantees contain safety constraints, which specify
requirements that should always hold, and liveness constraints, which specify
requirements that should hold repeatedly. Because of the implication, the
synthesized strategy is only required to satisfy the system guarantees if the
environment behaviors satisfy the assumptions.

While GR(1) synthesis can produce provably-correct robot strategies, the high-
level specification includes assumptions about the behavior of the
environment, such as the location of obstacles or the state of objects; if, at
runtime, these assumptions are violated, the behavior of the robot is no
longer guaranteed to satisfy the task. In this work we address the problem of
autonomously repairing such violations, if possible, to ensure the robot
satisfies its intended task.

Example 1. Consider the workspace in Fig. 1 with four regions. A robot,
initially in _Assembly_ , is asked to move to _Loading_ while ensuring that it
is not in the same region as an obstacle, initially located in _Walkway_. The
robot has a skill $move_{1}$ which moves the robot from _Assembly_ to
_Loading_ through _Aisle_. The user provides the assumption that the obstacle
is static and the synthesized strategy contains the action $move_{1}$. During
the skill execution when the robot is still in _Assembly_ , the obstacle moves
to _Aisle_ , violating the static-obstacle assumption – this may result in the
robot violating the requirement that it is not in the same region as the
obstacle. To repair, we would want the robot to have a skill that goes through
_Walkway_ instead of through _Aisle_.

Figure 1: Workspace of Example I.

Related work. Cooperative synthesis creates systems that do not attempt to
violate the environment assumptions [13, 14]. Jones et al. propose to detect
system anomalies by learning Signal Temporal Logic specifications from data
and using them to monitor system behaviors [15, 16]. Under topological changes
such as the discovery of unknown obstacles, some approaches modify the
abstraction and explore local resynthesis [17, 18] and replanning [19, 20] for
recovery. This paper unifies and extends the scope of [13, 14, 15, 16, 17, 18,
19, 20]. We attempt to recover from general assumption violations that can
arise from  (i) non-cooperative systems,  (ii) system anomalies such as robot
skill failures,  (iii) topological changes, and  (iv) uncontrollable
environment behaviors, such as unexpected changes in user inputs, which were
not addressed by [13, 14, 15, 16, 17, 18, 19, 20].

Wong et al. present a semi-automatic recovery method to tackle general
assumption violations for mobile robots [21, 22]. The method a-priori
synthesizes a strategy that tolerates temporary assumption violations, if
possible. At runtime, the method relaxes the environment assumptions to
include new environment behavior but requires user input if the new
specification is not realizable. Baran et al. propose a human-in-the-loop
system that leverages inverse reinforcement learning to adapt plans according
to user preferences [23].

Example I continued. In contrast to our approach, the approach in [21, 22]
recovers from the assumption violation in Example I by requiring the user to
provide a liveness assumption which states that repeatedly the obstacle is not
in _Aisle_. The robot then waits in _Loading_ until the obstacle moves away
and then resumes the execution of $move_{1}$.

This paper aims to recover from assumption violations during runtime
automatically. We consider a setting where obtaining all feasible robot skills
is intractable. Therefore, we assume the user provides a set of skills
sufficient to satisfy the task under the original environment assumptions. The
process of assumption relaxation allows the environment to have more
behaviors, but those may prevent the robot from achieving its task. Rather
than weaken the environment by introducing additional environment assumptions
as in [21, 22], we extend the robot’s capabilities by automatically suggesting
and adding new skills that enable it to fulfill its task under the new
environment assumptions. Recently, [24, 25, 26] present a technique for
offline repair of an unrealizable specification by suggesting robot skills
guaranteed to make the specification realizable. We utilize repair to discover
new robot skills to complete the task after assumption violations.

Figure 2: Our framework for automatic recovery from assumption violations
during task execution. Blue arrows represent regular execution; red arrows
represent our recovery process.

This paper presents a framework, depicted in Fig. 2, that detects environment
assumption violations and leverages the repair tool for recovery. We create a
specification from the user-provided tasks and an abstraction consisting of
the workspace, the objects in the workspace, and the robot skills. We
automatically create an online monitor for the environment safety assumptions
(Section IV-A). In response to assumption violations, we relax the violated
assumptions (Section IV-B) and perform repair to add a set of new skills that
enable the robot to complete the task (Section IV-C).

Example I continued. Our approach detects the assumption violation in Example
I and relaxes the static-obstacle assumption to include the possibility of the
obstacle moving from _Walkway_ to _Aisle_. The specification becomes
unrealizable after the assumption relaxation. We automatically create a new
skill $move_{2}$ which moves the robot from _Assembly_ to _Loading_ through
_Walkway_. We synthesize a new strategy that executes $move_{2}$ to bring the
robot to _Loading_.

Contributions. To our knowledge, this is the first framework to allow a robot
to autonomously recover from assumption violations of temporal logic
specifications during task execution. This work closes the loop of executing
correct-by-construction robot strategies in uncertain environments, for which
the initial environment assumptions may be inaccurate, by gradually adjusting
the assumptions to meet the actual environment behaviors and acquiring the
required robot skills to satisfy the tasks. This work will enable formal
synthesis to create autonomous robotic systems that are more applicable to
complex, real-world environments.

##  II Preliminaries

###  II-A Linear Temporal Logic

We use a fragment of LTL to capture specifications. Let $\mathcal{V}$ be a set
of atomic propositions. We define the syntax of LTL recursively using the
following grammar:

$\varphi\coloneqq\pi~{}|~{}\neg\varphi~{}|~{}\varphi\vee\varphi~{}|~{}\bigcirc\varphi~{}|~{}\varphi\
\mathcal{U}\ \varphi$

where $\pi\in\mathcal{V}$ is an atomic proposition, $\varphi$ is an LTL
formula, $\neg$ is negation, $\vee$ is disjunction, $\bigcirc$ is the next
operator, and $\mathcal{U}$ is the strong until operator. Conjunction
($\land$), implication ($\to$), equivalence ($\leftrightarrow$), eventually
($\lozenge$), and always ($\square$) can be derived from the grammar.

The semantics of LTL are defined over infinite sequences
$\sigma=\sigma_{0}\sigma_{1}\dots$ where $\sigma_{i}\subseteq\mathcal{V}$ is
the set of atomic propositions that are $True$ at step $i$. We denote that a
sequence $\sigma$ satisfies a formula $\varphi$ at step $i$ by
$\sigma^{i}\models\varphi$. A sequence $\sigma$ satisfies a formula $\varphi$,
denoted $\sigma\models\varphi$, iff $\sigma^{0}\models\varphi$. Formally,
$\sigma^{i}\models\pi$ iff $\pi\in\sigma_{i}$,
$\sigma^{i}\models\bigcirc\varphi$ iff $\sigma^{i+1}\models\varphi$,
$\sigma^{i}\models\lozenge\varphi$ iff $\exists j\geq i$ such that
$\sigma^{j}\models\varphi$, and $\sigma^{i}\models\square\varphi$ iff $\forall
j\geq i$, $\sigma^{j}\models\varphi$. The full semantics of LTL can be found
in [6].

###  II-B Abstractions

We partition the set of atomic propositions into sets of inputs
${\mathcal{X}}$ and outputs ${\mathcal{Y}}$
($\mathcal{V}={\mathcal{X}}\cup{\mathcal{Y}}$). The inputs describe the
environment states, such as the position of an object. An input state is a
subset of the inputs ($\sigma_{{\mathcal{X}}}\subseteq{\mathcal{X}}$). We
partition the set of inputs into sets of controllable inputs
${\mathcal{X}}_{\textrm{c}}$ and uncontrollable inputs
${\mathcal{X}}_{\textrm{u}}$
(${\mathcal{X}}={\mathcal{X}}_{\textrm{c}}\cup{\mathcal{X}}_{\textrm{u}}$).
Controllable inputs describe the part of the physical world that the robot can
control, for example its position. A controllable input state is a subset of
the controllable inputs
($\sigma_{\textrm{c}}\subseteq{\mathcal{X}}_{\textrm{c}}$). Uncontrollable
inputs describe the part of the physical world that the robot does not have
control over, such as the position of an obstacle, or a user input. The input
abstraction can be obtained automatically [2, 3]. In this paper, we obtain
${\mathcal{X}}$ by taking a Cartesian product of a set of regions
${\mathcal{R}}$ that partitions the workspace of the robot and a set of
objects ${\mathcal{O}}$ that includes the robot, along with a set of user-
controlled inputs
${\mathcal{X}}_{\textrm{user}}\subseteq{\mathcal{X}}_{\textrm{u}}$. The set of
inputs is ${\mathcal{X}}\coloneqq\\{\pi_{{o}}^{{r}}\mid
o\in{\mathcal{O}},r\in{\mathcal{R}}\\}\cup{\mathcal{X}}_{\textrm{user}}$ where
$\pi_{{o}}^{{r}}$ is $True$ when object $o$ is in region $r$. In Example I,
${\mathcal{O}}=\\{\textrm{robot},\textrm{obs}\\}$,
${\mathcal{R}}=\\{\textrm{assm},\textrm{aisle},\textrm{wlkwy},\textrm{load}\\}$,
${\mathcal{X}}_{\textrm{user}}=\emptyset$,
${\mathcal{X}}_{\textrm{c}}=\\{\pi_{{robot}}^{{r}}\mid r\in{\mathcal{R}}\\}$,
${\mathcal{X}}_{\textrm{u}}=\\{\pi_{{obs}}^{{r}}\mid
r\in{\mathcal{R}}\\}\cup{\mathcal{X}}_{\textrm{user}}$, and
${\mathcal{X}}={\mathcal{X}}_{\textrm{c}}\cup{\mathcal{X}}_{\textrm{u}}$.

A grounding function G maps an input proposition to a set of states in the
physical world $x=(x_{1},\dots,x_{n})\in X\subseteq\mathbb{R}^{n}$, i.e.
$\textrm{G}:{\mathcal{X}}\to 2^{X}$. We lift the grounding function to map an
input state $\sigma_{{\mathcal{X}}}$ to a set of physical states by taking the
intersection of the groundings of each input in $\sigma_{{\mathcal{X}}}$, i.e.
$\textrm{G}(\sigma_{{\mathcal{X}}})=\bigcap_{\pi\in\sigma_{{\mathcal{X}}}}\textrm{G}(\pi)\bigcap_{\pi\in{\mathcal{X}}\setminus\sigma_{{\mathcal{X}}}}(X\setminus\textrm{G}(\pi))$.
An inverse grounding function $\textrm{G}^{-1}:X\to 2^{\mathcal{X}}$ maps a
physical state $x\in X$ to an input state
$\sigma_{{\mathcal{X}}}\subseteq{\mathcal{X}}$ such that
$x\in\textrm{G}(\sigma_{{\mathcal{X}}})$ and
$\forall\pi\not\in\sigma_{{\mathcal{X}}},x\not\in\textrm{G}(\pi)$. In Example
I, if initially the robot is at $x_{\textrm{init}}^{\textrm{robot}}=(5,1)$,
and the obstacle is at $x_{\textrm{init}}^{\textrm{obs}}=(3.8,0.5)$, then the
initial abstract input state is
$\sigma_{\textrm{init}}=\textrm{G}^{-1}((x_{\textrm{init}}^{\textrm{robot}},x_{\textrm{init}}^{\textrm{obs}}))=\\{\pi_{{robot}}^{{assm}},\pi_{{obs}}^{{wlkwy}}\\}$.

The set of outputs ${\mathcal{Y}}$ represents the set of skills the robot can
execute. A skill can only be executed at a set of controllable input states
(initial preconditions), results in a set of controllable input states (final
postconditions), and may pass through a set of unique controllable input
states (intermediate states). Each state except for the final postconditions
has a set of postconditions. Each state except for the initial preconditions
has a set of preconditions. In Example I, the initial precondition of the
skill $move_{1}$ is
$\sigma_{{\mathcal{X}},\textrm{1}}=\\{\pi_{{robot}}^{{assm}}\\}$, the
postcondition of $move_{1}$ on $\sigma_{{\mathcal{X}},\textrm{1}}$ is
$\sigma_{{\mathcal{X}},\textrm{2}}=\\{\pi_{{robot}}^{{aisle}}\\}$, and the
postcondition of $move_{1}$ on $\sigma_{{\mathcal{X}},\textrm{2}}$ is
$\sigma_{{\mathcal{X}},\textrm{3}}=\\{\pi_{{robot}}^{{load}}\\}$. The state
$\sigma_{{\mathcal{X}},\textrm{3}}$ is also the final postcondition of
$move_{1}$. The skills are implemented by the robot’s low-level controllers.
The skill abstraction can be obtained automatically [4]. In this paper, we
assume that the user provides the skill abstraction. We assume that skill
execution does not terminate until it reaches the final postcondition, unless
an assumption violation occurs, in which case we terminate the skill
prematurely and start the recovery process.

###  II-C Synthesis and Specification Violation

In this paper, we consider the GR(1) fragment of LTL to leverage its synthesis
algorithm [7]. The specifications are of the form
$\varphi=\varphi_{\textrm{e}}\to\varphi_{\textrm{s}}$ where
$\varphi_{\textrm{e}}=\varphi_{\textrm{e}}^{\textrm{i}}\land\varphi_{\textrm{e}}^{\textrm{t}}\land\varphi_{\textrm{e}}^{\textrm{g}}$
is the environment assumption and
$\varphi_{\textrm{s}}=\varphi_{\textrm{s}}^{\textrm{i}}\land\varphi_{\textrm{s}}^{\textrm{t}}\land\varphi_{\textrm{s}}^{\textrm{g}}$
is the system guarantee:

  * $\bullet$

$\varphi_{\textrm{e}}^{\textrm{i}}$ and $\varphi_{\textrm{s}}^{\textrm{i}}$
are Boolean formulas over ${\mathcal{X}}$ and ${\mathcal{Y}}$, respectively,
specifying the initial conditions.

  * $\bullet$

$\varphi_{\textrm{e}}^{\textrm{t}}$ and $\varphi_{\textrm{s}}^{\textrm{t}}$
are the environment safety assumptions and the system safety guarantees,
respectively. They are of the form $\bigwedge_{i}\square\psi_{i}$ where
$\psi_{i}$ is a Boolean formula over $v$ and $\bigcirc u$. For
$\varphi_{\textrm{e}}^{\textrm{t}}$, $v\in{\mathcal{X}}\cup{\mathcal{Y}}$ and
$u\in{\mathcal{X}}$. For $\varphi_{\textrm{s}}^{\textrm{t}}$,
$v,u\in{\mathcal{X}}\cup{\mathcal{Y}}$. We divide
$\varphi_{\textrm{e}}^{\textrm{t}}$ into the skill assumptions
$\varphi_{\textrm{e}}^{\textrm{t,skill}}$ and the the hard assumptions
$\varphi_{\textrm{e}}^{\textrm{t,hard}}$
($\varphi_{\textrm{e}}^{\textrm{t}}=\varphi_{\textrm{e}}^{\textrm{t,skill}}\land\varphi_{\textrm{e}}^{\textrm{t,hard}}$).
The skill assumptions $\varphi_{\textrm{e}}^{\textrm{t,skill}}$ describe the
postconditions of the skills and can be modified by the repair process (see
Section IV-C). The assumptions in $\varphi_{\textrm{e}}^{\textrm{t,hard}}$ are
the hard assumptions that cannot be modified by repair.

  * $\bullet$

$\varphi_{\textrm{e}}^{\textrm{g}}$ and $\varphi_{\textrm{s}}^{\textrm{g}}$
are the environment liveness assumptions and the system liveness goals,
respectively. They are of the form $\bigwedge_{i}\square\lozenge J_{i}$ where
$J_{i}$ is a Boolean formula over ${\mathcal{X}}\cup{\mathcal{Y}}$.

The synthesis algorithm in [7] formulates a two-player game between the
environment and the system. The initial conditions of the specification define
the initial positions of the players, the safety formulas define the
transition relations of the players, and the liveness formulas induce the
winning condition for the system. The synthesis algorithm solves a
$\mu$-calculus formula with three nesting fixpoints on the game structure to
compute a winning strategy for the system.

Definition 1. A strategy is a deterministic finite state machine
${\mathcal{A}}=(\Sigma,\Sigma_{0},{\mathcal{X}},{\mathcal{Y}},\delta,\gamma_{\mathcal{X}},\gamma_{\mathcal{Y}})$
where

  * $\bullet$

$\Sigma$ is a set of states and $\Sigma_{0}\subseteq\Sigma$ is the set of
initial states.

  * $\bullet$

$\delta:\Sigma\times 2^{\mathcal{X}}\rightharpoonup\Sigma$ is the transition
function that maps a state and an input state to the next state.

  * $\bullet$

$\gamma_{\mathcal{X}}:\Sigma\to 2^{\mathcal{X}}$ maps a state to its input
state.

  * $\bullet$

$\gamma_{\mathcal{Y}}:\Sigma\to 2^{\mathcal{Y}}$ maps a state to its output
state.

For subset $V\subseteq\mathcal{V}$, let $\bigcirc
V\coloneqq\\{\bigcirc\pi\mid\pi\in V\\}$. We define the violation of safety
assumptions during strategy execution:

Definition 2. Given the safety formula $\square\psi$ where $\psi$ is a Boolean
formula over ${\mathcal{X}}\cup{\mathcal{Y}}\cup\bigcirc{\mathcal{X}}$, and a
triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
where
$\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{X}}}^{\prime}\subseteq{\mathcal{X}}$
and $\sigma_{{\mathcal{Y}}}\subseteq{\mathcal{Y}}$, the triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
violates $\square\psi$ iff
$\sigma_{{\mathcal{X}}}\cup\sigma_{{\mathcal{Y}}}\cup\bigcirc\sigma_{{\mathcal{X}}}^{\prime}\not\models\psi$.

##  III Problem Statement

This paper addresses the problem of automatically recovering from assumption
violations during the task execution.

Problem 1. Given  (i) a discrete abstraction of the environment
${\mathcal{X}}$,  (ii) a set of robot skills ${\mathcal{Y}}$, and  (iii) a
GR(1) task $\varphi_{\textrm{task}}$;  at runtime, detect violations of the
environment safety assumptions $\square\psi_{i}$ in
$\varphi_{\textrm{e}}^{\textrm{t}}=\bigwedge_{i}\square\psi_{i}$ and repair
the task, if possible.

Input: Spec. $\varphi_{\textrm{task}}$, Inverse grounding function
$\textrm{G}^{-1}$

Output: ${\tt{False}}$ if unrecoverable, otherwise the execution loop runs
indefinitely

1 ${\mathcal{A}}\coloneqq\tt{synthesize}(\varphi_{\textrm{task}})$;

2 ${\mathcal{M}}\coloneqq\tt{monitor\\_compiler(\varphi_{\textrm{task}})}$;

// Execution loop

3 while  _${\tt{True}}$_ do

4 $\sigma_{{\mathcal{X}}}\coloneqq\tt{get\\_inputs}(\textrm{G}^{-1})$;

5
$\sigma_{{\mathcal{Y}}}\coloneqq\tt{get\\_outputs}({\mathcal{A}},\sigma_{{\mathcal{X}}})$;

6 $\tt{execute}(\sigma_{{\mathcal{Y}}})$;

7 while
_$\neg\tt{finished}(\sigma_{{\mathcal{Y}}})\land(\sigma_{{\mathcal{X}}}=\tt{get\\_inputs}(\textrm{G}^{-1}))$_
do

8 continue;

9

10 end while

11
$\sigma_{{\mathcal{X}}}^{\prime}\coloneqq\tt{get\\_inputs}(\textrm{G}^{-1})$;

12
${\mathcal{I}}\coloneqq\tt{check\\_assump}({\mathcal{M}},(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime}))$;

13 if  _${\mathcal{I}}\neq\emptyset$_ then

14
$\varphi_{\textrm{task}}\coloneqq\tt{relax}(\varphi_{\textrm{task}},{\mathcal{I}},(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime}))$;

15 if  _$\tt{unrealizable}(\varphi_{\textrm{task}})$_ then

16
${\mathcal{Y}}_{\textrm{new}}\coloneqq\tt{repair}(\varphi_{\textrm{task}})$;

17 if  _${\mathcal{Y}}_{\textrm{new}}\coloneqq\emptyset$_ then

18 return ${\tt{False}}$;

19 end if

20
$\varphi_{\textrm{task}}\coloneqq\tt{add\\_skill}(\varphi_{\textrm{task}},{\mathcal{Y}}_{\textrm{new}})$;

21 ${\mathcal{A}}\coloneqq\tt{synthesize}(\varphi_{\textrm{task}})$;

22 ${\mathcal{M}}\coloneqq\tt{monitor\\_compiler(\varphi_{\textrm{task}})}$;

23

24 end if

25

26 end if

27

28 end while

Algorithm 1 Strategy Execution and Recovery

##  IV Approach

To solve Problem III, while the robot is executing strategy ${\mathcal{A}}$
synthesized from $\varphi_{\textrm{task}}$, we check whether the strategy
execution violates any environment safety assumption at every timestep. If so,
we relax the violated assumptions so that the execution no longer violates
them, and we allow the robot to resume the execution from the current state.
If the modified specification is no longer realizable, we find a set of new
skills to make it realizable.

Algorithm 1 describes our approach. Given a specification
$\varphi_{\textrm{task}}$, we use Slugs [27] to synthesize a strategy
${\mathcal{A}}$ and we generate a monitor ${\mathcal{M}}$ (Section IV-A) that
checks whether the safety assumptions are violated (lines 1-1). We then
execute the strategy in an execution loop (lines 1-1).

For each iteration of the execution loop, an inverse grounding function
$\textrm{G}^{-1}$ first gives the current input state $\sigma_{{\mathcal{X}}}$
(line 1). Given $\sigma_{{\mathcal{X}}}$, the strategy ${\mathcal{A}}$
produces an output state $\sigma_{{\mathcal{Y}}}$ (line 1). In lines 1-1, we
execute the robot skills in $\sigma_{{\mathcal{Y}}}$ and wait for either the
skills to complete the execution (i.e. the robot completed a transition in
${\mathcal{A}}$) or the input state to change (i.e. the environment changed
and we may need to change which skill the robot is activating). Next,
$\textrm{G}^{-1}$ gives the current input state
$\sigma_{{\mathcal{X}}}^{\prime}$ (line 1). Then in line 1, the monitor
${\mathcal{M}}$ checks whether the triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
violates any safety assumption and returns a set of assumptions
${\mathcal{I}}$ that are violated by the triplet (Section IV-A). If
${\mathcal{I}}$ is empty, the program jumps to line 1 and starts a new
iteration of the execution loop. If ${\mathcal{I}}$ is nonempty, in line 1 we
relax the violated assumptions in ${\mathcal{I}}$ and re-synthesize a strategy
(Section IV-B). If synthesis fails, in line 1 we leverage synthesis-based
repair [24, 25, 26] to find a set of new skills ${\mathcal{Y}}_{\textrm{new}}$
that allows the robot to complete the tasks (Section IV-C). If repair cannot
find any skills, i.e. ${\mathcal{Y}}_{\textrm{new}}=\emptyset$, the execution
terminates and we provide feedback to the user (lines 1-1). Otherwise, in
lines 1-1 we add ${\mathcal{Y}}_{\textrm{new}}$ to the specification, generate
a new strategy and the corresponding monitor, and go to line 1 to start a new
iteration.

###  IV-A Violation Detection

The violation detection procedure takes in a specification
$\varphi_{\textrm{task}}$ and a triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
where
$\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{X}}}^{\prime}\subseteq{\mathcal{X}}$
and $\sigma_{{\mathcal{Y}}}\subseteq{\mathcal{Y}}$. We use a monitor, compiled
from $\varphi_{\textrm{task}}$, to detect violations of environment safety
assumptions.

We use a compiler to translate the environment safety assumptions
$\varphi_{\textrm{e}}^{\textrm{t}}=\bigwedge_{i}\square\psi_{i}$ in
$\varphi_{\textrm{task}}$ into a monitor ${\mathcal{M}}$. The compiler first
uses a tokenizer and a parser to translate $\varphi_{\textrm{e}}^{\textrm{t}}$
into a set of Abstract Syntax Trees (ASTs) [28]. Each AST represents a Boolean
formula $\psi_{i}$ in a tree structure according to the syntax of the
specifications [27]. Then the compiler translates the ASTs to a set of Boolean
constraints for the SAT solver Z3 [29], which is then used to check whether
any safety assumptions are violated. In Example I, the compiler translates
$\pi_{{obs}}^{{wlkwy}}\to\bigcirc\pi_{{obs}}^{{wlkwy}}$ to the AST in Fig. 3
and creates the Boolean expression
$\tt{Implies}$$(\pi_{{obs}}^{{wlkwy}},\bigcirc\pi_{{obs}}^{{wlkwy}})$ in the
Z3 format.

Figure 3: Abstract Syntax Tree for
$\pi_{{obs}}^{{wlkwy}}\to\bigcirc\pi_{{obs}}^{{wlkwy}}$.

The monitor ${\mathcal{M}}$ uses the triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
to evaluate the environment safety assumption
$\varphi_{\textrm{e}}^{\textrm{t}}$. For each safety assumption
$\square\psi_{i}$, the monitor evaluates the truth value of the Boolean
formula $\psi_{i}$ given the literal values indicated by the triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$.
In practice, the monitor creates the following Boolean formula for each
assumption $\square\psi_{i}$:

$\begin{split}\psi_{i}^{\textrm{check}}\coloneqq\psi_{i}\land\bigwedge_{x\in\sigma_{{\mathcal{X}}}}x\land\bigwedge_{x\in{\mathcal{X}}\setminus\sigma_{{\mathcal{X}}}}\neg
x\land\bigwedge_{y\in\sigma_{{\mathcal{Y}}}}y\land\bigwedge_{y\in{\mathcal{Y}}\setminus\sigma_{{\mathcal{Y}}}}\neg
y\land\\\ \bigwedge_{x\in\sigma_{{\mathcal{X}}}^{\prime}}\bigcirc
x\land\bigwedge_{x\in{\mathcal{X}}\setminus\sigma_{{\mathcal{X}}}^{\prime}}\neg\bigcirc
x\end{split}$ (1)

The monitor uses the SMT solver Z3 [29] to compute the satisfiability of
Formula 1, which indicates whether the triplet violates the assumption
$\square\psi_{i}$ or not. The monitor returns a set of violated assumptions
${\mathcal{I}}\coloneqq\\{\square\psi_{i}\mid(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})\text{
violates }\square\psi_{i}\\}$.

In Example I, when the obstacle moves from Walkway to Aisle,
$\sigma_{{\mathcal{X}}}=\\{\pi_{{robot}}^{{assm}},\pi_{{obs}}^{{wlkwy}}\\}$,
$\sigma_{{\mathcal{Y}}}=\\{move_{1}\\}$,
$\sigma_{{\mathcal{X}}}^{\prime}=\\{\pi_{{robot}}^{{assm}},\pi_{{obs}}^{{aisle}}\\}$.
For $\psi_{i}=\pi_{{obs}}^{{wlkwy}}\to\bigcirc\pi_{{obs}}^{{wlkwy}}$,
$\psi_{i}^{\textrm{check}}$ in Formula 1 is unsatisfiable, therefore
${\mathcal{I}}=\\{\square(\pi_{{obs}}^{{wlkwy}}\to\bigcirc\pi_{{obs}}^{{wlkwy}})\\}$.

###  IV-B Assumption Relaxation

The assumption relaxation procedure takes in a specification
$\varphi_{\textrm{task}}$, a set of violated environment safety assumptions
${\mathcal{I}}$, and a triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
that violates the assumptions in ${\mathcal{I}}$. The procedure relaxes the
violated assumptions in ${\mathcal{I}}$ to admit the violated transition
indicated by the triplet. The procedure follows Environment Characterization
(EC) in [21, 22], which relaxes the assumptions solely using input states. In
contrast to EC, our procedure utilizes the complete observation triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
to rewrite violated assumptions. Consequently, our procedure can handle the
discovery of previously unknown nondeterminism in robot skills by
incorporating the nondeterminism into the skill abstraction. In addition, our
procedure allows the robot to resume the execution in the current input state
and continue to attempt the latest liveness goal.

Recall that we split the environment safety assumptions
$\varphi_{\textrm{e}}^{\textrm{t}}=\bigwedge_{i}\square\psi_{i}$ into the
skill assumptions $\varphi_{\textrm{e}}^{\textrm{t,skill}}$, which describe
the postconditions of the skills, and the hard assumptions
$\varphi_{\textrm{e}}^{\textrm{t,hard}}$, which cannot be modified by the
repair procedure in Section IV-C. For each violated assumption
$\square\psi_{i}$ in $\varphi_{\textrm{e}}^{\textrm{t,hard}}$, the procedure
replaces $\square\psi_{i}$ with
$\square(\psi_{i}\lor\psi_{\textrm{r}}^{\textrm{hard}})$ where
$\psi_{\textrm{r}}^{\textrm{hard}}$ is the following formula:

$\begin{split}\psi_{\textrm{r}}^{\textrm{hard}}\coloneqq\bigwedge_{x\in\sigma_{{\mathcal{X}}}}x\land\bigwedge_{x\in{\mathcal{X}}\setminus\sigma_{{\mathcal{X}}}}\neg
x\land\bigwedge_{y\in\sigma_{{\mathcal{Y}}}}y\land\bigwedge_{y\in{\mathcal{Y}}\setminus\sigma_{{\mathcal{Y}}}}\neg
y\land\\\ \bigwedge_{x\in\sigma_{{\mathcal{X}}}^{\prime}}\bigcirc
x\land\bigwedge_{x\in{\mathcal{X}}\setminus\sigma_{{\mathcal{X}}}^{\prime}}\neg\bigcirc
x\end{split}$ (2)

For each violated assumption $\square\psi_{i}$ in
$\varphi_{\textrm{e}}^{\textrm{t,skill}}$, the procedure replaces the
assumption $\square\psi_{i}$ with
$\square(\psi_{i}\lor\psi_{\textrm{r}}^{\textrm{skill}})$ where
$\psi_{\textrm{r}}^{\textrm{skill}}$ is shown in Formula 3. Intuitively, both
formulas add the observed behavior, using disjunction, to the assumptions,
thereby allowing for more environment behaviors. The difference between
Formula 3 and 2 is that the former only adds the controllable inputs, and the
latter adds all inputs. The reason for this distinction is that skill
abstractions are defined solely over controllable inputs, so we can only
modify them with controllable inputs, whereas the hard assumptions
$\varphi_{\textrm{e}}^{\textrm{t,hard}}$ are defined over all inputs.

$\begin{split}\psi_{\textrm{r}}^{\textrm{skill}}\coloneqq\bigwedge_{x\in\sigma_{{\mathcal{X}}}\cap{\mathcal{X}}_{\textrm{c}}}x\land\bigwedge_{x\in{\mathcal{X}}_{\textrm{c}}\setminus\sigma_{{\mathcal{X}}}}\neg
x\land\bigwedge_{y\in\sigma_{{\mathcal{Y}}}}y\land\bigwedge_{y\in{\mathcal{Y}}\setminus\sigma_{{\mathcal{Y}}}}\neg
y\land\\\
\bigwedge_{x\in\sigma_{{\mathcal{X}}}^{\prime}\cap{\mathcal{X}}_{\textrm{c}}}\bigcirc
x\land\bigwedge_{x\in{\mathcal{X}}_{\textrm{c}}\setminus\sigma_{{\mathcal{X}}}^{\prime}}\neg\bigcirc
x\end{split}$ (3)

Figure 4: Workflow of the assumption relaxation procedure.

Fig. 4 depicts the workflow of the relaxation procedure in practice. We relax
the violated assumptions by modifying the ASTs in the monitor compiler
(Section IV-A) according to Formulas 2 and 3. The compiler then generates the
new specification by recursively visiting every node in the modified ASTs and
generating the corresponding LTL formula.

Before generating the new specification, we set the initial input condition
$\varphi_{\textrm{e}}^{\textrm{i}}$ to be the current input state
$\sigma_{{\mathcal{X}}}^{\prime}$, as shown in Formula 4. Doing so allows the
robot to resume the task execution in the current input state.

$\varphi_{\textrm{e}}^{\textrm{i}}\coloneqq\bigwedge_{x\in\sigma_{{\mathcal{X}}}^{\prime}}x\land\bigwedge_{x\in{\mathcal{X}}\setminus\sigma_{{\mathcal{X}}}^{\prime}}\neg
x$ (4)

Moreover, we reorder the liveness goals to allow the robot to attempt the
latest goal first. Recall the liveness goal formula
$\varphi_{\textrm{s}}^{\textrm{g}}=\bigwedge_{i=1}^{m}\square\lozenge J_{i}$.
Suppose the strategy attempts to satisfy the $j^{\textrm{th}}$ liveness goal
$J_{j}$ before the violation happens. Since the synthesized strategy loops
through the liveness goals in a cyclic manner [7], we reorder
$\varphi_{\textrm{s}}^{\textrm{g}}$ by moving $J_{j}\dots J_{m}$ to the front
of $\varphi_{\textrm{s}}^{\textrm{g}}$.

###  IV-C Repair

The repair procedure takes in an unrealizable specification
$\varphi_{\textrm{task}}$ and the abstraction $({\mathcal{X}},{\mathcal{Y}})$.
We find a set of new skills ${\mathcal{Y}}_{\textrm{new}}$ and modify the
specification $\varphi_{\textrm{task}}$ based on the new abstraction
$({\mathcal{X}},{\mathcal{Y}}\cup{\mathcal{Y}}_{\textrm{new}})$ such that the
new specification includes the new skills ${\mathcal{Y}}_{\textrm{new}}$ and
is realizable.

We leverage the synthesis-based repair approach proposed in [24, 25, 26] to
find a set of new skills. The algorithm suggests new skills by alternating two
procedures:

  1. 1.

Modify-Preconditions. Randomly select an existing skill transition such that
the robot can satisfy the task from its postcondition. Modify the precondition
of the transition to a random new state from which the robot cannot satisfy
the task before the modification.

  2. 2.

Modify-Postconditions. Randomly select an existing skill transition such that
the robot cannot satisfy the task from either the pre- or postcondition of the
transition. Modify the postcondition to a random new state from which the
robot can satisfy the task.

In this work we change the Modify-Preconditions algorithm from [24, 25, 26] to
improve the efficiency of repair. Repair can be inefficient since both
modifying the pre- and postconditions involves randomly selecting a transition
and a new state. In Modify-Precondition, suppose the original precondition is
an intermediate state of a skill. Repair ensures that the new precondition is
reachable from the initial precondition of the skill by adding a transition
from the precondition of the original precondition (pre-precondition) to the
new precondition. However, even if the robot can satisfy the task from the new
precondition after the modification, the robot still cannot satisfy the task
from the pre-precondition because it has a nondeterministic transition to the
old precondition. We remove the transition from the pre-precondition to the
old precondition, allowing the robot to satisfy the task from the pre-
precondition. In Example I, the original Modify-Precondition algorithm returns
a symbolic skill $move^{\prime}$ which goes from $\pi_{{robot}}^{{assm}}$
nondeterministically to either $\pi_{{robot}}^{{wlkwy}}$ or
$\pi_{{robot}}^{{aisle}}$, and from $\pi_{{robot}}^{{wlkwy}}$ to
$\pi_{{robot}}^{{load}}$. Because of the nondeterminism, the robot cannot
guarantee it will reach Loading and requires further refinement of the skills.
Our approach returns the skill $move_{2}$, which goes from
$\pi_{{robot}}^{{assm}}$ to $\pi_{{robot}}^{{wlkwy}}$ to
$\pi_{{robot}}^{{load}}$, in one iteration of the repair.

Given a set of suggested skills ${\mathcal{Y}}_{\textrm{new}}$ from the repair
algorithm, in order to decrease the size of the abstraction, we attempt to
remove unnecessary skills in ${\mathcal{Y}}_{\textrm{new}}$. For each skill
$y\in{\mathcal{Y}}_{\textrm{new}}$, we remove $y$ from
${\mathcal{Y}}_{\textrm{new}}$ and check whether the specification with the
updated ${\mathcal{Y}}_{\textrm{new}}$ is realizable. If the result is
realizable, then we remove the skill $y$ permanently. Otherwise, we add the
skill $y$ back to the set of new skills.

We physically implement the new symbolic skills using a motion planner [30].
If we cannot physically implement a symbolic skill, we incorporate the skill
as a repair constraint, as done in [26], and continue the repair process.

Figure 5: Stretch moving $\tt{cup}$ between tables. The task is
$\square\lozenge(\pi_{{empty}}\to\pi_{{cup}}^{{t_{2}}})\land\square\lozenge(\neg\pi_{{empty}}\to\pi_{{cup}}^{{t_{4}}})$.
(A) Physical workspace. (B) Initial positions of the objects. (C) Original
behavior of the synthesized strategy. Arrows represent the motion of the
objects, orange: $\tt{block}$, grey: $\tt{cup}$, green: $\tt{base}$. The
numbers represent the order of their movements. (D) Recovery from Violation 1
where $\tt{stone}$ moves from $t_{0}$ to $t_{3}$. (E) Recovery from Violation
2 where $\tt{cup}$ becomes empty in $x_{2}$. (F) Recovery from Violation 3
where $\tt{cone}$ moves from $x_{3}$ to $x_{2}$. In (D)-(F), red dashed arrows
represent the violations and blue solid arrows represent the new skills.

##  V Demonstration

We demonstrate our approach by employing a Hello Robot Stretch [31] in a
factory-like setting. We present the abstraction, the tasks, and three
assumption violations and their recoveries within one run of the task
execution. We perform the computations (synthesis and repair) on a Linux
desktop with a 2.3GHz 8-core AMD RyzenTM-7 CPU. We run our framework on the
desktop and send control inputs to Stretch through ROS. We open-source the
code for our framework and
demonstration111https://github.com/MartinMeng008/env_repair. A video of the
demonstration is available at: https://youtu.be/OTUEyqQfQQs.

###  V-A Setting

Example 2. The robot is asked to repeatably bring a cup to a loading table if
the cup is empty and bring the cup to an assembly table if the cup is full,
while avoiding collisions with the block, the stone, and the cone (see Fig.
5A).

Abstraction. We partition the continuous workspace into a set of rectangular
regions ${\mathcal{R}}\coloneqq\\{x_{0},\dots,x_{4},t_{0},\dots,t_{4}\\}$,
where $x_{i}$ represents a region on the ground, and $t_{i}$ represents a
region on a table, as illustrated in Fig. 5B. The set of objects
${\mathcal{O}}$ includes the robot $\tt{base}$, the controllable $\tt{cup}$,
the controllable obstacle $\tt{block}$, and the uncontrollable obstacles
$\tt{cone}$ and $\tt{stone}$ (see Fig. 5A). We represent the state of the cup
(empty or full) using $\pi_{{empty}}$. For the objects that can be moved by
the robot ($\tt{cup,block}$), we add propositions indicating whether they are
in the robot end effector or not ($\pi_{{cup}}^{{ee}},\pi_{{block}}^{{ee}}$).
We define the set of input propositions as
${\mathcal{X}}\coloneqq\\{\pi_{{o}}^{{r}}\mid
o\in{\mathcal{O}},r\in{\mathcal{R}}\\}\cup\\{\pi_{{empty}},\pi_{{cup}}^{{ee}},\pi_{{block}}^{{ee}}\\}$.
We ground each input $\pi_{{o}}^{{r}}$ by
$\textrm{G}(\pi_{{o}}^{{r}})\coloneqq\\{x\mid\tt{pose}(x,o)\in\tt{region}(r)\\}$.
For $o\in\\{\tt{cup},\tt{block}\\}$,
$\textrm{G}(\pi_{{o}}^{{ee}})\coloneqq\\{x\mid\left\lVert\tt{pose}(x,o)-\tt{default\\_pose}(x,ee)\right\rVert<\epsilon\\}$
for some small $\epsilon$. We use an OptiTrack motion capture system to
determine the positions of the objects and the robot. We control the value of
input $\pi_{{empty}}$, indicating whether the cup is empty or not, through a
keyboard interface.

Skills. The robot has two mobile skills: $\tt{move_{1}}$ goes from
$\pi_{{base}}^{{x_{0}}}$ to $\pi_{{base}}^{{x_{2}}}$ to
$\pi_{{base}}^{{x_{4}}}$, and $\tt{move_{2}}$ goes from
$\pi_{{base}}^{{x_{4}}}$ to $\pi_{{base}}^{{x_{2}}}$ to
$\pi_{{base}}^{{x_{0}}}$, while other controllable inputs remain unchanged.
The robot has six manipulation skills: $\tt{pick_{1}}$ goes from
$\pi_{{cup}}^{{t_{2}}}$ to $\pi_{{cup}}^{{ee}}$, $\tt{pick_{2}}$ goes from
$\pi_{{cup}}^{{t_{4}}}$ to $\pi_{{cup}}^{{ee}}$, $\tt{pick_{3}}$ goes from
$\pi_{{block}}^{{t_{1}}}$ to $\pi_{{block}}^{{ee}}$, $\tt{place_{1}}$ goes
from $\pi_{{cup}}^{{ee}}$ to $\pi_{{cup}}^{{t_{2}}}$, $\tt{place_{2}}$ goes
from $\pi_{{cup}}^{{ee}}$ to $\pi_{{cup}}^{{t_{4}}}$, and $\tt{place_{3}}$
goes from $\pi_{{block}}^{{ee}}$ to $\pi_{{block}}^{{t_{3}}}$, while other
controllable inputs remain unchanged.

Tasks. The task is
$\varphi_{\textrm{s}}^{\textrm{g}}=\square\lozenge(\pi_{{empty}}\to\pi_{{cup}}^{{t_{2}}})\land\square\lozenge(\neg\pi_{{empty}}\to\pi_{{cup}}^{{t_{4}}})$;
when the cup is empty, the robot should place it on the loading table $t_{2}$,
and when the cup is full, the robot should place it on the assembly table
$t_{4}$.

Initialization. As shown in Fig. 5B, the robot starts in $x_{4}$
($\pi_{{base}}^{{x_{4}}}$), the uncontrollable $\tt{cone}$ is in $x_{3}$
($\pi_{{cone}}^{{x_{3}}}$), the uncontrollable $\tt{stone}$ is in $t_{0}$
($\pi_{{stone}}^{{t_{0}}}$), the controllable $\tt{block}$ is in $t_{1}$
($\pi_{{block}}^{{t_{1}}}$), and the controllable $\tt{cup}$ is in $t_{2}$
($\pi_{{cup}}^{{t_{2}}}$). The cup is initially empty ($\pi_{{empty}}$).

Constraints. The robot is required to satisfy the following safety constraints
during the task execution:

  1. 1)

A region can contain only one object at a time:
$\square\neg(\pi_{{o_{1}}}^{{r}}\land\pi_{{o_{2}}}^{{r}})\land\square\neg(\bigcirc\pi_{{o_{1}}}^{{r}}\land\bigcirc\pi_{{o_{2}}}^{{r}})$
for any objects $o_{1},o_{2}\in{\mathcal{O}}$ and region
$r\in{\mathcal{R}}\cup\\{ee\\}$.

  2. 2)

Since $\tt{block}$ is tall, the robot cannot pick up $\tt{cup}$ from $t_{2}$
if $\tt{block}$ is in $t_{1}$:
$\square(\pi_{{block}}^{{t_{1}}}\land\pi_{{cup}}^{{t_{2}}}\to\neg\bigcirc\pi_{{cup}}^{{ee}})$.

  3. 3)

We do not allow the robot to enter the assembly area $x_{0}$ with an empty
cup, nor enter the loading area $x_{4}$ with a full cup:
$\square(\pi_{{cup}}^{{ee}}\land\pi_{{empty}}\land\neg\pi_{{base}}^{{x_{0}}}\to\neg\bigcirc\pi_{{base}}^{{x_{0}}})\land\square(\pi_{{cup}}^{{ee}}\land\neg\pi_{{empty}}\land\neg\pi_{{base}}^{{x_{4}}}\to\neg\bigcirc\pi_{{base}}^{{x_{4}}})$.

Assumptions. We make the following environment safety assumptions to ensure
the specification is realizable:

  1. 1)

We assume that the uncontrollable obstacles are static:
$\square(\pi_{{o}}^{{r}}\to\bigcirc\pi_{{o}}^{{r}})$ for
$o\in\\{\tt{cone},\tt{stone}\\}$ and $r\in{\mathcal{R}}$.

  2. 2)

We assume that if the status of the cup changed from empty to full then it was
in $t_{2}$, and if it changed from full to empty it was in $t_{4}$:
$\square(\pi_{{empty}}\land\neg\bigcirc\pi_{{empty}}\to\pi_{{cup}}^{{t_{2}}})\land\square(\neg\pi_{{empty}}\land\bigcirc\pi_{{empty}}\to\pi_{{cup}}^{{t_{4}}})$.

Behavior. We synthesize a strategy and execute it with the Stretch robot, as
illustrated in Fig. 5C. Initially, while $\tt{cup}$ is empty, the robot does
not move. When $\tt{cup}$ is full, the robot first executes $\tt{pick_{3}}$
and $\tt{place_{3}}$ to pick up $\tt{block}$ from $t_{1}$ and place it in
$t_{3}$. Then the robot executes $\tt{pick_{1}}$, $\tt{move_{2}}$, and
$\tt{place_{2}}$ sequentially to pick up $\tt{cup}$ from $t_{2}$, move to
$x_{2}$ and then $x_{0}$, and place $\tt{cup}$ in $t_{4}$. While $\tt{cup}$
remains full the robot does not move. Once $\tt{cup}$ becomes empty, the robot
executes $\tt{pick_{2}}$, $\tt{move_{1}}$, and $\tt{place_{1}}$ sequentially
to pick up $\tt{cup}$ from $t_{4}$, move to $x_{2}$ and then $x_{4}$, and
finally place $\tt{cup}$ back in $t_{2}$. This behavior continues
indefinitely.

###  V-B Unexpected Obstacle Behavior - Stone

Violation 1. In Fig. 5D, after $\tt{cup}$ is full and the robot starts to
execute $\tt{pick_{3}}$, the uncontrollable $\tt{stone}$ is moved from
$t_{0}$, violating Assumption 1 ($\tt{stone}$ is static). The previous input
state is $\sigma_{{\mathcal{X}}}=\\{$ $\pi_{{cup}}^{{t_{2}}},$
$\pi_{{base}}^{{x_{4}}},$ $\pi_{{cone}}^{{x_{3}}},$ $\pi_{{block}}^{{t_{1}}},$
$\pi_{{stone}}^{{t_{0}}}\\}$, the previous output state is
$\sigma_{{\mathcal{Y}}}=\\{\tt{pick_{3}}\\}$, and the current input state is
$\sigma_{{\mathcal{X}}}^{\prime}=\\{\pi_{{cup}}^{{t_{2}}},$
$\pi_{{base}}^{{x_{4}}},$ $\pi_{{cone}}^{{x_{3}}},$ $\pi_{{block}}^{{t_{1}}},$
$\pi_{{stone}}^{{t_{3}}}\\}$.

The monitor detects that the triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
violates the assumption
$\varphi_{\textrm{violated}}=\square(\pi_{{stone}}^{{t_{0}}}\to\bigcirc\pi_{{stone}}^{{t_{0}}})$
and terminates the execution of $\tt{pick_{3}}$. The relaxation procedure took
0.4 seconds to relax $\varphi_{\textrm{violated}}$ with the triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
according to Formula 2. The specification becomes unrealizable because
$\tt{stone}$ is in $t_{3}$, preventing the robot from executing
$\tt{place_{3}}$ to place $\tt{block}$ in $t_{3}$. The repair took 16 seconds
to suggest a skill $\tt{place_{4}}$ that goes from $\pi_{{block}}^{{ee}}$ to
$\pi_{{block}}^{{t_{0}}}$ while other controllable inputs remain unchanged.

The framework took 1.1 seconds to synthesize a new strategy and the robot
follows the strategy to execute $\tt{pick_{3}}$ and $\tt{place_{4}}$
sequentially to pick up $\tt{block}$ and place it in $t_{0}$. The robot then
executes $\tt{pick_{1}}$ to pick up $\tt{cup}$ from $t_{2}$ and resumes the
behavior as described in Section V-A.

###  V-C Unexpected User Input Change

Violation 2. In Fig. 5E, After the robot picks up $\tt{cup}$, the robot
executes $\tt{move_{2}}$ to move from $x_{4}$ to $x_{0}$ through $x_{2}$. When
the robot is in $x_{2}$, $\tt{cup}$ becomes empty, violating Assumption 2 (the
status of $\tt{cup}$ can only change when $\tt{cup}$ is in $t_{2}$ or
$t_{4}$). The previous input state is $\sigma_{{\mathcal{X}}}=\\{$
$\pi_{{cup}}^{{ee}},$ $\pi_{{base}}^{{x_{2}}},$ $\pi_{{cone}}^{{x_{3}}},$
$\pi_{{block}}^{{t_{0}}},$ $\pi_{{stone}}^{{t_{3}}}\\}$, the previous output
state is $\sigma_{{\mathcal{Y}}}=\\{\tt{move_{2}}\\}$, and the current input
state is $\sigma_{{\mathcal{X}}}^{\prime}=\\{\pi_{{cup}}^{{ee}},$
$\pi_{{base}}^{{x_{2}}},$ $\pi_{{cone}}^{{x_{3}}},$ $\pi_{{block}}^{{t_{0}}},$
$\pi_{{stone}}^{{t_{3}}},$ $\pi_{{empty}}\\}$.

The monitor detects that the triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
violates the assumption $\varphi_{\textrm{violated}}=$
$\square(\neg\pi_{empty}\land\bigcirc\pi_{empty}\to\pi_{{cup}}^{{t_{4}}})$ and
terminates the execution of $\tt{move_{2}}$. The relaxation procedure took 0.4
seconds to relax the violated assumption $\varphi_{\textrm{violated}}$ with
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
according to Formula 2. The specification becomes unrealizable because the
robot is in $x_{2}$ with no existing skill having an initial precondition in
$x_{2}$, and the robot cannot continue executing $\tt{move_{2}}$ to reach
$x_{0}$, because bringing the empty cup to $x_{0}$ violates Constraint 3. The
repair took 10.7 seconds to suggest two skills: $\tt{move_{3}}$ goes from
$\pi_{{base}}^{{x_{2}}}$ to $\pi_{{base}}^{{x_{1}}}$ and $\tt{move_{4}}$ goes
from $\pi_{{base}}^{{x_{1}}}$ to $\pi_{{base}}^{{x_{4}}}$ while other
controllable inputs remain unchanged. In this particular run, the suggestion
is not minimal due to the inherent randomness in repair. In another run, the
repair took 38 seconds to provide a minimal suggestion containing only a
single skill that goes from $\pi_{{base}}^{{x_{2}}}$ to
$\pi_{{base}}^{{x_{4}}}$.

The framework took 1.4 seconds to synthesize a new strategy in which the robot
executes $\tt{move_{3}}$, $\tt{move_{4}}$ and $\tt{place_{1}}$ sequentially to
move from $x_{2}$ to $x_{1}$ and then $x_{4}$, and place $\tt{cup}$ back to
$t_{2}$. The robot does not move until $\tt{cup}$ becomes full again and
resumes the execution as described in Section V-A.

###  V-D Unexpected Obstacle Behavior - Cone

Violation 3. In Fig. 5F, after $\tt{cup}$ becomes full and the robot executes
$\tt{pick_{1}}$, the robot holds the cup and executes $\tt{move_{2}}$ to drive
from $x_{4}$ to $x_{0}$ through $x_{2}$. When the robot is still in $x_{4}$,
$\tt{cone}$ is moved from $x_{3}$ to $x_{2}$, violating Assumption 1
($\tt{cone}$ should be static). The previous input state is
$\sigma_{{\mathcal{X}}}=\\{$ $\pi_{{cup}}^{{ee}},$ $\pi_{{base}}^{{x_{4}}},$
$\pi_{{cone}}^{{x_{3}}},$ $\pi_{{block}}^{{t_{0}}},$
$\pi_{{stone}}^{{t_{3}}}\\}$, the previous output state is
$\sigma_{{\mathcal{Y}}}=\\{\tt{move_{2}}\\}$, and the current input state is
$\sigma_{{\mathcal{X}}}^{\prime}=\\{$ $\pi_{{cup}}^{{ee}},$
$\pi_{{base}}^{{x_{4}}},$ $\pi_{{cone}}^{{x_{2}}},$ $\pi_{{block}}^{{t_{0}}},$
$\pi_{{stone}}^{{t_{3}}}\\}$.

The monitor detects that the triplet
$(\sigma_{{\mathcal{X}}},\sigma_{{\mathcal{Y}}},\sigma_{{\mathcal{X}}}^{\prime})$
violates the assumption
$\varphi_{\textrm{violated}}=\square(\pi_{{cone}}^{{x_{3}}}\to\bigcirc\pi_{{cone}}^{{x_{3}}})$
and terminates the execution of $\tt{move_{2}}$. The relaxation procedure took
0.5 seconds to relax the violated assumption $\varphi_{\textrm{violated}}$
with the triplet according to Formula 2. The specification becomes
unrealizable because Constraint 1 prohibits the robot from entering $x_{2}$
and both $\tt{move_{1}}$ and $\tt{move_{2}}$ pass through $x_{2}$. The repair
took 1 minute and 35 seconds to suggest three skills: $\tt{move_{5}}$ goes
from $\pi_{{base}}^{{4}}$ to $\pi_{{base}}^{{1}}$ to $\pi_{{base}}^{{0}}$,
$\tt{move_{6}}$ goes from $\pi_{{base}}^{{0}}$ to $\pi_{{base}}^{{3}}$, and
$\tt{move_{7}}$ goes from $\pi_{{base}}^{{3}}$ to $\pi_{{base}}^{{4}}$, while
other controllable inputs do not change.

The framework took 2.6 seconds to synthesize a new strategy which behaves the
same as the original strategy (Section V-A) except that it replaces
$\tt{move_{2}}$ with $\tt{move_{5}}$ and $\tt{move_{1}}$ with $\tt{move_{6}}$
and $\tt{move_{7}}$. The robot executes $\tt{move_{5}}$ and $\tt{place_{2}}$
sequentially to reach $x_{0}$ through $x_{1}$ and place $\tt{cup}$ in $t_{4}$.
When $\tt{cup}$ becomes empty, the robot executes $\tt{pick_{2}}$,
$\tt{move_{6}}$, $\tt{move_{7}}$, and $\tt{place_{1}}$ in sequence to pick up
$\tt{cup}$ from $t_{4}$, reach $x_{4}$ through $x_{3}$, and place $\tt{cup}$
in $t_{2}$.

##  VI Conclusion

We provide a framework for automatically recovering from assumption violations
of temporal logic specifications. To do so we detect the assumption violations
during the robot execution, relax the violated assumptions to admit the
observed environment behavior, and add new robot skills for the robot to
complete the tasks. We demonstrate our approach with a physical robot in a
factory-like scenario.

There are assumption violations, however, from which our approach cannot
recover. If assumptions about the postconditions of skills are violated due to
faulty low-level robot controllers, then repair at the symbolic level cannot
solve the problem. In Example I, our framework cannot recover from the
violation if the low-level controller cannot reliably implement the new skill
$move_{2}$ due to severe localization error and uncertainty in Walkway.
Moreover, if an assumption violation results in the robot’s current state
violating its hard safety constraints, then no new skills can repair the task
from that violating state. In Example I, if the obstacle moves to Aisle when
the robot is already in Aisle, our approach cannot repair because the current
state violates the safety constraint which prohibits the robot and the
obstacle from being in the same region. In future work, we plan to tackle the
violations that our approach cannot repair, develop local repair to improve
the computational efficiency of our approach, and extend our framework to
multi-agent and human-robot interaction settings where assumptions about human
behaviors may be violated.

## References

  * [1] H. Kress-Gazit, M. Lahijanian, and V. Raman, “Synthesis for robots: Guarantees and feedback for robot behavior,” Annual Review of Control, Robotics, and Autonomous Systems, vol. 1, pp. 211–236, 2018.
  * [2] K. He, M. Lahijanian, L. E. Kavraki, and M. Y. Vardi, “Automated abstraction of manipulation domains for cost-based reactive synthesis,” IEEE Robotics and Automation Letters, vol. 4, no. 2, pp. 285–292, 2019.
  * [3] T. Silver, R. Chitnis, N. Kumar, W. McClinton, T. Lozano-Pérez, L. Kaelbling, and J. B. Tenenbaum, “Predicate invention for bilevel planning,” in Proceedings of the AAAI Conference on Artificial Intelligence, vol. 37, pp. 12120–12129, 2023.
  * [4] G. Konidaris, L. P. Kaelbling, and T. Lozano-Perez, “From skills to symbols: Learning symbolic representations for abstract high-level planning,” Journal of Artificial Intelligence Research, vol. 61, pp. 215–289, 2018.
  * [5] A. Ahmetoglu, M. Y. Seker, J. Piater, E. Oztop, and E. Ugur, “Deepsym: Deep symbol generation and rule learning for planning from unsupervised robot interaction,” Journal of Artificial Intelligence Research, vol. 75, pp. 709–745, 2022.
  * [6] E. Clarke, O. Grumberg, and D. Peled, Model Checking.  The MIT Press, 2000.
  * [7] R. Bloem, B. Jobstmann, N. Piterman, A. Pnueli, and Y. Sa’ar, “Synthesis of reactive (1) designs,” Journal of Computer and System Sciences, vol. 78, no. 3, pp. 911–938, 2012.
  * [8] G. E. Fainekos, “Revising temporal logic specifications for motion planning,” in 2011 IEEE International Conference on Robotics and Automation (ICRA), pp. 40–45, IEEE, 2011.
  * [9] W. Li, L. Dworkin, and S. A. Seshia, “Mining assumptions for synthesis,” in Ninth ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011), pp. 43–50, IEEE, 2011.
  * [10] V. Raman and H. Kress-Gazit, “Explaining impossible high-level robot behaviors,” IEEE Transactions on Robotics, vol. 29, no. 1, pp. 94–104, 2012.
  * [11] M. Guo, K. H. Johansson, and D. V. Dimarogonas, “Revising motion planning under linear temporal logic specifications in partially known workspaces,” in 2013 IEEE International Conference on Robotics and Automation (ICRA), pp. 5025–5032, IEEE, 2013.
  * [12] R. Alur, S. Moarref, and U. Topcu, “Counter-strategy guided refinement of gr (1) temporal logic specifications,” in 2013 Formal Methods in Computer-Aided Design, pp. 26–33, IEEE, 2013.
  * [13] R. Ehlers, R. Könighofer, and R. Bloem, “Synthesizing cooperative reactive mission plans,” in 2015 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 3478–3485, IEEE, 2015.
  * [14] R. Majumdar, N. Piterman, and A.-K. Schmuck, “Environmentally-friendly GR(1) synthesis,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 229–246, Springer, 2019.
  * [15] A. Jones, Z. Kong, and C. Belta, “Anomaly detection in cyber-physical systems: A formal methods approach,” in 53rd IEEE Conference on Decision and Control, pp. 848–853, IEEE, 2014.
  * [16] Z. Kong, A. Jones, and C. Belta, “Temporal logics for learning and detection of anomalous behavior,” IEEE Transactions on Automatic Control, vol. 62, no. 3, pp. 1210–1222, 2016.
  * [17] S. C. Livingston, R. M. Murray, and J. W. Burdick, “Backtracking temporal logic synthesis for uncertain environments,” in 2012 IEEE International Conference on Robotics and Automation (ICRA), pp. 5163–5170, IEEE, 2012.
  * [18] S. C. Livingston, P. Prabhakar, A. B. Jose, and R. M. Murray, “Patching task-level robot controllers based on a local $\mu$-calculus formula,” in 2013 IEEE International Conference on Robotics and Automation (ICRA), pp. 4588–4595, IEEE, 2013.
  * [19] M. Lahijanian, M. R. Maly, D. Fried, L. E. Kavraki, H. Kress-Gazit, and M. Y. Vardi, “Iterative temporal planning in uncertain environments with partial satisfaction guarantees,” IEEE Transactions on Robotics, vol. 32, no. 3, pp. 583–599, 2016.
  * [20] Y. Kantaros, M. Malencia, V. Kumar, and G. J. Pappas, “Reactive temporal logic planning for multiple robots in unknown environments,” in 2020 IEEE International Conference on Robotics and Automation (ICRA), pp. 11479–11485, IEEE, 2020.
  * [21] K. W. Wong, R. Ehlers, and H. Kress-Gazit, “Correct high-level robot behavior in environments with unexpected events.,” in Robotics: Science and Systems, p. 1, 2014.
  * [22] K. W. Wong, R. Ehlers, and H. Kress-Gazit, “Resilient, provably-correct, and high-level robot behaviors,” IEEE Transactions on Robotics, vol. 34, no. 4, pp. 936–952, 2018.
  * [23] R. Baran, X. Tan, P. Varnai, P. Yu, S. Ahlberg, M. Guo, W. S. Cortez, and D. V. Dimarogonas, “A ROS package for human-in-the-loop planning and control under linear temporal logic tasks,” in 2021 IEEE 17th International Conference on Automation Science and Engineering (CASE), pp. 2182–2187, IEEE, 2021.
  * [24] A. Pacheck, S. Moarref, and H. Kress-Gazit, “Finding missing skills for high-level behaviors,” in 2020 IEEE International Conference on Robotics and Automation (ICRA), pp. 10335–10341, IEEE, 2020.
  * [25] A. Pacheck, S. James, G. Konidaris, and H. Kress-Gazit, “Automatic encoding and repair of reactive high-level tasks with learned abstract representations,” The International Journal of Robotics Research, vol. 42, no. 4-5, pp. 263–288, 2023.
  * [26] A. Pacheck and H. Kress-Gazit, “Physically feasible repair of reactive, linear temporal logic-based, high-level tasks,” IEEE Transactions on Robotics, 2023.
  * [27] R. Ehlers and V. Raman, “Slugs: Extensible GR(1) synthesis,” in Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II 28, pp. 333–339, Springer, 2016.
  * [28] V. A. Alfred, S. L. Monica, and D. U. Jeffrey, Compilers Principles, Techniques & Tools.  Pearson Education, 2007.
  * [29] L. De Moura and N. Bjørner, “Z3: An efficient SMT solver,” in International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340, Springer, 2008.
  * [30] L. E. Kavraki, P. Svestka, J.-C. Latombe, and M. H. Overmars, “Probabilistic roadmaps for path planning in high-dimensional configuration spaces,” IEEE Transactions on Robotics and Automation, vol. 12, no. 4, pp. 566–580, 1996.
  * [31] C. C. Kemp, A. Edsinger, H. M. Clever, and B. Matulevich, “The design of Stretch: A compact, lightweight mobile manipulator for indoor human environments,” in 2022 IEEE International Conference on Robotics and Automation (ICRA), pp. 3150–3157, IEEE, 2022.