下面给出了计算E[ f ∪g ]的算法。
　　Check_EU(f, g) { /* compute E[f ∪g] */
　　　　Y = g; 　　　/* 最小不动点的初始值 */
　　　　DeltaY = g;　/* 每次迭代后Y的变化 */
　　　　do {
　　　　　　pY = f∧pre_image(DeltaY);
　　　　　　DeltaY = pY∧(┐Y);
　　　　　　Y = Y∨DeltaY;
　　　　} while (DeltaY≠false);
　　　　return Y;
　　}
　　请注意，其中所有的布尔操作都可以使用BDD实现，而且pre-image操作也可以使用BDD实现。在该算法中，最小不动点的计算结果保存在变量Y中，Y的初始值设为g，作为逆向可达性计算的起始状态集合。变量DeltaY存储新增加的状态，初始也设为g。然后该算法开始进行迭代计算，首先计算满足f并且能在一步逆向可达性计算中从DeltaY可以到达的状态集合。然后更新新到达的状态集合和已经到达的状态集合。如此迭代直至没有新的状态加入。此时即达到了最小不动点，整个计算完成。因为问题的对象是一个有限的状态空间，因此能访问到所有状态，从而保证该算法能正常终止。
　　EG f所求得的状态集合，应符合下述条件：其中任何一个状态s，都存在一条从s开始的计算路径p，在该路径上所有的状态始终满足f。根据这一定义，可以通过下述方法来递归地计算EG f ：
　　EG f在状态s成立当且仅当f在s成立并且EG f在s的某些后继状态也成立。用数学语言即表示为：
　　　　　　EG f ＝ f∧EX( EG f)
该等式说明EG f 为函数h(Z) = f ù EX Z的一个不动点。
　　下面给出了计算该不动点的算法：
　　Check_EG(f) { /* 求 EG f */
　　　　Y = f; /* 最大不动点的初始值*/
　　　　do {
　　　　　　Y' = Y; /* 保存Y上一次的值*/
　　　　　　Y = Y∧pre_image(Y);
　　　　} while (Y≠Y'); /*若Y=Y',表明没有新的状态去除，表明是一个最大不动点*/
　　　　return Y;
　　} 　　在计算得到这些满足CTL公式的状态集合T之后，只需要检查S是否为T的一个子集（即 ┐S(V) ∨ T(V) = true）。如果为真，则说明该系统满足该CTL公式。
　　S为T的一个子集，说明状态表示的功能都满足CTL的描述。