inria-00072795, version 1

Efficient Diagnostic Generation for Boolean Equation Systems

Radu Mateescu ¹

N° RR-3861 (2000)

• 1 :  VASY (Dijon) (INRIA Grenoble Rhône-Alpes)
• 
  INRIA France

Références bibliographiques

• Type de publication : Rapports
• Domaine : Informatique/Autre
• Titre : Efficient Diagnostic Generation for Boolean Equation Systems
• Résumé : 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.
• Langue du document : Anglais
• Date de publication : 01/2000
• Mots-clés : BOOLEAN EQUATION SYSTEM / DIAGNOSTIC / MODEL-CHECKING / MU-CALCULUS / TEMPORAL LOGIC / SPECIFICATION / VERIFICATION
• Date de rédaction : 01/2000
• Référence interne : RR-3861

Liste des fichiers attachés à ce document :

• inria-00072795, version 1
• http://hal.inria.fr/inria-00072795
• oai:hal.inria.fr:inria-00072795
• Contributeur : Rapport De Recherche Inria <>
• Soumis le : Mercredi 24 Mai 2006, 10:57:44
• Dernière modification le : Mercredi 31 Mai 2006, 14:24:27