Skip to Main content Skip to Navigation
Reports

Ordered Functional Decision Diagrams: A Functional Semantic For Binary Decision Diagrams

Joan Thibault 1 Khalil Ghorbal 1
1 HYCOMES - Modélisation hybride & conception par contrats pour les systèmes embarqués multi-physiques
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Résumé : Les Diagrammes de Décision Binaires (BDD) sont une structure qui a été décliné en de nombreux variants, chacun conçu pour exploiter au mieux une propriété particulière des fonctions Booléennes et ainsi réduire leur taille mémoire. Cependant, décider quel variant est le plus adapté à priori est aussi difficile que construire chaque représentation. De plus la conversion entre les variants coûte également trop chère pour être utilisable en pratique. Ces observations ont conduit naturellement à un intérêt grandissant pour combiner des variants pour tirer parti de leurs avantages respectifs. Cet article introduit un cadre théorique à cette problématique en introduisant une méta-structure nommée \lambdaDD qui adopte un point de vue purement fonctionnel sur les BDD. Les diagrammes λDD permettent d'abstraire les variants classiques (par exemple ROBDD et ZDD) ainsi que des variants récents (en particulier ChainDD et ESRBDD) comme des modèles d'une classe de modèles ordonnés que nous appelons λDD-O Dans ces modèles ordonnés, les variables sont évaluées en suivant un ordre global strict. Nous énumérons les éléments de cette classe et isolons son modèle le plus expressif que nous nommons λDD-O-NUCX. Ce modèle permet non seulement de capturer les variables canalisantes (ce qui le rend plus expressif que ESRBDD par exemple) mais exploite aussi une propriété supplémentaire: les xor-variables. Le modèle est également invariant par négation, ce qui permet de calculer la négation d'une fonction Booléenne en temps constant. La canonicité de λDD-O-NUCX est formellement vérifiée en utilisant l'assistant de preuve Coq. De plus, nous fournissons des résultats expérimentaux confirmant l'intérêt de λDD-O-NUCX.
Complete list of metadatas

https://hal.inria.fr/hal-02512117
Contributor : Joan Thibault <>
Submitted on : Thursday, March 19, 2020 - 2:18:52 PM
Last modification on : Wednesday, June 24, 2020 - 4:19:51 PM
Document(s) archivé(s) le : Saturday, June 20, 2020 - 2:35:46 PM

Licence


Copyright

Identifiers

  • HAL Id : hal-02512117, version 1
  • ARXIV : 2003.09340

Citation

Joan Thibault, Khalil Ghorbal. Ordered Functional Decision Diagrams: A Functional Semantic For Binary Decision Diagrams. [Research Report] RR-9333, Inria. 2020. ⟨hal-02512117⟩

Share

Metrics

Record views

59

Files downloads

326