Environments¶
The repository uses cooperative benchmark environments with explicit safety labels and named LTL formulas. Each environment package follows the same broad shape:
impl: environment mechanics and PettingZoo-style wrappers,constraints: named global LTL formulas,labelled: safety abstraction, emitted propositions, local alphabets, and exact transition kernels where available.
Formula Specialization¶
Most benchmark formulas use {agent} as a template placeholder. Before a
monitor is built, the experiment code specializes the template over the concrete
agent ids and conjoins the per-agent formulas. For example,
G(!{agent}_deadlocked) in Flatland becomes a global no-deadlock formula over
the trains in the current safety model.
Some formulas are already concrete global formulas. Pressure Plate's default
runner formula, for example, names agent_2 and the doors directly because the
runner and door-holder roles are fixed by the linear layout.
Local Alphabets¶
Contract candidate search is guided by model-local alphabets. A local alphabet is the set of atomic propositions that may appear in one agent's candidate obligations. These alphabets are deliberately smaller than the full emitted label set, so search focuses on propositions that are plausible local guarantees. Certification still checks the full contract profile against the authoritative labels emitted by the environment safety model.
Each environment page lists the exhaustive per-agent contract-local alphabets for the default experiment configuration. Those lists are the source of truth for what normal model-local candidate search can mention before any explicit candidate-label override or diagnostic alphabet is used.
Contract Shielding Vs Factorised Shielding¶
The Shielded-* baselines use ordinary local, or factorised, shields. Each
agent receives a mask that must be safe against arbitrary teammate behavior.
That is robust, but it can block actions whose safety depends on another agent
cooperating.
Contract-IPPO and Contract-IQL instead choose among certified contract
profiles. A contract profile adds local obligations for teammates, such as
yielding, holding a door, respecting a reserved route, or following
conservatively. Certification proves the whole profile against the same global
safety property, so reward gains come from less conservative masks rather than
from weakening safety. Saved paired runs currently show this most clearly in
Flatland and Car Platoon; the other environments have structural contract
profiles that still need fresh paired reward exports before claiming measured
dominance.
For Connector and RWARE, the default formulas expose this limitation as
unrealizability rather than mere conservatism. Connector's owner-state
route-clearance predicate can be violated by a teammate that the owner cannot
control. RWARE's queue-yield protocol can reach projected queue states with no
robust local clearing action. Their ordinary decentralized Shielded-*
baselines are therefore intentionally omitted for the default formulas; the
environment pages describe the contract or joint-shield alternatives to use
instead.
Implemented Benchmarks¶
| Environment | Default formula | Safety story |
|---|---|---|
| Connector | preserve_reserved_route_clearance |
Grid routing agents preserve reserved-route clearance while connecting to targets. |
| Flatland | avoid_deadlocks |
Trains avoid deadlock on a small railway abstraction. |
| Level-Based Foraging | avoid_failed_loads |
Agents avoid unsafe load attempts while coordinating on food. |
| Pressure Plate | runner_requires_return_routes |
The runner may be in or beyond protected doors only while a route back outside remains open. |
| RWARE | queue_yield_protocol |
Warehouse robots follow queue-yield behavior around requested carriers. |
| CookingZoo | kitchen_etiquette |
Kitchen agents avoid unsafe delivery, ingredient, and station-blocking behavior. |
| Car Platoon | maintain_safe_gap |
Controlled cars maintain safe following gaps. |
Current Contract Profile Signal¶
The current checked-in contract exports cover the six paper benchmarks under
exports/<env>/contracts/contract_profiles.json. CookingZoo remains
implemented in the local repository, but the paper snapshot intentionally omits
it and there is no current checked-in CookingZoo contract export alongside the
six rows below.
Additional-obligation profiles contain protocol APs beyond the ordinary global safety formula APs; they are the main source of expected reward separation from ordinary shielded baselines.
| Environment | Certified profiles | Canonical extra-obligation profile | Certifies |
|---|---|---|---|
| Connector | 2 | profile_0198: agent_1_respects_reservations_ok |
Reserved-route clearance under an explicit reservation-respect guarantee. |
| Flatland | 3 | profile_0002: agent_0_yields_to_agent_1_ok; profile_0024: agent_1_yields_to_agent_0_ok |
No deadlock while one train is contractually yielding. |
| Level-Based Foraging | 2 | profile_0002: agent_0_coop_load_ok |
No failed load while cooperative loading is exposed as a safe protocol. |
| Pressure Plate | 1 | profile_0001: agent_0_holds_door_0_ok; agent_1_holds_door_1_ok |
The runner may cross protected doors under holder obligations that preserve return routes. |
| RWARE | 1 | none retained in current export | Queue-yield safety under the global queue-yield APs only. |
| Car Platoon | 2 | profile_8004: agent_1_conservative_follow_ok |
Safe following gaps while a controlled follower behaves conservatively. |
These counts should now be refreshed from
exports/<env>/contracts/contract_profiles.json when HPC exports are available;
the checked-in feasibility report remains historical fallback evidence for the
same no-seed, core-alphabet setting. Extra-obligation entries show currently
available reward-relevant contract profiles. Certification means the
local-obligation tuple implies the selected global LTL formula and has a
non-empty assume-guarantee fixed point from the initial abstraction. It is
safety evidence, not automatic reward dominance: measured dominance still
requires paired training runs with identical seeds and budgets. The key
mechanism is always the same: ordinary local shields must be safe against
arbitrary teammate actions, while a certified contract can let an agent rely on
teammates satisfying their own local obligations.
Current local reward evidence is strongest for Flatland and Car Platoon. Their
saved paired exports show Contract-IPPO and Contract-IQL outperforming the
matching Shielded-* baselines while preserving zero safety violations. Pressure
Plate has a return-route holder profile, but still needs fresh paired
normal-contract runs before making a user-facing reward claim. Connector and
RWARE have structural contract evidence for their default formulas, but no
ordinary decentralized Shielded-* baseline should be reported for those
formulas because the local shields are not realizable. Level-Based Foraging
certifies cooperative-load profiles and now has a positive Contract-IPPO signal
against zero-reward Shielded-IPPO, while Contract-IQL still needs a fresh debug
run.
| Environment | Current reward-optimality read |
|---|---|
| Connector | Structural / pending safe baseline: owner-state route-clearance has no ordinary decentralized Shielded baseline for the default formula. |
| Flatland | High: saved Contract-IPPO and Contract-IQL runs beat Shielded runs with zero violations. |
| Level-Based Foraging | High for IPPO pending flagged rerun; IQL remains weak/pending, and older artifacts can contain larger menus than the canonical no-seed report. |
| Pressure Plate | Mixed pending rerun: current saved summaries show Contract-IPPO below Shielded-IPPO and Contract-IQL slightly above Shielded-IQL, all with zero violations. |
| RWARE | Structural / pending safe baseline: the current export retains only the global queue-yield profile, and ordinary decentralized queue-yield Shielded runs can hit empty masks. |
| Car Platoon | High: saved Contract-IPPO and Contract-IQL runs beat Shielded runs with zero violations. |
Future Candidates¶
POSGGym has additional cooperative grid-world tasks that could be adapted later: