Technical Summary: Decoupled Planning for Multiple Omega-Regular Objectives

Problem Statement

The paper addresses the problem of generating paths on a finite directed graph that satisfy a collection of $\omega$-regular objectives ($\phi_1, \dots, \phi_N$). Traditional approaches solve this by computing a single, monolithic policy for the conjunction of all objectives. This work proposes a decoupled framework where $N$ independent agents are assigned to individual objectives. Each agent $i$ selects a local policy $\pi_i$ to satisfy $\phi_i$ without knowledge of the other agents' objectives or policies. A scheduler $\sigma$, which is oblivious to the graph structure and the specific objectives, dynamically composes these policies by selecting which agent determines the next vertex at each time step.

The core challenge is to determine under what conditions a composition of independent local policies, guided by a scheduler, almost-surely satisfies the conjunction of all objectives ($\bigwedge \phi_i$), assuming such a path exists. The framework aims to achieve maximal modularity (agents design policies independently) while ensuring correctness.

Methodology

The Decoupled Framework

The system consists of:

1. Agents: $N$ agents, each responsible for one objective $\phi_i$.
2. Policies: Agents select policies from specific classes based on their knowledge of the scheduling process:
   • Path-aware: Traditional policies depending only on the path history.
   • Scheduled-aware: Policies knowing whether they were scheduled at previous steps.
   • Full history-aware: Policies knowing exactly which agent was scheduled at each previous step.
3. Scheduler: A stochastic scheduler $\sigma$ that selects an agent at each step. The paper argues that deterministic schedulers (even extremely fair ones) are insufficient for universal composition, necessitating stochastic schedulers with probabilistic fairness properties.

Decomposition of Objectives

The authors decompose $\omega$-regular objectives into safety and liveness components ($\phi = \phi_{safe} \cap \phi_{live}$).

• Safety: Requires avoiding unsafe states. The paper demonstrates that safety cannot be guaranteed under stochastic scheduling without communication. They introduce a shielded composition protocol where agents exchange sets of safe actions (maximally permissive policies) at each step. The scheduled agent must choose an action from the intersection of all agents' safe sets. Under the assumption of mutual safety-closure (every prefix of a path satisfying individual safety constraints can be extended to satisfy all), this protocol ensures safety.
• Liveness: Requires visiting good states infinitely often or eventually. Once safety is enforced (restricting the graph to the safe subgraph), the focus shifts to satisfying liveness objectives.

Conventions

Since uncoordinated policies can fail even for simple objectives (e.g., Büchi objectives in strongly connected graphs), the paper introduces conventions. A convention is a mapping from objective classes to restrictions on policy types (e.g., memory bounds, scheduling awareness) agreed upon a priori, before the specific graph or objectives are revealed. If all agents adhere to the convention, the composition is guaranteed to satisfy all objectives almost surely.

Key Contributions and Results

1. Impossibility of Universal Deterministic and Uncoordinated Stochastic Schedulers

• Deterministic Schedulers: The paper proves that no deterministic scheduler is universal. Even with extreme fairness (each agent scheduled infinitely often), there exist graphs and policies where the composition fails to satisfy the objectives (Example 1, Theorem 1).
• Uncoordinated Stochastic Schedulers: For Büchi objectives, even stochastic schedulers fail if agents use arbitrary policies. The authors construct a scenario where agents use policies with exponentially increasing "waiting times" (Example 2, Theorem 3). A stochastic scheduler cannot overcome the probability that agents miss each other's critical windows, leading to a failure to satisfy the conjunction almost surely. This extends to reachability objectives (Corollary 1).

2. Safety via Shielded Composition

The paper establishes that safety requires communication. They propose a protocol where agents broadcast their sets of safe successors. The scheduled agent selects an action from the intersection of these sets. Theorem 2 proves that if the objectives are mutually safety-closed, this shielded composition ensures the safety component is satisfied almost surely, reducing the problem to liveness on a safe subgraph.

3. Conventions for Liveness Objectives

The paper characterizes minimally restrictive conventions for major subclasses of $\omega$-regular objectives:

• Büchi Objectives:

  • Convention: Agents use finite-memory policies (specifically, policies with uniformly bounded expected hitting times for the target set).
  • Result: Theorem 4 shows that if all agents use such policies, a stochastic scheduler composes them to satisfy all Büchi objectives almost surely. No runtime coordination or knowledge of other agents is required.

• Co-Büchi Objectives:

  • Challenge: Simple finite-memory policies are insufficient (Theorem 5). Agents must eventually converge to a common cycle.
  • Convention: Agents use scheduled-aware policies that maintain a "guess" of a lasso-shaped path (a path to a good cycle).
  • Mechanism: If an agent is not scheduled and observes a transition conflicting with its current guess, it discards the guess and samples a new lasso path.
  • Result: Theorem 6 proves that this protocol leads to a consensus on a common lasso path almost surely, satisfying all co-Büchi objectives.

• Parity Objectives:

  • Challenge: Parity objectives are more complex; a single simple cycle may not suffice (Lemma 1).
  • Convention: Agents use full history-aware policies. Each agent maintains a tuple of internal memoryless policies, guessing the policy of every other agent (including itself).
  • Mechanism: If an agent observes a transition conflicting with its guess of another agent's policy, it randomly selects a new tuple of internal policies.
  • Result: Theorem 7 proves that this process converges to a consensus state where all agents agree on a set of policies that satisfy the parity objectives almost surely.

Significance and Claims

The paper claims to establish the foundation of a first-of-its-kind modular design framework for $\omega$-regular decision-making. Its significance lies in:

1. Modularity and Robustness: It enables the separation of concerns in policy design. Policies can be designed, added, removed, or modified independently without re-computing the entire system, provided the agents adhere to the agreed-upon conventions.
2. Lightweight Runtime: The schedulers are simple and stochastic, suitable for devices with limited processing capabilities (e.g., robots, drones).
3. Theoretical Limits: It rigorously characterizes the trade-off between the complexity of the objective class and the required level of coordination (scheduler awareness) among agents.
   • Büchi: Requires only path-aware policies.
   • Co-Büchi: Requires knowledge of scheduling status (scheduled-aware).
   • Parity: Requires knowledge of which agent was scheduled (full history-aware).
4. Safety vs. Liveness: It clarifies that while liveness can be achieved through probabilistic convergence via conventions, safety fundamentally requires a communication protocol (shielded composition) to ensure deterministic correctness on every path.

The authors note that while they prove the existence of such conventions and schedulers, the convergence time of the proposed protocols may be exponential, and improving this remains a topic for future work. They also distinguish their approach from "auction-based scheduling" (which is incomplete for multiple objectives) and "strategy templates" (which incur high computational overhead), positioning their method as a sound, complete, and modular alternative for strongly connected graphs.