Glossary¶

Atomic Proposition¶

A boolean fact emitted by a safety abstraction, such as door_0_open or agent_1_deadlocked.

Label¶

The set of atomic propositions true in one abstract state.

Global Safety Formula¶

An LTL formula describing the safety requirement for the whole system. The outer monitor checks this formula.

Local Obligation¶

A SafeLTL formula assigned to one agent over that agent's local alphabet. During certification it is compiled into that agent's local-obligation monitor and enforced by the projected contract shield.

Contract Profile¶

A tuple of local obligations, one per agent. The paper also calls this a SafeLTL contract.

Contract¶

A certified contract profile deployed at runtime. In code exports this is represented by the profile formulas plus compiled monitors, shield templates, permissiveness, and selector metadata.

Certified Library¶

The finite ordered set of certified contract profiles available to the learning-time selector. The selector may switch between entries only at reset boundaries; it never certifies a new profile online.

Assume-Guarantee Reasoning¶

Reasoning where an agent's safe actions can depend on obligations guaranteed by teammates. In this repository, the certification step is centralized over the whole contract profile: every agent may rely on the other agents' local obligations only because the full tuple is certified simultaneously.

Shield¶

A runtime filter that exposes safe action masks and prevents unsafe local actions from reaching the environment.

Winning Region¶

The set of product states from which at least one safe action strategy remains.

Product State¶

A combined state containing an abstract environment state and one or more monitor states.

Safety Projection¶

A model-specific projection that collapses reward-only state details during safety synthesis while preserving safety-relevant labels.