A local checking algorithm for Boolean Equation Systems

Jean-Claude Fernandez and Laurent Mounier

Rapport SPECTRE, 95-07, VERIMAG, Grenoble, March 1995

Abstract:

Given a boolean equation system (E) and one of its bound variables X_init, we propose a local algorithm for computing the solution delta(X_init) of (E). Two applications are presented in the framework of program verification: bisimulation checking, and model-checking for the alternation-free mu-calculus. The first one was studied early and an on the fly algorithm has been already, implemented within the CADP toolbox. In spite of its theoretical worst-case time complexity, it was successful in practice for on-the-fly verification of non trivial Lotos programs. From these interesting results, and since there is only an equivalence checker within CADP, the initial aim of the present work was to re-use this algorithm for alternation-free mu-calculus model checking. 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. This can be achieved by merging the on the fly checking and the strongly connected component detection. Thus, although allowing on-the-fly verification, its time complexity in the case of the mu-calculus matches the ones of already known algorithms.

15 pages

PDF

PostScript