Compositional Shielding¶

This project studies how cooperative multi-agent reinforcement learning can stay safe under explicit temporal specifications while still learning useful coordinated behavior.

The central idea is to start with a global safety formula in Linear Temporal Logic (LTL), then make each agent carry a local obligation expressed as its own LTL formula. The tuple of those local formulas is a contract profile. At runtime, the active contract profile is the contract: it says what each agent must guarantee locally, and what the rest of the team may rely on while choosing actions.

The project is intentionally about decentralized training and decentralized execution. The safety certification step is more centralized: it checks a whole contract profile against the global formula and the environment abstraction before the profile can be offered to the learners.

Reading Path¶

• Start with LTL Safety for labels, formulas, and monitors.
• Read Local Obligations for the contract framing.
• Read Shielding for ordinary local shields and contract-aware shields.
• Read Learning for Contract-IPPO, Contract-IQL, and the baselines.
• Use Environments to see which benchmark safety stories are implemented.
• Use Setup, Notebooks, and Experiments when running the code.

What Counts As Success¶

A run is interesting only when reward and safety are inspected together. The project compares ordinary shielded learners with contract learners that can switch among certified contract profiles. A contract learner should never violate the global safety monitor, and it should sometimes discover a less conservative safe behavior than a robust local shield allows.

Documentation Layout¶

The pages in this site are user-facing. The docs/AI directory is the companion engineering notebook for durable implementation details, audit notes, and design alternatives; it is useful when you need lower-level provenance behind a user page.