ATTENTION/WARNING - NE PAS DÉPOSER ICI/DO NOT SUBMIT HERE

Ceci est la version de TEST de DIAL.mem. Veuillez ne pas soumettre votre mémoire sur ce site mais bien à l'URL suivante: 'https://thesis.dial.uclouvain.be'.
This is the TEST version of DIAL.mem. Please use the following URL to submit your master thesis: 'https://thesis.dial.uclouvain.be'.
 

Visualization of binary decision diagram

Dollé, Xavier
(2016)

Files

Dollé_70500800_2016.pdf
  • UCLouvain restricted access
  • Adobe PDF
  • 640.49 KB

Details

Supervisors
Pecheur, Charles ; Busard, Simon
Faculty
Ecole polytechnique de Louvain
Degree label
Master [120] en sciences informatiques
Abstract
A binary decision diagram allows to represent a boolean function as direct acyclic graph structure and is very useful to explore very large state spaces. This data structure is widely used in NuSMV, a symbolic Model checker based on BDDs. Because of its compressed nature, it is quite difficult to represent a binary decision diagram (BDD) in an intelligible way. A direct representation of this data structure could be too large and complex to be understood. This thesis presents different visualization possibilities of BDDs integrated in PyNuSMV, a Python framework including BDD-based model checking based on NuSMV. The main topic will be to overcome the binary nature of this structure doing a decimal translation of it.