**Efficient Diagnostic Generation for Boolean Equation Systems**

*Radu Mateescu*

Proceedings of the 6th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems
TACAS'2000 (Berlin, Germany), March 2000

Full version available as INRIA Research Report RR-3861.

** Abstract:**

Boolean Equation Systems (BESs) provide a useful framework for the verification of concurrent finite-state systems. In practice, it is desirable that a BES resolution also yields diagnostic information explaining, preferably in a concise way, the truth value computed for a given variable of the BES. Using a representation of BESs as extended boolean graphs (EBGs), we propose a characterization of full diagnostics (i.e., both examples and counterexamples) as a particular class of subgraphs of the EBG associated to a BES. We provide algorithms that compute examples and counterexamples in linear time and can be straightforwardly used to extend known (global or local) BES resolution algorithms with diagnostic generation facilities.

23 pages | PostScript |

Cumulated slides about EVALUATOR 3.0 by R. Mateescu |