Skip to content

LTL Safety

Safety in this project is written as Linear Temporal Logic over atomic propositions emitted by an environment abstraction.

An atomic proposition is a boolean fact about the abstract state. Examples include agent_0_deadlocked, player_1_bad_delivery_attempt, door_0_open, and agent_1_queue_yield_ok. A label is the set of atomic propositions true in the current abstract state.

Global Formulas

Each benchmark exposes one or more named global formulas. Many formulas use the {agent} placeholder, which is specialized over the concrete agent ids before monitor construction. For example:

G(!{agent}_deadlocked)

becomes a concrete global formula over all agents in Flatland. The global formula is the safety story checked by the outer monitor.

Monitors

The shielding stack compiles safety formulas into deterministic monitors. A monitor state records how much of the safety obligation remains feasible after the labels seen so far. Entering a rejecting monitor state means the observed trace has violated the formula.

Spot is required for monitored, shielded, and contract experiments. The CLI tools ltlfilt, ltl2tgba, and autfilt must be on PATH; monitor construction and assume-guarantee checks fail fast if they are missing. When the Python Spot bindings are also importable, the automaton backend can use them for compilation, but the CLI tools remain required for validation and contract-synthesis checks.

Safety Abstractions

Every supported environment has a safety model under src/environments. The model is responsible for:

  • listing concrete agent ids,
  • exposing all labels it can emit,
  • mapping the live environment to an abstract state,
  • enumerating local and joint action effects,
  • producing the label for each abstract state.

Some models also define a safety projection. The projection collapses reward-only details when building product graphs, while exact transition kernels retain the details needed for reward and termination behavior.