Skip to content

Local Obligations

The contract view of this repository is:

  • each agent has a local obligation expressed as a SafeLTL formula over its local alphabet,
  • the tuple of one local obligation per agent is a contract profile, also called a SafeLTL contract in the paper,
  • the finite ordered set of certified contract profiles is the certified library used by Contract-IPPO and Contract-IQL.

This wording matters. Agents have local obligations, and those obligations are formulas. A profile is the collection of formulas deployed together. A certified library is the selector's finite action space over contracts.

Why Profiles Exist

Robust local shielding can be conservative. If one agent must choose an action that is safe against every possible teammate action, useful coordinated behavior may be ruled out. A contract can reduce that conservatism by saying that teammates are not arbitrary: they are also constrained by their own certified local obligations.

For example, one agent may be allowed to move through a shared region when the active contract also obligates another agent to yield, wait, or keep an access path clear.

Reward Optimality

Contract shielding is expected to beat ordinary shielding only when the global safety property leaves some high-reward coordinated behavior legal, but ordinary local shields cannot assume the teammate cooperation needed to take it. In that case, a certified profile can make the cooperation explicit:

  • one train yields while another enters a shared segment,
  • a loader attempts LOAD only under a cooperative-load obligation,
  • a plate holder keeps a door open while the runner crosses,
  • a routing or warehouse agent preserves a teammate's route or queue progress.

The certification step is the reason this can be less conservative without being less safe. The learner is not trusted to invent assumptions at runtime; it only chooses among profiles that were already checked against the global formula and the environment abstraction.

Centralized Assume-Guarantee Certification

The assume-guarantee reasoning here is centralized in the certification step. The system proposes candidate local SafeLTL formulas, builds a contract profile, and certifies the full tuple together.

A profile is certified only when:

  • the conjunction of the local obligations implies the fixed global safety formula,
  • the profile has a non-empty safe fixed point from the initial abstract state,
  • the resulting action permissions are rectangular across agents.

Rectangular permissions mean each agent receives a set of allowed local actions, and every joint action formed from those local sets must stay inside the certified fixed point. This keeps execution decentralized while certification uses the whole profile.

Candidate obligations are generated from atomic propositions exposed by the safety model. By default, contract-ready models provide local alphabets per agent. These alphabets restrict search to propositions that are plausible for that agent's local obligation, while certification still uses the authoritative global labels emitted by the model.

Candidate generation first tries the weakest profile, assigning t to every agent. If that profile does not imply or realize the global formula, it is rejected and the certified library starts from the first certified generated profile. Certified nontrivial profiles add formulas such as yielding, station-clearance, reservation, or gap-maintenance obligations.

The experiment notebooks expose two important search priors explicitly: contract_use_temporal_form_heuristic=True and contract_use_model_seed_formulas=False by default. The no-seed setting is the headline audit mode. When the goal is reward-seeking rather than no-seed evidence, model seed formulas can be enabled as a labeled seeded-prior ablation.

Runtime Contract Selection

Contract-IPPO and Contract-IQL receive a certified library of contract profiles. During training, a profile selector tries profiles and keeps score from recent team return. The default selector is a discounted UCB bandit. The selector treats profile ids as opaque arms; safety is already certified before the profile can be selected.