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 class-attribute instance-attribute 

temporally_extended: bool = True

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 class-attribute instance-attribute 

agent_id: str | None = None

Agent id this formula belongs to.

formula_str instance-attribute 

formula_str: str

Finite-trace LTL formula parsed by flloat.

reward_scalar class-attribute instance-attribute 

reward_scalar: float = 1.0

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

Per-agent episode summary stored by BoolRewardWrapper.

cum_reward instance-attribute 

cum_reward: float

Objective cumulative reward kept for backward-compatible plotting.

ep_len instance-attribute 

ep_len: int

Number of environment steps in the episode.

episode instance-attribute 

episode: int

Running episode index.

handcrafted_cum_reward class-attribute instance-attribute 

handcrafted_cum_reward: float | None = None

Learner reward for handcrafted baselines, when applicable.

learner_cum_reward class-attribute instance-attribute 

learner_cum_reward: float | None = None

Reward actually returned to the learner.

objective_cum_reward class-attribute instance-attribute 

objective_cum_reward: float | None = None

Cumulative terminal objective reward.

start_step class-attribute instance-attribute 

start_step: int | None = None

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

t_end instance-attribute 

t_end: int

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 

export(
    to_file: bool = True,
    dir: str = "exports",
    filename: str = "bool_rm.dot",
) -> Dict[AgentID, graphviz.Digraph]

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 

label(
    infos: Optional[Dict[AgentID, Dict[str, Any]]] = None,
    **kwargs,
) -> LabelReturn

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.