% Future timed temporal operators rho(eventually[a,b] φ, w, t) = -∞ if t + a ≥ |w| max_{t' in ([0, t] intersect [t+a, t+b])} ρ(φ, w, t') otherwise [0,t] intersect [t+a, t+b] does not result in any interval, did you mean [0,|w|] intersect [t+a, t+b]?