令S0为一个状态集合，要求其从该状态集合出发所能到达的所有状态的集合S。根据定义，计算时应从S0开始，利用前向可达性计算操作image进行迭代计算，最后得到的最小不动点就是所有能到达的状态集合S。下面给出可达性计算的算法：
　　　　Reachability_Analysis(S0) {
　　　　　S = S0; // 从S0出发。
　　　　　do {
　　　　　　　S_Reached = S; //保存当前状态集合。
　　　　　　　S = S ú image(S) //image(S)表示S中个状态的下一状态，并在状态集合中。
　　　　　　　} until S_Reached = S; //如果某一次循环找不到新的状态，循环结束。
　　　　　return S; // 返回的S就是找到的所有状态的集合
　　　　}
　　从S0出发，找到S0的次态，形成状态集合S；在S的基础上再找S中各状态的次态，形成新的状态集合S；这样一步步找下去，直到再找到的次态中不出现新的状态为止。对于局有多条路径的情况来说，这种方法实际上就是广度优先搜索法。
　　请注意，其中所有的布尔操作都可以使用BDD实现，而且image操作也可以使用BDD实现。在该算法中，计算结果保存在变量S中，S的初始值设为S0，作为可达性计算的起始状态集合。然后开始进行迭代计算，直至没有新的状态加入。此时即达到了最小不动点，整个计算完成。因为问题的对象是一个有限的状态空间，因此能访问到所有状态，从而保证该算法能正常终止。
　　所谓不动点，就是下一次迭代的结果没有变化，即没有新的状态。最小不动点是不能再添加新的状态的情况，最大不动点是不能再去除新状态的情况。该术语后面还会出现，请读者注意。