Car Platoon¶

Car Platoon studies safe following distances in a controlled platoon. The controlled cars choose acceleration actions while the safety model tracks gaps, velocities, and collision or falling-behind conditions.

Global Safety Formula¶

The default experiment formula is:

maintain_safe_gap = G({agent}_gap_safe)

For the two controlled agents in the default experiment, this specializes to:

(G(agent_0_gap_safe)) &
(G(agent_1_gap_safe))

The global monitor rejects traces where either controlled following gap becomes unsafe.

Local Alphabets¶

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

agent_0:
  agent_0_gap_safe
  agent_0_conservative_follow_ok
  agent_0_smooth_lead_ok

agent_1:
  agent_1_gap_safe
  agent_1_conservative_follow_ok
  agent_1_smooth_lead_ok

The diagnostic alphabet can also expose nearby gap diagnostics, damage, collision, falling-behind, closing/opening-fast, and acceleration-safety facts for the agent's own gap and the next gap ahead when available.

Emitted Labels¶

The safety model emits labels for:

• controlled-car velocities and front-car velocities,
• following distances,
• safe-gap, crash, and too-far status,
• near-min-gap and near-max-gap diagnostics,
• closing-fast and opening-fast diagnostics,
• safe-to-accelerate-if-front-coasts facts,
• damage and front-damage facts,
• conservative-follow and smooth-lead protocol facts.

Contract Intuition¶

A follower may safely choose less conservative actions when the relevant front car is constrained by smooth or conservative behavior. Contract profiles can encode those local guarantees, though the uncontrolled lead car still limits how much the contract can assume. The measured advantage over local/factorised Shielded-* baselines comes from reducing worst-case assumptions between controlled followers while leaving the safe-gap monitor unchanged.

Current Contract Profiles¶

With the current core alphabet and experiment synthesis parameters, the normal search-built feasibility audit certifies 2 nontrivial Car Platoon profiles, 1 of which adds a following-protocol obligation beyond the safe-gap APs. The canonical reward-relevant contract is profile_8004:

agent_0:
G(agent_0_gap_safe)

agent_1:
G(agent_1_gap_safe) & G(agent_1_conservative_follow_ok)

This profile exposes higher reward potential by distinguishing controlled follower interactions from the stochastic lead-car uncertainty. If a neighboring controlled car is obligated to follow conservatively, the local shield can permit actions that ordinary shielding would block under worst-case teammate behavior. Local paired exports currently show the strongest measured contract edge here: Contract-IPPO and Contract-IQL both beat their Shielded-* baselines while preserving zero safety violations. The current saved tail reward_mean comparison is about -3.495 versus -3.864 for IPPO and -4.476 versus -8.610 for IQL, where less negative is better.

Reward-optimality status: high. The contract does not control the stochastic lead car, but it can reduce worst-case assumptions between controlled followers. That is enough in the saved runs to improve reward without safety violations.

Reward Function¶

The default experiment uses:

min_distance = 0.0
max_distance = 20.0
initial_distance = 10.0
safety_violation_penalty = 100.0
terminate_on_violation = true

After the environment samples the uncontrolled front-car action, applies all accelerations, updates velocities, and updates the inter-car gaps, each controlled agent is rewarded from its own following gap:

r_i = -distance_i

If that gap is unsafe after the step, meaning distance_i <= min_distance or distance_i >= max_distance, the environment subtracts safety_violation_penalty. With the default experiment settings, unsafe gaps therefore receive an additional -100 and terminate the episode. The reward encourages tight platooning, while the safety formula and penalty keep the gap inside the allowed interval.

Spaces¶

For the default three-car experiment (n_cars=3, so two controlled agents):

Source Links¶

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