Continuous Execution of High-Level Collaborative Tasks for Heterogeneous Robot Teams

There is a wealth of literature in task assignment and scheduling for multi-robot systems. Multi-robot task allocation problems are often treated as optimization problems [2, 3, 4], such as the multiple traveling salesman problem [5] or the vehicle routing problem [6]. To mitigate the challenges of finding an exact solution, common approximate methods are used to solve the problem, such as learning algorithms, heuristics and meta-heuristics [7] [8], and contract net protocols [9] [10]. Coalition formation algorithms allow robots to automatically form teams to execute a task. Approaches include swarm algorithms [11] and multi-stage coalition formation [12], where the authors provide a two-stage approach to prune for a satisfying coalition.

The aforementioned approaches adopt a more generalized representation of tasks that are agnostic to the specific characteristics of each task, with the primary objective being to map agents to tasks. Each task is abstracted with certain constraints associated with it, such as cost or number of agents required. While these methods enable efficient task allocation algorithms, they do not account for the temporal dependencies and sequences of actions within the task itself. For describing temporally extended tasks, temporal logics can be useful; they allow users to rigorously define temporally extended tasks that may require complex action sequences and constraints. These logics define tasks with symbolic abstractions of the given continuous system. For multi-robot systems, existing work has extended Linear Temporal Logic (LTL) [13, 14, 15] and Signal Temporal Logic (STL) [16] [17] to encode tasks that require multiple robots to execute.

To ensure the satisfaction of multi-robot temporal logic specifications in continuous time, a common approach is to encode the task in STL, which allows for discrete-time continuous signals. For example, in [18], the authors synthesize coordinated trajectories of a heterogeneous multi-robot team to satisfy a global task written in STL. They also introduce integral predicates to provide a quantitative metric for the cumulative progress of the tasks. The type of coordination that can be encoded only includes accumulation (e.g. data collection), as opposed to highly collaborative tasks that require strict synchronization. To address strict synchronization constraints, the authors of [19] propose an event-based synchronization approach in which robots execute local LTL specifications and send synchronization requests when needed. This removes the necessity to synchronize at every discrete step, thus increasing efficiency. However, this work assumes that each robot is assigned a local specification a priori, as opposed to collectively satisfying a global task.

In [20], the authors address the problem of synthesizing controllers for a multi-agent system by extending Capability Temporal Logic (CaTL), which is a fragment of STL, to CaTL+. To ensure satisfiability, they encode two layers of logic, one for individual trajectories and one for the team trajectory. The controllers for each agent are then automatically synthesized by solving a centralized two-step optimization problem. For synchronization requirements, each task includes a counting proposition to indicate the timesteps in which synchronization must happen. The task explicitly encodes the number of capabilities required for each part of the task. In our work, we use LTL^ψ to define multi-agent tasks, which is an LTL-based grammar we first proposed in [1]. The grammar allows users to define tasks based on actions required instead of the number of agents/capabilities (e.g. “move the pallet and then pick up the package, irrespective of how many agents perform which actions”). In our work, we provide guarantees about the satisfaction of continuous controllers while using a discrete LTL-based logic. In this way, we can maintain the discrete abstraction of actions without any information about their specific timings.

To take into account the fact that actions may have varying durations, the authors in [21] generate reactive hybrid controllers for LTL tasks such that the continuous behavior of the robots are safe. The authors abstract actions with timing constraints by using initiation and completion propositions, and add constraints in the specification for activating these propositions. The specification also includes constraints to ensure collision avoidance across robots. While this approach accounts for collision avoidance, it does not consider collaborative tasks and therefore also does not account for any necessary synchronization constraints. [22] uses synchronization skeletons to coordinate a homogeneous swarm of robots to collectively satisfy a task. The task contains both a macro specification that describes the behavior of a group of robots, and a micro specification for individual robots to satisfy. To ensure the behavior satisfies the specification in the continuous space (i.e. when robots are between two regions), the authors propose an iterative method of synthesizing labeled transition systems, then removing unsafe transitions and adding safety formulas until a valid labeled transition system is found. Rather than an iterative synthesize-then-check approach, our work aims to automatically abstract continuous actions and synthesize symbolic controllers that are already correct-by-construction for continuous execution.

LTL formulas are constructed from atomic propositions $AP$, where $\pi\in AP$ are Boolean variables [23]. The atomic propositions represent an abstraction of robot actions. For example, $camera$ captures a robot taking a picture.

Syntax: We use the following syntax to define an LTL formula:

Semantics: The semantics of an LTL formula $\varphi$ are defined over an infinite trace $\sigma=\sigma(0)\sigma(1)\sigma(2)...$, where $\sigma(i)$ is the set of $AP$ that are true at step $i$. We use $\sigma\models\varphi$ to denote that the trace $\sigma$ satisfies LTL formula $\varphi$.

Intuitively, $\bigcirc\varphi$ is satisfied if $\varphi$ is satisfied in the next step of the sequence; $\Diamond\varphi$ is satisfied if $\varphi$ is true at some step in the sequence; $\Box\varphi$ is satisfied if $\varphi$ is true at every step in $\sigma$; $\varphi_{1}\ \mathcal{U}\ \varphi_{2}$ is satisfied if $\varphi_{1}$ remains true until $\varphi_{2}$ becomes true. See [23] for the full semantics.

An LTL formula $\varphi$ can be translated into a Nondeterministic Büchi Automaton that accepts infinite traces if and only if they satisfy $\varphi$. A Büchi automaton is a tuple $\mathcal{B}=(Z,z_{0},\Sigma_{\mathcal{B}},\delta_{\mathcal{B}},F)$, where $Z$ is the set of states, $z_{0}\in Z$ is the initial state, $\Sigma_{\mathcal{B}}$ is the input alphabet, $\delta_{\mathcal{B}}:Z\times\Sigma_{\mathcal{B}}\times Z$ is the transition relation, and $F\subseteq Z$ is a set of accepting states. An infinite run of $\mathcal{B}$ over a word $\sigma=\sigma_{1}\sigma_{2}\sigma_{3}...\in\Sigma_{\mathcal{B}}$ is an infinite sequence of states $z=z_{0}z_{1}z_{2}...$ such that $(z_{i-1},\sigma_{i},z_{i})\in\delta_{\mathcal{B}}$. A run is accepting if and only if Inf($z$) $\cap\ F\neq\emptyset$, where Inf($z$) is the set of states that appear in $z$ infinitely often [24].

We categorize the actions the robots can execute into two types, instantaneous and non-instantaneous. For example, the action of taking a picture is considered instantaneous; in contrast, the action of moving between rooms is non-instantaneous.

Each action is abstracted as an atomic proposition (AP) $\pi$, and its corresponding completion proposition, $\pi_{c}$. $\pi$ is true at $\sigma(i)$ iff the action associated with $\pi$ is being executed at position $i$ in the trace; $\pi_{c}\in AP$ is true at $\sigma(i)$ iff the action associated with $\pi$ has been completed at position $i$ in the trace. For example, $roomA$ indicates that the robot is currently moving towards room A; $roomA_{c}$ indicates the robot has finished executing the action $roomA$ and is currently in room A.

The set of all $AP$ is composed of the subsets $AP_{inst}$ and $AP_{non-inst}$, which are the sets of propositions representing instantaneous actions and non-instantaneous actions, respectively. Formally, an action is instantaneous iff $T(\pi,\pi_{c})=0$, where $T$ is the timing function that outputs the amount of time it takes for the action to be executed; thus, $\pi_{c}\in AP_{inst}$. Similarly, an action is considered non-instantaneous iff $T(\pi,\pi_{c})\neq 0$. For these types of actions, $\pi_{c}\in AP_{non-inst}$. For example, for the action of beeping, $T(beep,beep_{c})=0$ and therefore $beep_{c}\in AP_{inst}$. In contrast, $T(roomA,roomA_{c})\neq 0$ (i.e. moving into room A takes time), so $roomA_{c}\in AP_{non-inst}$.

Note that, for synchronization purposes, we assume that robots can coordinate such that they can execute an action simultaneously, so all $\pi$ are in the set of $AP_{inst}$. For example, $roomA_{c}\in AP_{non-inst}$ but $roomA\in AP_{inst}$; $beep,beep_{c}\in AP_{inst}$ (note that, for instantaneous actions, $\pi$ and $\pi_{c}$ have equivalent meanings).

Based on our prior work [25], each robot $j$ is modeled based on its set of capabilities, $\Lambda_{j}=\{\lambda_{1},...,\lambda_{k}\}$. Each capability is a weighted transition system $\mathcal{\lambda}=(X,x_{0},AP,\Delta,\mathcal{L},\mathcal{W})$, where $X$ is a finite set of states, $x_{0}\in X$ is the initial state, $AP$ is the set of atomic propositions representing the actions the capability can execute, $\Delta\subseteq X\times X$ is a transition relation, $\mathcal{L}:X\rightarrow 2^{AP}$ is the labeling function, and $\mathcal{W}:\Delta\rightarrow\mathbb{R}_{\geq 0}$ is the cost function assigning a weight to each transition. The cost function is predefined by the user and can represent execution time, power usage, etc.

A robot model $A_{j}$ is the cross product of its capabilities: $A_{j}=\lambda_{1}\times...\times\lambda_{k}$ such that $A_{j}=(S,s_{0},AP_{j},\gamma,L,W)$. $S=X_{1}\times...\times X_{k}$ is the set of states, $s_{0}\in S$ is the initial state, $AP_{j}=\bigcup_{i=1}^{k}AP_{i}$ is the set of propositions, $\gamma\subseteq S\times S$ is the transition relation, $L:S\rightarrow 2^{AP_{j}}$ is the labeling function, and $W:\gamma\rightarrow\mathbb{R}_{\geq 0}$ is the cost function (a function of $\mathcal{W}_{i}$). More details on the full definition can be found in [25]. See Fig. 1 for an example of a robot model.

We first introduced LTL^ψin [1]. In this work, because we are removing the assumption of instantaneous behavior, the “next” operator is no longer meaningful therfore we omit it. The task grammar for LTL^ψincludes atomic propositions that abstract robot action, logical and temporal operators, as in LTL, and bindings that relate actions to specific robots; any action labeled with a certain binding must be satisfied by all the robot(s) assigned that binding.

We define a task $\varphi^{\psi}$ recursively over LTL and binding formulas.

Semantics: The semantics of an LTL^ψ formula $\varphi^{\psi}$ are defined over the team trace $\sigma=\sigma_{1}\sigma_{2}...\sigma_{n}$, where each $\sigma_{j}$ is the trace for robot $j$; and the set of binding assignments $R=\{r_{1},r_{2},...,r_{n}\}$, where $r_{j}\in R$ is the set of bindings in $AP_{\psi}$ that are assigned to robot $j$. A robot’s binding assignment does not change throughout the task execution (i.e. $R$ remains the same). For example, $r_{1}=\{2\},r_{2}=\{1,3\}$ indicates that robot 1 is assigned binding 2, and robot 2 is assigned bindings 1 and 3.

Given a set of binding propositions $AP_{\psi}$, $\zeta:\psi\rightarrow 2^{2^{AP_{\psi}}}$ outputs all possible combinations of $\rho\in AP_{\psi}$ that satisfy $\psi$. For example, $\zeta\bigl{(}(1\wedge 2)\vee 3\bigr{)}=\{\{1,2\},\{3\},\{1,2,3\}\}$. We say that a team of robots satisfies the formula $\varphi^{\psi}$ if and only if a binding assignment exists in $\zeta(\psi)$ such that all the bindings are assigned to (at least one) robot, and the behavior of all robots with these binding assignments satisfy $\varphi$. A robot may be assigned to multiple bindings, and a binding may be assigned to multiple robots.

Formally, the semantics are defined recursively as follows:

• •

  $(\sigma(i),R)\!\models\varphi^{\psi}$ iff $\exists K\in\zeta(\psi)$ s.t. ($K\subseteq\bigcup\limits_{p=1}^{n}r_{p}$) and ($\forall j$ s.t. $K\cap r_{j}\neq\emptyset$, $\sigma_{j}(i)\models\varphi$)

• •

  $(\sigma(i),R)\!\models(\neg\varphi)^{\psi}$ iff $\exists K\in\zeta(\psi)$ s.t. ($K\subseteq\bigcup\limits_{p=1}^{n}r_{p}$) and ($\forall j$ s.t. $K\cap r_{j}\neq\emptyset$, $\sigma_{j}(i)\not\models\varphi$)

• •

  $(\sigma(i),R)\!\models\neg(\varphi^{\psi})$ iff $\exists K\in\zeta(\psi)$ s.t. ($K\subseteq\bigcup\limits_{p=1}^{n}r_{p}$) and ($\exists j$ s.t. $K\cap r_{j}\neq\emptyset$, $\sigma_{j}(i)\not\models\varphi$)

• •

  $(\sigma(i),\!R)\!\!\models\!\!\varphi_{1}^{\psi_{1}}\!\wedge\varphi_{2}^{\psi_{2}}$ iff $(\sigma(i),\!R)\!\!\models\!\varphi_{1}^{\psi_{1}}$and $(\sigma(i),\!R)\!\models\!\varphi_{2}^{\psi_{2}}$

• •

  $(\sigma(i),\!R)\!\models\!\varphi_{1}^{\psi_{1}}\!\vee\!\varphi_{2}^{\psi_{2}}$ iff $(\sigma(i),\!R)\!\models\!\varphi_{1}^{\psi_{1}}$or $(\sigma(i),R)\!\models\varphi_{2}^{\psi_{2}}$

• •

  $(\sigma(i),R)\models\bigcirc\varphi^{\psi}$ iff $\sigma(i+1),R\models\varphi^{\psi}$

• •

  $(\sigma(i),R)\!\models\varphi_{1}^{\psi_{1}}\mathcal{U}\varphi_{2}^{\psi_{2}}$ iff $\exists\ell\geq i$ s.t. $(\sigma(\ell),R)\models\varphi_{2}^{\psi_{2}}$ and $\forall i\leq k<\ell,(\sigma(k),R)\models\varphi_{1}^{\psi_{1}}$

• •

  $(\sigma(i),R)\models\Box\varphi^{\psi}$ iff $\forall\ell>i,(\sigma(\ell),R)\models\varphi^{\psi}$

In English, the specification captures “All robot(s) assigned binding 1 must eventually be at the dock. Anytime one of these robots is at the dock, all robot(s) assigned bindings 2 and 3 must be in room B taking pictures.” The second part of the task is a safety constraint that ensures that the dock is monitored anytime a robot assigned binding 1 is in that room.

To create a Büchi automaton from an LTL^ψ specification, we first modify the specification to constrain binding propositions solely to individual atomic propositions $\pi\in AP_{\varphi}$ (i.e. the formula contains only $\pi^{\rho}$). For example, the formula $(\Diamond(pickup\wedge roomA_{c}))^{1\vee 2}$ is rewritten as $(\Diamond(pickup^{1}\wedge roomA_{c}^{1})\vee(\Diamond(pickup^{2}\wedge roomA_{c}^{2}))$.

Using $AP_{\varphi}$ and $AP_{\psi}$, we define $AP_{\varphi}^{\psi}$, where $\forall\pi\in AP_{\varphi}$ and $\forall\rho\in AP_{\psi}$, $\pi^{\rho}\in AP_{\varphi}^{\psi}$. We automatically create the Büchi automaton from these propositions using Spot [26].

Prior to control synthesis, we first convert the transitions in the Büchi automaton, labeled with Boolean formulas, into disjunctive normal form (DNF). Subsequently, we substitute the transition labeled with a DNF formula containing $\ell$ conjunctive clauses with $\ell$ transitions between the same states. The label for each of these transitions is a distinct conjunction of the original label.

When constructing a Büchi automaton from an LTL formula $\varphi$, $\sigma\in\Sigma_{\mathcal{B}}$ are Boolean formulas over $AP_{\varphi}$, the atomic propositions that appear in $\varphi$. In this work, for a Büchi automaton of an LTL^ψ formula, $\Sigma_{\mathcal{B}}=2^{AP_{\varphi}^{\psi}}\times 2^{AP_{\varphi}^{\psi}}\times 2^{AP_{\varphi}^{\psi}}\times 2^{AP_{\varphi}^{\psi}}$, where $\sigma=(\sigma^{T},\sigma^{exT},\sigma^{F},\sigma^{exF})\in\Sigma_{\mathcal{B}}$ contains the set of propositions $\pi^{\rho}$ that must be true/false for all robots ($\sigma^{T}$ and $\sigma^{F}$), called for all propositions, and the set of propositions $\pi^{\rho}$ that must be true/false for at least one robot ($\sigma^{exT}$ and $\sigma^{exF}$), called there exists propositions. $\sigma^{exT}$ are the set of propositions in which $\neg(\neg\pi^{\rho})$ is true; $\sigma^{exF}$ are the set of propositions in which $\neg(\pi^{\rho})$ is true. Any proposition that does not appear in $\sigma$ can maintain any truth value.

We modify the definition of $\sigma$ compared to our prior work [1], where we assumed instantaneous robot actions; there, $\sigma=(\sigma_{T},\sigma_{F})$. While [1] also had there exists propositions, in practice the resulting behavior of there exists and for all propositions was the same. This is because, for a there exists proposition $\pi^{\rho}$, only one robot assigned binding $\rho$ needs to execute $\pi^{\rho}$. However, since the robots do not coordinate, if there are multiple robots assigned $\rho$, they all satisfy $\pi^{\rho}$ (satisfying for all propositions also satisfies there exists propositions). Thus, it was unnecessary in [1] to differentiate between these two types of propositions. This is not true for time varying actions; there are scenarios in which a there exists proposition is satisfied but a for all proposition is not.

Example. Consider the task defined in Eq. 4. Supposed we have two robots with $r_{green}=\{1\},r_{blue}=\{2,3\}$. Our prior approach may output a discrete teaming plan in which the blue robot enters the dock at exactly the same time the green robot enters room B. However, the physical execution of this plan may violate the specification; although the robots can begin moving towards their respective areas at the same time, the green robot may enter the dock before the blue robot enters room B, thus violating the safety constraint.

To formally define the product automaton, we first modify the functions introduced in [1]. For illustration, we will use the Büchi automaton for task 1 as our example (Fig. 2). Let the outer self-transition on state 1 be $\sigma_{11,o}$. $\sigma_{11,o}=(\sigma_{11,o}^{T},\sigma^{exT}_{11,o},\sigma_{11,o}^{F},\sigma^{exF}_{11,o})=(\{roomB_{c}^{2},camera^{2},roomB_{c}^{3},camera^{3}\},\emptyset,\emptyset,\{dock_{c}^{1}\})$.

$\mathfrak{B}_{\sigma}(\sigma)$ outputs the set of bindings that appear in a Büchi transition label $\sigma$. For example, $\mathfrak{B}_{\sigma}(\sigma_{11,o})=\{1,2,3\}$.

$\mathfrak{B}_{\Pi}(\Pi)$ outputs the set of bindings in a given set of LTL^ψ propositions $\Pi$. For example, for $\Pi=\{roomB_{c}^{2},camera^{2},roomB_{c}^{3},camera^{3},dock_{c}^{1}\}$, $\mathfrak{B}_{\Pi}(\Pi)=\{1,2,3\}$; for $\Pi=\{dock_{c}^{1}\}$, $\mathfrak{B}_{\Pi}(\Pi)=\{1\}$.

$C_{T}$ and $C_{F}$ are the sets of for all propositions that are True/False and appear with binding $\rho$ in label $\sigma$ of a Büchi transition and must be True/False for all robots assigned binding $\rho$; $C_{exT}$ and $C_{exF}$ are defined similarly but for there exists propositions with binding $\rho$. For example, for $\sigma_{11,o}=(\{roomB_{c}^{2},camera^{2},roomB_{c}^{3},camera^{3}\},\emptyset,\emptyset,\{dock_{c}^{1}\})$, $\mathfrak{C}(\sigma_{11,o},2)=(\{roomB_{c},camera\},\emptyset,\emptyset,\emptyset)$ (for binding 2, the relevant propositions are $roomB_{c}$ and $camera$, both of which must be true and are for all propositions, i.e. the set $\sigma^{T}$), and $\mathfrak{C}(\sigma_{11,o},1)=(\emptyset,\emptyset,\emptyset,\{dock_{c}\})$ ($dock_{c}$ is the only proposition with the binding 1 and is in $\sigma^{exF}$).

To synthesize behavior for a robot, we find the minimum cost accepting trace in its product automaton $\mathcal{G}_{j}=A_{j}\times\mathcal{B}$, where $A_{j}=(S,s_{0},AP_{j},\gamma,L,W)$ is the robot model, and $\mathcal{B}=(Z,z_{0},\Sigma_{\mathcal{B}},\delta_{\mathcal{B}},F)$ is the Büchi automaton.

Given a transition $(s,\sigma,s^{\prime})$, $\mathfrak{R}$ generates all possible combinations of binding propositions that can be assigned to a robot to satisfy $\sigma$. A robot can be assigned binding $\rho$ if and only if two conditions hold on the robot’s next state, $s^{\prime}$: 1) the state label of $s^{\prime}$ contains all propositions $\pi$ that appear in either $\sigma^{T}$ or $\sigma^{exT}$ as $\pi^{\rho}$, and 2) the state label of $s^{\prime}$ does not contain any propositions $\pi$ that appear in $\sigma^{F}$ or $\sigma^{exF}$ as $\pi^{\rho}$.

A binding assignment $r$ can contain any binding propositions not in $\sigma$, since there are no propositions required by those bindings. In addition, it follows from condition (2) that if a proposition $\pi^{\rho}$ is in $\sigma^{F}\cup\sigma^{exF}$ and $\pi$ is not in $AP_{j}$ (e.g. $camera^{1}\in\sigma^{F}$ and the robot does not have the capability $\lambda_{camera}$), $\rho$ can still be assigned to robot $j$.

Given the binding assignment function $\mathfrak{R}$, and as shown in [1], we can now define the product automaton:

To ensure correct team behavior when actions take different time durations, we add intermediate transitions to the Büchi automaton $\mathcal{B}$ to reason about and enforce an ordering on individual robot behaviors (Alg. 1). In doing so, we maintain the symbolic abstractions of actions while providing guarantees for the satisfaction of the task by a physical system.

To motivate the use of intermediate transitions, we look at the transitions $\sigma_{11,i}$ (the inner self-transition along state 1) and $\sigma_{10}$ of the Büchi automaton in Fig 2, where $\sigma_{11,i}=(\sigma_{11,i}^{T},\sigma^{exT}_{11,i},\sigma_{11,i}^{F},\sigma^{exF}_{11,i})=(\emptyset,\emptyset,\{dock_{c}^{1}\},\emptyset)$, $\sigma_{10}=(\sigma_{10}^{T},\sigma^{exT}_{10},\sigma_{10}^{F},\sigma^{exF}_{10})=(\{roomB_{c}^{2},camera^{2},roomB_{c}^{3},camera^{3},dock_{c}^{1}\},\emptyset,\emptyset,\emptyset)$. $\sigma_{10}$ requires all robots assigned binding 2 and 3 to be in roomB. Since it is unrealistic for multiple robots to enter the room simultaneously, we can leverage the fact that $\sigma_{11,i}$ does not explicitly assign truth values to $roomB_{c}^{2}$ and $roomB_{c}^{3}$ (i.e. these propositions can have any truth value over $\sigma_{11,i}$) in order to enforce that all the robots assigned bindings 2 and 3 enter room B at some point before executing the transition $\sigma_{10}$. For clarity in the remainder of the paper, we define a proposition $\pi^{\rho}$ to be assigned an explicit truth value over a transition $\sigma$ if it appears in $\sigma$, i.e. $\pi^{\rho}\in\sigma^{T}\cup\sigma^{exT}\cup\sigma^{F}\cup\sigma^{exF}$. If a proposition is not explicitly in $\sigma$, it can maintain any truth value over that transition.

To automatically construct intermediate transitions, we first define the intermediate propositions function, $\mathcal{I}(\sigma)$:

$I_{T}$, $I_{exT}$, $I_{F}$, and $I_{exF}$ are the sets of LTL^ψ propositions corresponding to non-instantaneous actions that are assigned truth values over $\sigma^{T},\sigma^{exT},\sigma^{F},\text{ and }\sigma^{exF}$, respectively. For example, in Fig. 2 where $\sigma_{11,o}=(\sigma_{11,o}^{T},\sigma^{exT}_{11,o},\sigma_{11,o}^{F},\sigma^{exF}_{11,o})=(\{roomB_{c}^{2},camera^{2},roomB_{c}^{3},camera^{3}\},\emptyset,\emptyset,\{dock_{c}^{1}\})$, the intermediate propositions are $\mathcal{I}(\sigma_{11,o})=(\{roomB_{c}^{2},roomB_{c}^{3}\},\emptyset,\emptyset,\{dock_{c}^{1}\})$, since all the motion propositions are non-instantaneous; $camera$ is instantaneous and therefore omitted from $\mathcal{I}(\sigma_{11,o})$.

We use the intermediate propositions function to determine which non-instantaneous propositions change truth values across two transitions; we then use these propositions to enforce constraints on the binding assignments and on robot behavior. Let $\sigma,\sigma^{\prime}$ be labels of two transitions in the Büchi automaton, and $\mathcal{I}(\sigma)=(I_{T},I_{exT},I_{F},I_{exF}),\mathcal{I}(\sigma^{\prime})=(I^{\prime}_{T},I^{\prime}_{exT},I^{\prime}_{F},I^{\prime}_{exF})$. To categorize how these propositions change their truth values, we define the following sets (Alg. 1, line 1):

$\Pi_{T},\Pi_{F}\subseteq AP_{non-inst}$ are the sets of non-instantaneous for all propositions that explicitly change truth values between $\sigma$ and $\sigma^{\prime}$.

$\Pi_{exT},\Pi_{exF}\subseteq AP_{non-inst}$ include any non-instantaneous proposition that is a there exists proposition in $\sigma$ that explicitly changes truth values between $\sigma$ and $\sigma^{\prime}$.

$\Pi_{\emptyset T},\Pi_{\emptyset exT},\Pi_{\emptyset F},\Pi_{\emptyset exF}\subseteq AP_{non-inst}$ are the sets of non-instantaneous propositions that are assigned truth values in $\sigma^{\prime}$ but not in $\sigma$.

Example: Task 1. In Fig. 2, consider the two transitions $(1,\sigma_{11,i},1)$, $(1,\sigma_{10},0)$, where $\sigma_{11,i}=(\emptyset,\emptyset,\{dock_{c}^{1}\},\emptyset)$ is the inner self-transition on state 1, and $\sigma_{10}=(\{roomB_{c}^{2},camera^{2},roomB_{c}^{3},camera^{3},dock_{c}^{1}\},\emptyset,\emptyset,\emptyset)$. Then $\Pi_{F}=\{dock_{c}^{1}\}$, $\Pi_{\emptyset T}=\{roomB_{c}^{2},roomB_{c}^{3}\}$; the remaining sets are empty.