Skip to content

LTLf Counterfactual Replay Design

The temporal-game trainers and all current environment suites support opt-in LTLf counterfactual replay (CER).

Scope

  • CER is enabled with COUNTERFACTUAL_REPLAY=True inside the trainer configs.
  • The experiment suites expose this as separate variants:
  • IPPO_CER
  • PR2_IPPO_CER
  • IQL_CER
  • PR2_IQL_CER
  • NASHQ_CER
  • The public suite flags are:
  • run_ippo_cer
  • run_pr2_ippo_cer
  • run_iql_cer
  • run_pr2_iql_cer
  • run_nashq_cer

CER is only supported for temporally-extended LTLf wrapper runs where the monitor state id is appended to the observation. The trainer probes the environment and fails fast if the wrapper does not expose counterfactual monitor support.

Monitor-Side Contract

The LTLf wrapper exposes the minimum state-machine surface needed for relabeling:

  • initial_state_id()
  • state_ids
  • successor_state_id(state_id, true_props)
  • is_accepting_state_id(state_id)

BoolRewardWrapper.step() also writes the true proposition set seen on that transition into info["ltlf_true_props"]. CER uses that label sequence to replay deterministic DFA transitions from alternative monitor states without changing the underlying environment transition.

The shared relabeling logic lives in src/monitor/counterfactual.py.

Relabeling Rule

For a stored rollout chunk or one-step transition:

  • Environment observations stay fixed except for the appended monitor-state component.
  • Actions stay fixed.
  • done stays fixed.
  • opponent_index stays fixed for PR2 methods.
  • Only the monitor-state path and the terminal 0/1 reward bit are recomputed.

The relabeler enumerates all alternative monitor start states, rolls DFA transitions over the observed label sequence, and deduplicates variants by:

  • relabeled monitor-state sequence
  • relabeled next-monitor-state sequence
  • relabeled reward sequence

The factual sample is always included exactly once.

Inside a rollout window, if a factual transition ended an episode, CER reapplies the chosen alternative start state at the next reset boundary before continuing the relabeled monitor rollout.

Trainer Integration

IQL / PR2-IQL

CER is applied at replay insertion time.

  • Each factual rollout window produces one or more relabeled transition sequences.
  • The factual sequence continues its environment stream across rollout updates.
  • Each synthetic sequence is assigned a fresh stream id and starts at an explicit recurrent reset, so replay cannot join unrelated monitor histories.
  • All variants use the same materialized replay schema with both obs and next_obs.
  • PR2-IQL preserves the factual opponent_index sequence across relabeled sequences.

Nash-Q

CER is applied online per observed step.

  • Each factual joint transition is expanded into multiple relabeled joint observation keys.
  • The same joint action is used for every relabeled update.
  • The next-state continuation value is computed from the relabeled next-state key.
  • Best-response mode still works: the active learner uses relabeled states while frozen opponents continue to use the frozen tables.
  • Joint counterfactual expansion is budgeted by COUNTERFACTUAL_MAX_JOINT_VARIANTS, which defaults to 1024.
  • None or values <= 0 keep full enumeration.
  • When the Cartesian product is at or below the cap, Nash-Q enumerates it exactly. When it is above the cap, Nash-Q always includes the factual joint transition and then samples deduplicated joint variants with the trainer's seeded NumPy RNG until the cap is reached.

IPPO / PR2-IPPO

PPO cannot safely reuse the factual rollout log_prob fields for synthetic samples, so the PPO variants rebuild rollout statistics after relabeling.

For CER updates:

  • factual and synthetic trajectories are concatenated per agent
  • rollout-time fields are recomputed under the pre-update policy snapshot
  • batches are padded in trajectory-count space to a stable per-agent monitor-state upper bound and then to NUM_MINIBATCHES divisibility
  • padded slots carry zero masks, and PPO losses/advantage normalization use masked means so synthetic padding does not alter sample weighting
  • JAX key-derived rollout seeds are preserved during seed coercion, so counterfactual padding no longer collapses parallel environment seeds.

IPPO recomputes:

  • value
  • log_prob

PR2-IPPO recomputes:

  • log_prob
  • response-aware advantage

PR2-IPPO targets continue to be derived from the relabeled next_obs batch inside the update step.

IPPO-CER caveat

Recomputing log_prob and value/advantage fields prevents internally stale PPO statistics, but it does not make a relabeled trajectory on-policy. Its action was sampled from the factual monitor-state history, not from the policy conditioned on the synthetic monitor-state history. Relabeling also changes the state-action occupancy distribution. The same limitation applies to the response-aware quantities in PR2-IPPO-CER.

Accordingly, IPPO-CER and PR2-IPPO-CER are biased replay heuristics, not canonical on-policy PPO estimators. There is currently no importance-sampling or occupancy-ratio correction in these trainers. Keep base IPPO/PR2-IPPO as the on-policy baselines and interpret CER comparisons as empirical ablations.

Why This Is LTLf-Specific

This is not the Buchi jump-transition construction from the LCER paper. For finite-trace LTLf:

  • monitors are DFAs, not Buchi automata
  • there are no epsilon/jump transitions to model
  • satisfaction is still determined by the terminal accepting condition

CER here is best described as an LTLf-specific counterfactual replay scheme inspired by LCER.

Main Files

  • src/monitor/reward_monitor.py
  • src/monitor/reward_wrapper.py
  • src/monitor/counterfactual.py
  • src/rl/iql.py
  • src/rl/pr2_iql.py
  • src/rl/ippo.py
  • src/rl/pr2_ippo.py
  • src/rl/nash_q.py
  • src/experiments/temporal_game_experiment.py
  • src/experiments/pursuit_experiment.py

Current Limitations

  • CER assumes the monitor state is the final observation component.
  • IPPO-CER and PR2-IPPO-CER are biased because factual actions and visitation frequencies are reused under synthetic monitor histories.
  • Nash-Q caps joint Cartesian expansion, but each agent's per-monitor-state variants are still generated before the joint budget is applied. Very large automata can still be expensive before sampling begins.