我们采用"(M, s) |= f"这个符号来表示在有限状态机模型M中的s状态下CTL性质f 成立。由此，CTL公式f 可以解释为满足f 的状态集合，即{s | (M, s) |= f}。本文对于公式本身以及使该公式为真的状态集合两者不加以区别。在这种解释下，CTL操作可以按下述定义进行计算：
　　· EX f = inverse_image( f )
　　· E[ f∪g ] = lfp Z [ g∨(f∧EX(Z))]
　　· EG f = gfp Z[ f∧EX(Z)]
其中，lfp Z[h(Z)] 和gfp Z[h(Z)]分别代表函数 h 的最小不动点和最大不动点。下面分别介绍计算这三种操作的算法。
　　EX f是求在其后继状态中满足 f的状态集合。因此，如果将公式f解释为使f为真的状态的集合，则EX f实际就是求f的前驱，也就是执行一次前面介绍的逆向搜索inverse_image(f)。
　　同理，E[f ∪g]所求得的状态集合，应符合下述条件：其中任何一个状态s，都存在一条从s开始的计算路径，在这条路径直到第一个g成立的状态之前的所有状态都应该满足f。因此，计算E[ f ∪g ]时就可以从g开始，并包括在满足f的情况下还能到达g的所有状态。换句话说，就是从g开始进行逆向的可达性计算，并在限制其前驱状态必须满足f的条件下逆向遍历整个状态空间。所有这样的状态的集合（即最后得到的最小不动点）就是满足E[f ∪g]的集合。