 An infinite computation is formally represented by a model of the linear time temporal logic LTL. Non-deterministic systems are modeled by branching time structures. Thus, both LTL and the computation tree logics CTL and CTL* have been very important for specification and verification of reactive and concurrent systems.