RWARE¶

RWARE is a warehouse queue and delivery benchmark. Robots move shelves through pickup, queue, and delivery zones. The contract benchmark focuses on queue conflicts around requested carriers.

Global Safety Formula¶

The default experiment formula is:

queue_yield_protocol = G({agent}_queue_yield_ok)

In the two-agent experiment, this specializes to:

(G(agent_0_queue_yield_ok)) &
(G(agent_1_queue_yield_ok))

The global monitor rejects traces where any agent violates its queue-yield protocol proposition.

Plain-Language Safety Property¶

The property protects requested-shelf carriers in the queue bottleneck. A robot that is carrying the requested shelf is allowed to keep moving toward delivery. If another robot is unloaded, sitting in the queue, and occupying the carrier's next forward cell, that unloaded robot becomes the blocker. The blocker must yield on that transition: after both robots act, it may not still occupy the carrier's forward cell.

So agent_i_queue_yield_ok means: agent i did not fail a yield obligation on the previous transition. It is false exactly when agent i was an unloaded queue blocker for a requested carrier and stayed in the blocking cell instead of clearing it. The LTL formula G({agent}_queue_yield_ok) says this must never happen, for every agent, at every step.

This is a safety property, not a delivery-progress objective. It does not say that a requested carrier must eventually deliver, and it does not reward movement. It only rules out the bad queue interaction where an unloaded robot keeps blocking a requested carrier's immediate path. The separate requested_carrier_progress_ok and delivery_lane_ok labels are available for diagnostics and contracts, but they are not part of the default global formula.

Why Ordinary Local Shielding Is Omitted¶

The default queue-yield formula exposes a real local-shield failure mode. An ordinary factorised shield can synthesize initial masks for the queue-conflict layout, but the mask must remain safe against arbitrary teammate actions at every reachable local abstraction state. Training can reach a queue-protocol state where a blocker is required to yield for a requested carrier, while the carrier and blocker positions leave no locally certified action that robustly clears the requested carrier's forward cell. The runtime symptom is an empty local mask, reported as No safe local action available.

A CPU-only 1M-step Shielded-IPPO reproduction reached this failure after initial local synthesis succeeded. The concrete failing state had queue_yield_required={0}, queue_yield_clear_forward={}, and requested_carrier_progress_violations={1}: the blocker owed a yield, but the projected local shield could not certify any one-step action as safe against all teammate moves. The default RWARE experiments therefore intentionally omit ordinary decentralized Shielded-* baselines for queue_yield_protocol and use contract or centralized/joint shielding comparisons instead.

This is not because the AP agent_i_queue_yield_ok is hard to emit. The label is local enough to monitor. The problem is the factorised shield certificate: each protected agent is synthesized separately, and a local action is allowed only if it is safe for every possible teammate action. Queue-yield safety is a joint transition fact. Whether the blocker really clears the carrier's next cell depends on both robots' same-step moves and collision resolution, and the next safe queue state may require the carrier and blocker to take compatible actions.

A factorised mask cannot say "allow this blocker move only when the carrier also takes the compatible carrier move." It exposes independent per-agent action sets, and every joint action formed by combining those sets must remain safe. If one robot's useful action is safe only under teammate cooperation, the ordinary shield must remove it; after enough such removals, the reachable local game can have no action left. A joint shield avoids this by choosing whole joint actions. A contract shield avoids it by certifying teammate obligations first, so the local masks are checked against obligation-constrained teammates rather than arbitrary teammates.

Local Alphabets¶

For the default two-agent queue-conflict experiment, the exhaustive contract-local alphabets are:

agent_0:
  agent_0_queue_yield_ok

agent_1:
  agent_1_queue_yield_ok

The diagnostic alphabet can also expose queue-zone, loaded, requested-carrier, blocking, delivery-lane, requested-carrier-progress, delivery-zone, pickup-zone, and requested-shelf facts.

Emitted Labels¶

The safety model emits labels for:

• robot positions and directions,
• highway, queue-zone, delivery-zone, and pickup-zone membership,
• loaded and carrying-requested status,
• requested shelf location,
• requested-carrier queue and near-goal status,
• blocking-requested-carrier facts,
• queue-yield, delivery-lane, and requested-carrier-progress protocol facts.

Contract Intuition¶

Useful delivery progress may depend on a teammate yielding queue space or keeping a delivery lane open. Contract profiles can encode those local obligations, giving a requested carrier safer room to move than a robust local factorised shield can assume. This is the intended contract mechanism: the global queue-yield property stays fixed, while a certified contract can make queue progress less adversarial without relying on an unrealizable ordinary local queue-yield shield.

Current Contract Profiles¶

With the current checked-in experiment synthesis export, the normal search-built RWARE library has 16 generated candidates and 1 retained certified profile. That profile uses only the global queue-yield APs; no additional-obligation profile is retained in the current export.

agent_0:
G(agent_0_queue_yield_ok)

agent_1:
G(agent_1_queue_yield_ok)

This is the retained profile_0154 in exports/rware/contracts/contract_profiles.json. It certifies the global queue-yield objective under the compact model-local alphabet, but it should not be described as a reward-relevant requested-carrier-progress contract. Broader diagnostic or fair-search audits may still include delivery_lane_ok, requested_carrier_progress_ok, coarser queue-slot labels, and route-intention labels that avoid relying on exact requested-shelf coordinates, but those labels are not part of the current default retained library.

Reward-optimality status: structural / pending safe baseline. The certified profile preserves the queue-yield safety objective, but the current retained library does not add a progress obligation beyond that objective. Ordinary decentralized Shielded-* baselines are intentionally omitted for this default because the local queue-yield shield can hit empty-mask states in long runs. Reward claims should therefore compare the default contract runs against unshielded or constrained learners, centralized joint shielding, or a refreshed contract library with certified progress obligations.

Reward Function¶

The default experiment constructs Warehouse directly with:

reward_type = RewardType.INDIVIDUAL
request_queue_size = 2
max_steps = 200

Rewards are sparse and delivery-driven. On each step, the base reward vector is all zeros. If a requested shelf is on a goal cell after movement and load-toggle updates, the environment replaces that request with a new shelf request and assigns reward according to reward_type.

With the default INDIVIDUAL reward, only the robot occupying the goal cell with the requested shelf receives +1. There is no movement cost, queue cost, or direct reward penalty for protocol violations. GLOBAL reward gives every robot +1 for each successful requested-shelf delivery. TWO_STAGE gives the delivering robot +0.5 at the goal and another +0.5 after it later unloads the delivered shelf away from the highway.

Spaces¶

For the default queue-conflict experiment (shelf_columns=3, column_height=8, shelf_rows=1, n_agents=2, flattened observations):

Source Links¶

• Environment implementation
• PettingZoo wrapper
• Formula module
• Labelled safety model
• Experiment notebook