# Rules of the Road: Safety and Liveness Guarantees for Autonomous Vehicles

Karena X. Cai, Tung Phan-Minh, Soon-Jo Chung, Richard M. Murray This research
supported by the National Science Foundation award CNS-1545126.

###### Abstract

The ability to guarantee safety and progress for all vehicles is vital to the
success of the autonomous vehicle industry. We present a framework for
designing autonomous vehicle behavior in a way that is safe and guarantees
progress for all agents. In this paper, we first introduce a new game paradigm
which we term the quasi-simultaneous game. We then define an agent protocol
that all agents must use to make decisions in this quasi-simultaneous game
setting. According to the protocol, agents first select an intended action
using a behavioral profile. Then, the protocol defines whether an agent has
precedence to take its intended action or must take a sub-optimal action. The
protocol ensures safety under all traffic conditions and liveness for all
agents under ‘sparse’ traffic conditions. We provide proofs of correctness of
the protocol and validate our results in simulation.

##  I Introduction

A prerequisite for introducing autonomous vehicles into our society is a
compelling proof of their safety and efficacy. Unfortunately, designing agent
strategies in interactive multi-agent settings is extremely difficult since
agent behavior is highly coupled and the computational complexity grows
exponentially when reasoning about joint action spaces.

Most approaches for designing agent behavior focus on designing an individual
agent’s strategy while modeling interactions with other agents using some
interactive behavioral model. Minimum violation motion-planning has been
proposed to help the vehicle choose the trajectory that minimizes violation of
a set of ordered rules [26, 30]. Rulebooks are a way to set priorities among
possibly conflicting sets of specifications [5]. The game-theoretic approach
has been to model agent decision-making as interacting partially-observable
Markov Decision Processes (POMDPs) [3, 10]. These methods often capture the
reactivity of agents by modeling a reward function defined on a joint action
space but suffers from the curse of dimensionality. Data-driven methods are
used to learn interactive models between agents and design an optimal strategy
for an individual agent based on this learned model [21, 20]. When designing
an individual agent strategy, how other agents are assumed to be behaving is
not explicitly defined—thereby preventing the ability to make complete safety
guarantees.

Instead of reasoning about safety on the individual agent level, the authors
in [24] introduce the idea of reasoning about safety as a property of the
collective of agents. In particular, they introduce the idea of social laws,
which are a set of rules imposed upon all agents in a multiagent system to
ensure some desirable global behaviors like safety or progress [24, 27]. The
design of social laws is intended to achieve the desirable global behavioral
properties in a minimally-restrictive way [24]. The problem of automatically
synthesizing useful social laws for a set of agents for a general state space,
however, has been shown to be NP-complete [24]. Model checking tools have also
been designed to verify correctness of agent protocols for multi-agent
systems, but these do not solve the protocol synthesis problem [14, 27]. The
Responsibility-Sensitive-Safety (RSS) framework [23] adopts a similar top-down
philosophy for guaranteeing safety by providing a set of rules like
maintaining distance, yielding, etc, but does not provide guarantees of agent
progress.

Similarly, the Assume-Guarantee framework for autonomous vehicles introduced
in [18] dictates all agents must abide by some behavioral contract where
agents make decisions according to a behavioral profile. With all agents
operating according to the behavioral profile, the interactions are not
necessarily coordinated. In particular, there might be multiple agents with
conflicting goals. The process for resolving multiple conflicting processes in
a local, decentralized manner is addressed in the Drinking Philosopher
problem, which provides a mechanism for resolving conflicts by defining a
local, decentralized algorithm for assigning precedence among agents [6]. We
introduce an agent protocol that is an adaptation of the Drinking Philosopher
problem. The agent protocol is defined so agents use a behavioral profile to
select an intended action. Additional constraints specified in the profile,
determine when an agent has precedence in taking its intended action. Unlike
[22], our framework leverages the structure of the driving road network and
takes into account the inertial properties of agents.

The main contributions of this paper are as follows: 1) The introduction of a
new game paradigm, which we term the quasi-simultaneous discrete-time multi-
agent game, 2) the definition of an agent protocol that defines local rules
agents must use to select their actions, 3) safety and liveness proofs when
all agents operate according to these local rules and 4) simulations as proof
of concept of the safety and liveness guarantees.

##  II Quasi-Simultaneous Discrete-Time Game

We propose a quasi-simultaneous discrete-time game paradigm, which we motivate
by looking at the shortcomings of more traditional game paradigms. In
synchronous games, all agents in the game are making decisions simultaneously.
Since agents are making decisions in the absence of other agent behaviors, it
does not capture the sequential nature of real-life decision making. Turn-
based games offer potential for capturing sequential decision-making, but the
turns are often assigned arbitrarily. The quasi-simultaneous discrete-time
game offers a way to assign turns, but in a turn order based on the agent
states defined with respect to the road network.

A state associated with a set of variables is an assignment of values to those
variables. A game evolves by a sequence of state changes. A quasi-simultaneous
game has the following two properties regarding state changes: 1) each agent
will get to take a turn in each time-step of the game and 2) each agent must
make their turn in an order that emerges from a locally-defined precedence
assignment algorithm. We define a quasi-simultaneous game where all agents act
in a local, decentralized manner as follows
$\mathfrak{G}=\langle\mathfrak{A},\mathcal{Y},Act_{[\cdot]},P\rangle$, where
$\mathfrak{A}$ is the set of all agents in the game, $\mathcal{Y}$ is the set
of all variables in the game, $Act_{\text{Ag}}$ be the set of all possible
actions Ag can take. Finally,
$P:\mathcal{Y}\rightarrow\text{PolyForest}(\mathfrak{A})$, is the precedence
assignment function where PolyForest is an operator that maps a set to a
polyforest graph object. The polyforest, with its nodes and directed edges,
defines the global turn order (of precedence) of the set of all agents based
on the agent states.

##  III Specific Agent Class

In order to make global guarantees on safety and progress, we first only
consider a single specific class of agents whose attributes, dynamics, motion-
planner, and perception capabilities are described in more detail in the
following section. Although assuming a single class of agents seems very
restrictive, the work can be easily extended to accommodate additional
variants of the agent class. These extensions, however, are beyond the scope
of this work.

###  III-A Agent Attributes

Each agent Ag is characterized by a set of variables
$\mathcal{V}_{\text{Ag}}\subseteq\mathcal{Y}$. We define
$\\{\texttt{Id}_{\text{Ag}},\texttt{Tc}_{\text{Ag}},\texttt{Goal}_{\text{Ag}}\\}~{}\subseteq~{}{\mathcal{V}}_{\text{Ag}}$
where $\texttt{Id}_{\text{Ag}}$, $\texttt{Tc}_{\text{Ag}}$, and
$\texttt{Goal}_{\text{Ag}}$ are the agent’s ID number, token count and goal
respectively. The token count and ID are defined in greater depth in Section
V-C. Agents are assumed to have the capability of querying the token counts of
neighboring agents.

In this paper, we only consider car agents such that if
$\text{Ag}\in\mathfrak{A}$, then $\mathcal{V}_{\text{Ag}}$ includes
$x_{\text{Ag}}$, $y_{\text{Ag}}$, $\theta_{\text{Ag}}$, $v_{\text{Ag}}$,
namely its absolute coordinates, heading and velocity. We let $S_{\text{Ag}}$
denote the set that contains all possible states of these variables in
$\mathcal{V}_{\text{Ag}}$. $\mathcal{V}_{\text{Ag}}$ also has parameters:
${a_{\text{min}}}_{\text{Ag}}\in\mathbb{Z},{a_{\text{max}}}_{\text{Ag}}\in\mathbb{Z},{v_{\text{min}}}_{\text{Ag}}\in\mathbb{Z}\text{
and }{v_{\text{max}}}_{\text{Ag}}\in\mathbb{Z}$ which define the minimum and
maximum accelerations and velocities respectively. The agent control actions
are defined by two parameters: 1) an acceleration value
$\text{acc}_{\text{Ag}}$ between ${a_{\text{min}}}_{\text{Ag}}$ and
${a_{\text{max}}}_{\text{Ag}}$ and 2) a steer maneuver
$\gamma_{\text{Ag}}\in${left-turn, right-turn, left-lane change, right-lane
change, straight}.

The discrete agent dynamics works as follows. At a given state $s\in
S_{\text{Ag}}$ at time $t$, for a given control action
$(\text{acc}_{Ag},\gamma_{Ag})$, the agent first applies the acceleration to
update its velocity $s.v_{Ag,t+1}=s.v_{Ag,t}+\text{acc}_{\text{Ag}}$. Once the
velocity is applied, the steer maneuver (if at the proper velocity) is taken
and the agent occupies a set of grid-points, specified in Fig. 1, while taking
its maneuver. The agent state-transition function
$\tau_{\text{Ag}}:S_{\text{Ag}}\times Act_{\text{Ag}}\rightarrow
S_{\text{Ag}}$ defines the state an agent will transition to by taking an
action $a$ at a given state $s_{\text{Ag}}$ and the state precondition
$\rho_{\text{Ag}}:S_{\text{Ag}}\rightarrow 2^{Act_{\text{Ag}}}$ functions
defines the set of allowable actions at a given state.

Figure 1: Shows different grid point occupancy associated with different
discrete agent maneuvers. Note the grid point occupancy represents a
conservative space in which the agent may occupy when taking the associated
maneuver.

During an agent state transition, an agent may, depending on the maneuver,
occupy a set of grid points. Before and after the state transition, the agent
is assumed to occupy only a single grid point. Fig. 1 shows the grid point
occupancy for different agent maneuvers. The concept of grid point occupancy
is defined as follows:

######  Definition III.1 (Grid Point Occupancy)

The notion of grid point occupancy is captured by the definitions of the
following maps for each $\text{Ag}\in\mathfrak{A}$. To define the grid point
an agent is occupying at a given time we use the map:
$\mathcal{G}_{\text{Ag},t}:S_{\text{Ag}}\rightarrow 2^{G}$, mapping each agent
to the single grid point the agent occupies. By a slight abuse of notation, we
let $\mathcal{G}_{Ag,t}:S_{\text{Ag}}\times{Act}_{\text{Ag}}\rightarrow 2^{G}$
be a function that maps each $s\in S_{\text{Ag}}$ and
$a\in\rho_{\text{Ag}}(s)$ to denote the set of all grid points that are
occupied by the agent Ag when it takes an allowable action $a$ from state $s$
at the time-step $t$.

Here we assume that any graph-based planning algorithm can be used to specify
an agent’s motion plan, where the motion plan is a set of critical points
along the graph that the agent must reach in order to get to its destination.

###  III-B Agent Backup Plan Action

A backup plan is a reserved set of actions an agent is entitled to execute at
any time while being immune to being at fault for a collision if one occurs.
In other words, an agent will always be able to safely take its backup plan
action. We show if each agent can maintain the ability to safely execute its
own backup plan (i.e. keep a far enough distance behind a lead agent), the
safety of the collective system safety is guaranteed. The default backup plan,
which we refer to as $a_{\text{bp}}$ adopted here is that of applying maximal
deceleration until a complete stop is achieved. Note, it may take multiple
time-steps for an agent to come to a complete stop because of the inertial
dynamics of the agent.

###  III-C Limits on Agent Perception

In real-life, agents make decisions based on local information. We model this
locality by defining a region of grid points around which agents have access
to the full state and intentions of the other agents. We assume agents have
different perception capabilities in different contexts of the road network.
For road segments, the region around which agents make decisions cannot be
arbitrarily defined. In fact, an agent’s bubble must depend on its state, and
the agent attributes and dynamics of all agents in the game. In particular,
the bubble can be defined as follows:

######  Definition III.2 (Bubble)

Let Ag with state $s_{0}\in S_{\text{Ag}}$. Then the bubble of Ag with respect
to agents of the same type is written as $\mathcal{B}_{\text{Ag}}(s_{0})$. The
bubble is the minimal region of space (set of grid points) agents need to have
full information over to guarantee they can make a decision that will preserve
safety under the defined protocol.

The details for the construction of the bubble for an agent with a particular
set of attributes and dynamics can be found in the Appendix. At intersections,
agents are assumed to be able to see across the intersection when making
decisions about crossing the intersection. More precisely, any Ag must be able
to know about any $\text{Ag}^{\prime}\in\mathfrak{A}$ that is in the lanes of
oncoming traffic. The computation of the exact region of perception necessary
depends on the agent dynamics.

##  IV Road Network Environment

Here we introduce the structure of the road network environment that agents
are assumed to be operating on. The road network is a grid world with
additional structure (e.g. lanes, bundles, road segments, intersections,
etc.). The road network is formalized as follows:

######  Definition IV.1 (Road Network)

A road network $\mathfrak{R}$ is a graph $\mathfrak{R}=(G,E)$ where $G$ is the
set of grid points and $E$ is the set of edges that represent immediate
adjacency in the Cartesian space among grid points. Note that each grid point
$g\in G$ has a set of associated properties $\mathcal{P}$, where
$\mathcal{P}=\\{p,d,\texttt{lo}\\}$ which denote the Cartesian coordinate,
drivability of the grid point and the set of legal orientations allowed on the
grid point respectively. Note, $p\in\mathbb{Z}^{2}$, $d\in\\{0,1\\}$ and
$\texttt{lo}\in\\{\texttt{north},\texttt{east},\texttt{south},\texttt{west}\\}$.

$\mathcal{S}_{\text{sources}}$ ($\mathcal{S}_{\text{sinks}}$) are the set of
grid points agents can enter or leave the road network from. Each intersection
of the road network is governed by traffic lights. The road network is
hierarchically decomposed into lanes, bundles and road segments, where a lane
$La(g)$ defines a set of grid points that contains $g$ and all grid points
that form a line going through $g$ and a bundle $Bu(g)$ is a set of grid
points that make up a set of lanes that are adjacent or equal to the lane
containing $g$ and have the same legal orientation. Each bundle can be
decomposed into a set of road segments $RS$, where the intersections are used
to partition each bundle into a set of road segments. These road components
can be seen in Fig.2.

We introduce the following graph definition since it will be used in the
liveness proof.

######  Definition IV.2 (Road Network Dependency Graph)

The road network dependency graph is a graph $G_{\text{dep}}=(RS,E)$ where
nodes are road segments and a directed edge $(rs_{1},rs_{2})$ denotes that
agents on $rs_{1}$ depends on the clearance of agents in $rs_{2}$ to make
forward progress.

##  V the Agent Protocol

The protocol is the set of rules agents use to select which action to
ultimately take at a given time step. According to the protocol, agents first
select an intended action using a profile. The protocol then defines
additional rules that an agent uses to determine whether it has priority to
take its intended action, and if not, which alternative, less-optimal actions
it is allowed to take. The protocol is defined in a way that 1) scales well in
the number of agents 2) is interpretable so there is a consistent and
transparent way agents make their decisions 3) ensures safety and progress of
all agents. In this section, we introduce the components that form the agent
protocol that make it such that all these properties are satisfied.

###  V-A Agent Precedence Assignment

The definition of the quasi-simultaneous game requires agents to locally
assign precedence, i.e. have a set of rules to define how to establish which
agents have higher, lower, equal or incomparable precedence to it.

Thus, the first element of the agent protocol is defining the agents’ local
precedence assignment algorithm so each agent knows its turn order relative to
neighboring agents. Our precedence assignment algorithm is motivated by
capturing how precedence among agents is generally established in real-life
scenarios on a road network. In particular, since agents are designed to move
in the forward direction, we aim to capture the natural inclination of agents
to react to the actions of agents visibly ahead of it.

Before presenting the precedence assignment rules, we must introduce a few
definitions. Let us define:
$\text{proj}^{B}_{\text{long}}:\mathfrak{A}\rightarrow\mathbb{Z}$, which is
restricted to only be defined on the bundle $B$. In other words,
$\text{proj}^{B}_{\text{long}}(Ag)$ is the mapping from an agent (and its
state) to its scalar projection onto the longitudinal axis of the bundle $B$
the agent Ag is in. If
$\text{proj}^{B}_{\text{long}}(\text{Ag}^{\prime})<\text{proj}^{B}_{\text{long}}(\text{Ag})$,
then the agent $\text{Ag}^{\prime}$ is behind Ag in $B$.

The following rules can be used to define the precedence relation among agents
$Ag$ and $Ag^{\prime}$.

####  V-A1 Local Precedence Assignment Rules

  1. 1.

If
$\text{proj}^{B}_{\text{long}}(\text{Ag}^{\prime})<\text{proj}^{B}_{\text{long}}(\text{Ag})$
and $Bu(\text{Ag}^{\prime})=Bu(\text{Ag})$, then
$\text{Ag}^{\prime}\prec\text{Ag}$, i.e. if agents are in the same bundle and
Ag is longitudinally ahead of $\text{Ag}^{\prime}$, Ag has higher precedence
than $\text{Ag}^{\prime}$.

  2. 2.

If
$\text{proj}^{B}_{\text{long}}(\text{Ag}^{\prime})=\text{proj}^{B}_{\text{long}}(\text{Ag})$
and $Bu(\text{Ag}^{\prime})=Bu(\text{Ag})$, then $\text{Ag}\sim Ag^{\prime}$
and we say Ag and $\text{Ag}^{\prime}$ are equivalent in precedence.

  3. 3.

If $\text{Ag}^{\prime}$ and Ag are not in the same bundle, then the two agents
are incomparable.

Each agent $\text{Ag}\in\mathfrak{A}$ only assigns precedence according to the
above rules locally to agents within its local region. Thus, we must show if
all agents locally assign precedence according to these rules, a globally-
consistent turn precedence among all agents is established. The linear
ordering induced by these local rules are used to prove this. The reader is
referred to the Appendix for the full proof.

Figure 2: Rules for precedence assignment.

Even when this turn-order is established, there is still some ambiguity as to
which agents have precedence. The ambiguity is resolved through the conflict-
cluster resolution, introduced in Section V-C.

###  V-B Behavioral Profile

The way in which agents select actions is the fundamental role of the agent
protocol. The behavioral profile serves the purpose of defining which action
an agent intends to take at a given time-step $t$. We define a specific
assume-guarantee profile with the mathematical properties defined in [18]. In
particular, we define a set of ten different specifications (rules) and place
a hierarchy of importance (ordering) on these rules.

Figure 3: Assume-guarantee profile that shows ordering of specifications,
where specifications on the same tier are incomparable to one another and Tier
1 has highest priority.

Each of the specifications is associated with an oracle that evaluates whether
or not an agent taking an action $a$ satisfies the specification. The reader
is referred to the Appendix for the precise oracle definitions. The
consistent-evaluating function, defined on this agent profile, will evaluate
actions based on which subset of specifications they satisfy–giving priority
to actions that satisfy the highest number of highest-valued specifications,
as described in [18]. The action with the highest value is then selected as
the action the agent intends to takes.

For this work, the agent profile defined in Fig. 3 is used to define both the
agent’s intended action $a_{i}$ and best straight action $a_{\text{st}}$
defined in Definition V.4. Since an agent would never propose a lane-change
action if $O_{\text{Ag},t,\text{dynamic safety}}(s,a,u)$ were included in the
profile, it is not included in the selection of the intended action $a_{i}$,
but rather evaluated later downstream in the protocol.

###  V-C Conflict-Cluster Resolution

At every time-step $t$, each agent will know when to take its turn based on
its local precedence assignment algorithm. Before taking its turn, the agent
will have selected an intended action $a_{i}$ using the Agent profile. When it
is the agent’s turn to select an action, it must choose whether or not to take
it’s intended action $a_{i}$. When the intended actions of multiple agents
conflict, the conflict-cluster resolution is a token-based querying method
used to help agents determine which agent has priority in taking its action.

Under the assumption agents have access to the intentions of other agents
within a local region as defined in Section III-C, agents can use the
following criteria to define when it conflicts with another agent.

######  Definition V.1 (Agent-Action Conflict)

Let us consider an agent Ag is currently at state $s\in S_{\text{Ag}}$ and
wants to take action $a$ and an agent $\text{Ag}^{\prime}$ at state
$s^{\prime}\in S_{\text{Ag}^{\prime}}$ wants to take action $a^{\prime}$. We
write an agent-action conflict exists
$(\text{Ag},s,a)\dagger(\text{Ag}^{\prime},s^{\prime},a^{\prime})$, if each of
the agents taking their respective actions will cause them to overlap in
occupancy grid points or end up in a configuration where the agent behind does
not have a valid safe backup plan action.

In the case that an agent’s action is in conflict with another agents’ action,
the agent must send a conflict request that ultimately serves as a bid the
agent is making to take its intended action. It cannot, however, send requests
to just any agent (e.g. agents in front of it). The following criteria are
used to determine the properties that must hold in order for an agent Ag to
send a conflict request to agent $\text{Ag}^{\prime}$: 1) Ag’s intended action
$a_{i}$ is a lane-change action, 2)
$\text{Ag}^{\prime}\in\mathcal{B}_{Ag}(s)$, i.e. $\text{Ag}^{\prime}$ is in
agent Ag’s bubble, 3) $\text{Ag}^{\prime}\precsim Ag$, i.e. Ag has equivalent
or higher precedence than $\text{Ag}^{\prime}$, 4) $Ag$ and $Ag^{\prime}$ have
the same heading, 5) $(Ag,a_{i})\dagger(Ag^{\prime},a_{i}^{\prime})$: agents
intended actions are in conflict with one another, and 6)
$\mathcal{F}_{\text{Ag}}(u,a_{i})=\texttt{F}$, where
$\mathcal{F}_{\text{Ag}}(u,a_{i})$ is the max-yielding-not enough flag and is
defined below.

######  Definition V.2 (maximum-yielding-not-enough flag)

The maximum-yielding-not-enough flag
$\mathcal{F}_{\text{Ag}}:\mathcal{U}\times
Act_{\text{Ag}}\rightarrow\mathbb{B}$ is set to T when Ag is in a
configuration where if Ag did a lane-change, $Ag$ would still violate the
safety of $\text{Ag}^{\prime}$’s backup plan action even if Ag’ applied its
own backup plan action.

We note that if $\mathcal{F}_{\text{Ag}}(u,a_{i})$ is set, Ag cannot send a
conflict request by the last condition. Even though Ag does not send a
request, it must use the information that the flag has been set in the agent’s
Action Selection Strategy defined in Section V-D. After a complete exchange of
conflict requests, each agent will be a part of a cluster of agents that
define the set of agents it is ultimately bidding for its priority (to take
its intended action) over. These clusters of agents are defined as follows:

######  Definition V.3 (Conflict Cluster)

A conflict cluster for an agent Ag is defined as
$\mathcal{C}_{Ag}=\\{Ag^{\prime}\in\mathfrak{A}\mid Ag\texttt{ send
}\text{Ag}^{\prime}\text{ or }Ag^{\prime}\texttt{ send }Ag\\}$, where
$\text{Ag}\texttt{ send }Ag^{\prime}$ implies Ag has sent a conflict request
to $\text{Ag}^{\prime}$. An agents’ conflict cluster defines the set of agents
in its bubble that an agent is in conflict with.

Fig. 4 shows an example scenario and each agents’ conflict clusters. Once the
conflict requests have been sent and an agent can thereby identify the other
agents in its conflict cluster, it needs to establish whether or not the
conflict resolution has resolved in it’s favor.

Figure 4: An example scenario with agents in a given configuration of agents,
their intended actions and their respective conflict clusters.

Once an agent has determined which agents are in its conflict cluster, it must
determine whether or not it has the priority to take its intended action. The
token resolution scheme is the way in which agents determine whether they have
precedence.

The token resolution strategy must be designed to be fair, meaning each agent
will always eventually wins their conflict resolution. The resolution is
therefore based on the agents’ token counts Tc, which is updated by agents to
represent how many times an agent has been unable to take a forward progress
action thus far.

The token count updates according to the agent’s chosen action. In particular,
if Ag selects action $a$: if $O_{\text{forward progress}}(s,a,u)=\texttt{T}$,
the the token count resets to 0, otherwise it increases by 1.

Then, a fair strategy would be to make it so that the agent with the highest
amount of tokens wins in its own conflict cluster. Thus, we define a token
resolution indicator variable for each Ag as
$\mathcal{W}_{\text{Ag}}\in\mathbb{B}$, indicating whether or not the agent
has won in its conflict cluster. The conflict cluster resolution indicator
variable $\mathcal{W}_{\text{Ag}}$ evaluates to T if $Ag$ has the highest
amount of tokens in its conflict cluster, where ties are broken via agent ID
comparison.

###  V-D Action Selection Strategy

The Action Selection Strategy is a decision tree that defines whether or not
an agent is allowed to take its intended action $a_{i}$ and if it is not,
which alternative action it should take. In the case where an agent is not
allowed to take $a_{i}$, the agent is restricted to take either: the best
straight action $a_{st}$, which is defined in Definition V.4, or its backup
plan action $a_{bp}$, where the best straight action is defined as follows:

######  Definition V.4 (Best Straight Action)

Let us consider Ag and its associated action set $\rho_{\text{Ag}}(s)$. The
best straight action is the action $a\in\rho_{\text{Ag}(s)}$ that is the
highest-ranked action (according to the profile defined in Section V-B), among
the set of all actions for which $\gamma_{\text{Ag}}=\text{straight}$.

The decision tree branches are defined based on the following five conditions:
1) $a_{i}$, the agent’s and other agents’ (in its bubble) intended actions 2)
Ag’s role in conflict request cluster being a) a conflict request sender, b) a
conflict request receiver, c) both a sender and a receiver, d) neither sender
or receiver, 3) the agent’s conflict cluster resolution
$\mathcal{W}_{\text{Ag}}$, 4) evaluation of $O_{\text{Ag},t,\text{dynamic
safety}}(s,a_{i},u)$ and 5) $\mathcal{F}_{\text{Ag}}(u,a_{i})$ for Ag is
raised, where $\mathcal{F}_{\text{Ag}}(u,a_{i})$ is the maximal-yielding-not-
enough flag defined in Section V-C.

If an agent receives a conflict cluster request and loses their conflict
cluster resolution, according to the action selection strategy, the agent must
take its backup plan action $a_{\text{bp}}$. An agent is only allowed to take
a lane-change action when the agent is a winner of its conflict cluster
resolution, $\mathcal{F}_{\text{Ag}}=\texttt{F}$ and the dynamic safety oracle
evaluates to true (i.e. $O_{\text{Ag},t,\text{dynamic
safety}}(s,a_{i},u)=\texttt{T}$). Finally, an agent that loses in its conflict
cluster but did not send requests must take $a_{\text{st}}$. A figure showing
the full decision-tree logic for selecting actions can be found in the
Appendix.

The agent protocol, as described in the above sections, has been designed in a
way such that if all agents are selecting actions via the protocol, we can
provide formal guarantees on safety and liveness. Theses safety and liveness
proofs are given in the following sections.

##  VI Formal Guarantees

Before introducing the formal guarantees of safety and liveness and their
respective proofs, we first make explicit the assumptions that must hold on
agents and the road network.

  1. 1.

Each $\text{Ag}\in\mathfrak{A}$ has access to the traffic light states.

  2. 2.

There is no communication error in the conflict requests, token count queries
and the agent intention signals.

  3. 3.

All intersections in the road network $R$ are governed by traffic lights.

  4. 4.

The traffic lights are designed to coordinate traffic such that if agents
respect the traffic light rules, they will not collide.

  5. 5.

Agents follow the agent dynamics defined in Section III-A.

  6. 6.

For $t=0$, $\forall\text{Ag}\in\mathfrak{A}$ in the quasi-simultaneous game is
initialized to be located on a distinct grid point on the road network and
have a safe backup plan action $a_{bp}$ such that
$S_{\text{Ag},bp}(s,u)=\texttt{T}$.

  7. 7.

The traffic lights are red a window of time $\Delta t_{\text{tl}}$ such that
$t_{\text{min}}<\Delta t_{\text{tl}}<\infty$, where $t_{\text{min}}$ is
defined so agents are slowed down long enough so agents that have been waiting
can take a lane-change action. More details can be found in the Appendix.

  8. 8.

The static obstacles are not on any grid point $g$ where $g.d=1$.

  9. 9.

Each Ag treats its respective goal $\text{Ag}.\texttt{g}$ as a static
obstacle.

  10. 10.

Bundles in the road network $\mathfrak{R}$ have no more than 2 lanes.

  11. 11.

All intersections in the road network $\mathfrak{R}$ are governed by traffic
lights.

###  VI-A Safety Guarantee

Safety is guaranteed when agents do not collide with one another. An agent
causes collision when it takes an action that satisfies the following
condition.

######  Definition VI.1 (Collision)

An agent Ag that takes an action $a\in Act_{\text{Ag}}$ will cause collision
if the grid point occupancy of $Ag$ ever overlaps with the grid point
occupancy of another agent $Ag^{\prime}$ or a static obstacle $O_{\text{st}}$.

A strategy where agents simply take actions that avoid collision in the
current time-step is insufficient for guaranteeing safety because of the
inertial properties of the agent dynamics. The agent protocol has therefore
been defined so an agent also avoids violating the safety of its own and any
other agent’s backup plan action $a_{bp}$ defined in Section III-B. An agent’s
backup plan action $a_{bp}$ is evaluated to be safe when the following
conditions hold:

###### Definition VI.2

[Safety of a Backup Plan Action] Let us define the safety of an agent’s backup
plan action $S_{\text{Ag},bp}:\mathcal{U}=\mathbb{B}$, where
$\mathbb{B}=\\{\texttt{T},\texttt{F}\\}$ is an indicator variable that
determines whether an agent’s backup plan action is safe or not. It is defined
as: $S_{Ag,bp}(u)=\land_{o\in O}o(s,a_{bp},u)$ where the set $O$ is the set of
all oracles in the top three tiers of the agent profile defined in Section
V-B.

An agent Ag takes an action $a\in Act_{\text{Ag}}$ that violates the safety
backup plan action of another agent $\text{Ag}^{\prime}$ when the following
conditions hold:

######  Definition VI.3 (Safety Backup Plan Violation Action)

Let us consider an agent Ag that is taking an action $a\in Act_{\text{Ag}}$,
and another agent $\text{Ag}^{\prime}$. The action
$(\text{Ag},a)\bot\text{Ag}^{\prime}$, i.e. agent Ag violates the safety
backup plan of an agent $\text{Ag}^{\prime}$ when by taking an action $a$,
then $S_{\text{Ag}^{\prime},bp}(u^{\prime})=\texttt{F}$, where $u^{\prime}$ is
the state of the game after Ag has taken its action. In other words, by taking
the action, the agent has ended in a state such that it violates the safety of
its own or another agents’ backup plan action.

The safety proof is based on the premise that all agents only take actions
that do not collide with other agents and maintain the invariance of the
safety of their own and other agents’ safety backup plan actions. The safety
theorem statement and the proof sketch are as follows.

We can treat the quasi-simultaneous game as a program, where each of the
agents are separate concurrent processes. A safety property for a program has
the form $P\Rightarrow\square Q$, where $P$ and $Q$ are immediate assertions.
This means if the program starts with $P$ true, then $Q$ is always true
throughout its execution [15].

######  Theorem VI.1 (Safety Guarantee)

Given all agents $\text{Ag}\in\mathfrak{A}$ in the quasi-simultaneous game
select actions in accordance to the Agent Protocol specified in Section V,
then we can show the safety property $P\Rightarrow\square Q$, where the
assertion $P$ is an assertion that the state of the game is such that $\forall
Ag,S_{\text{Ag},bp}(s,u)=\texttt{T}$, i.e. each agent has a backup plan action
that is safe, as defined in Section VI.2. We denote $P_{t}$ as the assertion
over the state of the game at the beginning of the time-step $t$, before
agents take their respective actions. $Q_{t}$ is the assertion that the agents
never occupy the same grid point when taking their respective action at time
step $t$.

The following is a proof sketch.

###### Proof:

To prove an assertion of this form, we need to find an invariant assertion $I$
for which i) $P\Rightarrow I$ ii) $I\Rightarrow\square I$ and iii)
$I\Rightarrow Q$ hold. We define $I$ to be the assertion that holds on the
actions that agents select to take at a time-step. We denote $I_{t}$ to be the
assertion on the actions agents take at time $t$ such that $\forall Ag$, Ag
takes $a\in Act_{\text{Ag}}$ where 1) it does not collide with other agents
and 2) it does not violate the safety of other agents’ back up plan actions
(i.e. $\forall\text{Ag},S_{\text{Ag},bp}(u^{\prime})=\texttt{T}$ where
$s^{\prime}=\tau_{\text{Ag}}(s,a)$, and $u^{\prime}$ is the corresponding
global state of the game after each Ag has taken its respective action $a$).

We can prove $P\Rightarrow\square Q$ by showing the following:

  1. 1.

$P_{t}\Rightarrow I_{t}$. This is equivalent to showing that if all agents are
in a state where $P$ is satisfied at time $t$, then all agents will take
actions at time $t$ where the $I$ holds. This can be proven by showing agents
will take actions that satisfy the conditions of $I$ as long as they are begin
a state where all agents have a safe backup action and they select actions
according to the protocol.

  2. 2.

$I\Rightarrow\square I$. If agents take actions such that at time $t$ such
that the assertion $I_{t}$ holds, then by the definition of the assertion $I$,
agents will end up in a state where at time t+1, assertion $P$ holds, meaning
$I_{t}\Rightarrow P_{t+1}$. Since $P_{t+1}\Rightarrow I_{t+1}$ from 1, we get
$I\Rightarrow\square I$.

  3. 3.

$I\Rightarrow Q$. If all agents take actions according to the assertions in
$I$, then collisions will not occur. This follows from the definition of $I$.

∎

The reader is referred to the Appendix for a full proof. Proof of safety alone
is not sufficient reason to argue for the effectiveness of the protocol, as
all agents could simply stop for all time and safety would be guaranteed. A
liveness guarantee, i.e. proof that all agents will eventually make it to
their final destination, is critical. In the following section, we present
liveness guarantees.

###  VI-B Liveness Guarantees

A liveness property asserts that program execution eventually reaches some
desirable state [15]. In this paper, we describe the eventual desirable state
for each agent is to reach their respective final destinations. Unfortunately,
deadlock occurs when agents indefinitely wait for resources held by other
agents [19]. Since the Manhattan grid road network has loops, agents can enter
a configuration in which each agent in the loop is indefinitely waiting for a
resource held by another agent. When the density of agents in the road network
is high enough, deadlocks along these loops will occur. We can therefore
guarantee liveness only when certain assumptions hold on the density of the
road network.

######  Definition VI.4 (Sparse Traffic Conditions)

Let $M$ denote the number of grid points in the smallest loop (defined by
legal orientation) of the road network, not including grid points
$g\in\mathcal{S}_{\text{intersections}}$. The sparsity condition must be such
that $N<M-1$, where $N$ is the number of agents in the road network. The
number of agents has to be such that the smallest loop does not become
completely saturated, in which deadlock would occur. Note, these sparsity
conditions are conservative because it is a bound defined by the worst
possible assignment of agents and their destinations.

Now, we introduce the liveness guarantees under these sparse traffic
conditions. The proof of liveness is based on the fact that 1) agent profile
include progress specifications and 2) conflict precedence is resolved by
giving priority to the agent that has waited the longest time (a quantity that
is reflected by token counts).

######  Theorem VI.2 (Liveness Under Sparse Traffic Conditions)

Under the Sparse Traffic Assumption given by Definition VI.4 and given all
agents $\text{Ag}\in\mathfrak{A}$ in the quasi-simultaneous game select
actions in accordance to the Agent Protocol specified in Section V, liveness
is guaranteed, i.e. all $\text{Ag}\in\mathfrak{A}$ will always eventually
reach their respective goals.

The following is a proof sketch.

###### Proof:

  1. 1.

The invariance of a no-deadlock state follows from the sparsity assumption and
the invariance of safety (no collision) follows from the safety proof.

  2. 2.

Inductive arguments related to control flow are used to show that all Ag will
always eventually take $a\in Act_{\text{Ag}}$ where $O_{\text{forward
progress}}(s,a,u)=\texttt{T}$.

    1. (a)

Let us consider a road segment $r\in RS$ that contains grid point(s)
$g\in\mathcal{S}_{\text{sinks}}$ meaning that the road segment contains grid
points with sink nodes. Inductive arguments based on the agents’ longitudinal
distance to destination grid points are used to show every $\text{Ag}\in r$
will be able to always eventually take $a\in Act_{\text{Ag}}$ for which the
forward progress oracle $O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

    2. (b)

Let us consider a road segment $rs\in RS$. Let us assume $\forall rs\in
RS,\exists(rs,rs^{\prime})\in G_{\text{dep}}$ meaning that the clearance of
$rs$ depends on the clearance of all $rs^{\prime}$. Inductive arguments based
on agents’ longitudinal distance to the front of the intersection show any Ag
on $rs$ will always eventually take $a\in Act_{\text{Ag}}$ where the forward
progress oracle $O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

    3. (c)

For any $\mathfrak{R}$ where the dependency graph $G_{\text{dep}}$ (as defined
in Definition IV.2) is a directed-acyclic-graph (DAG), inductive arguments
based on the linear ordering of road segments $rs\in G_{\text{dep}}$, combined
with the arguments 2a-2b, can be used to prove all $\text{Ag}\in\mathfrak{A}$
will always eventually take $a\in Act_{\text{Ag}}$ for which the forward
progress oracle $O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

    4. (d)

When the graph $G_{\text{dep}}$ is cyclic, the Sparsity Assumption VI.4 allows
for similar induction arguments in 2c to apply.

  3. 3.

By the above inductive arguments and the definition of $O_{\text{forward
progress}}(s,a,u)$, all Ag will always eventually take actions that allow them
to make progress towards their respective destinations.

∎

The reader is referred to the Appendix for a full proof.

##  VII Simulation Results

In order to streamline discrete-time multi-agent simulations, we have built a
traffic game simulation platform called Road Scenario Emulator (RoSE). We use
RoSE to generate different game scenarios and simulate how agents will all
behave if they each follow the agent strategy protocol introduced in this
paper.

Figure 5: City blocks map environment.

We simulate the game with randomized initialization of spawning agents at the
source nodes for three different road network environments: 1) the straight
road segment, 2) small city blocks grid and 3) large city blocks grid. A
snapshot of a small city blocks grid simulation is shown in Fig. 5.

The agent attributes in this simulation are as follows: $v_{\text{min}}=0$,
$v_{\text{max}}=3$, $a_{\text{min}}=-1$, and $a_{\text{max}}=1$. For each road
network environment, we simulate the game 100 times for $t=250$ time-steps.
During each time-step, agents will spontaneously spawn with some defined
probability $p$ at the source nodes and are randomly assigned a sink node as
their destination. Agents that make it to their destinations exit the map. For
all game simulation trials, collision does not occur. Although liveness is
only guaranteed in sparse traffic conditions, we simulate for a number of
agents $N>M-1$ specified in the sparsity condition and agents do not enter a
deadlock state. In particular, over the 100 trials for each of the maps
(straight, small and large city blocks), on average $77\%$, $36\%$ and $43\%$
made it to their respective destinations on the respective maps by the end of
the 250 time-steps.

##  VIII Conclusion and Future Works

In this paper, we have proposed a novel paradigm for designing safety-critical
decision-making modules for agents whose behavior is extremely complex and
highly-coupled with other agents. The main distinction of our proposed
architecture from the existing literature, is the shift from thinking of each
agents as separate, individual entities, to agents as a collective where all
all agents adopt a common local, decentralized protocol. The protocol defines
the agent attributes, the region it must reason over (i.e. the bubble), how
the agent chooses its intended agent, and how it ultimately selects which
action to take. With this protocol, we are able to formally guarantee
specifications safety and liveness (under sparse traffic conditions) for all
agents. We validate the safety and liveness guarantees in a randomized
simulation environment.

The current work still lacks 1) liveness guarantees in all scenarios, 2)
robustness to imperfect sensory information and 3) does not account for other
agent types like pedestrians and cyclists. Future work on modifying the agent
strategy architecture to prevent the occurrence of the loop deadlock
introduced in Section VI-B from occurring. Additionally, the architecture must
be modified in a way to effectively accommodate impartial and imperfect
information. We also hope to accommodate a diverse, heterogenous set of car
agents and also other agent types like pedestrians and cyclists. Although the
work needs to be extended to make more applicable to real-life systems, we
believe this work is a first step towards defining a comprehensive method for
guaranteeing safety and liveness for all agents in an extremely dynamic and
complex environment.

## Acknowledgments

We would like to acknowledge K. Mani Chandy who provided valuable input and to
Giovanna Amorim for her contributions to the simulation code.

## Author Contributions

K.X.C., R.M.M., and T.P-M. jointly conceived the conceptual framework. K.X.C.
and T.P-M. jointly developed the problem formulation and theoretical approach.
K.X.C. worked out the main proofs with input from T.P-M. K.X.C. drafted the
manuscript and figures with input from T.P-M. S-J.C. and R.M.M. provided
guidance on the overall approach and provided feedback on the final
manuscript.

## References

  * [1] N. Arechiga.  Specifying safety of autonomous vehicles in signal temporal logic.  In 2019 IEEE Intelligent Vehicles Symposium (IV), pages 58–63, Paris, France, 2019. IEEE.
  * [2] C. Baier and J-P. Katoen.  Principles of Model Checking.  MIT Press, Cambridge, Massachussetts, 2008.
  * [3] Craig Boutilier.  Sequential optimality and coordination in multiagent systems.  In IJCAI, volume 99, pages 478–485, 1999.
  * [4] A. Censi, S. Bolognani, J. G. Zilly, S. S. Mousavi, and E. Frazzoli.  Today me, tomorrow thee: Efficient resource allocation in competitive settings using karma games.  In 2019 IEEE Intelligent Transportation Systems Conference (ITSC), pages 686–693, Auckland, New Zealand, 2019. IEEE.
  * [5] A. Censi, K. Slutsky, T. Wongpiromsarn, D. Yershov, S. Pendleton, J. Fu, and E. Frazzoli.  Liability, ethics, and culture-aware behavior specification using rulebooks.  In 2019 International Conference on Robotics and Automation (ICRA), pages 8536–8542, Montreal, QC, Canada, 2019. IEEE.
  * [6] K. M. Chandy and J. Misra.  The drinking philosophers problem.  ACM Transactions on Programming Languages and Systems (TOPLAS), 6(4):632–646, 1984.
  * [7] C. Finn, S. Levine, and P. Abbeel.  Guided cost learning: Deep inverse optimal control via policy optimization.  In International conference on machine learning, pages 49–58, New York, New York, USA, 2016. JMLR.
  * [8] J. F. Fisac, E. Bronstein, E. Stefansson, D. Sadigh, S. S. Sastry, and A. D. Dragan.  Hierarchical game-theoretic planning for autonomous vehicles.  In 2019 International Conference on Robotics and Automation (ICRA), pages 9590–9596, Montreal, Canada, 2019. IEEE.
  * [9] D. Fudenberg and J. Tirole.  Game Theory.  MIT Press, USA, 1991.
  * [10] P. J. Gmytrasiewicz and P. Doshi.  A framework for sequential planning in multi-agent settings.  Journal of Artificial Intelligence Research, 24:49–79, 2005.
  * [11] N. A. Greenblatt.  Self-driving cars and the law.  IEEE Spectrum, 53(2):46–51, 2 2016.
  * [12] M. Herman, V. Fischer, T. Gindele, and W. Burgard.  Inverse reinforcement learning of behavioral models for online-adapting navigation strategies.  In 2015 IEEE International Conference on Robotics and Automation (ICRA), pages 3215–3222. IEEE, 2015.
  * [13] W. Li, D. Sadigh, S. S. Sastry, and S. A. Seshia.  Synthesis for human-in-the-loop control systems.  In TACAS, pages 470–484, Grenoble, France, 2014. Springer Berlin Heidelberg.
  * [14] A. Lomuscio, H. Qu, and F. Raimondi.  Mcmas: an open-source model checker for the verification of multi-agent systems.  International Journal on Software Tools for Technology Transfer, 19(1):9–30, 2017.
  * [15] S. Owicki and L. Lamport.  Proving liveness properties of concurrent programs.  ACM Transactions on Programming Languages and Systems (TOPLAS), 4(3):455–495, 1982.
  * [16] B. Paden, M. Cap, S. Z. Yong, D. Yershov, and E. Frazzoli.  A survey of motion planning and control techniques for self-driving urban vehicles.  T-IV, 1(1):33–55, 3 2016.
  * [17] C. H. Papadimitriou and J. N. Tsitsiklis.  The complexity of markov decision processes.  Mathematics of operations research, 12(3):441–450, 1987.
  * [18] T. Phan-Minh, K. X. Cai, and R. M. Murray.  Towards assume-guarantee profiles for autonomous vehicles.  In 2019 IEEE 58th Conference on Decision and Control (CDC), pages 2788–2795, Nice, France, 2019. IEEE.
  * [19] S. A. Reveliotis and E. Roszkowska.  On the complexity of maximally permissive deadlock avoidance in multi-vehicle traffic systems.  IEEE Transactions on Automatic Control, 55(7):1646–1651, 2010.
  * [20] D. Sadigh, A. D. Dragan, S. Sastry, and S. A. Seshia.  Active preference-based learning of reward functions.  In Robotics: Science and Systems (RSS), Berlin, Germany, 2013.
  * [21] D. Sadigh, S. Sastry, S. A. Seshia, and A. D. Dragan.  Planning for autonomous cars that leverage effects on human actions.  In Robotics: Science and Systems (RSS), volume 2, Ann Arbor, MI, USA, 2016.
  * [22] Y. E. Sahin and N. Ozay.  From drinking philosophers to wandering robots.  arXiv preprint arXiv:2001.00440, 2020.
  * [23] S. Shalev-Shwartz, S. Shammah, and A. Shashua.  On a Formal Model of Safe and Scalable Self-driving Cars.  arXiv e-prints, page arXiv:1708.06374, 8 2017.
  * [24] Y. Shoham and M. Tennenholtz.  On social laws for artificial agent societies: off-line design.  Artificial intelligence, 73(1-2):231–252, 1995.
  * [25] M. Sipser.  Introduction to the Theory of Computation.  Cengage Learning, USA, 2012.
  * [26] J. Tumova, G. C. Hall, S. Karaman, E. Frazzoli, and D. Rus.  Least-violating control strategy synthesis with safety rules.  In Proceedings of the 16th international conference on Hybrid systems: computation and control, pages 1–10, Philadelphia, Pennsylvania, USA, 2013. ACM.
  * [27] W. van Der Hoek, M. Roberts, and M. Wooldridge.  Social laws in alternating time: Effectiveness, feasibility, and synthesis.  Synthese, 156(1):1–19, 2007.
  * [28] T. Wongpiromsarn, S. Karaman, and E. Frazzoli.  Synthesis of provably correct controllers for autonomous vehicles in urban environments.  In ITSC, pages 1168–1173, Washington, DC, USA, 10 2011. IEEE.
  * [29] T. Wongpiromsarn, K. Slutsky, E. Frazzoli, and U. Topcu.  Minimum-violation planning for autonomous systems: Theoretical and practical considerations.  arXiv preprint arXiv:2009.11954, 2020.
  * [30] T. Wongpiromsarn, A. Ulusoy, C. Belta, E. Frazzoli, and D. Rus.  Incremental synthesis of control policies for heterogeneous multi-agent systems with linear temporal logic specifications.  In ICRA, pages 5011–5018, 5 2013.

###  -A Road Network

The following defines the set of properties that grid points can have.

####  -A1 Grid Point Properties

The set of properties $\mathcal{P}=\\{p,d,$ lo$\\}$ of each grid point $g\in
G$. $p\in\mathbb{Z}^{2}$ denotes the Cartesian coordinate of the grid point,
$d\in\\{0,1\\}$, which is an indicator variale that defines whether or not the
grid point is drivable, lo is the legal orientation, where the legal
orientation is an element of the set
$\\{\texttt{north},\texttt{east},\texttt{south},\texttt{west}\\}$. The set lo
may be empty when the grid point is not drivable.

Figure 6: Road network decomposition where each box represents a grid point.

The following are sets of labeled grid points on the road network map.

  1. 1.

$\mathcal{S}_{\text{intersection}}$: A set of grid points that contains all
grid points with more than one legal orientation.

  2. 2.

$\mathcal{S}_{\text{traffic light}}$: A set of grid points that represent the
traffic light states in the vertical or horizontal direction via its color
(for every intersection).

The road network is hierarchically decomposed into lanes and bundles, which
are defined informally as follows:

  * •

Lanes: Let lane $La(g)$ denote a set of grid points that contains all grid
points that are in the same ‘lane’ as $g$.
$La(g)=\\{g^{\prime}|\text{proj}_{x}(g^{\prime}.p)=\text{proj}_{x}(g.p)$ or
$\text{proj}_{y}(g.p)=\text{proj}_{y}(g.p),$
$g^{\prime}.\phi_{l}=g.\phi_{l},g.\texttt{drivable}=g^{\prime}.\text{drivable}=1\\}$.

  * •

Bundles: First, we define the set of adjacent lanes to lane $La(g)$ as
$\texttt{adj}(La(g))=\\{La(g^{\prime})\mid\exists
e=(\hat{g},\hat{g}^{\prime})\in\mathfrak{R}\text{ s.t. }(\hat{g}\in
La(g),\hat{g^{\prime}}\in La(g^{\prime}))\text{ and
}\hat{g}.\phi_{l}=\hat{g^{\prime}}.\phi_{l}\\}$. This represents the set of
lanes $La(g)$ in the same direction that the lane is adjacent to. Let $N(g)$ =
adj(La(g)). Let bundle $Bu(g)$ denote a set of lanes that are all connected to
one another and is defined recursively as follows:

$Bu(g)=\begin{cases}La(g)\cup N(g)\text{ if }N(g)\neq\emptyset\\\
La(g)&\text{otherwise}.\end{cases}$

For clarity of the road network decomposition, refer to Fig. 2. With slight
abuse of notation, we let $La(\text{Ag})$ refer to the lane ID associated with
the grid point $(s.x_{\text{Ag}},s.y_{\text{Ag}})$, and $Bu(\text{Ag})$ mean
the bundle ID associated with the lane $La(\text{Ag})$.

###  -B Agent Backup Plan Action

######  Definition .1 (Backup Plan Action)

The backup plan action $a_{bp}$ is a control action where $a=a_{\text{min}}$
and when applying $a_{\text{min}}$ causes the agent’s velocity to go below 0,
$a=\text{max}(a_{\text{min}},-s.v_{Ag})$ and
$\gamma_{\text{Ag}}=\texttt{straight}$.

###  -C Bubble Construction

In order to define the bubble for the agent dynamics specified in Section
III-A, we present some preliminary definitions. We first introduce the backup
plan node set (which is defined recursively) as follows:

######  Definition .2 (Backup Plan Node Set)

Let $\text{Ag}\in\mathfrak{A}$ and $s_{0}\in S_{\text{Ag}}$. The backup plan
grid point set $BP_{\text{Ag}}(s_{0})$ is all the grid points agent Ag
occupies as it applies maximum deceleration to come to a complete stop.

$BP_{\text{Ag}}(s_{0})=\begin{cases}\mathcal{G}_{\text{Ag}}(s_{0},a_{{\text{bp}}})\cup
BP_{\text{Ag}}(\tau_{\text{Ag}}(s_{0},a_{{\text{bp}}}))&\text{if
$\tau_{\text{Ag}}(s_{0},a_{{\text{bp}}}).v\neq 0$}\\\
\mathcal{G}_{\text{Ag}}(\tau(s_{0},a_{{\text{bp}}}))&\text{otherwise}.\end{cases}$

where $a_{\text{min}}$ is the agent’s action of applying maximal deceleration
while keeping the steering wheel at the neutral position.

######  Definition .3 (Forward/Backward Reachable States)

The (1-step) forward reachable state set of agent Ag denoted
$\mathcal{R}_{\text{Ag}}(s_{0})$ represents the set of all states reachable by
Ag from the state $s_{0}$. The forward reachable set is defined as
$\mathcal{R}_{\text{Ag}}(s_{0})\triangleq\\{s\in S_{\text{Ag}}\mid\exists
a\in\rho_{\text{Ag}}(s_{0}).s=\tau(s_{0},a)\\}$. Similarly, we define the
(1-step) backward reachable state set $\mathcal{R}^{-1}_{\text{Ag}}(s_{0})$ as
the set of all states from which the state $s_{0}$ can be reached by Ag.
Formally, $\mathcal{R}^{-1}_{\text{Ag}}(s_{0})\triangleq\\{s\in
S_{\text{Ag}}\mid\exists s\in S_{\text{Ag}}.\exists
a\in\rho_{\text{Ag}}(s).s_{0}=\tau(s,a)\\}.$

######  Definition .4 (Forward Reachable Nodes)

We denote by $\mathcal{G}^{\mathcal{R}}_{\text{Ag}}(s_{0})$ the forward
reachable node set, namely, the set of all grid points that can be occupied
upon taking the actions that brings the agent Ag from its current state
$s_{0}$ to a state in $\mathcal{R}_{\text{Ag}}(s_{0})$. Specifically,

$\mathcal{G}^{\mathcal{R}}_{\text{Ag}}(s_{0})\triangleq\bigcup_{a\in\rho_{Ag}(s_{0})}\mathcal{G}_{\text{Ag}}(s_{0},a)$

This set represents all the possible grid points that can be occupied by an
agent in the next time step.

######  Definition .5 (Occupancy Preimage)

For $n\in G$, where $G$ are the nodes in the road network graph
$\mathfrak{R}$, the occupancy preimage
$\mathcal{G}^{\mathcal{R}^{-1}}_{\text{Ag}}(n)$ is the set of states of agent
Ag from which there is an action that causes $n$ to be occupied in the next
time step. Formally,

$\mathcal{G}^{\mathcal{R}^{-1}}_{\text{Ag}}(n)=\\{s\in
S_{\text{Ag}}\mid\exists
a\in\rho_{\text{Ag}}(s).n\in\mathcal{G}_{\text{Ag}}(s,a)\\}$

In the next section, we define several different sets of grid points that are
defined to represent the locations where two agents may possibly interfere
with one another, which are shown in Fig. 7. The bubble is defined to be the
union of these sets of grid points.

Figure 7: Bubble if all $\text{Ag}\in\mathfrak{A}$ have the Agent Dynamics
specified in Section III-A. Construction of this set defined in the Appendix.

We begin by considering the ego agent whose bubble we are defining. In
particular, let us again consider an agent Ag at state $s_{0}\in S_{Ag}$. The
corresponding grid point set $\mathcal{G}_{\text{Ag}}^{\mathcal{R}}(s_{0})$ is
shown in the left-most figure in Fig. 7. The grid points an agent occupies
when executing its backup plan from a state in the agent’s forward reachable
set $\mathcal{R}_{\text{Ag}}(s_{0})$ is given by:

$\mathcal{G}^{\mathcal{R},BP}_{\text{Ag}}(s_{0})\triangleq\bigcup_{s\in\mathcal{R}_{\text{Ag}}(s_{0})}BP_{\text{Ag}}(s)$

These grid points are shown in the second from the left sub-figure in Fig. 7.
The set-valued map

$\mathcal{Z}_{\text{Ag}}(s_{0})\triangleq\mathcal{G}^{\mathcal{R}}_{\text{Ag}}(s_{0})\cup\mathcal{G}^{\mathcal{R},BP}_{\text{Ag}}(s_{0}).$

represents all the grid points an agent can possibly reach in the next state
or in the following time step were it to execute its backup plan. Let
$\text{Ag}^{\prime}\in\mathfrak{A}$ and $\text{Ag}^{\prime}\neq\text{Ag}$. The
set:

$\mathcal{S}_{\text{Ag}^{\prime}}^{\mathcal{R}}(\text{Ag},s_{0})\triangleq\bigcup_{n\in\mathcal{Z}_{\text{Ag}}(s_{0})}\mathcal{G}^{\mathcal{R}^{-1}}_{\text{Ag}^{\prime}}(n)$

defines the set of all states in which another agent $\text{Ag}^{\prime}$ can
reach any grid point in the other agents’ forward reachable grid points
$\mathcal{Z}_{\text{Ag}}(s_{0})$. Let us define the grid point projection of
these states as

$\mathcal{G}_{\text{Ag}^{\prime}}^{\mathcal{R}}(\text{Ag},s_{0})\triangleq\\{\mathcal{G}_{\text{Ag}^{\prime}}(s)\mid
s\in\mathcal{S}_{\text{Ag}^{\prime}}^{\mathcal{R}}(\text{Ag},s_{0})\\}.$

These grid points are defined in the third from the left subfigure in Fig. 7.

The bubble also needs to include any state where an agent $\text{Ag}^{\prime}$
where the agent has so much momentum it cannot stop fast enough to avoid
collision with the agent Ag. To define the set of states from which this might
occur, let us define the set:

$\mathcal{S}^{BP}_{Ag^{\prime}}(Ag,s_{0})=\\{s\in S_{Ag^{\prime}}\mid
BP_{Ag^{\prime}}(s)\cap\mathcal{Z}_{Ag}(s_{0})\neq\emptyset\\}.$

If another agent $\text{Ag}^{\prime}$ occupies a state in this set, then
execution of that agent’s backup plan will cause it to intersect with the set
of grid points that are in agents set $\mathcal{Z}_{\text{Ag}}(s_{0})$. Let

$\mathcal{S}^{\mathcal{R},BP}_{\text{Ag}^{\prime}}(\text{Ag},s_{0})=\bigcup_{s\in\mathcal{S}^{BP}_{\text{Ag}^{\prime}}(\text{Ag})}\mathcal{R}_{\text{Ag}^{\prime}}^{-1}(s).$

This is the set of all states backward reachable to the states in
$\mathcal{S}^{BP}_{\text{Ag}^{\prime}}(\text{Ag},s_{0})$. If an agent
$\text{Ag}^{\prime}$ occupies any of these states, it will end up in a state
where its backup plan will intersect with agent Ag’s potential grid points
that are defined in $\mathcal{Z}_{\text{Ag}}$. We project this set of states
to a set of grid points as

$\mathcal{G}^{\mathcal{R},BP}_{\text{Ag}^{\prime}}(\text{Ag},s_{0})=\\{\mathcal{G}_{Ag^{\prime}}(s)\mid
s\in\mathcal{S}^{BP}_{Ag^{\prime}}(Ag,s_{0})\\}.$

Note, this set of grid points is shown in the right-most subfigure in Fig. 7.
The bubble is then defined as the union of all the sets of grid points
specified above.

######  Definition .6 (Bubble)

Let us consider an agent Ag with state $s_{0}\in S_{\text{Ag}}$ and agent
$\text{Ag}^{\prime}$ be another agent. Then the bubble of Ag with respect to
agents of the same type as $\text{Ag}^{\prime}$ is given by

$\mathcal{B}_{\text{Ag}/\text{Ag}^{\prime}}(s_{0})\triangleq\mathcal{Z}_{\text{Ag}}(s_{0})\cup\mathcal{G}_{\text{Ag}^{\prime}}^{\mathcal{R}}(\text{Ag},s_{0})\cup\mathcal{G}^{\mathcal{R},BP}_{\text{Ag}^{\prime}}(\text{Ag},s_{0}).$

Note that under almost all circumstances, we should have

$\mathcal{Z}_{\text{Ag}}(s_{0})\subseteq\mathcal{G}^{\mathcal{R}}_{\text{Ag}^{\prime}}(Ag,s_{0})\subseteq\mathcal{G}^{\mathcal{R},BP}_{\text{Ag}^{\prime}}(\text{Ag},s_{0})$

so $\mathcal{B}_{\text{Ag}}(s_{0})$ is simply equal to
$\mathcal{G}^{\mathcal{R},BP}_{\text{Ag}^{\prime}}(\text{Ag},s_{0})$. This
holds true for the abstract dynamics we consider in this paper. This means the
bubble contains any grid points in which another agent $\text{Ag}^{\prime}$
occupying those grid points can interfere (via its own forward reachable
states or the backup plan it would use in any of its forward reachable states)
with at least one of agent Ag’s next possible actions and the backup plan it
would use if it were to take any one of those next actions.

###  -D Global Precedence Consistency

###### Lemma .1

If all agents assign precedence according to the local precedence assignment
rules to agents in their respective bubbles, then the precedence relations
will induce a polyforest on $\mathfrak{A}/\sim$, where $S/\sim$ defines the
quotient set of a set $S$.

###### Proof:

Suppose there is a cycle $C$ in $\mathfrak{A}/\sim$. For each of the
equivalent classes in $C$ ($C$ must have at least $2$ to be a cycle), choose a
representative from $\mathfrak{A}$ to form a set $R_{C}$. Let $\text{Ag}\in
R_{C}$ be one of these representatives. Applying the second local precedence
assignment rule inductively, we can see that all agents in $R_{C}$ must be
from Ag’s bundle. By the first local precedence assignment rule, any $C$ edge
must be from an agent with lower projected value to one with a higher
projected value in this bundle. Since these values are totally ordered (being
integers), they must be the same. This implies that $C$ only has one
equivalence class, a contradiction. ∎

The acyclicity of the polyforest structure implies the consistency of local
agent precedence assignments. Note, the local precedence assignment algorithm
establishes the order in which agents are taking turns.

###  -E Oracle Definitions

  1. 1.

$O_{\text{Ag},t,\text{unprotected left-turn safety}}(s,a,u)$ returns T when
the action $a$ from the state $s$ will result in the complete execution of a
safe, unprotected left-turn (invariant to agent precedence). Note, an
unprotected left turn spans over multiple time-steps. The oracle will return T
if Ag has been waiting to take left-turn (while traffic light is green),
traffic light turns red, and no agents in oncoming lanes.

  2. 2.

$O_{\text{static safety}}(s,a,u)$ returns T when the action $a$ from state $s$
will not cause the agent to collide with a static obstacle or end up in a
state where the agent’s safety backup plan $a_{bp}$ with respect to the static
obstacle is no longer safe.

  3. 3.

$O_{\text{traffic light law}}(s,a,u)$ returns T if the action $a$ from the
state $s$ satisfies the traffic light laws (not crossing into intersection
when red. It also requires that Ag be able to take $a_{bp}$ from
$s^{\prime}=\tau_{\text{Ag}}(s,a)$ and not violate the traffic-light law.

  4. 4.

$O_{\text{traffic orientation law}}(s,a,u)$ returns T if the action $a$ from
the state $s$ follows the legal road orientation.

  5. 5.

$O_{\text{traffic intersection clearance law}}(s,a,u)$ returns T if the action
causes the agent to enter the intersection and not leave it when the traffic
light turns red. Returns T if the action causes the agent to end in a state
where its backup plan action will cause the agent to enter the intersection
and not be able to leave it when the traffic light turns red.

  6. 6.

$O_{\text{traffic intersection lane change law}}(s,a,u)$ returns T if the
action is such that
$\gamma_{Ag}=\\{\texttt{left-lane change},\texttt{right-lane change}\\}$ and
the agent either begins in an intersection or ends up in the intersection
after taking the action.

  7. 7.

$O_{\text{maintains progress}}(s,a,u)$ returns T if the action $a$ from the
state $s$ stays the same distance to its goal.

###  -F Action Selection Strategy

Figure 8: Agent action selection strategy.

###  -G Safety Lemmas

In the following lemma, we show that an agent cannot send (or receive) a
conflict request to (from) an agent outside its bubble.

###### Lemma .2

Let us consider agent Ag with state $s$ and agent $\text{Ag}^{\prime}$ at
state $s^{\prime}$. $\text{Ag}\texttt{ send
}\text{Ag}^{\prime}\Rightarrow\text{Ag}\in\mathcal{B}_{\text{Ag}^{\prime}}(s^{\prime})$.

###### Proof:

If $A\texttt{ send }B$ this means that all of the conditions specified in
Section V.1, particularly that $(A,a_{i})\dagger(B,a_{i}^{\prime})$. This
condition is only valid if $\text{proj}_{G}s\in\mathcal{G}_{F,B}(B,A)$ or
$\text{proj}_{G}s\in\mathcal{G}_{F,BP}(B,A)$. Membership of Agent A’s state in
either of these sets implies $A\in\mathcal{B}(B)$. ∎

The following lemma follows from the lemma above.

###### Lemma .3

At most one agent will win in each agent’s conflict cluster.

###### Proof:

W.l.o.g. let us consider an agent Ag and its respective conflict cluster
$\mathcal{C}(\text{Ag})$. It follows from Lemma .2 that
$\forall\text{Ag}^{\prime}$, s.t. $\text{Ag}\texttt{ send
}\text{Ag}^{\prime}\text{Ag}^{\prime}\in\mathcal{B}_{Ag}(s)$ and
$\text{Ag}\in\mathcal{B}_{Ag^{\prime}}(s^{\prime})$. It also follows that
$\forall\text{Ag}^{\prime}\text{ s.t. },\text{Ag}\texttt{ send
}\text{Ag}^{\prime},\text{Ag}\in\mathcal{B}_{\text{Ag}^{\prime}}(s^{\prime})$
and $\text{Ag}^{\prime}\in\mathcal{B}_{\text{Ag}}(s)$. This means an agent has
access to all token counts and IDs of all agents in its conflict cluster, and
all agents in its conflict cluster have access to the agent’s token count and
ID. The conflict resolution implies that all agent edges are incident to the
winning agent, where edges point to the agent they cede to. This implies that
at most one agent can be the winner of each cluster. Less than one winner (per
conflict cluster) will occur when an agent that is in the intersection of more
than one conflict cluster wins. ∎

The following lemma states that if all $\text{Ag}\in\mathfrak{A}$ are
following the Agent Protocol, an agent Ag will not take an action that will
cause it to 1) collide with or 2) violate the safety backup plan of another
agent outside its bubble $\mathcal{B}_{\text{Ag}}(s)$.

###### Lemma .4

If Ag is following the Agent Protocol, and $S_{\text{Ag},bp}(u)=\texttt{T}$,
Ag will only choose an action $a\in Act_{\text{Ag}}$ for which the following
two conditions hold: 1)
$\mathcal{G}_{\text{Ag}}(s,a)\cap(\cup_{\text{Ag}^{\prime}\in
S}\mathcal{G}_{\text{Ag}^{\prime}}(s^{\prime},a^{\prime}))=\emptyset$ and 2)
$\forall\text{Ag}^{\prime}\in S$,
$\lnot((\text{Ag},a)\bot\text{Ag}^{\prime})$, where the set
$S\triangleq\\{\text{Ag}^{\prime}|\text{Ag}^{\prime}\notin\mathcal{B}_{\text{Ag}}(s)\land((\text{Ag}^{\prime}\sim\text{Ag})\lor(\text{Ag}^{\prime}\prec\text{Ag})\lor(\text{Ag}\prec\text{Ag'}))\\}$.

###### Proof:

This follows from the definition of the agent bubble, whose construction is
defined in -C. ∎

The following lemma states that an agent Ag following the Agent Protocol will
not take an action for which it violates the safety of its own backup plan.

###### Lemma .5

If Ag is following the Agent Protocol, and $S_{\text{Ag},bp}(u)=\texttt{T}$,
Ag will only choose an action $a\in Act_{\text{Ag}}$ for which the following
condition holds: $\forall\text{Ag}^{\prime}\in S$, $\lnot((\text{Ag},a)\bot
Ag^{\prime})$, where $S=\\{\text{Ag}\\}$.

###### Proof:

We prove this by using specific definition of elements in the Agent Protocol.

  1. 1.

Let us first show that any action $a\in Act_{\text{Ag}}$ that Ag takes will
satisfy the oracles in the top two tiers (safety and traffic rules) of Ag’s
profile defined in Section. V-B.

    1. (a)

According to the Action Selection Strategy defined in Section V-D, Ag will
choose one of three actions: the agent’s intended action $a_{i}$, the best
straight action $a_{st}$, or its backup plan action $a_{bp}$.

    2. (b)

Let us consider the actions $a_{i}$ and $a_{st}$.

      1. i.

Both $a_{i}$ and $a_{st}$ are selected via the Agent Profile and consistent-
function evaluator defined in Section V-B.

      2. ii.

Since $S_{\text{Ag},bp}(u)=\texttt{T}$, the agent will have at least one
action ($a_{bp}$) for which the top two tiers of specifications are satisfied.

      3. iii.

By definition of the Agent Profile and the consistent evaluator function, if
$S_{\text{Ag},bp}(u)=\texttt{T}$, the safety backup plan action $a_{bp}$ will
always be chosen over an action where any of the specifications in the top two
tiers of the profile are not satisfied.

      4. iv.

By 1(b)ii and 1(b)iii, Ag will have $a\in Act_{Ag}$ and will choose an action
for which the top two tiers of the Agent Profile are satisfied and thus
$a_{i}$ and $a_{st}$ are actions where all oracles in the top two tiers of the
profile are satisfied.

    3. (c)

Let us consider the action $a_{bp}$.

      1. i.

This follows from the assumption that $S_{\text{Ag},bp}(u)=\texttt{T}$ and the
definition of $S_{\text{Ag},bp}(u)$.

  2. 2.

If the oracles in the top two tiers are satisfied by an action $a$, by the
definition of the oracles in Section V-B, this implies that the action $a$
will take Ag to a state $s^{\prime}$ and the system will be in a new global
state $u^{\prime}$ where $S_{Ag,bp}(u^{\prime})=\texttt{T}$.

  3. 3.

$S_{Ag,bp}(u^{\prime})=T$ means Ag will end up in a state where $a_{bp}$ will
be an action that satisfies traffic rules, avoids inevitable collision with
static obstacles, and $\lnot((Ag,a_{i})\bot\text{Ag})$.

∎

The following lemma states that if all $\text{Ag}\in\mathfrak{A}$ are
following the Agent Protocol, any agent Ag will not take an action for which
it collides with or violates the safety backup plan of any agent with higher
precedence.

###### Lemma .6

If Ag is following the Agent Protocol, and $S_{\text{Ag},bp}(u)=\texttt{T}$,
Ag will only choose an action $a\in Act_{\text{Ag}}$ for which the following
two conditions hold: 1) $\mathcal{G}_{Ag}(s,a)\cap(\cup_{Ag^{\prime}\in
S}\mathcal{G}_{\text{Ag}^{\prime}}(s^{\prime},a^{\prime}))=\emptyset$ and 2)
$\forall\text{Ag}^{\prime}\in S$, $\lnot((Ag,a)\bot Ag^{\prime})$, where the
set $S\triangleq\\{\text{Ag}^{\prime}|\text{Ag}\prec\text{Ag}^{\prime}\\}$,
i.e. agents with higher precedence than Ag.

###### Proof:

We prove this by using arguments based on the definition of precedence, the
Agent Protocol, and Agent Dynamics.

  1. 1.

Let us first consider all $\text{Ag}^{\prime}$ where
$\text{Ag}\prec\text{Ag}^{\prime}$ and
$Ag^{\prime}\notin\mathcal{B}_{\text{Ag}}(s)$.

    1. (a)

Proof by Lemma .4.

  2. 2.

Now, let us consider all $\text{Ag}^{\prime}$ where
$\text{Ag}\prec\text{Ag}^{\prime}$ and
$\text{Ag}^{\prime}\in\mathcal{B}_{\text{Ag}}(s)$.

  3. 3.

According to Lemma .5, Ag will only take an action that satisfies all oracles
in the top two tiers, including
$O_{\text{dynamic safety}}(s,a,u)$.

  4. 4.

Since $a$ is such that $O_{\text{dynamic safety}}(s,a,u)=\texttt{T}$, by
definition of the oracle, $Ag$ will not cause collision with any
$Ag^{\prime}\in\mathcal{B}_{\text{Ag}}(s)$.

  5. 5.

For any $\text{Ag}\prec\text{Ag}^{\prime}$, where $\text{Ag}^{\prime}$ has
higher precedence than Ag, then
$\text{proj}_{\text{long}}(\text{Ag})<\text{proj}_{\text{long}}(\text{Ag}^{\prime})$,
i.e. $\text{Ag}^{\prime}$ is longitudinally ahead of Ag.

  6. 6.

In order for $(\text{Ag},a)\bot\text{Ag}^{\prime}$, the action $a$ would have
to be such that $s_{f}=\tau_{Ag}(s,a)$, and $La(s_{f})=La(s^{\prime})$ and
$\text{proj}_{\text{long}}(\text{Ag})>\text{proj}_{\text{long}}(\text{Ag}^{\prime})$,
where Ag is directly in front of $\text{Ag}^{\prime}$.

  7. 7.

Because of the agent dynamics defined in Section III-A, any $a$ such that
$(\text{Ag},a)\bot\text{Ag}^{\prime}$ will require
$\mathcal{G}(\text{Ag},a)\cap\mathcal{G}(\text{Ag}^{\prime})\neq\emptyset$.

  8. 8.

Thus, any such action $a$ will not satisfy the oracle
$O_{\text{dynamic safety}}(s,a,u)$.

  9. 9.

Since $S_{\text{Ag},bp}(u)=\texttt{T}$, by Assumption 6 in Section VI, the
agent will have at least one action $a_{bp}$ for which
$O_{\text{dynamic safety}}(s,a,u)=\texttt{T}$.

  10. 10.

Since the agent will only choose an action for which
$O_{\text{dynamic safety}}(s,a,u)=\texttt{T}$ and it always has at least one
action $a_{bp}$ that satisfies the oracle, the agent will always choose an
action for which $O_{\text{dynamic safety}}(s,a,u)=\texttt{T}$ and thus will
take an action such that $\lnot((\text{Ag},a)\bot\text{Ag}^{\prime})$.

∎

The following lemma states that if all $\text{Ag}\in\mathfrak{A}$ are
following the Agent Protocol, any agent Ag will not take an action for which
it collides with or violates the safety backup plan of any agent with lower
precedence.

###### Lemma .7

If Ag is following the Agent Protocol, and $S_{\text{Ag},bp}(u)=\texttt{T}$,
Ag will only choose an action $a\in Act_{\text{Ag}}$ for which the following
two conditions hold: 1) $\mathcal{G}_{Ag}(s,a)\cap(\cup_{Ag^{\prime}\in
S}\mathcal{G}_{\text{Ag}^{\prime}}(s^{\prime},a^{\prime}))=\emptyset$ and 2)
$\forall Ag^{\prime}\in S$, $\lnot((Ag,a)\bot Ag^{\prime})$, where the set
$S\triangleq\\{\text{Ag}^{\prime}|\text{Ag}^{\prime}\prec\text{Ag}\\}$, i.e.
agents with lower precedence than Ag.

###### Proof:

We prove this by using arguments based on the definition of precedence, the
Agent Protocol, and Agent Dynamics.

  1. 1.

Let us first consider all $\text{Ag}^{\prime}$ where
$\text{Ag}\prec\text{Ag}^{\prime}$ and
$\text{Ag}^{\prime}\notin\mathcal{B}_{\text{Ag}}(s)$.

    1. (a)

Proof by Lemma .4.

  2. 2.

Now, let us consider all $\text{Ag}^{\prime}$ where
$\text{Ag}\prec\text{Ag}^{\prime}$ and
$\text{Ag}^{\prime}\in\mathcal{B}_{\text{Ag}}(s)$.

  3. 3.

According to 3, Ag will only take an action that satisfies all oracles in the
top two tiers, including $O_{\text{dynamic safety}}(s,a,u)$.

  4. 4.

Since $a$ is such that $O_{\text{dynamic safety}}(s,a,u)=\texttt{T}$, by
definition of the oracle, $Ag$ will not cause collision with any
$Ag^{\prime}\in\mathcal{B}_{\text{Ag}}(s)$.

  5. 5.

According to the Action Selection Strategy defined in Section V-D, Ag will
choose one of three actions: the agent’s intended action $a_{i}$, the best
straight action $a_{st}$, or its backup plan action $a_{bp}$.

  6. 6.

Let us consider the backup plan action $a_{bp}$.

    1. (a)

By violation of safety backup plan,
$((\text{Ag},a_{bp})\bot\text{Ag}^{\prime})$ only if
$La(\text{Ag})=La(\text{Ag}^{\prime})$.

    2. (b)

W.l.o.g., let us consider $\text{Ag}^{\prime}$ that is directly behind Ag.

    3. (c)

Since $S_{\text{Ag}^{\prime},bp}(s,u)=\texttt{T}$, by Assumption 6 in Section
VI, $O_{\text{dynamic safety}}(s,a_{bp},u)=\texttt{T}$, meaning
$\text{Ag}^{\prime}$ will be far enough behind Ag so that if Ag executes its
backup plan action $a_{bp}$, $\text{Ag}^{\prime}$ can safely execute its own
backup plan action.

    4. (d)

Thus, by Definition VI.3, $\lnot((\text{Ag},a_{bp})\bot\text{Ag}^{\prime})$.

  7. 7.

Let us consider the best straight action $a_{st}$.

    1. (a)

This follows from the arguments made in 6, since $a_{st}$ is a less severe
action than $a_{bp}$.

  8. 8.

Let us consider the intended action $a_{i}$.

    1. (a)

Let us consider when $\gamma_{\text{Ag}}=\\{\texttt{straight}\\}$.

      1. i.

This follows from 6.

    2. (b)

Let us consider when $\gamma_{\text{Ag}}\in\\{\texttt{right-
turn},\texttt{left-turn}\\}$.

      1. i.

If Ag takes such an action, Ag will end up in a state where
$Bu(\text{Ag}^{\prime})\neq Bu(\text{Ag})$ and from Definition VI.3, agents in
different bundles cannot violate each others’ backup plans.

    3. (c)

Let us consider when $\gamma_{\text{Ag}}\in\\{\texttt{right-lane change}$
$\texttt{left-lane change}\\}$.

      1. i.

$(\text{Ag},a_{i})\bot\text{Ag}^{\prime}$ when $a_{i}$ is a lane change and
the agents Ag and $\text{Ag}^{\prime}$ are at a state such that
$s_{f}=\tau(s,a_{i})$ and $s_{f}^{\prime}=\tau(s^{\prime},a_{bp})$,
respectively, where $d(s_{f},s_{f}^{\prime})<gap_{req}$, where
$d(s_{f},s_{f}^{\prime})$ is the $l_{2}$ distance between $s_{f}$ and
$s_{f}^{\prime}$.

      2. ii.

When this condition holds, the agent’s max-yielding-not-enough flag
$\mathcal{F}_{\text{Ag}}(u,a_{i})$ defined in Section V.2 will be set.

      3. iii.

According to the action-selection strategy, Ag will only take $a_{i}$ when
$\mathcal{F}_{\text{Ag}}(u,a_{i})=\texttt{F}$.

      4. iv.

Thus, Ag will only take $a_{i}$ when $\lnot((Ag,a_{i})\bot Ag^{\prime})$.

∎

The following lemma states that if all $\text{Ag}\in\mathfrak{A}$ are
following the Agent Protocol, any agent Ag will not take an action for which
it collides with or violates the safety backup plan of any agent with equal
precedence.

###### Lemma .8

If Ag is following the Agent Protocol, and $S_{\text{Ag},bp}(u)=\texttt{T}$,
Ag will only choose an action $a\in Act_{\text{Ag}}$ for which the following
two conditions hold: 1)
$\mathcal{G}_{\text{Ag}}(s,a)\cap(\cup_{\text{Ag}^{\prime}\in
S}\mathcal{G}_{\text{Ag}^{\prime}}(s^{\prime},a^{\prime}))=\emptyset$ and 2)
$\forall\text{Ag}^{\prime}\in S$,
$\lnot((\text{Ag},a)\bot\text{Ag}^{\prime})$, where the set
$S\triangleq\\{\text{Ag}^{\prime}|\text{Ag}^{\prime}\sim\text{Ag}\\}$, i.e.
agents with equivalent precedence as the agent.

###### Proof:

We prove this by using arguments based on the definition of precedence, Agent
Dynamics, and the Agent Protocol.

  1. 1.

Let us first consider all $\text{Ag}^{\prime}$ where
$\text{Ag}\prec\text{Ag}^{\prime}$ and
$\text{Ag}^{\prime}\notin\mathcal{B}_{\text{Ag}}(s)$.

    1. (a)

Proof by Lemma .4.

  2. 2.

Now, let us consider all $\text{Ag}^{\prime}$ where
$\text{Ag}\prec\text{Ag}^{\prime}$ and
$\text{Ag}^{\prime}\in\mathcal{B}_{\text{Ag}}(s)$.

  3. 3.

Let us first consider the agent itself, since an agent has equivalent
precedence to itself.

    1. (a)

This is true by Lemma .5.

  4. 4.

This can be proven for any other agents of equivalent precedence that is not
the agent itself as follows.

  5. 5.

Agents with equal precedence take actions simultaneously so $O_{\text{dynamic
safety}}(s,a,u)$ does not guarantee no collision.

  6. 6.

According to the Action Selection Strategy defined in Section V-D, Ag will
choose one of three actions: the agent’s intended action $a_{i}$, the best
straight action $a_{st}$, or its backup plan action $a_{bp}$.

  7. 7.

By definition of precedence assignment, any $\text{Ag}^{\prime}$ for which
$\text{Ag}^{\prime}\sim\text{Ag}$ will be such that $La(\text{Ag})\neq
La(\text{Ag}^{\prime})$.

  8. 8.

Let us show if Ag selects $a_{bp}$, it will 1) not collide with any
$\text{Ag}^{\prime}\in S$ and 2)
$\lnot((\text{Ag},a_{bp})\bot\text{Ag}^{\prime})$.

    1. (a)

W.l.o.g., let us consider $\text{Ag}^{\prime}$ where $\text{Ag}^{\prime}\sim
Ag$.

    2. (b)

The flag $\mathcal{F}_{\text{Ag'}}(u,a_{i})=\texttt{T}$ if
$\text{Ag}^{\prime}s$ intended action $a_{i}$ causes collision with Ag or
$(Ag^{\prime},a_{i})\bot Ag$, i.e. it collides with or violates the safety of
Ag’s backup plan action.

    3. (c)

By the action-selection-strategy, $\text{Ag}^{\prime}$ will not take the
action $a_{i}$ when $\mathcal{F}_{\text{Ag'}}(u,a_{i})=\texttt{T}$, so this
guarantees Ag will not collide with $\text{Ag}^{\prime}$ when Ag takes
$a_{bp}$.

    4. (d)

By the Agent Dynamics, Ag’s backup plan action cannot cause Ag to end up in a
position where it can violate $\text{Ag}^{\prime}$’s backup plan without
colliding with it–for which $\text{Ag}^{\prime}$’s flag
$\mathcal{F}_{\text{Ag}}(u,a_{i})$ would be set.

  9. 9.

Let us show that Ag will only choose an $a_{st}$ if it will 1) not collide
with $\text{Ag}^{\prime}\in S$ and 2)
$\lnot((\text{Ag},a_{st})\bot\text{Ag}^{\prime})$.

    1. (a)

When $a_{st}=a_{bp}$, then the arguments in 8 hold.

    2. (b)

Ag selects an $a_{st}$ that is not $a_{bp}$ only when 1) its conflict cluster
is empty (i.e. $C_{\text{Ag}}=\emptyset$) or 2) when it has received a
conflict request from another agent and it has won its conflict cluster
resolution (i.e. $W_{\text{Ag}}=\texttt{T}$).

    3. (c)

If $C_{\text{Ag}}=\emptyset$, by definition of how conflict clusters are
defined in Section V.3, the agent’s action $a_{st}$ will not cause Ag to
collide with any $\text{Ag}^{\prime}\in S$, and $\forall\text{Ag}^{\prime}\in
S,\lnot((\text{Ag},a_{st})\bot\text{Ag}^{\prime})$.

    4. (d)

In the case Ag has received a conflict request and has won $W_{\text{Ag}}$, by
Lemma .2, if $W_{\text{Ag}}=\texttt{T}$, it will be the only agent in its
conflict cluster that has won.

    5. (e)

By definition of the conflict cluster, any $\text{\text{Ag}}^{\prime}\in
C_{\text{Ag}}$ where $\text{Ag}\sim\text{Ag}^{\prime}$ will take a straight
action.

    6. (f)

Since agents of equivalent precedence are initially in separate lanes by 7 and
any $\text{Ag}^{\prime}\in S$ will take a straight action, then
$La(s_{\text{Ag},t+1})\neq La(s_{\text{Ag'},t+1})$ when Ag takes $a_{st}$.

    7. (g)

Thus, by definition of agent dynamics and Definition VI.3, the action will not
cause Ag to collide with any $\text{Ag}^{\prime}\in S$, and
$\forall\text{Ag}^{\prime}\in
S,\lnot((\text{Ag},a_{st})\bot\text{Ag}^{\prime})$.

  10. 10.

Let us show that Ag will only choose an $a_{i}$ if it will 1) not collide with
any $\text{Ag}^{\prime}\in S$ and 2)
$\lnot((\text{Ag},a_{i})\bot\text{Ag}^{\prime})$.

    1. (a)

Let us consider when $\gamma_{\text{Ag}}=\texttt{straight}$ for $a_{i}$.

      1. i.

This follows from the same arguments presented in 9.

    2. (b)

Let us consider when $\gamma_{\text{Ag}}\in\\{\texttt{right-turn, left-
turn}\\}$ for $a_{i}$.

      1. i.

This follows from the fact that all other agents are following the Agent
Protocol and will not take a lane-change action in the intersection, and
because of the definition of the Agent Dynamics and Road Network.

    3. (c)

Let us consider when $\gamma_{\text{Ag}}\in\\{\texttt{right-lane change}$,
$\texttt{left-lane change}\\}$.

      1. i.

Ag will only take its intended action $a_{i}$ if the flag
$\mathcal{F}_{\text{Ag}}(u,a_{i})=\texttt{F}$, and in the case that it is part
of a conflict cluster, it is the winner of the conflict cluster resolution,
i.e. $\mathcal{W}_{\text{Ag}}=\texttt{T}$.

      2. ii.

By definition of $\mathcal{F}_{\text{Ag}}(u,a_{i})$, the agent will not take
$a_{i}$ when $a_{i}$ causes Ag to collide with any agent
$\text{Ag}^{\prime}\in S$ or when it causes $Ag$ to violate the safety of the
back up plan of another agent $Ag^{\prime}$, i.e. $\exists Ag^{\prime}$ s.t.
$(\text{Ag},a_{i})\bot\text{Ag}^{\prime}$.

      3. iii.

In the case the agent has received a conflict request and has won
$\mathcal{W}_{\text{Ag}}$, by Lemma .2, if
$\mathcal{W}_{\text{Ag}}=\texttt{T}$, it will be the only agent in its
conflict cluster that has won.

      4. iv.

By definition of the conflict cluster, any $\text{Ag}^{\prime}\in
C_{\text{Ag}}$ where $\text{Ag}\sim\text{Ag}^{\prime}$ will take its backup
plan action $a_{bp}$, and thus $s_{f}=\tau(s,a_{st})$, and
$s_{f}^{\prime}=\tau(s,a_{bp})$, where
$d(s_{f},s_{f}^{\prime})\geq gap_{\text{req}}$.

      5. v.

Thus, $a_{i}$ will only be selected when $a_{i}$ does not cause Ag to collide
with any $\text{Ag}^{\prime}\in S$ and
$\forall\text{Ag}^{\prime}\in
S,\lnot((\text{Ag},a_{i})\bot\text{Ag}^{\prime})$.

∎

The following lemma states that if all $\text{Ag}\in\mathfrak{A}$ are
following the Agent Protocol, any agent Ag will not take an action for which
it collides with or violates the safety backup plan of any agent with
incomparable precedence to it.

###### Lemma .9

If Ag is following the Agent Protocol, and $S_{\text{Ag},bp}(u)=\texttt{T}$,
Ag will only choose an action $a\in Act_{\text{Ag}}$ for which the following
two conditions hold: 1)
$\mathcal{G}_{\text{Ag}}(s,a)\cap(\cup_{\text{Ag}^{\prime}\in
S}\mathcal{G}_{\text{Ag}^{\prime}}(s^{\prime},a^{\prime}))=\emptyset$ and 2)
$\forall\text{Ag}^{\prime}\in S$,
$\lnot((\text{Ag},a)\bot\text{Ag}^{\prime})$, where the set
$S\triangleq\\{\text{Ag}^{\prime}|\text{Ag}^{\prime}\not\sim\text{Ag}\\}$,
i.e. agents with precedence incomparable to the agent.

###### Proof:

We prove this by using arguments based on the definition of precedence, Agent
Dynamics, and the Agent Protocol.

  1. 1.

Let us show when Ag chooses $a_{bp}$, it will 1) not collide with any
$\text{Ag}^{\prime}\in S$ and 2)
$\lnot((\text{Ag},a_{bp})\bot\text{Ag}^{\prime})$.

    1. (a)

Since $S_{\text{Ag},bp}(u)=\texttt{T}$, the agent will have at least one
action ($a_{bp}$) for which the top two tiers of specifications are satisfied.

    2. (b)

By 1a, the action $a_{bp}$ will only take Ag into the intersection if traffic
light is green.

    3. (c)

By Assumption 4, all traffic lights are coordinated so if agents respect
traffic light rules, they will not collide.

    4. (d)

By the assumption that all other $\text{Ag}^{\prime}\in\mathfrak{G}$ are
obeying the same protocol, each agent will only take actions that satisfy the
top two tiers of their profile.

    5. (e)

Any $\text{Ag}^{\prime}$ in a perpendicular bundle will not enter the
intersection since they have a red light.

    6. (f)

Thus, Ag cannot collide or violate the backup plan of agents in perpendicular
bundles.

    7. (g)

Any $\text{Ag}^{\prime}$ in an oncoming traffic bundle must only take an
unprotected left-turn when it satisfies
$O_{\text{unprotected left-turn}}(s,a,u)$.

    8. (h)

Thus Ag will not collide or violate the backup plan of agents in bundles of
oncoming traffic.

  2. 2.

Let us show that when Ag chooses $a_{st}$, it will 1) not collide with any
$\text{Ag}^{\prime}\in S$ and 2)
$\lnot((\text{Ag},a_{st})\bot\text{Ag}^{\prime})$.

    1. (a)

Since $a_{st}$ is chosen according to the Agent Profile, it will only be a
straight action that is not $a_{bp}$ as long as it satisfies the top-two tiers
of the profile and more.

    2. (b)

Thus, $a_{st}$ will only take Ag into intersection if traffic light is green.

    3. (c)

By the same arguments in 1, this holds.

  3. 3.

Let us show that when Ag chooses $a_{i}$, it will 1) not collide with any
$\text{Ag}^{\prime}\in S$ and 2)
$\lnot((\text{Ag},a_{i})\bot\text{Ag}^{\prime})$.

    1. (a)

Let us consider when $a_{i}$ is such that $\gamma_{Ag}=\texttt{straight}$.

      1. i.

This follows from the same arguments presented in 2.

    2. (b)

Let us consider when $a_{i}$ is such that $\gamma_{Ag}\in$
$\\{\texttt{left-lane change$,$right-lane change}\\}$.

      1. i.

Ag will never select such an action at an intersection since
$O_{\text{intersection lane-change}}(s,a,u)$ will evaluate to F.

    3. (c)

Let us consider when $a_{i}$ is such that $\gamma_{Ag}\in\\\ \\{\texttt{left-
turn, right-turn}\\}$.

      1. i.

By the assumption that all other agents are following the Agent Protocol, all
$\text{Ag}^{\prime}$ that are in bundle perpendicular to $Bu(Ag)$ will not be
in the intersection and will not collide with Ag.

      2. ii.

Further, the traffic light oracle $O_{\text{traffic light}}(s,a,u)=\texttt{T}$
only when $\lnot((\text{Ag},a_{i})\bot\text{Ag}^{\prime})$ when
$\gamma_{\text{Ag}}=\texttt{right-turn}$.

      3. iii.

Thus, when $\gamma_{\text{Ag}}=\texttt{right-turn}$ proof by 3(c)i and 3(c)ii.

      4. iv.

For an action $a_{i}$ where $\gamma_{\text{Ag}}=\texttt{left-turn},\text{Ag}$
will only take $a_{i}$ if $O_{\text{traffic-light}}(s,a,u)=\texttt{T}$ and
$O_{\text{unprotected left-turn}}(s,a,u)=\texttt{T}$.

      5. v.

Since all agents are following the law based on Proof -H, $O_{\text{traffic
light}}(s,a,u)=\texttt{T}$ means action will not cause the agent to collide
with or violate the safety of the backup plan in perpendicular bundles.

      6. vi.

By the definition of the unprotected-left-turn oracle, $Ag$ will only take the
left-turn action when it does not violate the safety of the backup plan of
agents in oncoming traffic.

∎

###  -H Safety Proof

###### Theorem .10

Given all agents $\text{Ag}\in\mathfrak{A}$ in the quasi-simultaneous game
select actions in accordance to the Agent Protocol specified in Section V, we
can show the safety property $P\Rightarrow\square Q$, where the assertion $P$
is an assertion that the state of the game is such that $\forall
Ag,S_{\text{Ag},bp}(s,u)=\texttt{T}$, i.e. each agent has a backup plan action
that is safe, as defined in VI.2. We denote $P_{t}$ as the assertion over the
state of the game at the beginning of the time-step $t$, before agents take
their respective actions. $Q$ is the assertion that the agents never occupy
the same grid point in the same time-step (e.g. collision never occurs when
agents take their respective actions during that time-step). We denote $Q_{t}$
as the assertion for the agent states/actions taken at time-step $t$.

###### Proof:

To prove an assertion of this form, we need to find an invariant assertion $I$
for which i) $P\Rightarrow I$, ii) $I\Rightarrow\square I$, and iii)
$I\Rightarrow Q$ hold. We define $I$ to be the assertion that holds on the
actions that agents select to take at a time-step. We denote $I_{t}$ to be the
assertion on the actions agents take at time $t$ such that $\forall Ag$, Ag
takes $a\in Act_{\text{Ag}}$ where 1) it does not collide with other agents
and 2) $\forall\text{Ag},S_{\text{Ag},bp}(u^{\prime})=\texttt{T}$ where
$s^{\prime}=\tau_{\text{Ag}}(s,a)$, and $u^{\prime}$ is the corresponding
global state of the game after Ag has taken its action $a$.

It suffices to assume:

  1. 1.

Each $\text{Ag}\in\mathfrak{A}$ has access to the traffic light states.

  2. 2.

There is no communication error in the conflict requests, token count queries,
and the agent intention signals.

  3. 3.

All intersections in the road network $R$ are governed by traffic lights.

  4. 4.

The traffic lights are designed to coordinate traffic such that if agents
respect the traffic light rules, they will not collide.

  5. 5.

Agents follow the agent dynamics defined in Section III-A.

  6. 6.

For $t=0$, $\forall\text{Ag}\in\mathfrak{A}$ in the quasi-simultaneous game is
initialized to:

     * •

Be located on a distinct grid point on the road network.

     * •

Have a safe backup plan action $a_{bp}$ such that
$S_{\text{Ag},bp}(s,u)=\texttt{T}$.

We can prove $P\Rightarrow\square Q$ by showing the following:

  1. 1.

$P_{t}\Rightarrow I_{t}$. This is equivalent to showing that if all agents are
in a state where $P$ is satisfied at time $t$, then all agents will take
actions at time $t$ where the $I$ holds.

    1. (a)

In the case that the assertion $P_{t}$ holds, let us show that Ag will only
choose an action $a\in Act_{Ag}$ for which the following two conditions hold:
1) $\mathcal{G}_{Ag}(s,a)\cap(\cup_{Ag^{\prime}\in
S}\mathcal{G}_{\text{Ag}^{\prime}}(s^{\prime},a^{\prime}))=\emptyset$ and 2)
$\forall Ag^{\prime}\in S$, $\lnot((\text{Ag},a)\bot\text{Ag}^{\prime})$,
where the set $S$ is:

      1. i.

The set
$S\triangleq\\{\text{Ag}^{\prime}|\text{Ag}\prec\text{Ag}^{\prime}\\}$, i.e.
agents with higher precedence than Ag. Proof by Lemma .6.

      2. ii.

$S\triangleq\\{\text{Ag}^{\prime}|\text{Ag}^{\prime}\prec\text{Ag}\\}$, i.e.
agents with lower precedence than Ag. Proof by Lemma .7.

      3. iii.

$S\triangleq\\{\text{Ag}^{\prime}|\text{Ag}^{\prime}\sim\text{Ag}\\}$, i.e.
agents with equal precedence than the agent. Proof by Lemma .8.

      4. iv.

$S\triangleq\\{\text{Ag}^{\prime}|\text{Ag}^{\prime}\not\sim\text{Ag}\\}$,
i.e. agents with precedence incomparable to the agent. Proof by Lemma .9.

    2. (b)

The set of all agents, agents with lower precedence, higher precedence, equal
precedence, and incomparable precedence, is complete and includes all agents.

    3. (c)

By 1-1(a)iv and 1b, an agent will not take an action that will cause collision
with any other agents (including itself) or violate the safety of the safety
backup plan of all other agents, and thus any action taken by any agent will
be such that following the action, the assertion $P$ still holds.

  2. 2.

$P_{t}\Rightarrow I_{t}$. This is equivalent to showing that if all agents are
in a state where $P$ is satisfied at time $t$, then all agents will take
actions at time $t$ where the $I$ holds. This can be proven using arguments
based on the design of the Agent Protocol. More details can be found in Lemmas
A..4-A..9 in the Appendix.

  3. 3.

$I\Rightarrow\square I$. If agents take actions at time $t$ such that the
assertion $I_{t}$ holds, then by the definition of the assertion $I$, agents
will end up in a state where at time t+1, assertion $P$ holds, meaning
$I_{t}\Rightarrow P_{t+1}$. Since $P_{t+1}\Rightarrow I_{t+1}$, from 2, we get
$I\Rightarrow\square I$.

  4. 4.

$I\Rightarrow Q$. This is equivalent to showing that if all agents take
actions according to the assertions in $I$, then collisions will not occur.
This follows from the invariant assertion that agents are taking actions that
do not cause collision, and the fact that all Ag have a safe backup plan
action $a_{bp}$ to choose from, and thus will always be able to (and will)
take an action from which it can avoid collision in future time steps.

∎

###  -I Liveness Lemmas

###### Lemma .11

If the only $a\in Act_{Ag}$ for an agent Ag for which $O_{\text{destination
reachability}}(s,a,u)=\texttt{T}$ and $O_{\text{forward
progress}}(s,a,u)=\texttt{T}$ is an action such that:
$\gamma_{\text{Ag}}\in\\{\texttt{right-turn, left-turn}\\}$ and the grid-point
$s_{f}=\tau_{\text{Ag}}(s,a)$ is unoccupied (for a left-turn, where $a$ is the
final action of the left-turn maneuver), Ag will always eventually take $a$.

###### Proof:

W.l.o.g., let us consider agent $\text{Ag}\in\mathfrak{A}$ in the quasi-
simultaneous game $\mathfrak{G}$. We prove this by showing that all criteria
required by the Agent Protocol are always eventually satisfied, thereby
allowing Ag to take action $a$.

  1. 1.

By the definition of $\mathfrak{R}$ and the agent dynamics, when Ag is in a
position where only $\gamma_{\text{Ag}}\in\\{\texttt{right-turn},\texttt{left-
turn}\\}$, it will neither send nor receive requests from other agents and
$\mathcal{F}_{\text{Ag}}(u,a_{i})$ will never be set to T.

  2. 2.

In accordance with the Action Selection Strategy, for Ag to take action $a$,
all the oracles in the Agent Profile must be simultaneously satisfied (so it
will be selected over any other $a^{\prime}\in Act_{\text{Ag}}$). Thus, we
show:

    1. (a)

The following oracle evaluations will always hold when Ag is in this state:
$O_{\text{traffic intersection lane-
change}}(s,a,u)=\texttt{T}$,$O_{\text{legal orientation}}(s,a,u)=\texttt{T}$,
$O_{\text{static safety}}(s,a,u)=\texttt{T}$ and
$O_{\text{traffic intersection clearance}}(s,a,u)=\texttt{T}$.

      1. i.

The first oracle is true vacuously and the following are true by the road
network constraints and agent dynamics, Assumption 8, and the assumption in
the lemma statement that $s_{f}=\tau(s,a)$ is unoccupied respectively.

    2. (b)

To show that the following oracles will always eventually simultaneously hold
true, let us first consider when $\gamma=\\{\texttt{right-turn}\\}$.

      1. i.

By the assumption, the traffic light is red for a finite time, and when the
traffic light is green, $O_{\text{traffic light}}(s,a,u)=\texttt{T}$.

      2. ii.

$O_{\text{unprotected left-turn}}(s,a,u)$ is vacuously true for a right-turn
action.

      3. iii.

Since $O_{\text{traffic intersection clearance}}(s,a,u)=\texttt{T}$ and by the
safety proof -H, all Ag are only taking actions in accordance with traffic
laws so there will never be any $\text{Ag}^{\prime}\in\mathfrak{A}$ blocking
the intersection, making $O_{\text{dynamic safety}}(s,a,u)=\texttt{T}$.

      4. iv.

Thus, all oracles are always eventually simultaneously satisfied and Ag can
take $a$ where $\gamma=\\{\texttt{right-turn}\\}$

    3. (c)

Let us consider when $\gamma_{\text{Ag}}=\\{\texttt{left-turn}\\}$.

      1. i.

By Assumption 7, traffic lights are green for a finite time.

      2. ii.

By the safety proof -H, all Ag are only taking actions in accordance with
traffic laws so there will never be any $\text{Ag}^{\prime}\in\mathfrak{A}$
blocking the intersection.

      3. iii.

When $\gamma_{\text{Ag}}=\texttt{left-turn}$, by definition of the unprotected
left-turn oracle, $\square\lozenge O_{\text{unprotected left-turn}}(s,a,u)$,
specifically when the traffic light switches from green to red and Ag has been
waiting at the traffic light.

      4. iv.

Thus, $\square\lozenge O_{\text{unprotected left-turn}}(s,a,u)$ after the
light turns from green to red.

      5. v.

Further, $O_{\text{unprotected left-turn}}(s,a,u)=\texttt{T}$ combined with
$O_{\text{traffic intersection clearance}}(s,a,u)=\texttt{T}$ implies
$O_{\text{dynamic safety}}(s,a,u)=\texttt{T}$.

      6. vi.

Thus, all oracles are always eventually simultaneously satisfied and Ag can
take $a$ where $\gamma=\\{\texttt{left-turn}\\}$.

  3. 3.

Thus, we have shown all oracles in the Agent Profile will always eventually be
satisfied, and Ag will take $a$ such that $O_{\text{destination
reachability}}(s,a,u)=\texttt{T}$ and
$O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

∎

###### Lemma .12

If the only $a\in Act_{\text{Ag}}$ for which
$O_{\text{destination reachability}}(s,a,u)=\texttt{T}$ and $O_{\text{forward
progress}}(s,a,u)=\texttt{T}$ is when $a$ has
$\gamma_{\text{Ag}}\in\\{\texttt{right-lane change, left-lane change}\\}$ and
the grid-point(s) $\mathcal{G}(s,a)$ is (are) either unoccupied or agents that
occupy these grid points will always eventually clear these grid points, Ag
will always eventually take this action $a$.

###### Proof:

W.l.o.g., let us consider agent $\text{Ag}\in\mathfrak{A}$ in the quasi-
simultaneous game $\mathfrak{G}$. We prove this by showing that all criteria
required by the Agent Protocol are always eventually satisfied, thereby
allowing Ag to take its action $a$.

  1. 1.

Let us consider Case A, when $a$ is such that
$s_{f}=\tau_{\text{Ag}}(s,a)=\texttt{Goal}_{\text{Ag}}$, i.e. the action takes
the agent to its goal, and let us show that Ag will always eventually be able
to take $a$.

  2. 2.

In accordance with the Action Selection Strategy, for Ag to take $a$ is that
1) all the oracles in the agent profile must be simultaneously satisfied (so
the action $a$ is chosen over any other $a^{\prime}\in Act_{\text{Ag}}$, 2)
$\mathcal{F}_{\text{Ag}}(u,a_{i})=0$, and 3) $W_{\text{Ag}}=\texttt{T}$.

  3. 3.

We first show all the oracles for Ag will always be simultaneously satisfied:

    1. (a)

When Ag is in this state, the following oracle evaluations always hold:
$O_{\text{traffic light}}(s,a,u)=\texttt{T}$,
$O_{\text{traffic intersection lane-change}}(s,a,u)=\texttt{T}$,
$O_{\text{unprotected left turn}}(s,a,u)=\texttt{T}$,
$\square\lozenge O_{\text{traffic intersection clearance}}(s,a,u)$,
$O_{\text{static safety}}(s,a,u)=\texttt{T}$, $O_{\text{traffic
orientation}}(s,a,u)=\texttt{T}$.

      1. i.

The first four hold vacuously, the others hold by Assumption 8, and the last
holds by Agent dynamics and the Road Network.

    2. (b)

$O_{\text{dynamic safety}}(s,a,u)=\texttt{T}$.

      1. i.

By the definition Road Network $\mathfrak{R}$, agent dynamics in Section
III-A, and the condition that $\forall\text{Ag}\in\mathfrak{A}$ will leave
$\mathfrak{R}$ (i.e. Ag does not occupy any grid point on $\mathfrak{R}$ when
it reaches its respective goal $\texttt{Goal}_{\text{Ag}}$). Thus,
$O_{\text{dynamic safety}}(s,a,u)=\texttt{T}$ whenever an agent is in this
state.

  4. 4.

In accordance with the action selection strategy, for Ag to take $a$, it must
be that $\mathcal{F}_{\text{Ag}}(u,a_{i})=0$, i.e. the max-yielding-flag-not-
enough must not be set. Let us show that this is always true.

    1. (a)

The only $\text{Ag}^{\prime}$ that can cause the
$\mathcal{F}_{\text{Ag}}(u,a_{i})=1$ of Ag is when an agent
$\text{Ag}^{\prime}$ is in a state where
$La(Ag^{\prime})=\texttt{Goal}_{\text{Ag}}$.

    2. (b)

W.l.o.g. let us consider such an $\text{Ag}^{\prime}$. By liveness Assumption
9, upon approaching the goal, the agent $\text{Ag}^{\prime}$ must be in a
state where $\text{Ag}^{\prime}$ backup plan action $a_{bp}$ will allow it to
a complete stop before reaching its goal.

    3. (c)

By 4b, $\text{Ag}^{\prime}$ will always be in a state for which the max-
yielding-not-enough flag for Ag is $\mathcal{F}_{\text{Ag}}(u,a_{i})=0$.

  5. 5.

In order for Ag to take $a$, it must be that $W_{Ag}=1$. Let us show that this
is always eventually true.

    1. (a)

In the case that Ag has the maximum number of tokens, $\mathcal{W}_{Ag}=1$ and
Ag will be able to take its forward action since all criteria are satisfied.

    2. (b)

Any $\text{Ag}^{\prime}\in\mathcal{C}_{Ag}$ will be of equal or lower
precedence than Ag.

    3. (c)

Any $\text{Ag}^{\prime}$ with the maximum number of tokens will move to its
goal since $\mathcal{W}_{\text{Ag}}=1$ and all the other criteria required for
that agent to take its action will be true.

    4. (d)

By definition of the Action Selection Strategy in Section V-D, any agent
$\hat{\text{Ag}}$ that replaces $\text{Ag}^{\prime}$ will have taken a forward
progress action and its respective token count will reset to 0.

    5. (e)

Thus, any $\text{Ag}^{\prime}$ will be allowed to take its action before Ag,
but Ag’s token count $\texttt{Tc}_{\text{Ag}}$ will increase by one for every
time-step this occurs.

    6. (f)

Thus, by 5d and by 5e, Ag will always eventually have the highest token count
in its conflict cluster such that $W_{\text{Ag}}=1$.

    7. (g)

Since conditions 3 and 4 are always true, and 5 is always eventually true,
then all conditions will simultaneously always eventually be true and the Ag
will always eventually take the action $a$.

  6. 6.

Let us consider Case B, when $a$ is the final action to take for an agent to
reach its sub-goal (i.e. a critical left-turn or right-turn tile), and let us
show Ag will always eventually be able to take a forward progress action where
$\gamma_{\text{Ag}}\in\\{\texttt{left-lane change},\texttt{right-lane
change}\\}$.

  7. 7.

In accordance with the Action Selection Strategy, for Ag to take $a$ is that
1) $W_{\text{Ag}}=1$, 2) $\mathcal{F}_{\text{Ag}}(u,a_{i})=0$, i.e. the max-
yielding-flag-not-enough must not be set and 3) all the oracles in the Agent
Profile must be simultaneously satisfied.

  8. 8.

Let us first consider when $W_{\text{Ag}}=1$, then $\square W_{\text{Ag}}$
until Ag takes its forward progress action $a$ because by definition of
$W_{\text{Ag}}$, Ag has the highest token count in its conflict cluster,
$\text{Ag}.\texttt{tc}=\text{Ag}.\texttt{tc}+1$, while Ag does not select $a$
(and thus does not make forward progress) and any Ag that newly enters Ag’s
conflict cluster will have a token count of 0.

  9. 9.

All the oracles are either vacuously or trivially satisfied by the assumptions
except for $O_{\text{dynamic safety}}(s,a,u)$.

  10. 10.

By the Assumption 7, the traffic light will always cycle through red-to-green
and green-to-red at the intersection Ag is located at.

  11. 11.

By the Assumption on the minimum duration of the red traffic light, all
$\text{Ag}^{\prime}$ will be in a state such that
$\mathcal{F}_{\text{Ag}}(u,a_{i})=0$.

  12. 12.

By the lemma assumption that all $Ag^{\prime}$ occupying grid points will
always eventually take their respective forward progress actions,
$\square\lozenge O_{\text{dynamic safety}}(s,a,u)$.

  13. 13.

Thus, all criteria for which Ag can take its forward progress action $a$ will
be simultaneously satisfied.

  14. 14.

When $W_{\text{Ag}}$ = 0, we must show $\square\lozenge W_{\text{Ag}}$.

    1. (a)

For Ag, all agents in its conflict cluster have equal or lower precedence and
are not in the same lane as Ag.

    2. (b)

For any such $\text{Ag}^{\prime}$ with equal precedence, $\text{Ag}^{\prime}$
will always eventually take its forward progress action by the arguments in
8-14 if $\text{Ag}^{\prime}$ intends to make a lane-change.

    3. (c)

By the lemma assumption, any agents $Ag^{\prime}$ occupying the grid points
that $Ag$ needs to take its action will always eventually take its forward
progress action so $\square\lozenge O_{\text{dynamic safety}}(s,a,u)$.

    4. (d)

Any $\hat{\text{Ag}}$ with lower precedence and higher token count that Ag
will take $\text{Ag}^{\prime}$’s position and in doing so will have a token
count of 0 and any Ag that replaces any agents with higher token count than Ag
and is in Ag’s conflict cluster will have token count 0.

    5. (e)

Thus $\square\lozenge W_{\text{Ag}}$.

∎

###### Lemma .13

Let us consider a road segment $rs\in RS$ where there exist grid points
$g\in\mathcal{S}_{\text{sinks}}$. Every $\text{Ag}\in rs$ will always
eventually be able to take $a\in Act_{\text{Ag}}$ for which $O_{\text{forward
progress}}(s,a,u)=\texttt{T}$.

###### Proof:

We prove this by induction. W.l.o.g, let us consider
$\text{Ag}\in\mathfrak{A}$. Let
$m_{\text{Ag}}=\text{proj}_{\text{long}}(\texttt{Goal}_{\text{Ag}})-\text{proj}_{\text{long}}(Ag.s)$.

  1. 1.

Base Case: $m_{\text{Ag}}=1$, i.e. Ag only requires a single action $a$ to
reach its goal $\texttt{Goal}_{\text{Ag}}$.

    1. (a)

If $a$ is such that
$\gamma_{Ag}\in\\{\texttt{left-lane change, right-lane change}\\}$, then Ag
will take always eventually this action by Lemma .12.

    2. (b)

If $a$ is such that $\gamma_{\text{Ag}}=\texttt{straight}$:

    3. (c)

In accordance with the Action Selection Strategy, for Ag to take $a$ is that
1) all the oracles in the agent profile must be simultaneously satisfied (so
the action $a$ is chosen over any other $a^{\prime}\in Act_{\text{Ag}}$, and
2) $W_{\text{Ag}}$ = 1.

    4. (d)

First, we show that all oracles in the agent profile will always be
simultaneously satisfied.

      1. i.

These all follow from the same arguments presented when
$\gamma_{Ag}=\\{\text{right-lane change},\text{left-lane change}\\}$ in Case A
in Lemma .12.

    5. (e)

In accordance with the Action Selection Strategy, we must show that
$\square\lozenge W_{\text{Ag}}$. This is vacuously true since no Ag will be in
the agent’s conflict cluster when an agent is in this state.

  2. 2.

Case $m=N$: Let us assume that any $\forall\text{Ag}$ where $m_{\text{Ag}}=N$
always eventually take $a\in Act_{\text{Ag}}$ for which
$O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

  3. 3.

Case $m=N+1$: Let us show $\forall\text{Ag}$ where $m_{\text{Ag}}=N+1$ always
eventually take $a$ for which
$O_{\text{forward progress}}=\texttt{T}$.

    1. (a)

Any Ag for which $m_{\text{Ag}}>1$ will always have an $a$ where
$\gamma_{\text{Ag}}=\texttt{straight}$ such that $O_{\text{forward
progress}}(s,a,u)=\texttt{T}$.

    2. (b)

Thus, we show that Ag always eventually will take
$\gamma_{\text{Ag}}=\texttt{straight}$ such that $O_{\text{forward
progress}}(s,a,u)=\texttt{T}$.

    3. (c)

W.l.o.g., let us consider Ag for which $m_{\text{Ag}}=N+1$.

    4. (d)

In accordance with the Action Selection Strategy, for Ag to take $a$ is 1)
$W_{\text{Ag}}$ = 1 and 2) all the oracles in the agent profile must be
simultaneously satisfied (so the action $a$ is chosen over any other
$a^{\prime}\in Act_{\text{Ag}}$).

    5. (e)

In accordance with the Action Selection Strategy, we must show
$\square\lozenge W_{\text{Ag}}$.

      1. i.

Any $\text{Ag}^{\prime}\in\mathcal{C}_{\text{Ag}}$ will be an agent of equal
or higher precedence and in separate lane.

      2. ii.

Any such agent with higher token count than Ag that is in its conflict cluster
will always eventually be able to go by the inductive assumption in 2.

      3. iii.

After all such agents take a forward progress action, they will no longer be
in Ag’s conflict cluster and Ag will have the highest token count since all
$Ag$ that newly enter the conflict cluster will have token count of $0$.

    6. (f)

After the assignment $W_{\text{Ag}}=1$, $\square W_{\text{Ag}}$ until Ag
selects $a$. This is true because by definition of $W_{\text{Ag}}$, Ag has the
highest token count in its conflict cluster,
$\text{Ag}.\texttt{tc}=Ag.\texttt{tc}+1$, while Ag does not select $a$, and
any Ag that enters Ag’s conflict cluster will have a token count of 0.

    7. (g)

Let us show that the oracles in the Agent Profile will always evaluate to T.

      1. i.

The same arguments hold here as in Lemma .12.1 for all oracles except for
$O_{\text{dynamic safety}}(s,a,u)$, where $\square\lozenge O_{\text{dynamic
safety}}(s,a,u)=\texttt{T}$ by the inductive Assumption 2.

∎

###### Lemma .14

Let Ag be on a road segment $rs\in RS$, where $RS$ is the set of nodes in the
dependency road network dependency graph $\mathcal{G}_{\text{dep}}$. Let $rs$
be a road segment for which $\forall rs^{\prime}\in RSs.t.\exists
e:(rs^{\prime},rs)$. Each road segment $rs^{\prime}$ has vacancies in the grid
points where $\text{Ag}\in rs$ would occupy if it crossed the intersection
(i.e. $s_{f}=\tau_{\text{Ag}}(s,a)$), and we show that Ag will always
eventually take an action $a\in Act_{\text{Ag}}$ where $O_{\text{progress
oracle}}(s,a,u)=\texttt{T}$.

###### Proof:

We prove this with induction. W.l.o.g., let us consider
$\text{Ag}\in\mathfrak{A}$. Let
$m_{\text{Ag}}=\text{proj}_{\text{long}}(g_{\text{front of
rs}})-\text{proj}_{\text{long}}(\text{Ag}.s)$, where $g_{\text{front of
intersection}}$ represents a grid point at the front of the road segment.

  1. 1.

Base Case $m_{\text{Ag}}=0$: Let us consider an Ag whose next action will take
will bring Ag to cross into the intersection and show that Ag will always
eventually take $a$ for which $O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

    1. (a)

If the only $a$ where $O_{\text{forward progress}}=\texttt{T}$ is such that
$\gamma_{\text{Ag}}\in\\{\texttt{left-turn},\texttt{ right-turn}$}, proof by
Lemma .11.

    2. (b)

If the only $a$ where $O_{\text{forward progress}}(s,a,u)=\texttt{T}$ is such
that $\gamma_{\text{Ag}}=\texttt{straight}$.

      1. i.

In accordance with the Action Selection Strategy, for Ag to take $a$ is that
1) all the oracles in the Agent Profile must be simultaneously satisfied (so
the action $a$ is chosen over any other $a^{\prime}\in Act_{\text{Ag}}$, 2)
$W_{\text{Ag}}$ = 1.

        1. A.

$O_{\text{unprotected left-turn}}(s,a,u)=\texttt{T}$,
$O_{\text{traffic intersection lane-change}}(s,a,u)=\texttt{T}$,
$O_{\text{static safety}}(s,a,u)=\texttt{T}$,
$O_{\text{traffic intersection clearance}}(s,a,u)=\texttt{T}$
$O_{\text{legal orientation}}(s,a,u)=\texttt{T}$.

        2. B.

The first two oracles are true vacuously, followed by Assumption 8, and by
agent dynamics and the road network $\mathfrak{R}$ definition, respectively,
and by the assumption in the lemma statement.

        3. C.

$\square\lozenge O_{\text{traffic light}}(s,a,u)$ by Assumption 7.

        4. D.

$O_{\text{dynamic obstacle}}(s,a,u)=\texttt{T}$ because by the safety proof,
all Ag take $a\in Act_{\text{Ag}}$ that satisfy the first top tiers of the
agent profile so there will be no $\text{Ag}^{\prime}\in\mathfrak{A}$ that are
in the intersection when the traffic light for Ag is green. Thus, whenever
$O_{\text{traffic light}}(s,a,u)=\texttt{T}$, then it $O_{\text{dynamic
obstacle}}(s,a,u)=\texttt{T}$ as well.

      2. ii.

$W_{Ag}=1$ vacuously since neither Ag or any
$\text{Ag}^{\prime}\in\mathfrak{A}$ will send a conflict request at the front
of the intersection since all $a_{i}$ must satisfy $O_{\text{traffic
intersection lane-change}}(s,a,u)$ according to the Safety Proof in Section
A-H.

    3. (c)

By the safety proof in -H, Ag will only take $a\in Act_{\text{Ag}}$ that
satisfy the top two tiers of the Agent Profile, so Ag will not take an $a$
where
$\gamma_{\text{Ag}}\in\\{\texttt{left-lane change},\texttt{right-lane
change}$} into an intersection.

  2. 2.

Case $m_{Ag}=N$: Let us assume that Ag with $m_{\text{Ag}}=N$ will always
eventually take $a\in Act_{\text{Ag}}$ for which
$O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

  3. 3.

Case $m_{Ag}=N+1$: Let us show that any Ag that is at a longitudinal distance
of $N+1$ from the destination will always eventually take $a$ for which
$O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

    1. (a)

Let us consider when Ag’s only $a$ such that
$O_{\text{forward progress}}(s,a,u)=\texttt{T}$ is
$\gamma_{\text{Ag}}\in\\{\texttt{right-lane change},\texttt{left-lane change}$
}.

    2. (b)

Although $Ag$ may not have priority (since it does not have max tokens in its
conflict cluster), any $Ag$ that occupies grid points $\mathcal{G}(s,a,u)$
will always eventually make forward progress by Argument 1.

    3. (c)

Further,

    4. (d)

Once these agents have made forward progress, any $\hat{Ag}$ that replace
$\text{Ag}^{\prime}$ will have a $\texttt{Tc}_{Ag}=0$ and since $Ag$ is always
increasing its token counts as it cannot make forward progress, it will always
eventually have the max tokens and thus have priority over those grid points.

    5. (e)

Thus, this can be proven by using Case B in Lemma .12.

    6. (f)

For all other $a\in Act_{\text{Ag}}$ are actions for which
$\gamma_{\text{Ag}}=\texttt{straight}$, and the same arguments as in the proof
of straight actions for $rs$ with $g\in\mathcal{S}_{\text{sinks}}$ in 3 hold.

∎

###  -J Liveness Proof

######  Theorem .15 (Liveness Under Sparse Traffic Conditions)

Under the Sparse Traffic Assumption given by VI.4 and given all agents
$\text{Ag}\in\mathfrak{A}$ in the quasi-simultaneous game select actions in
accordance with the agent protocol specified in Section V, liveness is
guaranteed, i.e. all $\text{Ag}\in\mathfrak{A}$ will always eventually reach
their respective goals.

###### Proof:

It suffices to assume:

  1. 1.

$\forall\text{Ag}\in\mathfrak{A}$,
$\forall\text{Ag}^{\prime}\in\mathbb{B}_{\text{Ag}}$, Ag knows
$\text{Ag}^{\prime}.s,Ag^{\prime}.i$, i.e. the other agent’s state
$\text{Ag}.s$ and intended action $a_{i}$ and all Ag within a region around
the intersection defined in the Appendix.

  2. 2.

Each $\text{Ag}\in\mathfrak{A}$ has access to the traffic light states.

  3. 3.

There is no communication error in the conflict requests, token count queries,
and the agent intention signals.

  4. 4.

For $t=0$, $\forall\text{Ag}\in\mathfrak{A}$ in the quasi-simultaneous game is
initialized to:

     * •

Be located on a distinct grid point on the road network.

     * •

Have a safe backup plan action $a_{bp}$ such that
$S_{\text{Ag},bp}(u)=\texttt{T}$.

  5. 5.

The traffic lights are red for some time window $\Delta t_{\text{tl}}$ such
that $t_{\text{min}}<\Delta t_{\text{tl}}<\infty$, where $t_{\text{min}}$ is
defined in the Appendix in Section -K1.

  6. 6.

The static obstacles are not on any grid point $g$ where
$g.d=1$.

  7. 7.

Each Ag treats its respective goal $\text{Ag}.\texttt{g}$ as a static
obstacle.

  8. 8.

Bundles in the road network $\mathfrak{R}$ have no more than 2 lanes.

  9. 9.

The road network $R$ is such that all intersections are governed by traffic
lights.

and prove:

  1. 1.

Let us consider a road segment $r\in RS$ that contains grid point(s)
$g\in\mathcal{S}_{\text{sinks}}$. Every $\text{Ag}\in r$ will be able to
always eventually take $a\in Act_{Ag}$ for which $O_{\text{forward
progress}}(s,a,u)=\texttt{T}$.

  2. 2.

Let us consider a road segment $rs\in RS$. Let us assume $\forall rs\in
RS,\exists(rs,rs^{\prime})\in G_{\text{dep}}$, i.e. the clearance of $rs$
depends on the clearance of all $rs^{\prime}$. We use inductive reasoning to
show that any Ag on $rs$ will always eventually take an $a\in Act_{\text{Ag}}$
where $O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

  3. 3.

For any $\mathfrak{R}$ where the dependency graph $G_{\text{dep}}$ (as defined
in IV.2) is a directed-acylcic-graph (DAG), we prove all
$\text{Ag}\in\mathfrak{A}$ will always eventually take $a\in Act_{Ag}$ for
which
$O_{\text{forward progress}}(s,a,u)=\texttt{T}$ inductively as follows.

    1. (a)

A topological sorting of a directed acyclic graph G = (V, E) is a linear
ordering of vertices V such that $(u,v)\in E\rightarrow u$ appears before $v$
in ordering.

    2. (b)

If and only if a graph $G$ is a DAG, then $G$ has a topological sorting. Since
$G_{\text{dep}}$ is a $DAG$, it has a topological sorting.

    3. (c)

We can then use an argument by induction on the linear ordering provided by
the topological sorting to show that all Ag always eventually take $a\in
Act_{Ag}$ for which
$O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

      1. i.

Let $l$ denote the linear order associated with the road network dependency
graph $G_{\text{dep}}$, where an ordering of $l=0$ denotes a road segment with
source nodes.

      2. ii.

Base Case $l=0$. This can be proven true by Lemma .13.

      3. iii.

Let us assume this is true for any road segment where $l=N$.

      4. iv.

Under the Inductive Assumption 3(c)iii, there will be clearance in any road
segment that agent Ag depends on for Ag to make forward progress to its
destination.

      5. v.

Since all Ag are following the traffic laws by the Safety proof in -H, the
clearance spots will be given precedence to $\text{Ag}\in rs$ for a positive,
finite time, and thus the assumptions required in Lemma .11 and .12 used to
prove Lemma .14 will hold.

      6. vi.

Thus, the Lemma .14 to show that all Ag for which $l=N+1$ always eventually
take an action for which
$O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

  4. 4.

When the graph $G_{\text{dep}}$ is cyclic, the Sparsity Assumption VI.4 can be
used to prove all agents always eventually take an action for which
$O_{\text{forward progress}}(s,a,u)=\texttt{T}$.

    1. (a)

The sparsity assumption VI.4 ensures that there is at least one vacancy in any
map loop.

    2. (b)

Let us consider $Ag$ inside a map loop.

      1. i.

Let us consider $Ag$ in the loop for which the vacancy is directly ahead of
$Ag$. If the vacancy is directly ahead of $Ag$, then if the only forward
progress action $a$ keeps $Ag$ in the loop, $Ag$ will always eventually take
its action by Lemmas .11, .12 and the arguments in Lemma .14 1b. If the only
forward progress action $a$ makes $Ag$ leave the loop, $Ag$ will always
eventually take its action by the sparsity assumption VI.4 and the inductive
arguments in 2c.

      2. ii.

By 4(b)i, it can then be inductively shown that any $Ag$ in the loop will
always eventually have a vacancy for which it can take a forward progress
action.

    3. (c)

Let us consider $Ag$ on a road segment that is not part of a map loop.

      1. i.

Let us consider an action $a$ that takes $Ag$ into a map loop. If the grid
point required by $Ag$ to make forward progress is occupied, by 4(b)ii, it
will always eventually be unoccupied. If the only action $Ag$ can take is such
that $\gamma_{Ag}=\\{\texttt{lane-change}\\}$ since all $Ag^{\prime}$ in the
loop are reset when they take forward progress action, $Ag$ will always
eventually have the max token count. Thus, the same arguments in Lemma .12
hold. If the only action $Ag$ can take is such that $Ag$ crosses into an
intersection, the traffic light rules ensure that $Ag$ has precedence over any
$Ag$ in the loop. Thus, $Ag$ will always eventually take a forward progress
action by Lemma .11 and Lemma .14 1b.

      2. ii.

For any action $a$ that does not take $Ag$ into a map loop, $Ag$ can take a
forward action because of the sparsity assumptions VI.4 and the inductive
arguments in 2c.

  5. 5.

By the induction arguments and by definition of the forward progress oracle
$O_{\text{forward progress}}(s,a,u)$, all Ag will always eventually take
actions that allow them to make progress to their respective destinations, and
liveness is guaranteed.

∎

###  -K Traffic Light Assumptions

A traffic light grid point contains three states
$g.s=\\{\texttt{red},\texttt{yellow},\texttt{green}\\}$. The traffic lights at
each intersection are coordinated so that if all agents obey the traffic
signals, collision will not occur (i.e. the lights for the same intersection
will never be simultaneously green) and the lights are both red for long
enough such that Ag that entered the intersection when the light was yellow
will be able to make it across the intersection before the other traffic light
turns green.

####  -K1 Traffic Light Minimum Time

In order to guarantee that agents will always eventually be able to make a
lane-change to a critical tile, the traffic light has to be red for
sufficiently long such that any $Ag^{\prime}$ that may cause
$\mathcal{F}_{\text{Ag}}(u,a_{i})=\texttt{T}$ is slowed down for long enough
such that $Ag$ can take its lane-change action. This can be computed simply
once given the dynamics of Ag. Normally a simple heuristic can be used instead
of computing this specific lower-bound.

###  -L Simulation Maps

Figure 9: Straight road map environment. Figure 10: City blocks map
environment.

###  -M Simulation Environment Features

A road network environment, complete with legal lane orientations,
intersections, and traffic lights, can be specified via a CSV file. The
specified (by the user) road network environment forms a map data structure
graph, which decomposes the roads into bundles, mentioned in V-A.

The map will automatically parse the boundaries and lane directions of the
road network to define where agents can either spawn from or exit the road
network. In each game scenario, agents will randomly spawn according to a
specified spawn rate.

Each agent has the following attributes in our simulation: parameters like min
and max velocity and accelerations, dynamics specified by agent actions and
their corresponding occupancy grids, goal location, agent color, ID, token
count. Note, these attributes can be modified depending on what the user wants
to include. For each agent, a graph-planning algorithm is used to compute a
high-level motion plan on the map graph to get the agent to its goal.

Each game scenario is comprised of the road network graph and a set of agents
(constantly changing over time as new agents spawn and old agents reach their
goals and leave). The game is simulated forward for a specified number of time
steps and the traces from the simulation are saved. The animation module in
RoSE animates the traces from the simulated game.

RoSE also offers a collection of debugging tools to help reconstruct scenarios
that occurred during a simulated game. If the user would like to regenerate
the same initialization, the simulation has a feature where users can specify
a specific randomization seed. There is a configuration tool that allows users
to prescribe the states of a set of agents and their respective goals. A final
debugging tool outputs the variables of the agent that were relevant to the
decision-making process.