Auction-Based Scheduling

TL;DR

The paper addresses the challenge of satisfying multiple, potentially conflicting objectives in sequential decision tasks by introducing auction-based scheduling as a modular framework. It assigns each objective its own policy and a bounded budget, and uses runtime bidding to decide which policy selects the next action, ensuring joint satisfaction $\Phi_1\cap\Phi_2$ when tenders are compatible via $\mathbb{B}_1+\mathbb{B}_2<1$. The authors formalize tenders as triples $\langle \alpha,\beta,\mathbb{B}\rangle$, define their composition $\bowtie$, and study three decentralized synthesis classes—Strong, Assume-admissible, and Assume-guarantee—providing PTIME results for binary graphs and NP$\cap$coNP results in general. They show that for path-planning problems with two $\omega$-regular objectives, admissible-winning tenders exist in PTIME on binary graphs for reachability, while AA-SYNT may fail for Büchi objectives, highlighting nuanced differences between objective types. Overall, the framework enables modular, scalable synthesis with independent policy development and runtime composition, offering a principled approach to multi-objective planning with provable guarantees.

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.

Figures (1)

• 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 are 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.

Theorems & Definitions (3)

• definition thmcounterdefinition: Bidding policies
• definition thmcounterdefinition: Tenders
• definition thmcounterdefinition: Composition of tenders