Connector¶

Connector is a grid routing task. Agents move from start cells to target cells while leaving path trails behind them. The contract benchmark focuses on a reservation-conflict layout where one agent's route can make another route unusable unless agents respect reserved cells.

Global Safety Formula¶

The default experiment formula is:

preserve_reserved_route_clearance = G({agent}_reserved_route_clear_ok)

In the two-agent experiment, this specializes to:

(G(agent_0_reserved_route_clear_ok)) &
(G(agent_1_reserved_route_clear_ok))

The global monitor therefore rejects traces where any agent violates its reserved-route-clearance proposition.

Why Ordinary Local Shielding Is Omitted¶

The default route-clearance formula is not locally controllable by a factorised shield. The proposition agent_i_reserved_route_clear_ok describes whether agent i's reserved route is clear, but a violation can be caused by a teammate entering or remaining on that route. A local shield for agent_i must be safe against every teammate action, and agent_i has no action that can force the teammate off its reserved cells. Conversely, the teammate's ordinary local shield cannot rely on an owner-specific route-clearance promise unless that promise is part of a certified contract profile.

The default experiments therefore intentionally omit ordinary decentralized Shielded-* baselines for preserve_reserved_route_clearance and avoid_reserved_route_blocking. The older respect_reserved_routes formula is an agent-local ablation and can use ordinary local shielding, but it is not the default reward-dominance objective for this environment.

Local Alphabets¶

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

agent_0:
  agent_0_keeps_reserved_routes_clear_ok
  agent_0_keeps_agent_1_reserved_route_clear_ok
  agent_0_reserved_route_clear_ok
  agent_1_reserved_route_clear_ok
  agent_0_respects_reservations_ok
  agent_0_respects_agent_1_reservation_ok

agent_1:
  agent_1_keeps_reserved_routes_clear_ok
  agent_1_keeps_agent_0_reserved_route_clear_ok
  agent_0_reserved_route_clear_ok
  agent_1_reserved_route_clear_ok
  agent_1_respects_reservations_ok
  agent_1_respects_agent_0_reservation_ok

The diagnostic alphabet can also expose reserved-route blocking propositions for every agent.

Emitted Labels¶

The safety model emits labels for:

• agent positions and targets,
• connection status,
• blocked and reserved-route-blocked states,
• reserved-route occupancy,
• aggregate and pairwise reservation-respect facts,
• available local actions.

Contract Intuition¶

A certified contract profile can assign explicit reservation-respect obligations, allowing one agent to rely on another keeping a route usable while still preserving the global monitor. That is the intended route by which Contract-IPPO or Contract-IQL can recover useful behavior for the default route-clearance task: the safety formula is unchanged, but the mask is computed under certified teammate commitments rather than under arbitrary teammate actions.

Current Contract Profiles¶

With the current core alphabet and experiment synthesis parameters, the no-seed normal search-built feasibility audit certifies 2 nontrivial Connector profiles, including 1 extra-obligation route-clearance contract. The canonical additional-obligation profile is profile_0198; it assigns the global reserved-route-clearance guarantee to agent_1 and adds an explicit reservation-respect obligation:

agent_0:
t

agent_1:
G(agent_0_reserved_route_clear_ok & agent_1_reserved_route_clear_ok) &
G(agent_1_respects_reservations_ok)

Because the ordinary decentralized Shielded-* baseline is not realizable for the default owner-state route-clearance objective, reward reporting should not wait for a paired factorised-shield run under this formula. The relevant comparisons are unshielded or constrained learners, centralized joint shielding, and agent-local ablations such as respect_reserved_routes.

Reward-optimality status: structural / pending safe baseline. The certified profile is reward-relevant because ordinary local shielding must assume a teammate might block a reserved route, while the contract can require reservation-respect behavior.

Reward Function¶

The default experiment uses dense per-agent rewards:

reward_mode = "dense"
connected_reward = 1.0
timestep_reward = -0.03

For agent i, the environment records whether the agent was connected before the step and whether it has just reached its target after the step. The default dense reward is:

r_i = 1.0 * newly_connected_i - 0.03 * was_unconnected_i

So an unconnected agent pays a small step cost, an agent that connects on this step receives 0.97 net reward, and agents that were already connected receive 0. The sparse modes omit the timestep cost and pay only the newly-connected indicator. The shared_dense and shared_sparse modes first compute those per-agent rewards, then give every agent their sum.

Spaces¶

For the default reservation-conflict experiment (grid_size=5, n_agents=2):

Source Links¶

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