Skip to Main content Skip to Navigation
Reports

Efficient Diagnostic Generation for Boolean Equation Systems

Radu Mateescu 1
1 VASY - System validation - Research and applications
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
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.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00072795
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 10:57:44 AM
Last modification on : Thursday, November 19, 2020 - 1:00:27 PM
Long-term archiving on: : Sunday, April 4, 2010 - 9:05:38 PM

Identifiers

  • HAL Id : inria-00072795, version 1

Collections

Citation

Radu Mateescu. Efficient Diagnostic Generation for Boolean Equation Systems. RR-3861, INRIA. 2000. ⟨inria-00072795⟩

Share

Metrics

Record views

207

Files downloads

383