11institutetext: University of Haifa, Haifa, Israel,
11email<EMAIL_ADDRESS>
11email<EMAIL_ADDRESS>
22institutetext: Institute of Science and Technology Austria (ISTA),
Klosterneuburg, Austria,
22email<EMAIL_ADDRESS>
# Auction-Based Scheduling

Guy Avni 11 Kaushik Mallik 22 Suman Sadhukhan 11

###### Abstract

Many sequential decision-making tasks require satisfaction of multiple,
partially contradictory objectives. Existing approaches are monolithic, namely
all objectives are fulfilled using a single policy, which is a function that
selects a sequence of actions. We present _auction-based scheduling_ , a
modular framework for multi-objective decision-making problems. Each objective
is fulfilled using a separate policy, and the policies can be independently
created, modified, and replaced. Understandably, different policies with
conflicting goals may choose conflicting actions at a given time. In order to
resolve conflicts, and compose policies, we employ a novel auction-based
mechanism. We allocate a bounded budget to each policy, and at each step, the
policies simultaneously bid from their available budgets for the privilege of
being scheduled and choosing an action. Policies express their scheduling
urgency using their bids and the bounded budgets ensure long-run scheduling
fairness. We lay the foundations of auction-based scheduling using path
planning problems on finite graphs with two temporal objectives. We present
decentralized algorithms to synthesize a pair of policies, their initially
allocated budgets, and bidding strategies. We consider three categories of
decentralized synthesis problems, parameterized by the assumptions that the
policies make on each other: (a) strong synthesis, with no assumptions and
strongest guarantees, (b) assume-admissible synthesis, with weakest
rationality assumptions, and (c)  _assume-guarantee synthesis_ , with explicit
contract-based assumptions. For reachability objectives, we show that,
surprisingly, decentralized assume-admissible synthesis is always possible
when the out-degrees of all vertices are at most two.

##  1 Introduction

Sequential decision-making tasks often require satisfaction of multiple,
partially contradictory objectives. For example, the policy of a traffic light
needs to choose the signals in a way that the traffic throughput is maximized
while minimizing the waiting time [35], the policy that navigates an unmanned
aerial vehicle needs to ensure that the destination is eventually reached
while avoiding no-fly zones [34], the policy of the resource manager in a
multi-threaded system needs to allocate resources in a way that deadlock is
avoided while maintaining fairness [3].

We propose a decentralized synthesis framework for policies when tasks are
given as a conjunction of two objectives $\Phi_{1}$ and $\Phi_{2}$. The idea
is that $\Phi_{1}$ and $\Phi_{2}$ will be accomplished using two policies
$\alpha_{1}$ and $\alpha_{2}$, respectively, that are designed independently.
We compose $\alpha_{1}$ and $\alpha_{2}$ at runtime to obtain a policy for
$\Phi_{1}\wedge\Phi_{2}$. Such a composition is not trivial since $\alpha_{1}$
and $\alpha_{2}$ may propose conflicting candidate actions at a given point in
time, whereas only one action needs to be chosen. We propose a novel
composition mechanism called _auction-based scheduling_ : both policies have
bounded monetary budgets, and at each point in time, an auction (aka bidding)
is held, where the policies bid for the privilege to get scheduled for
choosing the next action. On one hand, the auction encourages the policies
with higher scheduling urgency to bid higher, and on the other hand, the
bounds on the budgets ensure fairness, namely that no policy is starved. Our
goal is to design decentralized synthesis algorithms that output policies with
a bidding component that are both sound—i.e., the composition of the output
policies satisfies both objectives—and complete—i.e., under the given
restrictions, when policies exist, they are found.

The key advantage of auction-based scheduling is modularity. First, since the
designs of the policies do not depend on each other, they can be created
independently and in parallel, e.g., by different vendors. Second, since the
policies operate independently, they can be modified and replaced separately,
e.g., when the objective changes. This avoids the expensive redesign of the
whole system.

Let us now go into more detail. The concrete problem that we consider is path
planning on a given finite graph $\mathcal{G}$ where the path needs to satisfy
two given $\omega$-regular objectives $\Phi_{1}$ and $\Phi_{2}$,
simultaneously. The building blocks of auction-based scheduling are _tenders_
; for $i\in\left\\{1,2\right\\}$, a tender $\tau_{i}$ for the objective
$\Phi_{i}$ is a triple
$\left\langle\alpha_{i},\beta_{i},\mathbb{B}_{i}\right\rangle$, where at each
point in time, the action policy $\alpha_{i}$ proposes the next edge to be
taken, the _bidding policy_ $\beta_{i}$ proposes a bid from the available
budget, and the _threshold budget_ $\mathbb{B}_{i}$ indicates that the initial
budget allocation needs to be strictly greater than $\mathbb{B}_{i}$ in order
to guarantee $\Phi_{i}$. The _composition_ of $\tau_{1}$ and $\tau_{2}$,
denoted $\tau_{1}\\!\bowtie\\!\tau_{2}$, is a policy in $\mathcal{G}$
augmented with a register to keep track of the available budgets; the
composition works as follows. Firstly, $\tau_{1}$ and $\tau_{2}$ are
_compatible_ (for composition) only if $\mathbb{B}_{1}+\mathbb{B}_{2}<1$,
because then we can initially distribute the total budget—normalized to
$1$—between the two tenders in a way that they have more budgets than their
thresholds. The current configuration is a pair $\langle v,B_{1}\rangle$,
meaning that the current vertex is $v$ and $B_{1}$ is the available budget of
the first tender. With the normalization of the total budget, the available
budget of the second tender is implicitly $B_{2}=1-B_{1}$. The initial
configuration is $\langle v^{0},B^{0}_{1}\rangle$ such that, for each
$i\in\left\\{1,2\right\\}$, we have $\mathbb{B}_{i}<B_{i}^{0}\leq 1$. At each
point in time, tender $\tau_{i}$ proposes independently an action $\langle
u_{i},b_{i}\rangle$ (given respectively by $\alpha_{i}$ and $\beta_{i}$),
where $b_{i}\leq B_{i}$ is a bid and $u_{i}$ is the vertex to proceed to upon
winning the bidding. The higher bidder chooses the next vertex and pays the
lower bidder; formally, if $b_{1}\geq b_{2}$, the next configuration is
$\langle u_{1},B_{1}-b_{1}\rangle$, and otherwise it is $\langle
u_{2},B_{1}+b_{2}\rangle$. The central problem studied in this paper is
decentralized synthesis of tenders for auction-based scheduling: Given
$\mathcal{G}$, $\Phi_{1}$, and $\Phi_{2}$, synthesize $\tau_{1}$ such that for
every $\tau_{2}^{\prime}$, the path generated by
$\tau_{1}\\!\bowtie\\!\tau_{2}^{\prime}$ satisfies $\Phi_{1}$, and—
_independently_ —synthesize $\tau_{2}$ such that for every
$\tau_{1}^{\prime}$, the path generated by
$\tau_{1}^{\prime}\\!\bowtie\\!\tau_{2}$ satisfies $\Phi_{2}$. It follows that
the path generated by $\tau_{1}\\!\bowtie\\!\tau_{2}$ satisfies
$\Phi_{1}\land\Phi_{2}$.

We consider three instantiations of decentralized synthesis based on the
tradeoff between the strengths of the solutions and the strengths of the
assumptions that the tenders make on each other:

Strong decentralized synthesis. Here, tenders make no assumptions on each
other, thus the solutions provide the strongest (the most robust) guarantees.

$a$start$b$$c$$d$$e$$f$$g$ (a) Strong

$a$start$b$$c$$d$$e$$f$$g$ (b) Assume-admissible

$a$start$b$$c$$d$$e$$f$$g$ (c) Assume-guarantee

Figure 1: Graphs with two reachability objectives given by targets:
$T_{\mathsf{blue}}$, depicted in blue, $T_{\mathsf{red}}$ depicted in red, and
$T_{\mathsf{blue}}\cap T_{\mathsf{red}}$ depicted in purple. The action
policies of the red and blue tenders choose edges with, respectively, red and
blue shadows (shared edges in purple). If no edges from a vertex have red or
blue shadow, then the respective tender is indifferent about the choice made.
Thick edges depict the paths taken by the compositions of tenders.

###### Example 1

Consider the graph depicted in Fig. 1(a), with a pair of reachability
objectives: the “blue” targets are $T_{\mathsf{blue}}=\left\\{c,d,g\right\\}$
and the “red” targets are $T_{\mathsf{red}}=\left\\{d,f\right\\}$. Their
intersection $\left\\{d\right\\}$ is depicted in purple. We present a pair of
robust tenders $\tau_{\mathsf{blue}}$ and $\tau_{\mathsf{red}}$ with
$\mathbb{B}_{\mathsf{blue}}=\nicefrac{{1}}{{4}}$ and
$\mathbb{B}_{\mathsf{red}}=\nicefrac{{1}}{{2}}$, thus $\tau_{\mathsf{blue}}$
and ${\tau_{\mathsf{red}}}$ are compatible. We will show that
$\tau_{\mathsf{blue}}$ guarantees that no matter which compatible tender it is
composed with, eventually $T_{\mathsf{blue}}$ is reached, and similarly
$\tau_{\mathsf{red}}$ ensures that $T_{\mathsf{red}}$ is reached. Thus,
necessarily, $\tau_{\mathsf{blue}}\\!\bowtie\\!\tau_{\mathsf{red}}$ ensures
that $d$ is reached.

We first describe $\tau_{\mathsf{blue}}$. Consider an initial configuration
$\langle a,\nicefrac{{1}}{{4}}+\epsilon\rangle$, for any $\epsilon>0$. Note
that the other tender’s budget is $\nicefrac{{3}}{{4}}-\epsilon$. The first
action of $\tau_{\mathsf{blue}}$ is $\langle b,\nicefrac{{1}}{{4}}\rangle$.
There are two possibilities. First, $\tau_{\mathsf{blue}}$ wins the bidding,
then we reach the configuration $\langle b,\epsilon\rangle$, and since both
successors of $b$ are in $T_{\mathsf{blue}}$, the objective is satisfied.
Second, $\tau_{\mathsf{blue}}$ loses the bidding, meaning that the other
tender bids at least $\nicefrac{{1}}{{4}}$, thus in the worst case, we proceed
to the configuration $\langle e,\nicefrac{{1}}{{2}}+\epsilon\rangle$. Next,
$\tau_{\mathsf{blue}}$ chooses $\langle g,\nicefrac{{1}}{{2}}\rangle$. Since
the other budget is $\nicefrac{{1}}{{2}}-\epsilon$, this ensures winning the
bidding and reaching $g\in T_{\mathsf{blue}}$. We stress that the only
assumption made on the other tender is the implicit knowledge of its initial
budget.

We describe $\tau_{\mathsf{red}}$. Consider an initial configuration $\langle
a,\nicefrac{{1}}{{2}}+\epsilon\rangle$, for any $\epsilon>0$. Initially,
$\tau_{\mathsf{red}}$ bids $0$, because it does not have a preference between
going left or right. In the worst case, the budget stays
$\nicefrac{{1}}{{2}}+\epsilon$ in the next turn. Since both $b$ and $e$ have
single successors in $T_{\mathsf{red}}$, thus $\tau_{\mathsf{red}}$ must win
the bidding. It does so by bidding $\nicefrac{{1}}{{2}}$, which exceeds the
available budget of the other tender. $\triangle$

Our algorithms for decentralized synthesis internally solve zero-sum bidding
games [39, 38]. A bidding game is played on a finite graph by two players
called $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ and
$\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$. The game proceeds as
follows. The players have bounded budgets, and in each turn, both players bid
for the right to take an action. A strategy in a bidding game, using our
terminology, is a pair $\langle\alpha,\beta\rangle$ of action and bidding
policies. The central question is to find a winning strategy, namely a
strategy that guarantees winning, with respect to a given objective, no matter
which strategy the opponent follows. For $\omega$-regular objectives, it was
shown in [39, 38, 10] that each vertex $v$ can be associated with a threshold
$\mathit{Th}(v)$ such when $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$’s
budget at $v$ is $B_{X}>\mathit{Th}(v)$,
$\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ has a winning strategy, and
when $B_{X}<\mathit{Th}(v)$, $\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$
has a winning strategy.

Our algorithm to solve strong decentralized synthesis proceeds as follows.
Given a graph $\mathcal{G}$ with an initial vertex $v^{0}$ and two objectives
$\Phi_{1}$ and $\Phi_{2}$, we solve two zero-sum bidding games
$\mathcal{G}_{1}$ and $\mathcal{G}_{2}$, independently. Both games are played
on the graph $\mathcal{G}$. In $\mathcal{G}_{1}$,
$\mathit{\mathit{Player}\leavevmode\nobreak\ X}$’s objective is $\Phi_{1}$ and
in $\mathcal{G}_{2}$, his objective is $\Phi_{2}$. Let
$\mathit{Th}_{1}(v^{0})$ and $\mathit{Th}_{2}(v^{0})$ respectively denote the
thresholds at $v^{0}$ in $\mathcal{G}_{1}$ and $\mathcal{G}_{2}$. We show that
a pair of robust tenders exist iff
$\mathit{Th}_{1}(v^{0})+\mathit{Th}_{2}(v^{0})<1$. When they exist, for
$i\in\left\\{1,2\right\\}$, we output the tender
$\tau_{i}=\langle\alpha_{i},\beta_{i},\mathit{Th}_{i}(v^{0})\rangle$, where
the pair $\langle\alpha_{i},\beta_{i}\rangle$ is a winning
$\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ strategy in the game
$\mathcal{G}_{i}$. Since $\tau_{i}$ is a winning strategy, it ensures that
objective $\Phi_{i}$ is satisfied when composed with any compatible strategy.
Thus, necessarily, the composition $\tau_{1}\\!\bowtie\\!\tau_{2}$ of two
tenders in $\mathcal{G}$ ensures that both objectives are satisfied!

Assume-admissible decentralized synthesis. While the guarantees of strong
decentralized synthesis are appealing, the weakness is that it often fails due
to the pessimistic assumptions that the tenders make on each other. We address
this issue by considering a weak concept of rationality called admissiblity
[23]. We illustrate the idea in the following example.

###### Example 2

Consider the graph in Fig. 1(b), with reachability objectives given by targets
$T_{\mathsf{blue}}=\left\\{d,g\right\\}$ and
$T_{\mathsf{red}}=\left\\{d,f\right\\}$. We argue that strong decentralized
synthesis is not possible. Indeed, using the same reasoning for
$\tau_{\mathsf{red}}$ in Ex. 1, we have
$\mathit{Th}_{\mathsf{blue}}(a)=\mathit{Th}_{\mathsf{red}}(a)=0.5$. On the
other hand, observe that when synthesizing $\tau_{\mathsf{red}}$, since
$c\notin T_{\mathsf{blue}}$, we know that a “rational” $\tau_{\mathsf{blue}}$
(formally, admissible $\tau_{\mathsf{blue}}$, see Sec. 6), will not proceed
from $b$ to $c$, thus we can omit the edge. In turn, the threshold in $a$
decreases to $\nicefrac{{1}}{{4}}$ for both objectives. Since the sum of
thresholds is now less than $1$, two compatible tenders can be obtained.
$\triangle$

In general, we seek an admissible-winning tender, which ensures that its
objective is satisfied when being composed with any admissible tender. Note
that we maintain modularity: an admissible-winning tender can be reused
provided that the set of admissible actions of the other tender remains
unchanged. For example, even when vertex $g$ is added to the red target set,
the blue tender can be used with no change. Somewhat surprisingly, we show
that in graphs in which all vertices have out-degree at most $2$, assume-
admissible decentralized synthesis is always possible, and finding a pair of
admissible-winning tenders is in PTIME.

Assume-guarantee decentralized synthesis. Sometimes, even the admissible
assumption is too weak, and we need more direct synchronization of the
tenders. We consider assume-guarantee decentralized synthesis, where each
tender needs to respect a pre-specified _contract._ The contracts ensures that
a composition of such tenders satisfies both objectives. We illustrate the
idea below.

###### Example 3

Consider the graph depicted in Fig. 1(c), with reachability objectives given
by targets $T_{\mathsf{blue}}=\left\\{c,d,g\right\\}$ and
$T_{\mathsf{red}}=\left\\{d,f\right\\}$. Here, the strong decentralized
synthesis fails due to reasons similar to Ex. 2. The assume-admissible
decentralized synthesis fails because from $e$, both objectives cannot be
fulfilled, and from $b$, no matter which tender wins the bidding can use an
admissible edge that violates the other objective (e.g., $(b,c)$ is admissible
for $\tau_{\mathsf{blue}}$ but violates $T_{\mathsf{red}}$). We consider the
contract $\left\langle
G_{\mathsf{blue}},G_{\mathsf{red}}\right\rangle=\left\langle\mathbf{G}\,\lnot
c,\mathbf{G}\,\lnot f\right\rangle$, which is satisfied when (a) if
$\alpha_{\mathsf{blue}}$ fulfills $G_{\mathsf{blue}}$, then
$\alpha_{\mathsf{red}}$ fulfills $G_{\mathsf{red}}$, and (b) if
$\alpha_{\mathsf{red}}$ fulfills $G_{\mathsf{red}}$, then
$\alpha_{\mathsf{blue}}$ fulfills $G_{\mathsf{blue}}$. Now whichever tender
wins the bidding at $b$ needs to fulfill its guarantee, because it cannot
judge from the past interaction if the other tender fulfills its guarantee.
Therefore, from $b$, the next vertex will be $d$ under the contract, and using
the same tenders from Ex. 2, both objectives will be fulfilled.

###  1.1 Related Work

_Shielding_ [36] is a framework in which a runtime monitor called a shield
enforces an unverified policy $\pi$ (e.g., generated using reinforcement
learning [7]) to satisfy a given specification. A shield operates by
observing, at each point in time, the action proposed by $\pi$ and can alter
it, e.g., if safety is violated. The choice of who acts at each point in time,
$\pi$ or the shield, can be seen as a scheduling choice similar to our
setting. However, the goals of the two approaches are different: our goal is
to design tenders for modular policy synthesis, whereas a shield is meant as a
verified “wrapper” for a complex policy. Technically, in auction-based
scheduling, the scheduling depends on the auction which is external to the
policies, whereas in shielding, it is the shield who chooses whether to
override $\pi$.

In distributed reactive synthesis [43, 37, 33], the goal is to design a
collection of Mealy machines whose communication is dictated by a given
communication architecture. Distributed synthesis is well studied and we point
to a number of works that considered objectives that are a conjunction
$\Phi_{1}\land\Phi_{2}\land\ldots$ of sub-objectives
$\Phi_{1},\Phi_{2},\ldots$ [31, 20, 40, 32, 17, 6]. While there is a
conceptual similarity between our synthesis of tenders and the synthesis of
Mealy machines, there is a fundamental difference between the approaches.
Namely, our composition is based on scheduling, i.e., exactly one policy is
scheduled at each point in time, whereas in distributed synthesis, the
composition of the Mealy machines is performed in parallel, i.e., they all
read and write at each point in time.

Our algorithms build upon the rich literature on bidding games on graphs. The
bidding mechanism that we focus on is called Richman bidding [39, 38, 10].
Other bidding mechanisms have been studied: poorman [11], taxman [13], and
all-pay [14, 15]. Auction-based scheduling can be instantiated with any of
these mechanisms and the properties from bidding games transfer immediately
(which differ significantly for quantitative objectives). Of particular
interest in practice is discrete bidding, in which the granularity of the bids
is restricted [28, 2, 16]. To the best of our knowledge, beyond our work, non-
zero-sum bidding games have only been considered in [41]. The solution concept
that they consider is subgame perfect equilibrium (SPE). While it is suitable
to model the interaction between selfish agents, we argue that it is less
suitable in decentralized synthesis.

There are many works on designing optimal policies for multi-objective
sequential decision making problems for various different system models; see
the survey by Roijers et al. [44] and works on multi-objective stochastic
games [19, 20, 25]. To the best of our knowledge, no prior work considers the
decomposition of the problem into individual task-dependent policies like us.
Auctions to distribute tasks to agents have been consideredextensively [30,
45, 26, 29, 18, 27, 42]. Their goal is very different: their agents bid for
tasks, that is, a bid represents an agent’s cost (e.g., in terms of resources)
for performing a task. The auction then allocates the tasks to agents so as to
minimize the individual costs, giving rise to an efficient global policy.

##  2 Preliminaries

Let $\Sigma$ be a finite alphabet. We use $\Sigma^{*}$ and $\Sigma^{\omega}$
to respectively denote the set of finite and infinite words over $\Sigma$, and
$\Sigma^{\infty}$ to denote $\Sigma^{*}\cup\Sigma^{\omega}$. Let for two words
$u\in\Sigma^{*}$ and $v\in\Sigma^{\infty}$, $u\leq v$ denote that $u$ is a
prefix of $v$, i.e., there exists a $w$ such that $v=uw$. Given a language
$L\subseteq\Sigma^{\infty}$, define $\mathsf{pref}(L)$ to be the set of every
finite prefix in $L$, i.e.,
$\mathsf{pref}(L)\coloneqq\left\\{u\in\Sigma^{*}\mid\exists v\in L\;.\;u\leq
v\right\\}$.

##### Graphs.

We formalize path planning problems on _graphs_. A graph $\mathcal{G}$ is a
tuple $\left\langle V,v^{0},E\right\rangle$ where $V$ is a finite set of
vertices, $v^{0}$ is a designated initial vertex, and $E\subseteq V\times V$
is a set of directed edges. If $(u,v)\in E$, then $v$ is a _successor_ of $u$.
A _binary graph_ is a graph whose every vertex has at most two successors. A
_path_ over $\mathcal{G}$ is a sequence of vertices $v^{0}v^{1}\ldots$ so that
every $(v^{i},v^{i+1})\in E$. Unless explicitly mentioned, paths always start
at $v^{0}$. We use $\mathit{Paths}^{\mathsf{fin}}(\mathcal{G})$ and
$\mathit{Paths}^{\mathsf{inf}}(\mathcal{G})$ to denote the sets of finite and
infinite paths, respectively.

A _strongly connected component_ (SCC) of the graph $\mathcal{G}$ is a set $S$
of vertices, such that there is a path between every pair of vertices of $S$.
An SCC $S$ is called a _bottom strongly connected component_ (BSCC) if there
does not exist any edge from a vertex in $S$ to a vertex outside of $S$. The
graph $\mathcal{G}$ is itself called strongly connected if $V$ is an SCC.

##### Objectives.

Fix a graph $\mathcal{G}$. An _objective_ $\Phi$ _in_ $\mathcal{G}$ is a set
of infinite paths, i.e.,
$\Phi\subseteq\mathit{Paths}^{\mathsf{inf}}(\mathcal{G})$. For an infinite
path $\rho$, we use $\mathit{Inf}(\rho)$ to denote the set of vertices that
$\rho$ visits infinitely often. We focus on the following objectives:

Reachability:

for $S\subseteq V$,
$\mathit{Reach}_{\mathcal{G}}(S)\coloneqq\left\\{v^{0}v^{1}\ldots\in\mathit{Paths}^{\mathsf{inf}}(\mathcal{G})\mid\exists
i\geq 0\;.\;v^{i}\in S\right\\}$,

Safety:

for $S\subseteq V$,
$\mathit{Safe}_{\mathcal{G}}(S)\coloneqq\left\\{v^{0}v^{1}\ldots\in\mathit{Paths}^{\mathsf{inf}}(\mathcal{G})\mid\forall
i\geq 0\;.\;v^{i}\in S\right\\}$,

Büchi:

for $S\subseteq V$,
$\mathit{B\ddot{u}chi}_{\mathcal{G}}(S)\coloneqq\left\\{\rho\in\mathit{Paths}^{\mathsf{inf}}(\mathcal{G})\mid\mathit{Inf}(\rho)\cap
S\neq\emptyset\right\\}$,

Parity (max, even):

for $\mathit{Col}\colon V\to[0;k]$ for some $k>0$,
$\mathit{Parity}_{\mathcal{G}}(\mathit{Col})\coloneqq\left\\{\rho\in\mathit{Paths}^{\mathsf{inf}}(\mathcal{G})\mid\max\left\\{i\mid\exists
v\in\mathit{Inf}(\rho)\;.\;\mathit{Col}(v)=i\right\\}\text{ is
even}\right\\}$,

Given an objective $\Phi$, we will use $\Phi^{c}$ to denote its complement,
i.e., $\Phi^{c}=\mathit{Paths}^{\mathsf{inf}}(\mathcal{G})\setminus\Phi$. In
particular,
$(\mathit{Reach}_{\mathcal{G}}(S))^{c}=\mathit{Safe}_{\mathcal{G}}(V\setminus
S)$.

##### Action policies.

Fix a graph $\mathcal{G}$. An _action policy_ is a function
$\alpha\colon\mathit{Paths}^{\mathsf{fin}}(\mathcal{G})\to V$, choosing the
next vertex to extend any given finite path $\rho v$, where $\left\langle
v,\alpha(\rho v)\right\rangle\in E$. The action policy $\alpha$ is
_memoryless_ if for every pair of distinct finite paths $\rho
v,\rho^{\prime}v$ that end in the same vertex $v$, it holds that $\alpha(\rho
v)=\alpha(\rho^{\prime}v)$; in this case we simply write $\alpha(v)$. An
action policy $\alpha$ generates a unique infinite path in $\mathcal{G}$,
denoted $\mathit{out}(\alpha)$, and defined inductively as follows. The
initial vertex is $v^{0}$. For every prefix $v^{0},\ldots,v^{i}$ of
$\mathit{out}(\alpha)$, for $i\geq 0$, $v^{i+1}=\alpha(v^{0},\ldots,v^{i})$.
We say that the policy $\alpha$ _satisfies_ a given objective $\Phi$, written
$\alpha\models\Phi$ iff $\mathit{out}(\alpha)\in\Phi$.

##  3 The Auction-Based Scheduling Framework

Consider a graph $\mathcal{G}=\left\langle V,v^{0},E\right\rangle$ and a pair
of objectives $\Phi_{1},\Phi_{2}\subseteq V^{\omega}$ with nonempty
intersection (i.e., $\Phi_{1}\cap\Phi_{2}\neq\emptyset$), called _overlapping_
objectives from now on. The _multi-objective planning problem_ asks to
synthesize an action policy that satisfies the _global_ objective
$\Phi_{1}\cap\Phi_{2}$.

We propose a decentralized approach to the problem. Our goal is to design two
_local_ action policies $\alpha_{1}$ and $\alpha_{2}$ for $\Phi_{1}$ and
$\Phi_{2}$, respectively. Understandably, $\alpha_{1}$ and $\alpha_{2}$ may
choose conflicting successors for extending a given finite path. In order to
decide whose choice to accept, an auction (aka bidding) is held, where the
policies bid for the privilege of being _scheduled_ and choosing the next
vertex. To add the bidding ability, we instrument each action policy with a
_bidding policy_ and an initial _budget_ allocation. At each point in time,
the two bidding policies simultaneously propose their bids. The one that bids
higher chooses the next vertex and “pays” the bid amount to the other policy.
We formalize the framework below.

Every tender has a budget $B\in[0,1]$ that changes over time. At any point,
based on the available budget $B$ and the current vertex, a bidding policy
provides a bid not greater than $B$. History-dependent bidding policies are
possible, but not needed.

######  Definition 1 (Bidding policies)

A _bidding policy_ is a function $\beta\colon V\times[0,1]\to[0,1]$, with the
constraint that $\beta(v,B)\leq B$ for every $v,B$.

Bidding policies are ineffective without sufficient budget. We introduce
_tenders_ , each of which encapsulates an action policy, a bidding policy, and
the _threshold budget_ , which represents the greatest lower bound on the
initial available budget for the bidding and action policies to function as
intended. The goal of our decentralized framework is to independently
synthesize a pair of tenders which fulfill each objective separately. We
stress that the threshold budget is tied to the initial vertex, which will be
fixed to $v^{0}$ in all our graphs.

######  Definition 2 (Tenders)

A _tender_ for a given graph $\mathcal{G}$ is a triple
$\left\langle\alpha,\beta,\mathbb{B}\right\rangle$ of an action policy
$\alpha$, a bidding policy $\beta$, and a _threshold budget_
$\mathbb{B}\in[0,1]$. The set of all tenders for $\mathcal{G}$ is denoted
$\mathcal{T}^{\mathcal{G}}$. A tender $\tau$ _satisfies_ an objective $\Phi$,
denoted $\tau\models\Phi$, iff $\alpha\models\Phi$.

A single isolated tender is uninteresting. We take two tenders and compose
them via auction-based scheduling. The composition produces an action policy
that uses a register of memory to keep track of the available budgets. We
introduce some notation. A configuration is a pair $\left\langle
v,B_{1}\right\rangle$, indicating that the location is vertex $v$ and the
available budget for the first tender is $B_{1}$. We normalize the sum of
budgets to $1$, hence implicitly, the available budget for the second tender
is $B_{2}=1-B_{1}$. Let $\mathcal{C}=V\times[0,1]$ be the set of all
configurations, and for a given sequence of configurations
$s=(v^{0},B_{1}^{0})(v^{1},B_{1}^{1})\ldots\in\mathcal{C}^{\infty}$, let
$\mathsf{proj}_{V}(s)$ denote the path $v^{0}v^{1}\ldots$. A _history_ is a
finite sequence of configurations $\left\langle
v^{0},B_{1}^{0}\right\rangle\ldots\left\langle
v^{k},B_{1}^{k}\right\rangle\in\mathcal{C}^{*}$ with the constraint that
$\mathsf{proj}_{V}(s)\in\mathit{Paths}^{\mathsf{fin}}(\mathcal{G})$. Let
$\mathcal{H}$ be the set of all histories. The composition takes every history
$hc\in\mathcal{H}$ ending at $c\in\mathcal{C}$, and extends it with the next
configuration $c^{\prime}=(v^{\prime},B_{1}^{\prime})$ obtained as follows.
The configuration $c$ is fed to the two bidding policies to obtain two bids,
the highest bidder is determined, $\mathsf{proj}_{V}(hc)$ is fed to the
highest bidder’s action policy to obtain $v^{\prime}$, and the bid amount is
transferred from the highest bidder’s budget to the lowest bidder’s budget,
updating the first tender’s budget to $B_{1}^{\prime}$.

######  Definition 3 (Composition of tenders)

Let $\mathcal{G}$ be a graph, and
$\tau_{1}=\left\langle\alpha_{1},\beta_{1},\mathbb{B}_{1}\right\rangle$ and
$\tau_{2}=\left\langle\alpha_{2},\beta_{2},\mathbb{B}_{2}\right\rangle$ be two
tenders. The tenders $\tau_{1}$ and $\tau_{2}$ are _compatible_ iff
$\mathbb{B}_{1}+\mathbb{B}_{2}<1$. If compatible, then their _composition_ ,
denoted $\tau_{1}\\!\bowtie\\!\tau_{2}$, is a function
$\tau_{1}\\!\bowtie\\!\tau_{2}\colon\mathcal{H}\to\mathcal{C}$ defined as
follows. Given a history $h=\left\langle
v^{0},B_{1}^{0}\right\rangle\ldots\left\langle
v^{k},B_{1}^{k}\right\rangle\in\mathcal{H}$, let
$b_{1}\coloneqq\beta_{1}(v^{k},B_{1}^{k})$ and
$b_{2}\coloneqq\beta_{2}(v^{k},1-B_{1}^{k})$. Then,

  * •

if $b_{1}\geq b_{2}$, then
$\tau_{1}\\!\bowtie\\!\tau_{2}(h)=\left(\alpha_{1}(\rho
v),B_{1}-b_{1}\right)$, and

  * •

if $b_{1}<b_{2}$, then $\tau_{1}\\!\bowtie\\!\tau_{2}(h)=\left(\alpha_{2}(\rho
v),B_{1}+b_{2}\right)$.

Given an initial configuration $\left\langle v^{0},B_{1}^{0}\right\rangle$
with $B_{1}^{0}>\mathbb{B}_{1}$ and $B_{2}^{0}=1-B_{1}^{0}>\mathbb{B}_{2}$,
the composition outputs an infinite sequence of configurations, denoted
$\mathrm{out}(\tau_{1}\\!\bowtie\\!\tau_{2})$, where
$\mathrm{out}(\tau_{1}\\!\bowtie\\!\tau_{2})\coloneqq\left\langle
v^{0},B_{1}^{0}\right\rangle\left\langle
v^{1},B_{1}^{1}\right\rangle\ldots\in\mathcal{C}^{\omega}$ such that for every
$k$, $\left\langle
v^{k},B_{1}^{k}\right\rangle=\tau_{1}\\!\bowtie\\!\tau_{2}\left(\left\langle
v^{0},B_{1}^{0}\right\rangle\ldots\left\langle
v^{k-1},B_{1}^{k-1}\right\rangle\right)$. We will say
$\tau_{1}\\!\bowtie\\!\tau_{2}$ satisfies a given objective $\Phi$, written
$\tau_{1}\\!\bowtie\\!\tau_{2}\models\Phi$, iff
$\mathsf{proj}_{V}(\mathrm{out}(\tau_{1}\\!\bowtie\\!\tau_{2}))\in\Phi.$

We will often use the index $i\in\left\\{1,2\right\\}$ to refer to either of
the two tenders or their attributes, and will use $-i=3-i$ for the “other”
one, e.g., $\tau_{i}$ and $\tau_{-i}$.

For a given graph $\mathcal{G}$ and a given pair of overlapping objectives
$\Phi_{1}$ and $\Phi_{2}$, we informally state the three classes of
decentralized synthesis problem that we will study.

Strong decentralized synthesis:

For each $i\in\left\\{1,2\right\\}$, design a $\tau_{i}$ such that for every
compatible $\tau_{-i}$, $\tau_{i}\\!\bowtie\\!\tau_{-i}\models\Phi_{i}$;

Assume-admissible decentralized synthesis:

For each $i\in\left\\{1,2\right\\}$, design a $\tau_{i}$ such that for every
compatible _admissible_ $\tau_{-i}$,
$\tau_{i}\\!\bowtie\\!\tau_{-i}\models\Phi_{i}$, where admissibility is an
established formalization of rationality [21, 24];

Assume-guarantee decentralized synthesis:

Let $A_{1},A_{2}\subseteq V^{\omega}$ be a pair of languages, called the
_assumptions_. For each $i\in\left\\{1,2\right\\}$, design a $\tau_{i}$ such
that such that for every compatible $\tau_{-i}$, at any point if $\tau_{-i}$
has fulfilled $A_{-i}$ in the past, then $\tau_{i}$ fulfills $A_{i}$ in
return, and additionally ensures
$\tau_{i}\\!\bowtie\\!\tau_{-i}\models\Phi_{i}$.

We will formalize the above synthesis problems in the subsequent sections, and
for each of them, we will identify the classes of problem instances for which
a solution exists. We will observe that strong decentralized synthesis
provides the most robust solutions, but the tenders usually require higher
threshold budgets, and compatible tenders may not always exist. Assume-
guarantee decentralized synthesis provides the least robust solutions and
requires direct synchronization of the tenders through assumptions, but with
the right type of contracts they can always be found. Assume-admissible
decentralized synthesis strikes a balance in terms of robustness and chances
of success; most importantly, we show that for reachability objectives in
binary graphs, a solution can always be found.

##  4 An Aside on Bidding Games on Graphs

All our synthesis algorithms internally solve bidding games, which we briefly
review here; see the survey [8] for more details.

A two-player bidding game is played between
$\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ and
$\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$, and is a tuple
$\langle\mathcal{G},\Phi\rangle$, where $\mathcal{G}=\langle V,E\rangle$ is
the (finite, directed) graph and $\Phi\subseteq V^{\omega}$ is the objective
for $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$. The game is _zero-sum_ ,
meaning that the objective of $\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$
is the violation of $\Phi$, i.e., $V^{\omega}\setminus\Phi$. The dynamics of a
bidding game is the same as auction-based scheduling. A strategy for a player
is a pair $\langle\alpha,\beta\rangle$. As in composition of tenders, two
strategies and an initial configuration $\langle v,B_{1}\rangle$ give rise to
an infinite sequence of configurations called a play. A strategy is winning if
no matter which strategy the opponent follows, the play satisfies the player’s
objective. A central quantity in bidding games is the threshold budget in a
vertex $v$, which is intuitively, a necessary and sufficient initial budget
for $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ to guarantee winning.
Formally,

######  Definition 4 (Threshold budgets)

Consider a bidding game $\langle\mathcal{G},\Phi\rangle$ where
$\mathcal{G}=\left\langle V,E\right\rangle$. The thresholds of
$\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ are given by
$\mathit{Th}_{\Phi}^{\mathcal{G}}:V\rightarrow[0,1]$, where for every $v\in
V$, we have
$\mathit{Th}_{\Phi}^{\mathcal{G}}(v)=\inf_{B}\left\\{\text{$\mathit{\mathit{Player}\leavevmode\nobreak\
X}$ has a winning strategy from }\langle v,B\rangle\right\\}$.

The threshold from $\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$’s
perspective is denoted $\mathit{Th}_{\Phi^{c}}^{\mathcal{G}}(v)$. The
following theorem shows that the two thresholds coincide as well as
characterize their structure, which has complexity implications. In App. 0.A,
we present intuition on the structure of thresholds and how winning strategies
can be constructed from the thresholds.

######  Theorem 4.1 ([39])

Consider a reachability bidding game
$\left\langle\mathcal{G},\Phi\right\rangle$ given by a set of target vertices
$T$ that are sinks. For every vertex $v$, we have
$\mathit{Th}_{\Phi}^{\mathcal{G}}(v)=1-\mathit{Th}_{\Phi^{c}}^{\mathcal{G}}(v)$.
Moreover, for every sink vertex $t$, we have
$\mathit{Th}_{\Phi}^{\mathcal{G}}(t)=0$, if $t\in T$, and
$\mathit{Th}_{\Phi}^{\mathcal{G}}(t)=1$ otherwise. For every vertex $v$, we
have
$\mathit{Th}_{\Phi}^{\mathcal{G}}(v)=0.5\cdot(\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{+})+\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{-}))$,
where $v^{-}$ and $v^{+}$ are successors of $v$, such that for every other
successor $u$, we have
$\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{-})\leq\mathit{Th}_{\Phi}^{\mathcal{G}}(u)\leq\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{+})$.
For a binary graph $\mathcal{G}$, finding the thresholds can be done in PTIME.

For infinite-horizon objectives, like parity, it is known that eventually one
of the BSCCs will be reached, and inside every BSCC every vertex can be
reached by both players infinitely often with every arbitrary initial budget.
This implies that for every parity objective, the threshold of every vertex
inside every BSCC in a game graph is either $0$ or $1$, and fulfilling a given
parity objective is equivalent to _reaching_ a BSCC whose every vertex has
threshold $0$. We state this formally.

###### Theorem 4.2

[10] Consider a bidding game $\left\langle\mathcal{G},\Phi\right\rangle$ with
a parity objective $\Phi$. Let $S$ be a BSCC of $\mathcal{G}$. Every vertex in
$S$ has threshold either $0$ or $1$, and it is $1$ iff the highest parity
index in $S$ is odd. Moreover, for a vertex $v$ not in a BSCC, we have
$\mathit{Th}_{\Phi}^{\mathcal{G}}(v)=\mathit{Th}_{\mathit{Reach}_{\mathcal{G}}(T)}^{\mathcal{G}}(v)$,
where $T$ are BSCCs whose vertices have threshold $0$.

##  5 Strong Decentralized Synthesis

In this section, we study the strong decentralized synthesis problem in which
the goal is to synthesize two compatible robust tenders, where a robust tender
is one that guarantees its objective when composed with any compatible tender.

######  Definition 5 (Robust tenders)

Let $\mathcal{G}$ be a graph and $\Phi_{i}$ be an objective in $\mathcal{G}$.
A tender $\tau_{i}$ is _robust_ for $\Phi_{i}$ if for every other compatible
tender $\tau_{-i}\in\mathcal{T}^{\mathcal{G}}$, we have
$\tau_{i}\\!\bowtie\\!\tau_{-i}\models\Phi_{i}$.

###### Problem 1

Define $\mathsf{STRONG\mathchar 45\relax SYNT}$ as the problem whose input is
a tuple $\left\langle\mathcal{G},\Phi_{1},\Phi_{2}\right\rangle$, where
$\mathcal{G}$ is a graph and $\Phi_{1}$ and $\Phi_{2}$ are overlapping
$\omega$-regular objectives in $\mathcal{G}$, and the goal is to decide
whether there exists a pair of tenders
$\tau_{1},\tau_{2}\in\mathcal{T}^{\mathcal{G}}$ such that:

  1. (I)

$\tau_{1}$ and $\tau_{2}$ are compatible,

  2. (II)

$\tau_{1}$ is robust for $\Phi_{1}$, and

  3. (III)

$\tau_{2}$ is robust for $\Phi_{2}$.

Since each robust tender $\tau_{i}$ guarantees that $\Phi_{i}$ is satisfied
when composed with any tender, the composition of two robust tenders satisfies
both objectives:

###### Proposition 1

Let $\tau_{1}$ and $\tau_{2}$ be two compatible robust tenders for
$\left\langle\mathcal{G},\Phi_{1},\Phi_{2}\right\rangle$, then
$\tau_{1}\\!\bowtie\\!\tau_{2}\models\Phi_{1}\cap\Phi_{2}$.

We reduce the strong decentralized synthesis problem to the solution of two
independent bidding games, both played on the graph $\mathcal{G}$, one with
$\mathit{\mathit{Player}\leavevmode\nobreak\ X}$’s objective $\Phi_{1}$ and
one with $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$’s objective
$\Phi_{2}$. When the sum of thresholds is less than $1$, we set the two
tenders to be winning $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$
strategies in the two games. Since both are winning strategies for their
respective objectives, we are guaranteed that the composition satisfies both
objectives. Detailed proof can be found in App. 0.B.

######  Theorem 5.1 (Strong decentralized synthesis)

Let $\mathcal{G}=\left\langle V,v^{0},E\right\rangle$ be a graph and
$\Phi_{1}$ and $\Phi_{2}$ be a pair of overlapping $\omega$-regular
objectives. A pair of robust tenders exists iff
$\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{0})+\mathit{Th}_{\Phi_{2}}^{\mathcal{G}}(v^{0})<1$.
Moreover, $\mathsf{STRONG\mathchar 45\relax SYNT}$ is in NP $\cap$ coNP and in
PTIME for binary graphs.

We identify a setting where strong decentralized synthesis is always possible.
The following theorem follows from the result that threshold budgets in a
strongly-connected Büchi game in which there is one accepting vertex are $0$.

######  Theorem 5.2 (Strong decentralized synthesis on SCCs)

Consider a strongly-connected graph $\mathcal{G}$ and a pair of non-empty
Büchi objectives in $\mathcal{G}$. Then, a pair of robust tenders exists in
$\mathcal{G}$.

##  6 Assume-Admissible Decentralized Synthesis

In assume-admissible decentralized synthesis, each tender assumes that the
other tender is _rational_ and pursues its own objective. We formalize
rationality by adapting the well-known concepts of dominance and admissibility
from game theory [1, 22]. Intuitively, when $\tau_{1}$ dominates
$\tau^{\prime}_{1}$, there is no reason to use $\tau^{\prime}_{1}$ since it is
always as good (and sometimes better) to use $\tau_{1}$. An admissible tender
is a valid choice of tender.

######  Definition 6 (Dominance, admissibility)

Let $\mathcal{G}$ be a graph and $\Phi$ be an objective. We provide
definitions for the first tender and the definitions for the second tender are
dual. Let $\mathbb{B}_{1}<1$. For two tenders $\tau_{1}$ and
$\tau_{1}^{\prime}$ that have the same budget allocation, $\tau_{1}$ dominates
$\tau^{\prime}_{1}$ when

  1. (a)

$\tau_{1}$ performs as well as $\tau^{\prime}_{1}$ when composed with any
compatible $\tau_{2}$; formally, for every compatible tender $\tau_{2}$,
$\tau_{1}^{\prime}\\!\bowtie\\!\tau_{2}\models\Phi$ implies
$\tau_{1}\\!\bowtie\\!\tau_{2}\models\Phi$, and

  2. (b)

there is a compatible tender $\tau_{2}$ for which $\tau_{1}$ performs better
than $\tau^{\prime}_{1}$; formally, there exists a compatible $\tau_{2}$ with
$\tau_{1}\\!\bowtie\\!\tau_{2}\models\Phi$, and
$\tau_{1}^{\prime}\\!\bowtie\\!\tau_{2}\not\models\Phi$.

A tender $\tau_{1}$ is called $\Phi$-admissible in $\mathcal{G}$ iff it is not
dominated by any other tender. We denote the set of $\Phi$-admissible tenders
in $\mathcal{G}$ by $\textit{Adm}^{\mathcal{G}}(\Phi)$.

Next, we define admissible-winning tenders, which are tenders that fulfill
their objectives when composed with any admissible tender.

######  Definition 7 (Admissible-winning tenders)

Let $\mathcal{G}$ be a graph and $\Phi_{1},\Phi_{2}$ be a pair of overlapping
objectives in $\mathcal{G}$. A tender $\tau_{i}$ is called _$\Phi_{-i}$
-admissible-winning_ for $\Phi_{i}$ if and only if
$\tau_{i}\in\textit{Adm}^{\mathcal{G}}(\Phi_{i})$, and for every other tender
$\tau_{-i}\in\textit{Adm}^{\mathcal{G}}(\Phi_{-i})$ compatible with
$\tau_{i}$, we have $\tau_{i}\\!\bowtie\\!\tau_{-i}\models\Phi_{i}$.

When the objectives are clear from the context, we will omit them and will
simply write a tender is “admissible tender,” “admissible-winning tender,”
etc.

###### Problem 2

Define $\mathsf{AA\mathchar 45\relax SYNT}$ as the problem whose input is a
tuple $\left\langle\mathcal{G},\Phi_{1},\Phi_{2}\right\rangle$, where
$\mathcal{G}$ is a graph and $\Phi_{1}$ and $\Phi_{2}$ are overlapping
$\omega$-regular objectives in $\mathcal{G}$, and the goal is to decide
whether there exists a pair of tenders
$\tau_{1}\in\textit{Adm}^{\mathcal{G}}(\Phi_{1})$ and
$\tau_{2}\in\textit{Adm}^{\mathcal{G}}(\Phi_{2})$ such that:

  1. (I)

$\tau_{1}$ and $\tau_{2}$ are compatible,

  2. (II)

$\tau_{1}$ is $\Phi_{2}$-admissible-winning for $\Phi_{1}$, and

  3. (III)

$\tau_{2}$ is $\Phi_{1}$-admissible-winning for $\Phi_{2}$.

The following proposition follows from the requirement that $\tau_{1}$ and
$\tau_{2}$ are admissible.

###### Proposition 2

Let $\tau_{1}$ and $\tau_{2}$ be tenders that fulfill the requirements stated
in Prob. 2. Then, $\tau_{1}\\!\bowtie\\!\tau_{2}\models\Phi_{1}\cap\Phi_{2}$.

###### Remark 1

Note that the synthesis procedure for each $\Phi_{-i}$-admissible-winning
tender $\tau_{i}$ for $\Phi_{i}$ requires the knowledge of
$\textit{Adm}^{\mathcal{G}}(\Phi_{-i})$. Assume-admissible decentralized
synthesis is modular in the following sense. First, the specific
implementation of the tender $\tau_{-i}$ with which each $\tau_{i}$ is
composed is not known during synthesis. All that is known is the objective
$\Phi_{-i}$ for which $\tau_{-i}$ is synthesized. Second, each $\tau_{i}$ can
remain unchanged even when $\Phi_{-i}$ changes to $\Phi_{-i}^{\prime}$, as
long as
$\textit{Adm}^{\mathcal{G}}(\Phi_{-i}^{\prime})\subseteq\textit{Adm}^{\mathcal{G}}(\Phi_{-i})$.

###  6.1 Reachability objectives

Throughout this section we focus on overlapping reachability objectives
$\Phi_{1}=\mathit{Reach}_{\mathcal{G}}(T_{1})$ and
$\Phi_{2}=\mathit{Reach}_{\mathcal{G}}(T_{2})$ with $T_{1},T_{2}\subseteq V$
being sets of sink target vertices. This is without loss of generality, as
every graph with non-sink target vertices can be converted into a graph with
sink target vertices by adding memory (see App. 0.C).

We reduce the decentralized assume-admissible synthesis problem to solving a
pair of zero-sum bidding games on a sub-graph of $\mathcal{G}$. Intuitively,
an edge $e=\langle u,v\rangle$ is dominated for the $i$-th tender, for
$i\in\left\\{1,2\right\\}$, if it is possible to achieve the objective
$\Phi_{i}$ from $u$ but not from $v$. Clearly, a tender that chooses $e$ is
dominated and is thus not admissible (see the proof of the lemma below in App.
0.D). Recall that $\mathit{Th}_{\Phi_{i}}^{\mathcal{G}}(v)$ denotes the
threshold in the zero-sum bidding game played on $\mathcal{G}$ with the
$\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ objective $\Phi_{i}$, and
that $\mathit{Th}_{\Phi_{i}}^{\mathcal{G}}(v)=1$ means there is no path from
$v$ to $T_{i}$.

######  Lemma 1 (A necessary condition for admissibility)

For every vertex $u$ having at least two successors $v,w$ with
$\mathit{Th}_{\Phi_{i}}^{\mathcal{G}}(v)<1$ and
$\mathit{Th}_{\Phi_{i}}^{\mathcal{G}}(w)=1$, if a
$\mathit{\mathit{Player}\leavevmode\nobreak\ i}$ tender
$\left\langle\alpha_{i},\beta_{i},\mathbb{B}_{i}\right\rangle$ is in
$\textit{Adm}^{\mathcal{G}}(\Phi_{i})$, then $\alpha_{i}(u)\neq w$, for both
$i\in\left\\{1,2\right\\}$.

We obtain the reduced graph by omitting edges that are dominated for both
players. For example, in Fig. 1(b), the edge $\langle b,c\rangle$ is dominated
for both players (see Ex. 2) and in Fig. 1(c), no edge is dominated for both
players (see Ex. 3).

######  Definition 8 (Largest admissible sub-graphs)

The largest admissible sub-graph of $\mathcal{G}$ with respect to two
reachability objectives $\Phi_{1}$ and $\Phi_{2}$ is
$\widehat{\mathcal{G}}_{\Phi_{1},\Phi_{2}}=\left\langle
V^{\prime},E^{\prime}\right\rangle$ with $V^{\prime}=V\setminus\left\\{v\in
V\mid\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v)=1\land\mathit{Th}_{\Phi_{2}}^{\mathcal{G}}(v)=1\right\\}$
and $E^{\prime}=(V^{\prime}\times V^{\prime})\cap E$. We omit
$\Phi_{1},\Phi_{2}$ from $\widehat{\mathcal{G}}_{\Phi_{1},\Phi_{2}}$ when it
is clear from the context.

For a vertex $v$ in $\mathcal{G}$ and $i\in\left\\{1,2\right\\}$, recall that
$\mathit{Th}_{\mathcal{G}}^{\Phi_{i}}(v)$ denotes the threshold in
$\mathcal{G}$ for objective $\Phi_{i}$, and
$\mathit{Th}_{\widehat{\mathcal{G}}}^{\Phi_{i}}(v)$ denotes the threshold in
the reduced graph. Observe that a winning strategy in $\mathcal{G}$ will never
cross a dominated edge. Removing dominat ed edges restricts the opponent, thus
$\mathit{Th}_{\mathcal{G}}^{\Phi_{i}}(v)\geq\mathit{Th}_{\widehat{\mathcal{G}}}^{\Phi_{i}}(v)$.
The next lemma shows that, surprisingly, the decrease in sum of thresholds is
guaranteed to be significant. The proof (see App. 0.E) which holds for non-
binary graphs, intuitively follows from observing that in
$\widehat{\mathcal{G}}$, necessarily a sink that is a target for one of the
players is reached, and since there is an overlap in at least one sink, the
sum of thresholds is at most $1$.

######  Lemma 2 ()

For every vertex $v$, we have
$\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v)+\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v)\leq
1$. Moreover, when $\mathcal{G}$ is binary, we have
$\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v)+\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v)<1$.

Our synthesis procedure proceeds as in strong decentralized synthesis: find
and output a pair of robust tenders in $\widehat{\mathcal{G}}$, which are
guaranteed to exist when $\mathcal{G}$ is binary. In order to maintain
soundness (see Prop. 2), it is key to show that a robust tender $\tau_{i}$ in
$\widehat{\mathcal{G}}$ is admissible in $\mathcal{G}$. The proof of the
following lemma is intricate (see App. 0.F). We show that even when one can
find $\tau^{\prime}_{i}$ and $\tau_{-i}$ such that
$\tau_{i}\\!\bowtie\\!\tau_{-i}\not\models\Phi_{i}$ but
$\tau_{i}^{\prime}\\!\bowtie\\!\tau_{-i}\models\Phi_{i}$, it is possible to
construct $\tau_{-i}^{\prime}$ for which
$\tau_{i}\\!\bowtie\\!\tau_{-i}^{\prime}\models\Phi_{i}$ but
$\tau_{i}^{\prime}\\!\bowtie\\!\tau_{-i}^{\prime}\not\models\Phi_{i}$, thus
$\tau^{\prime}_{i}$ does not dominate $\tau_{i}$. Furthermore, such a tender
wins against a set of tenders which _over-approximates_ admissible tender for
$\Phi_{-i}$.

######  Lemma 3 ()

For $i\in\left\\{1,2\right\\}$, a robust tender for $\Phi_{i}$ in
$\widehat{\mathcal{G}}$ is $\Phi_{-i}$-admissible-winning for $\Phi_{i}$ in
$\mathcal{G}$.

The following theorem is obtained by combining Lemmas 2 and 3.

######  Theorem 6.1 (Assume-admissible decentralized synthesis for
reachability)

The problem $\mathsf{AA\mathchar 45\relax SYNT}$ is a tautology for binary
graphs: for every binary graph and two overlapping reachability objectives,
there exists a pair of compatible admissible-winning tenders. Moreover, the
tenders can be computed in PTIME.

###### Remark 2

For general (i.e., non-binary) graphs, $\mathsf{AA\mathchar 45\relax SYNT}$ is
not a tautology anymore; a counter-example is given in Ex. 3. However, the
same PTIME algorithm for computing tenders can still be used to obtain a sound
solution; the completeness question is left open for future work.

###  6.2 Büchi objectives

In this section, we consider binary graphs with a pair of overlapping Büchi
objectives. We first demonstrate that, unlike reachability, it is not
guaranteed that an assume-admissible decentralized solution exists.

$a$$b$start$c$$d$ Figure 2: A graph with no assume-admissible decentralized
solution.

###### Example 4

Consider the graph depicted in Fig. 2 with the Büchi objectives given by the
accepting vertices $S_{\mathsf{red}}=\left\\{b,d\right\\}$ and
$S_{\mathsf{blue}}=\left\\{a,c\right\\}$. Note that the objectives are
overlapping since the path $(bc)^{\omega}$ satisfies both. We argue that no
pair of compatible admissible-winning tenders exist. Note that a robust (hence
dominant) red tender forces reaching $d$, thus forcing $\Phi_{\mathsf{red}}$
to be satisfied. Dually, a robust blue tender forces $\Phi_{\mathsf{blue}}$ in
$a$. It can be shown that
$\mathit{Th}_{\Phi_{\mathsf{red}}}^{\mathcal{G}}(b)=\nicefrac{{2}}{{3}}$ and
$\mathit{Th}_{\Phi_{\mathsf{blue}}}^{\mathcal{G}}(b)=\nicefrac{{1}}{{3}}$.
Thus, for any $\mathbb{B}_{\mathsf{red}}$ and $\mathbb{B}_{\mathsf{blue}}$
with $\mathbb{B}_{\mathsf{red}}+\mathbb{B}_{\mathsf{blue}}<1$, there is a
robust tender that violates the other tender’s objective. $\triangle$

We generalize the concept of largest admissible subgraphs to Büchi objectives.
It is not hard to show that proceeding into a BSCC with an accepting state is
admissible. Indeed, Thm. 4.2 shows that there is a robust (hence admissible)
tender in such BSCCs. On the other hand, proceeding to a BSCC with no
accepting vertex is clearly not admissible. The largest admissible subgraph is
obtained by repeatedly removing BSCC that are not admissible for both tenders.
Formally, for a given action policy $\alpha$ and a given vertex $v$ of
$\mathcal{G}$, we will write $\alpha\not\models_{v}\Phi_{1}\cup\Phi_{2}$ to
indicate that the action policy cannot fulfill $\Phi_{1}\cup\Phi_{2}$ from the
initial vertex $v$.

###### Definition 9

The largest admissible sub-graph $\widehat{\mathcal{G}}_{\mathcal{B}}$ of
$\mathcal{G}$ for the Büchi objectives $\Phi_{1},\Phi_{2}$ is the graph
$\left\langle V^{\prime},E^{\prime}\right\rangle$ with
$V^{\prime}=V\setminus\left\\{v\in V\mid\forall\text{ action policy
}\alpha\;.\;\alpha\not\models_{v}\Phi_{1}\cup\Phi_{2}\right\\}$, and
$E^{\prime}=(V^{\prime}\times V^{\prime})\cap E$.

We describe a reduction to reachability games. For $i\in\left\\{1,2\right\\}$,
let $T_{i}$ denote the union of BSCCs of $\widehat{\mathcal{G}}_{\mathcal{B}}$
in which there is at least one Büchi accepting vertex for $\Phi_{i}$. We call
$\left\langle T_{1},T_{2}\right\rangle$ the _reachability core_ of
$\left\langle\Phi_{1},\Phi_{2}\right\rangle$ in
$\widehat{\mathcal{G}}_{\mathcal{B}}$. Let
$\Phi_{1}^{\prime}=\mathit{Reach}_{\widehat{\mathcal{G}}_{\mathcal{B}}}(T_{1})$
and
$\Phi_{2}^{\prime}=\mathit{Reach}_{\widehat{\mathcal{G}}_{\mathcal{B}}}(T_{2})$.
We proceed as in strong decentralized synthesis: we find
$\mathit{Th}_{\Phi_{1}^{\prime}}^{\widehat{\mathcal{G}}_{\mathcal{B}}}(v^{0})$
and
$\mathit{Th}_{\Phi_{2}^{\prime}}^{\widehat{\mathcal{G}}_{\mathcal{B}}}(v^{0})$
and return a pair of robust tenders if their sum is strictly less than $1$.
Note that unlike reachability objectives, in Büchi objectives the sum might be
$1$ as in Ex. 4. Moreover, as Ex. 4 illustrates, when the sum is $1$, no pair
of admissible-winning tenders exist. By adapting results from the previous
section, we obtain the following.

######  Theorem 6.2 (Assume-admissible decentralized synthesis for Büchi)

Let $\mathcal{G}$ be a binary graph and $\Phi_{1},\Phi_{2}$ be a pair of
overlapping Büchi objectives. Let $\left\langle T_{1},T_{2}\right\rangle$ be
the reachability core of $\left\langle\Phi_{1},\Phi_{2}\right\rangle$ in the
largest admissible sub-graph of $\mathcal{G}$ (for $\Phi_{1},\Phi_{2}$). A
pair of admissible-winning tenders exists iff $T_{1}\cap T_{2}\neq\emptyset$.
Moreover, $\mathsf{AA\mathchar 45\relax SYNT}$ for Büchi objectives is in
PTIME.

Like reachability (see Rem. 2), for Büchi objectives the same algorithm for
$\mathsf{AA\mathchar 45\relax SYNT}$ for binary graphs can be used to obtain a
sound solution for general graphs, and the completeness question is left open
for future work.

##  7 Assume-Guarantee Decentralized Synthesis

We present the assume-guarantee decentralized synthesis problem, the one with
the highest degree of synchronization among the tenders, with the benefit of
the most applicability. In this synthesis procedure, we assume that we are
given a pair of languages $A_{1},A_{2}\subseteq V^{\omega}$, called the
_assumptions_. Intuitively, each tender $\tau_{i}$ can _assume_ $A_{i}$ is
fulfilled by the other tender, and, in return, needs to _guarantee_ that
$A_{-i}$ is fulfilled, in addition to fulfilling own objective.

###### Definition 10

Let $\mathcal{G}$ be a graph, $\Phi_{i}$ be an $\omega$-regular objective, and
$A_{1},A_{2}$ be a pair of $\omega$-regular assumptions in $\mathcal{G}$. We
say a tender
$\tau_{i}=\left\langle\alpha_{i},\cdot,\cdot\right\rangle\in\mathcal{T}^{\mathcal{G}}$
fulfills $\Phi_{i}$ under the contract $\left\langle
A_{1},A_{2}\right\rangle$, written $\tau_{i}\models\langle
A_{i}\triangleright\Phi_{i}\triangleright A_{-i}\rangle$, iff

  1. (a)

for every finite path $\rho$, if $\rho$ is in $\mathsf{pref}(A_{i})$, then
$\rho\cdot\alpha_{i}(\rho)\in\mathsf{pref}(A_{1}\cap A_{2})$, and

  2. (b)

for every other compatible tender $\tau_{-i}\in\mathcal{T}^{\mathcal{G}}$, we
have
$\tau_{i}\\!\bowtie\\!\tau_{-i}\models\mathit{Safe}_{\mathcal{G}}(\mathsf{pref}(A_{1}\cap
A_{2}))\implies\left(A_{-i}\land\left(A_{i}\implies\Phi_{i}\right)\right)$.

Here, each tender $\tau_{i}$ only make safety assumption on the other tender
(Cond. (a)), namely that the path does not leave the safe set
$\mathsf{pref}(A_{i})$, and in return, provides full guarantee on $A_{-i}$
(Cond. (b)). Normally, safety assumptions are not enough for fulfilling
liveness guarantees and objectives [5]. But in bidding games, within the safe
set, the players can use a known bidding tactic [9] to accumulate enough
budgets from time to time to reach the liveness goals always eventually. We
use $A_{1},A_{2}$ as $\omega$-regular sets, though we conjecture that safety
assumptions suffice. The assume-guarantee distributed synthesis problem asks
to compute a pair of tenders that fulfill their objectives under the given
contract, as stated below.

###### Problem 3

Define $\mathsf{AG\mathchar 45\relax SYNT}$ as the problem that takes as input
a tuple $\left\langle\mathcal{G},\Phi_{1},\Phi_{2},A_{1},A_{2}\right\rangle$,
where $\mathcal{G}$ is a graph, $\Phi_{1}$ and $\Phi_{2}$ are overlapping
objectives in $\mathcal{G}$, and $A_{1}$ and $A_{2}$ are two $\omega$-regular
languages over $V$ with $v^{0}\in\mathsf{pref}(A_{1}\cap A_{2})$, and the goal
is to decide whether there exists a pair of tenders
$\tau_{1},\tau_{2}\in\mathcal{T}^{\mathcal{G}}$ such that:

  1. (I)

$\tau_{1}$ and $\tau_{2}$ are compatible,

  2. (II)

$\tau_{1}\models\langle A_{1}\triangleright\Phi_{1}\triangleright
A_{2}\rangle$, and

  3. (III)

$\tau_{2}\models\langle A_{2}\triangleright\Phi_{2}\triangleright
A_{1}\rangle$.

When the assumptions allow all behaviors, i.e., $A_{1}=A_{2}=V^{\omega}$, then
$\mathsf{AG\mathchar 45\relax SYNT}$ is equivalent to $\mathsf{STRONG\mathchar
45\relax SYNT}$. On the other hand, when the assumptions allow only each
other’s objectives, i.e., $A_{1}=\Phi_{1}$ and $A_{2}=\Phi_{2}$, then we
obtain a purely cooperative synthesis algorithm. We prove (see App. 0.H) that
satisfaction of the contracts by a pair of tenders will imply satisfaction of
$\Phi_{1}\cap\Phi_{2}$.

######  Proposition 3 ()

Let $\tau_{1}$ and $\tau_{2}$ be tenders that fulfill the requirements stated
in Prob. 3. Then, $\tau_{1}\\!\bowtie\\!\tau_{2}\models\Phi_{1}\cap\Phi_{2}$.

In bidding games literature, it is unknown how to compute strategies for
objectives which can be violated if a given assumption is violated by the
opponent, like in Cond. (a) in Def. 10. The challenge stems from the lack of
separation of the set of available actions to the players, preventing us to
impose assumptions only on the opponent’s behavior. We present a practically
motivated sound, but possibly incomplete, solution for the decentralized
synthesis problem, by using a stronger way of satisfying the contract, namely
by requiring each tender $\tau_{i}$ to use actions so that the generated path
remains in $\mathsf{pref}(A_{1}\cap A_{2})$ all the time. Formally, we say
that the tender $\tau_{i}$ _strongly_ fulfills $\Phi_{i}$ under the contract
$\left\langle A_{1},A_{2}\right\rangle$, written $\tau_{i}\models_{s}\langle
A_{i}\triangleright\Phi_{i}\triangleright A_{-i}\rangle$, if, instead of Cond.
(a) of Def. 10, for every finite path $\rho$, we have
$\rho\cdot\alpha_{i}(\rho)\in\mathsf{pref}(A_{1}\cap A_{2})$, regardless of
whether $\rho\in\mathsf{pref}(A_{i})$ or not, and moreover Cond. (b) of Def.
10 is fulfilled. It is easy to show that $\tau_{i}\models_{s}\langle
A_{i}\triangleright\Phi_{i}\triangleright A_{-i}\rangle$ implies
$\tau_{i}\models\langle A_{i}\triangleright\Phi_{i}\triangleright
A_{-i}\rangle$, so that $\Phi_{1}\cap\Phi_{2}$ will be fulfilled.

Similar to $\mathsf{AA\mathchar 45\relax SYNT}$, we extract a sub-graph
$\mathcal{G}^{\prime}$ of $\mathcal{G}$, called the _largest contract-
satisfying sub-graph_ , whose every path belongs to $\mathsf{pref}(A_{1}\cap
A_{2})$, and vice versa; we omit the construction, which follows usual
automata-theoretic procedure from the literature [4]. For example, in Ex. 3,
the largest contract-satisfying sub-graph of the graph in Fig. 1(c) is the one
that only excludes the vertices $c$ and $f$. It follows that when the tenders
strongly fulfill their objectives under the contracts, it is guaranteed that
every path always remains in $\mathcal{G}^{\prime}$.

######  Theorem 7.1 ()

Let $\mathcal{G}=\left\langle V,v^{0},E\right\rangle$ be a graph, $\Phi_{1}$
and $\Phi_{2}$ be a pair of overlapping $\omega$-regular objectives, and
$A_{1}$ and $A_{2}$ be $\omega$-regular assumptions. Let
$\mathcal{G}^{\prime}$ be the largest contract-satisfying sub-graph of
$\mathcal{G}$. A pair of robust tenders exist if
$\mathit{Th}_{A_{2}\cap\Phi_{1}}^{\mathcal{G}^{\prime}}(v^{0})+\mathit{Th}_{A_{1}\cap\Phi_{2}}^{\mathcal{G}^{\prime}}(v^{0})<1$.
Moreover, $\mathsf{AG\mathchar 45\relax SYNT}$ is in PTIME.

##  8 Conclusion and Future Work

We present the auction-based scheduling framework. Rather than synthesizing a
monolithic policy for a conjunction of objectives $\Phi_{1}\land\Phi_{2}$, we
synthesize two independent tenders for each of the objectives and compose the
tenders at runtime using auction-based scheduling. The key advantage of the
framework is modularity; each tender can be synthesized and modified
independently. We study three instantiations of decentralized synthesis in
planning problems with varying degree of flexibility and practical usability,
and develop algorithms based on bidding games. Interestingly, we show that a
pair of admissible-winning tenders always exists in binary graphs for
reachability objectives and they can be found in PTIME. This positive result
illustrates the strength and potential of the auction-based scheduling
framework.

There are plenty of directions of future research and we list a handful.
First, we consider only qualitative objectives and it is interesting to lift
the results to _quantitative_ objectives, where one can quantify the fairness
achieved by the scheduling mechanism in a fine-grained manner. Moreover, it is
appealing to employ the rich literature on mean-payoff bidding games. Second,
we consider a conjunction of two objectives, and it is interesting to extend
the approach to a conjunction of multiple objectives. This will require
extending the theory of bidding games to the multi-player setting, which have
not yet been studied. Finally, it is particularly interesting to extend the
technique of auction-based scheduling beyond path-planning problems, for
example, it is interesting to consider decentralized synthesis of controllers
that operate in an adversarial or probabilistic environment. Again, the
corresponding bidding games need to be studied (so far only sure winning has
been considered for bidding games played on MDPs [12]).

#### Acknowledgements

This work was supported in part by the ERC project ERC-2020-AdG 101020093 and
by ISF grant no. 1679/21.

## References

  * [1] Adam, B., Amanda, F., Keisler, H.J.: Admissibility in games. In: Econometrica (2008)
  * [2] Aghajohari, M., Avni, G., Henzinger, T.A.: Determinacy in discrete-bidding infinite-duration games. Log. Methods Comput. Sci. 17(1) (2021)
  * [3] de Alfaro, L., Faella, M., Majumdar, R., Raman, V.: Code aware resource management. In: Proceedings of the 5th ACM international conference on Embedded software. pp. 191–202 (2005)
  * [4] Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distributed computing 2, 117–126 (1987)
  * [5] Amla, N., Emerson, E.A., Namjoshi, K., Trefler, R.: Assume-guarantee based compositional reasoning for synchronous timing diagrams. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 465–479. Springer (2001)
  * [6] Anand, A., Nayak, S.P., Schmuck, A.K.: Contract-based distributed synthesis in two-objective parity games. arXiv preprint arXiv:2307.06212 (2023)
  * [7] Avni, G., Bloem, R., Chatterjee, K., Henzinger, T.A., Könighofer, B., Pranger, S.: Run-time optimization for learned controllers through quantitative games. In: Proc. 31st CAV. pp. 630–649 (2019)
  * [8] Avni, G., Henzinger, T.A.: A survey of bidding games on graphs. In: Proc. 31st CONCUR. LIPIcs, vol. 171, pp. 2:1–2:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020)
  * [9] Avni, G., Henzinger, T.A., Chonev, V.: Infinite-duration bidding games. In: Proc. 28th CONCUR. LIPIcs, vol. 85, pp. 21:1–21:18 (2017)
  * [10] Avni, G., Henzinger, T.A., Chonev, V.: Infinite-duration bidding games. J. ACM 66(4), 31:1–31:29 (2019)
  * [11] Avni, G., Henzinger, T.A., Ibsen-Jensen, R.: Infinite-duration poorman-bidding games. In: Proc. 14th WINE. LNCS, vol. 11316, pp. 21–36. Springer (2018)
  * [12] Avni, G., Henzinger, T.A., Ibsen-Jensen, R., Novotný, P.: Bidding games on markov decision processes. In: Proc. 13th RP. pp. 1–12 (2019)
  * [13] Avni, G., Henzinger, T.A., Zikelic, D.: Bidding mechanisms in graph games. J. Comput. Syst. Sci. 119, 133–144 (2021)
  * [14] Avni, G., Ibsen-Jensen, R., Tkadlec, J.: All-pay bidding games on graphs. In: Proc. 34th AAAI. pp. 1798–1805. AAAI Press (2020)
  * [15] Avni, G., Jecker, I., Žikelić, Đ.: Infinite-duration all-pay bidding games. In: Proc. 32nd SODA. pp. 617–636 (2021)
  * [16] Avni, G., Sadhukhan, S.: Computing threshold budgets in discrete-bidding games. In: Proc. 42nd FSTTCS. LIPIcs, vol. 250, pp. 30:1–30:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
  * [17] Bansal, S., De Giacomo, G., Di Stasio, A., Li, Y., Vardi, M.Y., Zhu, S.: Compositional safety ltl synthesis. In: Working Conference on Verified Software: Theories, Tools, and Experiments. pp. 1–19. Springer (2022)
  * [18] Basile, F., Chiacchio, P., Di Marino, E.: An auction-based approach to control automated warehouses using smart vehicles. Control Engineering Practice 90, 285–300 (2019)
  * [19] Basset, N., Kwiatkowska, M., Topcu, U., Wiltsche, C.: Strategy synthesis for stochastic games with multiple long-run objectives. In: Tools and Algorithms for the Construction and Analysis of Systems: 21st International Conference, TACAS 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings 21\. pp. 256–271. Springer (2015)
  * [20] Basset, N., Kwiatkowska, M., Wiltsche, C.: Compositional strategy synthesis for stochastic games with multiple objectives. Information and Computation 261, 536–587 (2018)
  * [21] Berwanger, D.: Admissibility in infinite games. In: Annual Symposium on Theoretical Aspects of Computer Science. pp. 188–199. Springer (2007)
  * [22] Berwanger, D.: Admissibility in infinite games. In: Thomas, W., Weil, P. (eds.) STACS 2007, 24th Annual Symposium on Theoretical Aspects of Computer Science, Aachen, Germany, February 22-24, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4393, pp. 188–199. Springer (2007)
  * [23] Brenguier, R., Raskin, J.F., Sankur, O.: Assume-admissible synthesis. arXiv preprint arXiv:1507.00623 (2015)
  * [24] Brenguier, R., Raskin, J.F., Sassolas, M.: The complexity of admissibility in omega-regular games. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–10 (2014)
  * [25] Chatterjee, K., Piterman, N.: Combinations of qualitative winning for stochastic parity games. arXiv preprint arXiv:1804.03453 (2018)
  * [26] Chong, C.Y., Kumar, S.P.: Sensor networks: evolution, opportunities, and challenges. Proceedings of the IEEE 91(8), 1247–1256 (2003)
  * [27] De Ryck, M., Versteyhe, M., Debrouwere, F.: Automated guided vehicle systems, state-of-the-art control algorithms and techniques. Journal of Manufacturing Systems 54, 152–173 (2020)
  * [28] Develin, M., Payne, S.: Discrete bidding games. The Electronic Journal of Combinatorics 17(1), R85 (2010)
  * [29] Dias, M.B., Zlot, R., Kalra, N., Stentz, A.: Market-based multirobot coordination: A survey and analysis. Proceedings of the IEEE 94(7), 1257–1270 (2006)
  * [30] Farber, D.J., Larson, K.C.: The structure of a distributed computing system–software. In: Proceedings of the Symposium on Computer-communications Networks and Teletraffic. pp. 539–545 (1972)
  * [31] Filiot, E., Jin, N., Raskin, J.F.: Compositional algorithms for ltl synthesis. In: International Symposium on Automated Technology for Verification and Analysis. pp. 112–127. Springer (2010)
  * [32] Finkbeiner, B., Passing, N.: Compositional synthesis of modular systems. Innovations in Systems and Software Engineering 18(3), 455–469 (2022)
  * [33] Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: 20th Annual IEEE Symposium on Logic in Computer Science (LICS’05). pp. 321–330. IEEE (2005)
  * [34] Hahn, E.M., Perez, M., Schewe, S., Somenzi, F., Trivedi, A., Wojtczak, D.: Multi-objective omega-regular reinforcement learning. Formal Aspects of Computing (2023)
  * [35] Houli, D., Zhiheng, L., Yi, Z.: Multiobjective reinforcement learning for traffic signal control using vehicular ad hoc network. EURASIP journal on advances in signal processing 2010, 1–7 (2010)
  * [36] Könighofer, B., Alshiekh, M., Bloem, R., Humphrey, L., Könighofer, R., Topcu, U., Wang, C.: Shield synthesis. Formal Methods in System Design 51(2), 332–361 (2017)
  * [37] Kupermann, O., Varfi, M.: Synthesizing distributed systems. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science. pp. 389–398. IEEE (2001)
  * [38] Lazarus, A.J., Loeb, D.E., Propp, J.G., Stromquist, W.R., Ullman, D.H.: Combinatorial games under auction play. Games and Economic Behavior 27(2), 229–264 (1999)
  * [39] Lazarus, A.J., Loeb, D.E., Propp, J.G., Ullman, D.: Richman games. Games of No Chance 29, 439–449 (1996)
  * [40] Majumdar, R., Mallik, K., Schmuck, A.K., Zufferey, D.: Assume–guarantee distributed synthesis. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 39(11), 3215–3226 (2020)
  * [41] Meir, R., Kalai, G., Tennenholtz, M.: Bidding games and efficient allocations. Games and Economic Behavior 112, 166–193 (2018)
  * [42] Ouelhadj, D., Petrovic, S.: A survey of dynamic scheduling in manufacturing systems. Journal of scheduling 12, 417–431 (2009)
  * [43] Pneuli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: Proceedings [1990] 31st Annual Symposium on Foundations of Computer Science. pp. 746–757. IEEE (1990)
  * [44] Roijers, D.M., Vamplew, P., Whiteson, S., Dazeley, R.: A survey of multi-objective sequential decision-making. Journal of Artificial Intelligence Research 48, 67–113 (2013)
  * [45] Smith, R.G.: The contract net protocol: High-level communication and control in a distributed problem solver. IEEE Transactions on computers 29(12), 1104–1113 (1980)

##  Appendix 0.A Proof Sketch of Thm. 4.1

See 4.1 Fix a bidding game $\left\langle\mathcal{G},\Phi\right\rangle$ with
the reachability objective
$\Phi=\mathit{Reach}_{\mathcal{G}}(\left\\{t\right\\})$ for the single target
$t\in V$. If the game starts at $t$, since the objective is already
fulfilled—irrespective of the budget, hence
$\mathit{Th}_{\Phi}^{\mathcal{G}}(t)=0$. For every other vertex $v$, it is
known that the threshold can be represented as:

$\displaystyle\mathit{Th}_{\Phi}^{\mathcal{G}}(v)=\frac{1}{2}\left(\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{+})+\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{-})\right),$
(1)

where $v^{+}$ and $v^{-}$ represent the successors of $v$ with the largest and
the smallest thresholds, respectively. Then if the initial configuration is
$\left\langle v,B\right\rangle=\left\langle
v,\mathit{Th}_{\Phi}^{\mathcal{G}}+\epsilon\right\rangle$, for any given
$\epsilon>0$, $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ can bid
$\beta(v)=\nicefrac{{1}}{{2}}(\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{+})-\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{-}))$
and go to $\alpha(v)=v^{-}$ upon winning. If he wins and moves the token to
$v^{-}$, then his new budget will be
$B-\beta(v)=\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{-})+\epsilon$. If he loses and
$\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$ moves the token to a
successor $v^{\prime}$, then we know that
$\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$ must have bid higher than
$\beta(v)$ which $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ will
receive, so that $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$’s new budget
will be at least
$B+\beta(v)=\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{+})+\epsilon$, larger than
$\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{\prime})+\epsilon$ by definition of
$v^{+}$. This way, the strategy $\left\langle\alpha,\beta\right\rangle$ can
ensure that for every vertex $v^{\prime}$ where the token may reach from $v$
in one step, the invariant $B>\mathit{Th}_{\Phi}^{\mathcal{G}}(v^{\prime})$ is
maintained, so that $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ can win
from $v^{\prime}$, which can be repeated and eventually
$\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ will reach $t$. This strategy
works on DAGs. For graphs with cycles, a little extra work on the bidding
policy is needed to get out of cycles and move towards the target [38].

##  Appendix 0.B Proof of Thm. 5.1

See 5.1

###### Proof

First, assume that
$\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{0})+\mathit{Th}_{\Phi_{2}}^{\mathcal{G}}(v^{0})<1$.
For $i\in\left\\{1,2\right\\}$, let $\langle\alpha_{i},\beta_{i}\rangle$
denote a winning $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ strategy in
the bidding game $\langle\mathcal{G},\Phi_{i}\rangle$ from every configuration
$\langle v^{0},B\rangle$ with $B>\mathit{Th}_{\Phi_{i}}^{\mathcal{G}}(v^{0})$.
We argue that the render
$\tau_{1}=\langle\alpha_{1},\beta_{1},\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{0})\rangle$
is robust for $\Phi_{1}$, and the proof for $\tau_{2}$ is dual. Indeed, for
any compatible tender
$\tau^{\prime}_{2}=\langle\alpha^{\prime}_{2},\beta^{\prime}_{2},\mathbb{B}^{\prime}_{2}\rangle$,
the pair $\langle\alpha^{\prime}_{2},\beta^{\prime}_{2}\rangle$ corresponds to
a $\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$ strategy in the bidding
game $\langle\mathcal{G},\Phi_{1}\rangle$. The resulting play coincides with
$out(\tau_{1}\\!\bowtie\\!\tau^{\prime}_{2})(\langle v^{0},B\rangle)$ and
satisfies $\Phi_{1}$ since the strategy $\langle\alpha_{1},\beta_{1}\rangle$
is winning.

Second, suppose that
$\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{0})+\mathit{Th}_{\Phi_{2}}^{\mathcal{G}}(v^{0})\geq
1$. For any allocation $\mathbb{B}_{1}+\mathbb{B}_{2}<1$, there is an
$i\in\left\\{1,2\right\\}$ such that
$\mathbb{B}_{i}\leq\mathit{Th}_{\Phi_{i}}^{\mathcal{G}}(v^{0})$. Assume WLog
that $\mathbb{B}_{1}\leq\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{0})$. Consider
a winning $\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$ strategy
$\langle\alpha_{2},\beta_{2}\rangle$ in the bidding game
$\langle\mathcal{G},\Phi_{1}\rangle$ from $\langle
v^{0},\mathbb{B}_{1}\rangle$. The tender
$\tau^{\prime}_{2}=\langle\alpha_{2},\beta_{2},1-\mathbb{B}_{1}\rangle$ is
compatible and $out(\tau_{1}\\!\bowtie\\!\tau^{\prime}_{2}(\langle
v^{0},\mathbb{B}_{1}\rangle))$ violates $\Phi_{1}$.

Finally, in order to obtain the complexity bounds, we guess memoryless action
policies in both games, which are known to exist [38], and verify that they
are optimal. Based on the guess, we devise a linear program to compute the
thresholds. Finally, we verify that the sum of thresholds in $v^{0}$ is less
than $1$. For binary graphs, there is no need to guess the action policy in
order to find thresholds (Thm. 4.1). ∎

##  Appendix 0.C Reduction from Non-sink Targets to Sink Targets

Since a pair of reachability objectives with non-sink targets can be turned
into a pair of reachability objectives $\Phi_{1}^{\prime},\Phi_{2}^{\prime}$
with sink targets $T_{1}^{\prime},T_{2}^{\prime}$ on a larger graph
$\mathcal{G}^{\prime}$. The graph $\mathcal{G}^{\prime}$ contains three copies
of $\mathcal{G}$, call them $\mathcal{G}_{\bot}$, $\mathcal{G}_{1}$, and
$\mathcal{G}_{2}$, which memorize which objective has been fulfilled so far,
if any. Initially the token is placed on $v^{0}$ of $\mathcal{G}_{\bot}$, and
as soon as either $T_{1}$ or $T_{2}$ is visited, the token is moved to the
respective vertex in $G_{1}$ or $G_{2}$, respectively. In each
$\mathcal{G}_{i}$, every sink vertex belongs to $T_{i}^{\prime}$. Furthermore,
if there exists a $t\in T_{i}$, then the copy of $t$ in $G_{-i}^{\prime}$
belongs to $T_{i}^{\prime}$. It can be shown that a path in $\mathcal{G}$
fulfills $\Phi_{1}\cap\Phi_{2}$ iff the corresponding path in
$\mathcal{G}^{\prime}$ fulfills $\Phi_{1}^{\prime}\cap\Phi_{2}^{\prime}$.

##  Appendix 0.D Proof of Lem. 1

See 1 We argue that choosing $w$ from $u$ is dominated by the action of
choosing $v$ from $u$, no matter what the budget at $u$ is. Firstly, Cond. (a)
of Def. 6 trivially holds. Secondly, consider the other tender $\tau_{-i}$
which bids zero at $u$, and later cooperates with $\tau_{i}$ to satisfy
$\Phi_{i}$. Clearly, the $\tau_{i}$’s action policy that selects $v$ at $u$
will be able to satisfy $\Phi_{i}$, but the one that selects $w$ will not.

##  Appendix 0.E Proof of Lem. 2

See 2

###### Proof

Let
$\mathcal{G},\widehat{\mathcal{G}},\Phi_{1}=\mathit{Reach}_{\widehat{\mathcal{G}}}(T_{1}),\Phi_{2}=\mathit{Reach}_{\widehat{\mathcal{G}}}(T_{2})$
are as in the statement of the lemma. By the definition of thresholds, we know
that
$\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v)=1-\mathit{Th}_{\Phi_{1}^{c}}^{\widehat{\mathcal{G}}}(v)$.
Since every target vertex in $T_{1}$ and $T_{2}$ is a sink vertex, and since
we removed every vertex $v$ with
$\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v)=\mathit{Th}_{\Phi_{2}}^{\mathcal{G}}(v)=1$
in $\widehat{\mathcal{G}}$, hence we know that $\widehat{\mathcal{G}}$ does
not have any sink vertex that is outside of $T_{1}\cup T_{2}$, as all such
vertices have threshold $1$ for both objectives and got removed. Moreover,
because $T_{1}\cap T_{2}\neq\emptyset$, hence $T2\subseteq T_{1}^{c}$,
implying $\Phi_{2}\subseteq\Phi_{1}^{c}$. It can be shown, by inductively
applying the threshold operator from Eq. (1) starting at the sink vertices and
reaching up to the root vertices, that
$\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v)\leq\mathit{Th}_{\Phi_{1}^{c}}^{\widehat{\mathcal{G}}}(v)$.
Therefore, we have $\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v)\leq
1-\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v)$, implying the claim.

We proceed to show that when $\mathcal{G}$ is a binary graph, we have
$\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}_{\Phi_{1},\Phi_{2}}}(v)+\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}_{\Phi_{1},\Phi_{2}}}(v)<1$.
The proof is via induction over the length of the shortest path from $v$ to
any vertex in $T_{1}\cap T_{2}$, which is unique and bounded (by the number of
vertices) for every $v$ and henceforth called the _distance_ between $v$ and
$T_{1}\cap T_{2}$. The base case is when the distance is $0$, i.e., for every
vertex $v$ in $T_{1}\cap T_{2}$, for which we immediately obtain
$\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v)+\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v)=0+0<1$.
Now suppose for every vertex $v$ with distance $d$, the claim holds. For every
vertex $v$ with distance $d+1$, we know that $v$ has a successor $v^{\prime}$
whose distance is $d$, so that
$\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v^{\prime})+\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v^{\prime})<1$.
Let $v^{\prime\prime}$ be the other successor of $v$ with any arbitrary
distance. Using the characterization of thresholds from (1), and observing
that for two successors, the distinction between $v^{-}$ and $v^{+}$ is
immaterial:

$\displaystyle\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v)+\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v)$
$\displaystyle=\frac{1}{2}\left(\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v^{\prime})+\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v^{\prime\prime})\right)+\frac{1}{2}\left(\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v^{\prime})+\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v^{\prime\prime})\right)$
$\displaystyle=\frac{1}{2}\underbrace{\left(\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v^{\prime})+\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v^{\prime})\right)}_{<1\text{
(induction
hypothesis)}}+\frac{1}{2}\underbrace{\left(\mathit{Th}_{\Phi_{1}}^{\widehat{\mathcal{G}}}(v^{\prime\prime})+\mathit{Th}_{\Phi_{2}}^{\widehat{\mathcal{G}}}(v^{\prime\prime})\right)}_{\leq
1\text{ (Lem.\leavevmode\nobreak\ \ref{lem:aa:reach:sum of thresholds leq
1})}}$ $\displaystyle<\frac{1}{2}\cdot 1+\frac{1}{2}\cdot 1$
$\displaystyle=1.$

∎

##  Appendix 0.F Proof of Lem. 3

See 3

###### Proof

We prove it for $i=1$, the other case is dual. Suppose
$\tau_{1}=\left\langle\alpha,\beta,\mathbb{B}\right\rangle$ is a tender that
follows a $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$ winning strategy in
the game $\langle\widehat{\mathcal{G}},\Phi_{1}\rangle$. Suppose towards
contradiction that $\tau_{1}$ is dominated by a tender
$\tau_{1}^{\prime}=\left\langle\alpha^{\prime},\beta^{\prime},\mathbb{B}\right\rangle$.
That is, there is a tender
$\tau_{2}=\left\langle\alpha_{2},\beta_{2},\mathbb{B}_{2}\right\rangle$ that
is compatible with both such that
$\tau_{1}\\!\bowtie\\!\tau_{2}\not\models\Phi_{1}$ but
$\tau_{1}^{\prime}\\!\bowtie\\!\tau_{2}\models\Phi_{1}$. We will reach a
contradiction by constructing another compatible tender
$\tau_{2}^{\prime}=\left\langle\alpha_{2}^{\prime},\beta_{2}^{\prime},\mathbb{B}_{2}\right\rangle$
that achieves the opposite, namely
$\tau_{1}\\!\bowtie\\!\tau_{2}^{\prime}\models\Phi_{1}$ but
$\tau_{1}\\!\bowtie\\!\tau_{2}^{\prime}\not\models\Phi_{1}$.

We construct $\tau_{2}^{\prime}$ as follows. Let $h$ be the longest common
prefix of $\tau_{1}\\!\bowtie\\!\tau_{2}$ and
$\tau_{1}^{\prime}\\!\bowtie\\!\tau_{2}$, and the last configuration of $h$ is
$\langle v,B_{v}\rangle$. Denote the actions of $\tau_{1}$ and
$\tau_{1}^{\prime}$ following $h$ respectively by $\langle b_{1},u_{1}\rangle$
and $\langle b_{1}^{\prime},u_{1}^{\prime}\rangle$. Note that these differ
since $h$ is the longest common prefix. We construct $\tau^{\prime}_{2}$ to
follow the same actions and bids as $\tau_{2}$ so that the prefix $h$ is
generated. Let $\langle u_{1},B_{1}\rangle=\tau_{1}\\!\bowtie\\!\tau_{2}(h)$
and $\langle
u_{1}^{\prime},B_{1}^{\prime}\rangle=\tau^{\prime}_{1}\\!\bowtie\\!\tau_{2}(h)$.
Since $h$ is maximal, $\langle u,B_{1}\rangle\neq\langle
u^{\prime},B_{1}^{\prime}\rangle$. We show that both budgets are below the
adversarial threshold, i.e., $\mathit{Th}_{\mathcal{G}}^{\Phi_{1}}(u)>B_{1}$
and $\mathit{Th}_{\mathcal{G}}^{\Phi_{1}}(u^{\prime})>B_{1}^{\prime}$. This
means that we can set $\tau^{\prime}_{2}$ to follow a winning
$\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$ strategy in the game
$\langle\mathcal{G},\Phi_{1}\rangle$ from $\langle
u_{1}^{\prime},B_{1}^{\prime}\rangle$ to violate $\Phi_{1}$. On the other
hand, we set $\tau^{\prime}_{2}$ to follow some
$\mathit{\mathit{Player}\leavevmode\nobreak\ Y}$ strategy in
$\widehat{\mathcal{G}}$ from $\langle u_{1},B_{1}\rangle$, and since
$\tau_{1}$ is winning in $\widehat{\mathcal{G}}$, the objective $\Phi_{1}$ is
satisfied. Let $\langle b_{2},u_{2}\rangle$ denote the action of $\tau_{2}$
following $h$. Note that it cannot be case that $b_{2}>b_{1},b^{\prime}_{1}$
since otherwise,
$\tau_{1}\\!\bowtie\\!\tau_{2}(h)=\tau^{\prime}_{1}\\!\bowtie\\!\tau_{2}(h)$.
We show the claim separately for each of the four remaining orders of
$b_{1},b^{\prime}_{1}$, and $b_{2}$.

  1. (i)

$b_{1}<b_{2}<b_{1}^{\prime}$. $\tau_{2}^{\prime}$ bids $b_{2}$ as well, and
choose whatever $\tau_{2}$ does. Therefore, $\tau_{2}^{\prime}$, after losing
the bid at $v$, can simulate an adversarial strategy for $\Phi_{1}$, and does
so (just like $\tau_{2}$ does against $\tau_{1}$). This makes
$\tau_{1}^{\prime}\\!\bowtie\\!\tau_{2}^{\prime}\not\models\Phi_{1}$. On the
other hand, upon winning the bid at $v$, $\tau_{2}^{\prime}$, and remain
within the longest admissible sub-graph $\widehat{\mathcal{G}}$ of
$\mathcal{G}$. In the latter case, $\tau_{1}$ is a winning strategy, therefore
$\tau_{1}\\!\bowtie\\!\tau_{2}^{\prime}\models\Phi_{1}$.

  2. (ii)

$b_{1}^{\prime}<b_{2}<b_{1}$. Again, $\tau_{2}^{\prime}$ bids $b_{2}$ as well,
but upon winning the bid at $v$, $\alpha_{2}^{\prime}$ chooses $v^{+}$.
Because $B_{v}<\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v)$, and $b_{1}$ is an
optimal bid, when $\tau_{1}^{\prime}$ loses the bid again $\tau_{2}^{\prime}$,
its budget becomes
$B_{v}+b_{2}<\frac{\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{+})+\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{-})}{2}+\frac{\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{+})-\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{-})}{2}=\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{+})$.
Therefore, from $v^{+}$, $\tau_{2}^{\prime}$ can simulate an adversarial
strategy for $\Phi_{1}$, and does so, making
$\tau_{1}^{\prime}\\!\bowtie\\!\tau_{2}^{\prime}\not\models\Phi_{1}$. On the
other hand, after losing the bidding at $v$ against $\tau_{1}$, from $u$
onwards, $\tau_{2}^{\prime}$ only chooses edges within
$\widehat{\mathcal{G}}$. Again, as $\tau_{1}$ wins against any tender within
$\widehat{\mathcal{G}}$, we have
$\tau_{1}\\!\bowtie\\!\tau_{2}^{\prime}\models\Phi_{1}$.

  3. (iii)

$b_{2}<b_{1}<b_{1}^{\prime}$. Here, again $\tau_{2}^{\prime}$ simulates
$\tau_{2}$ up to $v$, and loses the current bid against both $\tau_{1}$ and
$\tau_{1}^{\prime}$. But $t_{1}^{\prime}$ remains in a better position (budget
wise) than in $\tau_{1}$. Against $\tau_{1}^{\prime}$, $\tau_{2}$ does what
$\tau_{2}$’s choices against $\tau_{1}$. This is well defined, because
$\tau_{2}^{\prime}$ in a better position (budget-wise) $\tau_{2}$ to do that,
and as a result
$\tau_{1}^{\prime}\\!\bowtie\\!\tau_{2}^{\prime}\not\models\Phi_{1}$. On the
other hand, against $\tau_{1}$, $\tau_{2}^{\prime}$ only chooses edges within
$\widehat{\mathcal{G}}$ from $u$, making
$\tau_{1}\\!\bowtie\\!\tau_{2}^{\prime}\models\Phi_{1}$.

  4. (iv)

$b_{2}<b_{1}^{\prime}<b_{1}$. If $\tau_{2}^{\prime}$ has a budget such that it
can bid some $b_{2}^{\prime}$ satisfying
$b_{1}^{\prime}<b_{2}^{\prime}<b_{1}$, $\beta_{2}^{\prime}$ does that,
thereafter $\tau_{2}^{\prime}$ follows as it does in case (ii). Otherwise,
$\tau_{2}^{\prime}$’s (and $\tau_{2}$) budget at
$v,B_{2}=1-B_{v}<b_{1}^{\prime}<b_{1}$. Now, $\tau_{1}$ is by construction an
optimal tender for $\Phi_{1}$. The optimal bid $b_{1}$ is strictly more than
$\tau_{1}$’s budget means
$\mathit{Th}_{\Phi_{1}}^{\mathcal{G}^{\prime}}(v)=1$, as then only it becomes
urgent to win the current bid for $\tau_{1}$. Therefore, we have
$\mathit{Th}_{\Phi_{1}}^{\mathcal{G}^{\prime}}(v)=(1+\mathit{Th}_{\Phi_{1}}^{\mathcal{G}^{\prime}}(v^{-}))/2\implies\mathit{Th}_{\Phi_{1}}^{\mathcal{G}^{\prime}}(v^{-})=\mathit{Th}_{\Phi_{1}}^{\mathcal{G}^{\prime}}(v)-(1-\mathit{Th}_{\Phi_{1}}^{\mathcal{G}^{\prime}}(v))$.
We already assumed, $B_{v}<\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v)$.
Therefore,

$\displaystyle B_{v}-b_{1}^{\prime}$
$\displaystyle<\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v)-(1-B_{v})$
$\displaystyle<\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v)-(1-\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v))$
$\displaystyle=\mathit{Th}_{\Phi_{1}}^{\mathcal{G}}(v^{-})$

Therefore, even when $\tau_{2}^{\prime}$ does not have enough budget to bid
between $b_{1}$ and $b_{1}^{\prime}$, upon losing the bid at $v$,
$\tau_{2}^{\prime}$ can choose to play an adversarial strategy from $v^{-}$
against $\tau_{1}^{\prime}$ has budget $B_{1}^{\prime}=B_{v}-b_{1}^{\prime}$,
and choose to play edges only within $\mathcal{G}^{\prime}$ against $t_{1}$
when it has a budget $B_{1}=B_{v}-b_{1}$. Thus,
$\tau_{1}\\!\bowtie\\!\tau_{2}^{\prime}\models\Phi_{1}$, but
$\tau_{1}^{\prime}\\!\bowtie\\!\tau_{2}^{\prime}\not\models\Phi_{1}$.

Now, in Lem. 1, we showed that the no admissible tender (for either
specifications) takes the edges that we remove from $\mathcal{G}$ in order to
construct $\widehat{\mathcal{G}}$, i.e, any $\Phi_{i}$-admissible tenders can
only constitute of edges remaining in $\mathcal{G}^{\prime}$ for both $i$. As
a robust tender $\tau_{i}$ for $\Phi_{i}$ from $\widehat{\mathcal{G}}$, when
composed with any tenders constituted only by edges present in
$\widehat{\mathcal{G}}$, satisfies $\Phi_{i}$, we can say that it does so when
it is composed with an $\Phi_{2}$-admissible tenders (which is a subset of
tenders present in $\widehat{\mathcal{G}}$). ∎

##  Appendix 0.G Proof of Thm. 6.2

See 6.2

###### Proof

Let us suppose $\Phi_{i}=\mathit{B\ddot{u}chi}(\mathcal{B}_{i})$ for
$i=\\{1,2\\}$. We consider $\mathcal{G}^{\prime}$ that is obtained from
$\widehat{\mathcal{G}}_{\mathcal{B}}$ after replacing every BSCC $D$ with sink
$d$, as explained before. From Thm. 6.1, $\langle
G^{\prime},T_{1},T_{2}\rangle$ is in $\mathsf{AA\mathchar 45\relax SYNT}$.
Therefore, we get a pair of tenders
$\tau_{1}^{\prime}=\langle\alpha_{1}^{\prime},\beta_{1}^{\prime},\mathbb{B}_{1}\rangle$
and
$\tau_{2}^{\prime}=\langle\alpha_{2}^{\prime},\beta_{2}^{\prime},\mathbb{B}_{2}\rangle$
as certificates, and by design they are compatible. We now construct tenders
$\tau_{1}=\langle\alpha_{1},\beta_{1},\mathbb{B}_{1}\rangle$ and
$\tau_{2}=\langle\alpha_{1},\beta_{2},\mathbb{B}_{2}\rangle$, such that
$\alpha_{i}$ follows $\alpha_{i}^{\prime}$, and $\beta_{i}^{\prime}$ follows
$\beta_{i}^{\prime}$ before reaching any BSCCs. Because
$\tau_{1}^{\prime}\\!\bowtie\\!\tau_{2}^{\prime}\models T_{1}\cap T_{2}$,
$\tau_{1}\\!\bowtie\\!\tau_{2}$ reach a BSCC $\mathcal{S}$ such that
$\mathcal{S}\cap B_{i}\neq\emptyset$ for $i=\\{1,2\\}$. Within $\mathcal{S}$,
we let $\tau_{i}$ follow $\mathit{\mathit{Player}\leavevmode\nobreak\ X}$
winning strategy for the bidding game
$\mathcal{S},\mathit{B\ddot{u}chi}(\mathcal{B}_{i})$, which exists because the
threshold budget for Büchi objective is 0. Thus,
$\tau_{1}\\!\bowtie\\!\tau_{2}\models\Phi_{1}\cap\Phi_{2}$. ∎

##  Appendix 0.H Proof of Prop. 3

In the following, for a given language $L\in V^{\omega}$, we write
$\mathit{Safe}_{\mathcal{G}}(\mathsf{pref}(L))$ to denote the set of infinite
paths which can always be extended to $L$, i.e.,
$\left\\{v^{0}v^{1}\ldots\in\mathit{Paths}^{\mathsf{inf}}(\mathcal{G})\mid\forall
i\geq 0\;.\;v^{0}\ldots v^{i}\in\mathsf{pref}(L)\right\\}$.

See 3

###### Proof

We claim that both assumptions $A_{1},A_{2}$ will be fulfilled, from which
Cond. (b) of Def. 10 will imply satisfaction of both $\Phi_{1}$ and $\Phi_{2}$
by $\tau_{1}$ and $\tau_{2}$, respectively. Let $A=A_{1}\cap A_{2}$, and $A$
can be decomposed into safety and liveness components as
$A=\mathit{Safe}_{\mathcal{G}}(\mathsf{pref}(A))\cap\left(\mathit{Safe}_{\mathcal{G}}(\mathsf{pref}(A))\implies
A\right)$. We prove the claim on the two components separately. Firstly, the
fact that $\tau_{1}\\!\bowtie\\!\tau_{2}$ implements $\mathsf{pref}(A)$ on
$\mathcal{G}$ can be proven by induction over the length of the generated
path: The base case is given by the assumption
$v^{0}\in\mathsf{pref}(A_{1}\cap A_{2})$, and for every finite path $\rho$, if
$\tau_{i}$ wins the bidding and if $\rho\in\mathsf{pref}(A_{1}\cap
A_{2})\subset\mathsf{pref}(A_{i})$ then $\tau_{i}$ needs to ensure that the
next vertex $v^{\prime}$ satisfies $\rho v^{\prime}\in\mathsf{pref}(A_{i}\cap
A_{-i})$ (consequence of Cond. II-III of Prob. 3 and Cond. (a) of Def. 10),
thereby implying that the path will always remain inside
$\mathsf{pref}(A_{1}\cap A_{2})$, proving the safety part.

For the liveness part of the claim, we use known results from Richman bidding
games, which guarantees that in an infinite horizon game, with any arbitrary
positive initial budget, players can accumulate sufficient budget from time to
time and can always eventually visit any vertex that can be reached [38]. This
implies that if the invariance
$\mathit{Safe}_{\mathcal{G}}(\mathsf{pref}(A_{1}\cap A_{2}))$ holds, then each
tender $\tau_{i}$ can actually fulfill $A_{-i}$ (they are required to do so by
Cond. (b) of Def. 10) when composed with any compatible tender in the long
run. Therefore, $A_{1}\cap A_{2}$ will be fulfilled. ∎

##  Appendix 0.I Proof of Thm. 7.1

See 7.1

###### Proof

Let $\mathcal{G},\Phi_{1},\Phi_{2},A_{1}$, and $A_{2}$ are as in the theorem
statement. We construct a new graph $\mathcal{G}^{\prime}$, which is a sub-
graph of $\mathcal{G}$, whose every path belongs to $\mathsf{pref}(A_{1}\cap
A_{2})$ in $\mathcal{G}$, and vice versa; the construction follows usual
automata-theoretic procedure from the literature [4]. We assume that tenders
strongly fulfill their objectives under the contracts, which guarantees that
every path will remain inside $\mathcal{G}^{\prime}$ all the time.

We now solve the strong decentralized synthesis problems on
$\mathcal{G}^{\prime}$ with objectives $\Phi_{1}^{\prime}=A_{2}\cap\Phi_{1}$
and $\Phi_{2}^{\prime}=A_{1}\cap\Phi_{2}$, and if
$\left\langle\mathcal{G}^{\prime},\Phi_{1}^{\prime},\Phi_{2}^{\prime}\right\rangle\in\mathsf{STRONG\mathchar
45\relax SYNT}$, we claim that
$\left\langle\mathcal{G}^{\prime},\Phi_{1},\Phi_{2},A_{1},A_{2}\right\rangle\in\mathsf{AG\mathchar
45\relax SYNT}$, and the certificates $\tau_{1},\tau_{2}$ of
$\mathsf{STRONG\mathchar 45\relax SYNT}$ are also certificates of
$\mathsf{AG\mathchar 45\relax SYNT}$. The claim follows by observing that the
tenders are compatible, and moreover each tender $\tau_{i}$ always maintains
that the path remains inside $\mathsf{pref}(A_{1}\cap A_{2})$ (i.e.,
$\mathcal{G}^{\prime}$), and moreover it fulfills $\Phi_{i}^{\prime}$, thereby
satisfying $\tau_{i}\models_{s}\langle
A_{i}\triangleright\Phi_{i}\triangleright A_{-i}\rangle$, which implies the
satisfaction of $\tau_{i}\models\langle
A_{i}\triangleright\Phi_{i}\triangleright A_{-i}\rangle$. ∎