Letteratura scientifica selezionata sul tema "Diagrammes de Décision Binaire (BDD)"

Cette dissertation introduit et formalise la notion de structures comme moyen mathématique de capturer diverses propriétés dans plusieurs domaines scientifiques. Nous définissons les représentations structurelles comme des arbres ou des graphes acycliques dirigés (DAG) de structures, où la sémantique globale est la composition des structures individuelles, permettant un raisonnement inductif et modulaire. Nous formaliserons les notions de représentations inductives et de représentations canoniquement inductives. Nous étudions les conditions nécessaires et suffisantes pour que les représentations structurelles soient canoniques, en introduisant le concept de « confluence structurelle », non formalisée auparavant, et en proposant plusieurs approximations. Nous appliquons notre théorie aux fonctions Booléennes, montrant qu'elle unifie la plupart des variantes de diagrammes de décision binaire tout en suggérant une manière systématique d'en concevoir de nouvelles. Enfin, nous discutons brièvement de leur mise en œuvre et des résultats expérimentaux encourageants, qui soutiennent notre affirmation selon laquelle les représentations basées sur la structure sont conçues pour une utilisation pratique
This dissertation introduces and formalizes the notion of structures as a mathematically sound way to capture various patterns in several domains across sciences. We introduce the notion of structure-based representations as essentially trees or directed acyclic graphs (DAG) of structures. The overall semantics is the composition of the individual structures which allows for inductive and modular reasoning. We formalize the intuitive notions of inductive representations and inductively canonical representations. We prove that the latter are, somewhat, equivalent to canonical structure-based representations. We study necessary and/or sufficient conditions under which structure-based representations are canonical, highlighting the need for a notion of "structural confluence" that was not formalized in previous work and for which we formalize several approximations in this dissertation. Structural confluence allows us to avoid various pitfalls associated with the usual (rewriting-rule oriented) notion of confluence, in particular, the difficulty to generally prove (or disprove) it without further assumptions. We apply our theoretical results to the case of Boolean functions. We show that our theory not only unifies most variants of Binary Decision Diagrams but also suggests new ones in a principled way. We briefly discuss their implementation and encouraging experimental results supporting our claim that structure-based representations are designed for practical use

Sont présentés les différents travaux que j'ai pu effectuer: dans le domaine des automates cellulaires et de leur programmation, puis les travaux portant sur les fonctions Booléennes et leur complexité.

The Discrete Controller Synthesis (DCS) technique is used for automatic generation of correct-by-construction hardware controllers. For a given plant (a state-based model), and an associated control specification (a behavioral requirement), DCS generates a controller which, composed with the plant, guarantees the satisfaction of the specification. The DCS technique used relies on binary decision diagrams (BDDs). The controllers generated must be compliant with standard RTL hardware synthesis tools. Two main issues have been investigated: the combinational explosion, and the actual generation of the hardware controller. To address combinational explosion, common approaches follow the "divide and conquer" philosophy, producing modular control and/or decentralized control. Most of these approaches do not consider explicit communication between different components of a plant. Synchronization is mostly achieved by sharing of input events, and outputs are abstracted away. We propose an incremental DCS technique which also applies to communicating systems. An initial modular abstraction is followed by a sequence of progressive refinements and computations of approximate control solutions. The last step of this sequence computes an exact controller. This technique is shown to have an improved time/memory efficiency with respect to the traditional global DCS approach. The hardware controller generation addresses the control non-determinism problem in a specific way. A partially closed-loop control architecture is proposed, in order to preserve the applicability of hierarchical design. A systematic technique is proposed and illustrated, for transforming the automatically generated control equation into a vector of control functions. An application of the DCS technique to the correction of certain design errors in a real design is illustrated. To prove the efficiency of the incremental synthesis and controller implementation, a number of examples have been studied.

Cette these aborde, d'un point de vue algorithmique, le probleme lie aux calculs et a la representation des modeles d'une formule de la logique propositionnelle. Notre approche est fondee sur les diagrammes de decision binaire (bdd). Ils permettent de representer facilement l'ensemble des modeles et d'y gerer l'incrementalite. Le premier travail propose dans ce memoire est une etude sur des ordres pour l'insertion de formules particulieres de la logique propositionnelle dans un bdd. Pour cela, nous proposons deux actions complementaires, la premiere pour reduire la taille du bdd (ordre sur les variables de la formule) et la seconde pour reduire le temps de calcul (strategie pour l'insertion). Ceci nous a permis de determiner certaines limites pour l'utilisation des bdd. Dans un second temps, nous proposons d'etendre le formalisme des formules a traiter afin de pouvoir prendre en compte la dynamicite dans les bdd. L'ajout de formules ne posant pas de probleme grace aux bdd, notre extension porte sur le maintien de la coherence lors de l'ajout ou de la suppression de formules. Nous proposons de resoudre le probleme a l'aide d'un codage judicieux et presentons comment appliquer ces travaux dans le cadre des problemes de satisfaction de contraintes dynamiques. Un impliquant premier peut etre vu comme la representation d'un ensemble de modeles. Une extension naturelle de nos travaux, nous a conduit a elaborer un algorithme de calcul et de gestion des impliquants premiers. Nous montrons ici, comment l'effectuer avec un couplage entre un algorithme enumeratif et un bdd. Des experimentations sont presentees pour illustrer et comparer les differentes approches proposees dans cette these.

Cette thèse traite des approches implicites et explicites, ainsi que de leur convergence, de l'exploration d'espace d'états atteignables de circuits logiques provenant de programmes réactifs synchrones écrits en Esterel, ECL ou SyncCharts. Nos travaux visent à réduire les coûts de ces explorations à l'aide de
techniques génériques ou spécifiques à notre cadre de travail. Nous utilisons les résultats de ces explorations à des fins de vérification formelle de propriétés de sûreté, de génération d'automates explicites ou de génération de séquences de tests exhaustives. Nous décrivons trois outils.
Le premier outil est un vérificateur formel implicite, à base de Diagrammes de Décisions Binaires (BDDs). Ce vérificateur présente plusieurs techniques permettant de réduire le nombre de variables impliquées dans les calculs d'espace d'états. Nous proposons notamment l'abstraction de variables à l'aide d'une logique trivaluée. Cette nouvelle méthode étend la technique usuelle de remplacement de variables d'états par des entrées libres. Ces deux méthodes calculant des sur-approximations de l'espace d'états atteignables, nous proposons différentes techniques utilisant des informations concernant la structure du modèle et permettant de réduire la sur-approximation.
Le deuxième outil est un moteur d'exploration explicite, basé sur l'énumération des états accessibles.
Ce moteur repose sur la simulation de la propagation du courant électrique dans les portes du circuit et supporte les circuits cycliques. Ce moteur comporte de nombreuses optimisations et fait appel à différentes heuristiques visant à éviter les explosions en temps ou en espace inhérentes à cette approche, ce qui lui
confère de très bonnes performances. Ce moteur a été appliqué à la génération d'automates explicites et à la vérification formelle.
Enfin, le troisième outil est une évolution hybride implicite/explicite du moteur purement explicite. Dans cette évolution, les états sont toujours analysés individuellement mais symboliquement à l'aide de BDDs. Ce moteur a également été appliqué à la génération d'automates explicites, mais il est plutôt destiné à la vérification formelle ou la génération de séequences de tests exhaustives.
Nous présentons des résultats d'expérimentations de ces différentes approches sur plusieurs exemples industriels.

Cette thèse présente des techniques de génération de code liées à la vérification dynamique de types de séquences hétérogènes mais régulières. Nous généralisons les expressions rationnelles classiques aux expressions rationnelles de type, en adaptant leur surface syntaxique, représentation interne, calcul, optimisation, et sérialisation (génération de code). Nous comparons la forme native basée sur des S-Expressions avec une représentation par Diagrammes de Décision Binaire, enrichis pour représenter les opérations booléennes dans un treillis de types prenant en charge le sous-typage. Nous introduisons alors la notion de Décomposition Maximale en Types Disjoints, nous prouvons l'existence et l'unicité d'une telle décomposition, et nous explorons plusieurs solutions algorithmiques pour calculer celle-ci. La Décomposition Maximale en Types Disjoints est utilisée pour générer un automate fini et déterministe représentant une expression rationnelle de type. Cet automate est utilisé à la compilation pour générer à son tour du code de vérification dynamique de type. Le code ainsi généré ne tient a priori pas compte d'éventuelles redondances dans les vérifications de type. Nous étudions donc ces problèmes plus en détail et utilisons à nouveau la théorie des Diagrammes de Décision Binaire afin d'éliminer les calculs redondants et de produire ainsi du code optimisé. Le travail présenté dans cette thèse s'attache à traiter des problèmes de représentations et de calcul sur des types dans les langages dynamiques
This thesis presents code generation techniques related to run-time type checking of heterogeneous but regular sequences. We generalize traditional regular expressions to accommodate surface syntax, internal representation, computation, optimization, and serialization (code generation) of rational type expressions. We explore traditional s-expression based representation contrasted with Binary Decision Diagrams which have been enhanced to represent Boolean operations in a type lattice supporting subtyping. We introduce the Maximal Disjoint Type Decomposition, prove the existence and uniqueness of a solution, and further explore several alternative algorithms for calculating it. The Maximal Disjoint Type Decomposition is used to generate a deterministic finite automaton representing a rational type expression, after which compile-time code is generated which will perform run-time type membership checks. Such code generation risks dealing with redundant type checks. We further investigate these potential problems and again use the theory of Binary Decision Diagrams to eliminate these redundant checks to produce optimized type checking code. The techniques and algorithms introduced and discussed in this thesis explore representations and computations dealing with type based computations in dynamic programming languages