Skip to content

LTLf Rewards And Discounting

This repo's current LTLf monitor setup is not implementing the "eventual discounting" surrogate from Voloshin et al., Eventual Discounting Temporal Logic Counterfactual Experience Replay (arXiv:2303.02135).

Current behavior

src/monitor/reward_wrapper.py gives each agent:

  • reward 0.0 on every non-terminal step
  • reward 1.0 on the terminal step iff the final monitor state is accepting
  • reward 0.0 on the terminal step otherwise

That means the wrapper encodes a Bernoulli success signal for finite-trace objective satisfaction:

  • cum_reward == 1 means the episode's finite trace satisfied the LTLf formula
  • cum_reward == 0 means it did not

This is the behavior assumed by the plotting utilities in src/visualisation/ltlf_success_common.py.

Why this differs from the paper

The paper studies infinite-trace LTL with a Buchi-style accepting set and uses "eventual discounting":

  • reward 1 whenever the automaton is in an accepting state
  • discount factor gamma is applied only when the current automaton state is accepting
  • non-accepting stretches are effectively undiscounted

That construction is meant to approximate probability of LTL satisfaction without introducing the usual myopic bias toward policies that revisit accepting states quickly.

For LTLf, that idea does not transfer directly:

  • there is no Buchi recurrence condition
  • acceptance is about the final finite trace, not infinite revisits
  • an accepting DFA state may be visited before the episode ends

Examples from flloat:

  • F a: once a has happened, the automaton stays accepting
  • G !a: the initial state is accepting, but leaving it can later make the whole trace rejecting

So paying reward every time an LTLf automaton is in an accepting state would generally be the wrong objective. The current "terminal 0/1 only" wrapper is the right shape for finite-trace satisfaction.

Where time preference still enters

Even though the wrapper is terminal-only, the trainers still use standard RL discounting in their Bellman/return targets, e.g.:

  • src/rl/iql.py
  • src/rl/pr2_iql.py
  • src/rl/pr2_ippo.py

So with variable episode lengths, the learned objective is:

E[gamma^(T-1) * 1{satisfied}]

instead of pure satisfaction probability:

P[satisfied]

Consequences:

  • if two policies have the same satisfaction probability but one succeeds earlier, standard discounting prefers the earlier one
  • if one policy succeeds later but with higher probability, discounting can still prefer a lower-probability faster policy
  • this bias disappears only when all episodes have the same length, because the factor gamma^(T-1) is then a policy-independent constant

Practical interpretation for this repo

If the intended objective is:

  • maximize LTLf satisfaction probability: use terminal 0/1 reward and set learner discount as close to 1 as practical, ideally 1 in finite-horizon settings if the algorithm remains stable

  • trade off success probability against speed of success: keep terminal 0/1 reward and choose gamma < 1

That second objective is valid, but it is no longer "pure probabilistic satisfaction"; it explicitly values earlier successful termination more highly.