Skip to content

Concepts

This page defines the terms used across the codebase and notebooks.

Agents And Policy Profiles

An agent is one learner in a PettingZoo-style parallel environment. A policy profile is the collection of one policy per agent. Training produces a policy profile; verification asks how that profile behaves when evaluated jointly or when one agent deviates.

The project usually names agents as player_0, player_1, and so on. Environments are expected to expose one temporal specification for every agent in env.possible_agents.

Finite-Trace Temporal Goals

The repository uses LTLf-style formulas over finite episodes. Common operators include:

  • F p: eventually proposition p becomes true.
  • G p: proposition p is always true.
  • X p: proposition p is true at the next step.
  • !, &, and |: not, and, or.

Examples:

F player_0_resource_claimed
G !guard_intruder_collision
F (both_stag & X (both_stag & G !unmirrored))

Each formula is parsed by flloat and converted into a deterministic automaton. The automaton state tracks how much of the temporal goal has been satisfied or failed so far.

Temporal Atoms

Atoms are Boolean propositions produced by environment label mixins. They should describe domain events, not verifier results.

Good atoms are concrete:

  • player_i_apple_collected
  • player_i_resource_claimed
  • guard_intruder_collision
  • both_stag

Avoid using atoms such as nash, equilibrium, or alpharank. Those are properties of a learned policy profile and are checked after training.

Reward Monitors

BoolRewardWrapper attaches one Boolean monitor per agent. On each environment step:

  1. The wrapped environment returns observations, native rewards, done flags, and infos.
  2. The environment label mixin computes the current atom valuation.
  3. Each agent's monitor advances through its automaton.
  4. At the end of an episode, the wrapper gives objective reward 1.0 if the agent's monitor is accepting and 0.0 otherwise.

The default reward mode is objective, which means the learner trains directly on the terminal satisfaction bit. Some experiments also expose handcrafted baselines that train on shaped or native rewards while still tracking objective satisfaction.

See the Monitor API for the wrapper, monitor, and counterfactual replay reference.

Temporally Extended Observations

Many temporal goals are non-Markovian in the raw environment state. By default, the reward wrapper appends the monitor-state id to each agent's observation. This exposes temporal progress to the learner and is required by counterfactual replay.

The temporal wrapper currently assumes flat-compatible gymnasium.spaces.Box values. Visual gridworld experiments therefore request rgb_array and convert native RGB dictionaries into pooled, normalized tensors before the LTLf wrapper appends monitor state. Direct render_mode=None environments instead expose low-memory structured observations.

Satisfaction

Satisfaction is the event that a finite episode ends in an accepting monitor state for an agent's formula. Training curves usually plot rolling or exponentially weighted averages of these terminal satisfaction bits.

Final satisfaction evaluation estimates this probability with fresh rollouts and reports Hoeffding confidence intervals.

Equilibrium

Equilibrium is not encoded in the temporal formula. In this repo, equilibrium is estimated after training by freezing a learned policy profile and asking whether a unilateral best response can improve an agent's objective satisfaction probability.

This is intentionally model-free: the verifier uses rollouts and learned deviation policies rather than an explicit transition model.