A local checking algorithm for Boolean Equation Systems

Given a boolean equation system E and one of its bound variables X init , we propose a local algorithm for computing the solution ffi (X init ) of E . This algorithm relies on depth-first traversals of the dependency graph of E : the boolean equation system is solved during the depth-first search, and the algorithm terminates as soon as the value obtained for X init is correct. Two applications are presented in the framework of program verification: bisimulation checking, and model-checking for the alternation-free ¯-calculus. This algorithm has been implemented within the Caesar-Ald' ebaran toolbox and experimental results on rather large examples demonstrated its practical interest. 1 Introduction In 1991 we proposed an algorithm for computing various bisimulation relations between two labeled transition systems (lts) [FM91]. The main feature of this algorithm is to rely on a depth-first traversal of a synchronous product of the two ltss. Thus, it does not require to store in memo..