Skip to content

Monitor API

The monitor layer turns finite-trace LTLf formulas into per-agent terminal objective rewards. It also exposes the small state-machine surface needed by counterfactual replay.

Core Types

Configuration for reward-monitor observation augmentation.

temporally_extended = True class-attribute instance-attribute

Append the current monitor-state id to each learner observation.

Reward-monitor specification for one agent.

If agent_id is None, the spec is treated as shared and applied to all agents in a parallel PettingZoo environment.

agent_id = None class-attribute instance-attribute

Agent id this formula belongs to.

formula_str instance-attribute

Finite-trace LTL formula parsed by flloat.

reward_scalar = 1.0 class-attribute instance-attribute

Reward scalar retained for monitor construction; objective rewards are terminal 0/1 bits.

Per-agent episode summary stored by BoolRewardWrapper.

cum_reward instance-attribute

Objective cumulative reward kept for backward-compatible plotting.

ep_len instance-attribute

Number of environment steps in the episode.

episode instance-attribute

Running episode index.

handcrafted_cum_reward = None class-attribute instance-attribute

Learner reward for handcrafted baselines, when applicable.

learner_cum_reward = None class-attribute instance-attribute

Reward actually returned to the learner.

objective_cum_reward = None class-attribute instance-attribute

Cumulative terminal objective reward.

start_step = None class-attribute instance-attribute

Global timestep at the first step of the episode, when known.

t_end instance-attribute

Global timestep at episode termination or truncation.

Finite-trace LTLf monitor backed by a deterministic automaton.

Bases: BaseParallelWrapper

PettingZoo Parallel reward wrapper
  • One BoolMonitor per agent (one LTLf spec per agent).
  • label() is shared (computed once per step).
  • Rewards are monitor-based.
  • Tracks EpisodeLog per agent across episodes.

export(to_file=True, dir='exports', filename='bool_rm.dot')

Export one automaton per agent monitor.

  • If filename contains "{agent}", it will be formatted with the agent id. Example: filename="rm_{agent}.dot"
  • Otherwise, we append the agent id before the extension: "bool_rm.dot" -> "bool_rm_player_0.dot"
  • If filename includes subdirectories (e.g. "graphs/rm.dot"), they are created too.

label(infos=None, **kwargs)

Override in subclass. Should return dict[str,bool] (shared labels, applied to every agent). Possibly extensible to agent-specific labels, with type: dict[agent_id, dict[str,bool]]

Counterfactual Replay

Agent-specific DFA adapter used by counterfactual replay.

Relabeled monitor-state trajectory for one factual rollout window.

Split augmented observations into base observations and monitor ids.

Append monitor ids as the final feature of a base observation batch.

Build next-observation monitor ids from current ids and a final id.

Find the reward wrapper and return replay-ready monitor models.

Read the true LTLf propositions written into step infos.

Return only the monitor-state component of augmented observations.

Return augmented observations with replacement monitor-state ids.

Enumerate unique LTLf monitor relabelings for a factual trajectory.