A note on the characterization of TL[EF]

In this note, we give a new proof for Bojańczyk and Walukiewicz's effective characterization of TL[EF] (the fragments of Computation Tree Logic (CTL), with EF modality only) following the Ehrenfeucht–Fraïssé game approach. Then, we extend the proof to the effective characterization of TL[EFns] (Fns is the non-strict “future” temporal operator, while F is the strict one).