Making prophecies with decision predicates shows how LTL can be lazily reduced to CTL with some help of automatically inferred "prophecy variables".
Temporal property verification as a program analysis problem shows how known tools can be used to prove CTL properties of infinite state programs