Pressure Plate¶

Pressure Plate is a role-structured grid task. Door-holder agents can stand on plates to open doors, while the runner must cross those doors safely. The linear layout makes local responsibilities natural: holders maintain doors and the runner respects door state.

Global Safety Formula¶

The default experiment formula is a concrete global formula:

runner_requires_return_routes =
G(((!goal_achieved & (agent_2_in_door_0 | agent_2_after_door_0)) ->
   agent_2_can_return_before_door_0) &
  ((!goal_achieved & (agent_2_in_door_1 | agent_2_after_door_1)) ->
   agent_2_can_return_before_door_1))

The global monitor rejects traces where the runner is in or beyond a protected door without a route back to the outside side of that door. Return routes are no longer required after goal_achieved.

agent_2_can_return_before_door_i is computed by BFS from the runner's current cell to any cell with y > door_i_row. Walls and currently closed doors block the search, teammate occupancy is ignored, and the runner's current cell is allowed as the start even when that cell is a closed door.

Strict Crossing Variant¶

Pressure Plate also exposes an experimental doorway-phase safety formula:

runner_crosses_open_doors_strict =
G(((agent_2_crossing_door_0 | agent_2_in_door_0) -> door_0_open) &
  ((agent_2_crossing_door_1 | agent_2_in_door_1) -> door_1_open))

This variant uses one-step transition labels. agent_2_crossing_door_i is emitted on the post-step state when the runner enters door i or leaves it toward the far side; agent_2_in_door_i is emitted while the runner occupies the door cell. The strict post-step semantics reject a crossing step if the holder leaves the matching plate in the same joint step, but they do not require the holder to keep the door open forever after the runner has passed.

The variant is intended for controlled Shielded-* versus Contract-* comparisons: ordinary local shields must be robust to arbitrary same-step holder departures, while a certified contract profile can require holders to keep the relevant door open while the runner is waiting at or occupying that doorway.

The older open-door formula is also still available:

runner_requires_open_doors =
G((agent_2_after_door_0 -> door_0_open) &
  (agent_2_after_door_1 -> door_1_open))

Local Alphabets¶

For the default three-agent linear layout, the exhaustive contract-local alphabets are:

agent_0:
  agent_0_holds_door_0_ok
  door_0_open
  agent_2_after_door_0
  agent_2_crossing_door_0
  agent_2_in_door_0
  agent_2_waiting_at_door_0
  goal_achieved
  plate_0_pressed
  agent_0_on_plate
  agent_0_on_plate_0

agent_1:
  agent_1_holds_door_1_ok
  door_1_open
  agent_2_after_door_1
  agent_2_crossing_door_1
  agent_2_in_door_1
  agent_2_waiting_at_door_1
  goal_achieved
  plate_1_pressed
  agent_1_on_plate
  agent_1_on_plate_1

agent_2:
  agent_2_waits_for_door_0_ok
  agent_2_after_door_0
  door_0_open
  agent_2_waiting_at_door_0
  agent_2_crossing_door_0
  agent_2_in_door_0
  agent_2_can_return_before_door_0
  agent_2_waits_for_door_1_ok
  agent_2_after_door_1
  door_1_open
  agent_2_waiting_at_door_1
  agent_2_crossing_door_1
  agent_2_in_door_1
  agent_2_can_return_before_door_1
  goal_achieved

Emitted Labels¶

The safety model emits labels for:

• agent positions and goal status,
• before-door, after-door, and waiting-at-door phases,
• strict crossing and in-door transition phases,
• return-route availability for the runner,
• plate occupancy,
• door-open facts,
• door-holder protocol facts,
• runner wait-for-door protocol facts,
• global goal achievement.

Contract Intuition¶

The runner can progress only when plate holders keep the relevant doors open. Under the return-route default, ordinary local shielding cannot assume that teammates will keep those routes open, so it conservatively keeps the runner out of protected doors. Contract profiles can place local obligations on holders and runner phases so the team can coordinate around doors without violating the global formula. Compared with the local/factorised Shielded-* baseline, the contract path can outperform when holder obligations make a route back outside the door certified rather than merely hoped for.

Current Contract Profiles¶

The current default should first be evaluated with the hand-authored holders_preserve_return_routes profile:

agent_0:
G((!goal_achieved &
   (agent_2_waiting_at_door_0 | agent_2_in_door_0 | agent_2_after_door_0))
  -> X(door_0_open))

agent_1:
G((!goal_achieved &
   (agent_2_waiting_at_door_1 | agent_2_in_door_1 | agent_2_after_door_1))
  -> X(door_1_open))

agent_2:
runner_requires_return_routes

The older no-seed normal search-built feasibility audit for runner_requires_open_doors certified 3 nontrivial Pressure Plate profiles, including 1 profile with extra holder/runner coordination obligations. The canonical useful profile was profile_0001; it pairs door-holder commitments with the runner's global door-open condition:

agent_0:
G(agent_0_holds_door_0_ok)

agent_1:
G(agent_1_holds_door_1_ok)

agent_2:
G((agent_2_after_door_0 -> door_0_open) &
  (agent_2_after_door_1 -> door_1_open))

This profile certifies the concrete global runner safety formula by making the door-holder responsibilities explicit: the runner only crosses doors while the corresponding holders keep those doors open. Current saved summaries are mixed: Contract-IPPO is worse than Shielded-IPPO, while Contract-IQL is slightly better than Shielded-IQL, and all four runs preserve zero safety violations. Fresh paired runs should test whether the balanced holder/runner profile can beat the ordinary role-specific Shielded-* baselines consistently.

Reward-optimality status: pending return-route rerun. The return-route profile is structurally reward-relevant because the ordinary local baseline is safe but cannot cross protected doors, while the contract profile can permit progress when holders preserve routes back.

Reward Function¶

Pressure Plate uses dense position shaping, with different role targets. For the door-holder agents, the role target is that holder's assigned pressure plate. For the runner, the role target is the goal cell.

The layout is split into rooms by the horizontal wall rows. The helper curr_room is 0 in the starting room and increases as an agent moves toward the goal. If agent i is in its assigned room, its reward is the negative Manhattan distance to its role target, normalized by the environment's max_dist constant:

r_i = -manhattan_distance(agent_i, role_target_i) / max_dist

If the agent is outside its assigned room, the reward is a coarse room-progress value:

r_i = curr_room - (num_rooms - 1)

For the default three-agent linear layout, this outside-room value ranges from -2 in the starting room to 0 in the top room. Reaching the goal terminates the episode. The raw environment defaults preserve historical behavior with success_reward=0.0 and timestep_penalty=0.0. The Pressure Plate experiment notebook passes pp_success_reward=10.0 and pp_timestep_penalty=0.01 by default, subtracting the timestep penalty every step and adding the success reward to every agent on the goal-reaching transition.

Spaces¶

For the default linear three-agent experiment (height=7, width=4, n_agents=3, sensor_range=3):

Source Links¶

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