Flatland¶

Flatland is a small railway-routing abstraction built around train conflicts. The contract benchmark uses a single-track meeting scenario where progress may require one train to yield so the team avoids deadlock.

Global Safety Formula¶

The default experiment formula is:

avoid_deadlocks = G(!{agent}_deadlocked)

In the two-train experiment, this specializes to:

(G(!agent_0_deadlocked)) &
(G(!agent_1_deadlocked))

The global monitor rejects any trace where a train becomes deadlocked.

Local Alphabets¶

For the default two-train experiment, the exhaustive contract-local alphabets are:

agent_0:
  agent_0_yields_to_agent_1_ok
  agent_0_deadlocked
  agent_1_deadlocked

agent_1:
  agent_1_yields_to_agent_0_ok
  agent_0_deadlocked
  agent_1_deadlocked

This lets one train's local obligation mention both its own yielding protocol and the global no-deadlock facts needed for certification.

Emitted Labels¶

The safety model emits labels for:

• train positions,
• target and off-map status,
• Flatland train state such as ready, moving, stopped, malfunction, and done,
• deadlock and conflict-stop facts,
• pairwise yield-protocol facts.

Contract Intuition¶

A train moving into a shared track segment may be safe only if the opposing train is constrained to yield. Contract profiles can encode that assumption directly, while ordinary local, or factorised, shields must stay safe against arbitrary teammate behavior. This is why the saved Contract-IPPO and Contract-IQL runs can outperform Shielded-IPPO and Shielded-IQL here without changing the global no-deadlock monitor.

Current Contract Profiles¶

With the current core alphabet and experiment synthesis parameters, the normal search-built feasibility audit certifies 3 nontrivial Flatland profiles, 2 of which add yield obligations beyond the no-deadlock formula APs. The canonical reward-relevant contracts are profile_0002 and profile_0024. They combine the global no-deadlock monitor with one pairwise yield fact: profile_0002 obligates agent_0 to yield to agent_1, and profile_0024 obligates agent_1 to yield to agent_0.

agent_0:
G(!agent_0_deadlocked & !agent_1_deadlocked) &
G(agent_0_yields_to_agent_1_ok)

agent_1:
G(!agent_0_deadlocked & !agent_1_deadlocked)

or:

agent_0:
G(!agent_0_deadlocked & !agent_1_deadlocked)

agent_1:
G(!agent_0_deadlocked & !agent_1_deadlocked) &
G(agent_1_yields_to_agent_0_ok)

These profiles expose higher reward potential because a train can safely take progress actions into a shared railway segment when the opposing train is under a certified yield obligation. Ordinary local shielding has to assume the opposing train may also contest the segment, so it is expected to be more conservative. The local paired exports now show that mechanism translating into reward: Contract-IPPO's tail reward_mean is about 0.590 versus Shielded-IPPO's 0.157, and Contract-IQL is about 0.537 versus Shielded-IQL's 0.153, with zero safety violations in those saved runs.

Reward-optimality status: high. Flatland is the clearest example because the reward bottleneck and the contract proposition are the same social fact: one train must yield so the other can make progress safely.

Reward Function¶

The default experiment uses the wrapper's progress reward:

reward_mode = "progress"
progress_reward_scale = 1.0
arrival_bonus = 5.0
deadlock_penalty = 5.0
step_penalty = 0.01

For train i, the wrapper compares the Flatland shortest-path distance to the target before and after the step:

progress_i = max(previous_distance_i - next_distance_i, 0)
r_i = progress_i * progress_reward_scale - step_penalty

If the train reaches DONE on this step, it also receives arrival_bonus. If Flatland marks the train deadlocked, it receives -deadlock_penalty. If the computed progress reward is non-finite, the wrapper falls back to the native Flatland reward for that train. With reward_mode="native", the wrapper passes the underlying RailEnv reward through unchanged.

Spaces¶

For the default single-track meeting experiment (scenario="single_track_meet", n_agents=2, tree_depth=1, predictor_depth=10):

Source Links¶

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