HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 10:57:44 AM
Last modification on : Friday, February 4, 2022 - 3:24:28 AM
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

71

Files downloads

170