Thèses sur le sujet « Diagramme de décision »

Les diagrammes de décision Multi-valués (MDD) sont des structures de données efficaces et largement utilisées dans les domaines tels que la vérification, l’optimisation et la programmation dynamique. Dans cette thèse, nous commençons par améliorer les principaux algorithmes tels que la réduction de MDD, permettant aux MDD de potentiellement compresser exponentiellement des ensembles de tuples, ou la combinaison de MDD, tels que l’intersection ou l’union. Ensuite, nous proposons des versions parallèles de ces algorithmes ainsi que des versions permettant de travailler avec la version non déterministe des MDD. De plus, dans le domaine des MDD relâchés, un domaine de plus en plus étudié, nous définissons les notions de réduction et combinaison relâchés, ainsi que leurs algorithmes associés. Nous résolvons le problème de l’échantillonnage des solutions d’un MDD avec respect de loi de probabilité tels que des fonctions de probabilité de masse ou des chaines de Markov. Pour permettre d’utiliser les MDD dans les solveurs de programmation par contraintes, nous proposons de nouveaux propagateurs pour toutes les contraintes basées sur des MDD, améliorant les performances des algorithmes existants, puis nous en introduisons une nouvelle contrainte, la contrainte de channeling. Grâce à eux, nous montrons que nous pouvons reformuler plusieurs contraintes et en définir de nouvelles tout en étant basés sur des MDD. Finalement nous appliquons nos algorithmes à des problèmes industriels réels de génération de texte et musique, et de modélisation de réservoir de pétrole
Multivalued Decision Diagrams (MDDs) are efficient data structures widely used in several fields like verification, optimization and dynamic programming. In this thesis, we first focus on improving the main algorithms such as the reduction, allowing MDDs to potentially exponentially compress set of tuples, or the combination of MDDs such as the intersection of the union. We go further by designing parallel algorithms, and algorithms handling non-deterministic MDDs. We then investigate relaxed MDDs, that are more and more used in optimization, and define the notions of relaxed reduction or operation and design efficient algorithms for them. The sampling of solutions stored in a MDD is solved with respect to probability mass functions or Markov chains. In order to combine MDDs with constraint Programming, we design the propagators of all the types of MMDD constraints in solvers, and introduce a new one, the channeling constraint. These new propagators outperform the existing ones and allow the reformulation of several other constraints such as the dispersion constraint, and even to define new ones easily. We finally apply our algorithm to several real world industrial problems such as text and music generation and geomodeling of a petroleum reservoir

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é.

L’intérêt des différents langages de la famille des diagrammes de décisionvalués (VDD) est qu’ils admettent des algorithmes en temps polynomialpour des traitements (comme l’optimisation, la cohérence inverse globale,l’inférence) qui ne sont pas polynomiaux (sous l’hypothèse P 6= NP), si ilssont effectués sur le problème dans sa forme originale tel que les réseaux decontraintes ou les réseaux bayésiens.Dans cette thèse, nous nous intéressons au problème de configuration deproduit, et plus spécifiquement, la configuration en ligne avec fonction de valuationassociée (typiquement, un prix). Ici, la présence d’un utilisateur enligne nous impose une réponse rapide à ses requêtes, rapidité rendant impossiblel’utilisation de langages n’admettant pas d’algorithmes en temps polynomialpour ces requêtes. La solution proposée est de compiler hors-ligneces problèmes vers des langages satisfaisant ces requêtes, afin de diminuer letemps de réponse pour l’utilisateur.Une première partie de cette thèse est consacrée à l’étude théorique desVDD, et plus particulièrement les trois langages Algebraic Decision Diagrams,Semi ring Labelled Decision Diagrams et Affine Algebraic Decision Diagrams(ADD, SLDD et AADD). Nous y remanions le cadre de définition des SLDD,proposons des procédures de traductions entre ces langages, et étudions la compacitéthéorique de ces langages. Nous établissons dans une deuxième partie lacarte de compilation de ces langages, dans laquelle nous déterminons la complexitéalgorithmique d’un ensemble de requêtes et transformations correspondantà nos besoins. Nous proposons également un algorithme de compilationà approche ascendante, ainsi que plusieurs heuristiques d’ordonnancement devariables et contraintes visant à minimiser la taille de la représentation aprèscompilation ainsi que le temps de compilation. Enfin la dernière partie estconsacrée à l’étude expérimentale de la compilation et de l’utilisation de formescompilées pour la configuration de produit. Ces expérimentations confirmentl’intérêt de notre approche pour la configuration en ligne de produit.Nous avons implémenté au cours de cette thèse un compilateur (le compilateurSALADD) pleinement fonctionnel, réalisant la compilation de réseauxde contraintes et de réseaux bayésiens, et avons développés un ensemble defonctions adaptées à la configuration de produit. Le bon fonctionnement etles bonnes performances de ce compilateur ont été validés via un protocole devalidation commun à plusieurs solveurs
The different languages from the valued decision diagrams (VDD) family benefitfrom polynomial-time algorithms for some tasks of interest (such as optimization,global inverse consistency, inference) for which no polynomial-timealgorithm exists (unless P = NP) when the input is a constraint network ora Bayesian network considered at start.In this thesis, we focus on configuration product problems, and more specificallyon-line configuration with an associated valuation function (typically, aprice). In this case, the existence of an on-line user forces us to quickly answerto his requests, making impossible the use of languages that does not admitpolynomial-time algorithm for this requests. Therefore, our solution consistsin an off-line compilation of these problems into languages that admit suchpolynomial-time algorithms, and thus decreasing the latency for the user.The first part of this thesis is dedicated to the theoretical study of VDDs,an more specifically Algebraic Decision Diagrams (ADDs), Semi ring LabelledDecision Diagrams (SLDDs) and Affine Algebraic Decision Diagrams(AADDs). We revisit the SLDD framework, propose translation proceduresbetween these languages and study the succinctness of these languages. In asecond part, we establish a knowledge compilation map of these languages,in which we determine the complexity of requests and transformations correspondingto our needs. We also propose a bottom-up compilation algorithmand several variables and constraints ordering heuristics whose aim is to reducethe size of the compiled form, and the compilation time. The last partis an experimental study of the compilation and the use of the compiled formin product configuration. These experimentations confirm the interest of ourapproach for on-line product configuration.We also implemented a fully functional bottom-up compiler (the SALADDcompiler), which is capable of compiling constraints network and Bayesian networkinto SLDDs. We also developed a set of functions dedicated to productconfiguration. The proper functioning and good performances of this programwas validated by a validation protocol common to several solvers

La problématique abordée dans cette thèse est la conception d'un modèle informatique qui permet de générer automatiquement les rétroactions épistémiques en se basant sur l'état de connaissance de l'apprenant et en prenant ainsi en compte la dimension didactique de la connaissance. Ce travail se situe dans le cadre d'un environnement informatique pour l'apprentissage de la formation professionnelle.
Dans le cadre de notre travail, les résultats du diagnostic de l'état de connaissance de l'apprenant ne peuvent être déduits qu'avec un certain degré d'incertaine. De ce fait, nous avons choisi les réseaux bayésiens pour représenter la connaissance et le diagnostic, et l'approche de la théorie de la décision pour automatiser la prise de décisions didactiques.
L'état de connaissance de l'apprenant est déduit en appliquant l'inférence dans le réseau bayésien en fonction des traces de ses activités. Les résultats du diagnostic sont ensuite utilisés dans le modèle de la prise de décisions didactiques pour produire les rétroactions épistémiques en quatre étapes : 1) le choix de la cible qui permet de sélectionner les connaissances visées par la rétroaction ; 2) la détermination de l'objectif qui permet de définir le but de la rétroaction du point de vue de l'apprentissage ; 3) le choix de la forme de la rétroaction ; 4) la détermination du contenu de la rétroaction.
Nous avons implémenté et intégré le modèle de prise de décisions didactiques dans la plateforme de TELEOS. Ainsi, nous avons testé et évalué la cohérence du comportement informatique du modèle, sa sensibilité aux modifications des probabilités et des paramètres, et la pertinence des rétroactions produites.

L'objet de cette thèse est la formalisation et l'automatisation du raisonnement géométrique au sein de l'assistant de preuve Coq.
Dans une première partie, nous réalisons un tour d'horizon des principales axiomatiques de la géométrie puis nous présentons une formalisation des huit premiers chapitres du livre de Schwabäuser, Szmielew et Tarski: Metamathematische Methoden in der Geometrie.
Dans la seconde partie, nous présentons l'implantation en Coq d'une procédure de décision pour la géométrie affine plane : la méthode des aires de Chou, Gao et Zhang. Cette méthode produit des preuves courtes et lisibles.
Dans la troisième partie, nous nous intéressons à la conception d'une interface graphique pour la preuve formelle en géométrie : Geoproof. GeoProof combine un logiciel de géométrie dynamique avec l'assistant de preuve Coq.
Enfin, nous proposons un système formel diagrammatique qui permet de formaliser des raisonnements dans le domaine de la réécriture abstraite. Il est par exemple possible de formaliser dans ce système la preuve diagrammatique du lemme de Newman. La correction et la complétude du système sont prouvées vis-à-vis d'une classe de formules appelée logique cohérente.

Cette thèse se situe dans le cadre de la synthèse logique. Elle a pour objet la synthèse logique optimisée de circuits sur réseaux programmables à base de «tables de vérité» de type «Xilinx». Ces réseaux programmables ont été à l'origine du premier succès commercial des réseaux reprogrammables à faible granularité. Une première solution pratiquée industriellement a consisté à associer une bibliothèque équivalente de primitives logiques simples de type «cellule standard» à un réseau Xilinx. Une telle approche conduit à une très pauvre utilisation de la technologie cible car elle ne tire pas profit de la richesse de la cellule de base. Cette thèse s'intéresse, en conséquence, à des approches plus ciblées. Il s'agit de décomposer de façon optimisée les parties combinatoires en sous-fonctions «saturant» les possibilités des cellules élémentaires. Pour ceci, le traitement des fonctions booléennes sera effectué dès l'étape de factorisation en fonction du but final. Après un rappel de la factorisation «lexicographique», qui a comme fondement l'existence d'un ordonnancement des entrées, une méthode de décomposition en sous fonctions de k variables est proposée. Elle sert de base à des méthodes de décomposition technologique pour les séries Xilinx 3000 et Xilinx 4000. Deux alternatives à cette factorisation lexicographique sont proposées, une factorisation utilisant une représentation par diagramme de décision binaire (ROBDD) et une factorisation algébrique classique adaptée aux caractéristiques de la cible Xilinx. La dernière étape de synthèse concerne de façon plus fine le regroupement des sous-fonctions dans la cellule physique Xilinx et se préoccupe de l'optimisation des points de mémorisation, des buffers et des ressources d'horloge. Une évaluation sur un ensemble d'exemples internationaux et industriels démontre l'efficacité des méthodes proposées. Ce travail a fait l'objet d'un transfert technologique vers le logiciel industriel ASYL+

Avec la complexité croissante des systèmes informatiques se pose la question de la mise en oeuvre de méthodes automatiques pour leur vérification formelle. Parmi ces méthodes, le model-checking se fonde sur l'exploration exhaustive du comportement d'un système. Plus celui-ci sera complexe, plus cette exploration se traduira par une explosion combinatoire de l'espace des états du système. Diverses approches ont été proposées pour résoudre ce problème, notamment les méthodes symboliques qui sont bases sur une représentation compacte d'ensembles d'états. Depuis les travaux de R. E. Bryant et la définition des Diagrammes de Décision Binaires (BDD), de nombreuses représentations en DAG d'espaces d'états ont vu le jour, parmi celles-ci, on trouve les Diagrammes de Décision de Données (DDD), qui procurent une représentation compacte d'ensemble d'états et sont pourvus de mécanismes de parcours définis localement pour la réalisation des modifications sur ces états et des opérations ensemblistes. Parallélement, les travaux de G. J. Holzmann ont abouti à la création de l'outil de vérification SPIN, basé sur des méthodes énumératives explicites, pour des systèmes décrits en langage Promela. Ces systèmes sont proches de ceux qui sont utilisés pour la synthèse de haut niveau. Nous proposons une approche de vérification symbolique de systèmes matériels décrits dans un sous-ensemble du langage Promela. La représentation symbolique d'ensembles d'états est basée sur les Diagrammes de Décision de Données qui évitent de d'écrire le système au niveau booléen. Nous présentons d'abord la sémantique du langage Promela ainsi que les DDD puis les mécanismes mis en oeuvre pour la vérification de propriétés de logique CTL. Les conclusions tirées de cette première étape conduisent à proposer l'utilisation des Diagrammes de Décision d'Ensembles (SDD) pour améliorer les performances de la vérification automatique. Nous montrons que, bien que pourvus d'une implémentation et d'une terminologie différentes, il se prévalent du même formalisme que les DDD tout en procurant un étiquetage symbolique des arcs de la structure. Nous expérimentons ensuite cette approche sur des systèmes académiques et sur des systèmes issus d'applications industrielles. Ces expérimentations corroborent nos premiers résultats : les SDD couplés aux méthodes de saturation constituent une alternative sérieuse pour la vérification de systèmes à fort degré de concurrence. Nous proposons des perspectives de recherche pour améliorer encore la vérification de tels systèmes mais également pour introduire le concept de hiérarchie dans la description du système

Dans de nombreuses applications réelles, nous sommes souvent confrontés à des problèmes de décision: de choisir des actions et de renoncer à d'autres. Les problèmes de décision deviennent complexes lorsque les connaissances disponibles sont entachées d'incertitude ou lorsque le choix établi présente un risque.L'un des principaux domaines de l'Intelligence Artificielle (IA) consiste à représenter les connaissances, à les modéliser et à raisonner sur celles-ci. Dans cette thèse, nous sommes intéressés à une discipline inhérente à l'IA portant sur les problèmes de décision. La théorie de la décision possibiliste qualitative a élaboré plusieurs critères, selon le comportement de l'agent, permettant de l'aider à faire le bon choix tout en maximisant l'un de ces critères. Dans ce contexte, la théorie des possibilités offre d'une part un cadre simple et naturel pour représenter l'incertitude et d'autre part, elle permet d'exprimer les connaissances d'une manière compacte à base de modèles logiques ou de modèles graphiques. Nous proposons dans cette thèse d'étudier la représentation et la résolution des problèmes de la décision qualitative en utilisant la théorie des possibilités. Des contreparties possibilistes des approches standards ont été proposées et chaque approche a pour objectif d'améliorer le temps de calcul des décisions optimales et d'apporter plus d'expressivité à la forme de représentation du problème. Dans le cadre logique, nous avons proposé une nouvelle méthode, pour résoudre un problème de la décision qualitative modélisé par des bases logiques possibilistes, basée sur la fusion syntaxique possibiliste. Par la suite, dans le cadre graphique, nous avons proposé un nouveau modèle graphique, basé sur les réseaux possibilistes, permettant la représentation des problèmes de décision sous incertitude. En effet, lorsque les connaissances et les préférences de l'agent sont exprimées de façon qualitative, nous avons proposé de les représenter par deux réseaux possibilistes qualitatifs distincts. Nous avons développé un algorithme pour le calcul des décisions optimales optimistes qui utilise la fusion de deux réseaux possibilistes. Nous avons montré aussi comment une approche basée sur les diagrammes d'influence peut être codée d'une manière équivalente dans notre nouveau modèle. Nous avons en particulier proposé un algorithme polynomial qui permet de décomposer le diagramme d'influence en deux réseaux possibilistes. Dans la dernière partie de la thèse, nous avons défini le concept de la négation d'un réseau possibiliste qui pourra servir au calcul des décisions optimales pessimistes
In many applications, we are often in presence of decision making problems where the choice of appropriate actions need to be done. When the choice is clear and the risks are null, the decision becomes easy to select right actions. Decisions are more complex when available knowledge is flawed by uncertainty or when the established choice presents a risk. One of the main areas of Artificial Intelligence (AI) is to model, represent and reason about knowledge. In this thesis, we are interested in an inherent discipline in AI which concerns decision making problems.The qualitative possibility decision theory has developed several criteria, depending on the agent behavior, for helping him to make the right choice while maximizing one of these criteria. In this context, possibility theory provides a simple and natural way to encode uncertainty. It allows to express knowledge in a compact way using logical and graphical models. We propose in this thesis to study the representation and resolution of possibilistic qualitative decision problems. Possibilistic counterparts of standard approaches have been proposed and each approach aims to improve the computational complexity of computing optimal decisions and to provide more expressiveness to the representation model of the problem. In the logical framework, we proposed a new method for solving a qualitative decision problem, encoded by possibilistic bases, based on syntactic representations of data fusion problems. Subsequently, in a graphical framework, we proposed a new graphical model for decision making under uncertainty based on qualitatif possibilistic networks. Indeed, when agent's knowledge and preferences are expressed in a qualitative way, we suggest to encode them by two distinct qualitative possibilistic networks. We developed an efficient algorithm for computing optimistic optimal decisions based on syntactic counterparts of the possibilistic networks fusion. We also showed how an influence diagram can be equivalently represented in our new model. In particular, we proposed a polynomial algorithm for equivalently decomposing a given possibilistic influence diagram into two qualitatif possibilistic networks. In the last part of the thesis, we defined the concept of negated possibilistic network that can be used for computing optimal pessimistic decisions

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.

Le domaine de prise de décision est un domaine multidisciplinaire en relation avec plusieurs disciplines telles que l'économie, la recherche opérationnelle, etc. La théorie de l'utilité espérée a été proposée pour modéliser et résoudre les problèmes de décision. Ces théories ont été mises en cause par plusieurs paradoxes (Allais, Ellsberg) qui ont montré les limites de son applicabilité. Par ailleurs, le cadre probabiliste utilisé dans ces théories s'avère non approprié dans certaines situations particulières (ignorance totale, incertitude qualitative). Pour pallier ces limites, plusieurs travaux ont été élaborés concernant l'utilisation des intégrales de Choquet et de Sugeno comme critères de décision d'une part et l'utilisation d'une théorie d'incertitude autre que la théorie des probabilités pour la modélisation de l'incertitude d'une autre part. Notre idée principale est de profiter de ces deux directions de recherche afin de développer, dans le cadre de la décision séquentielle, des modèles de décision qui se basent sur les intégrales de Choquet comme critères de décision et sur la théorie des possibilités pour la représentation de l'incertitude. Notre objectif est de développer des modèles graphiques décisionnels, qui représentent des modèles compacts et simples pour la prise de décision dans un contexte possibiliste. Nous nous intéressons en particulier aux arbres de décision et aux diagrammes d'influence possibilistes et à leurs algorithmes d'évaluation
The field of decision making is a multidisciplinary field in relation with several disciplines such as economics, operations research, etc. Theory of expected utility has been proposed to model and solve decision problems. These theories have been questioned by several paradoxes (Allais, Ellsberg) who have shown the limits of its applicability. Moreover, the probabilistic framework used in these theories is not appropriate in particular situations (total ignorance, qualitative uncertainty). To overcome these limitations, several studies have been developed basing on the use of Choquet and Sugeno integrals as decision criteria and a non classical theory to model uncertainty. Our main idea is to use these two lines of research to develop, within the framework of sequential decision making, decision models based on Choquet integrals as decision criteria and possibility theory to represent uncertainty. Our goal is to develop graphical decision models that represent compact models for decision making when uncertainty is represented using possibility theory. We are particularly interested by possibilistic decision trees and influence diagrams and their evaluation algorithms

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 propose un nouveau type de systèmes de ré-écriture, appelé les systèmes de réécriture fonctionnels. Nous montrons que notre modèle a la puissance d'expression des systèmes de ré-écriture et qu'il est bien adapté à l'étude de propriétés de sûreté et de propriétés de logique temporelle de modèles.Nous avons mis en évidence une sous classe de systèmes fonctionnels, les élémentaires et les élémentaires à droite, préservant la puissance d'expression des systèmes fonctionnels et des techniques d'accélération des calculs aboutissant à un outil de vérification symbolique efficace.Dans la partie expérimentale, nous avons comparé notre outil, d'une part avec des outils de ré-écriture tels que Timbuk, Maude et TOM, d'autre part avec des outils de vérification tels que SPIN, NuSMV, SMART, HSDD. Nos benchmarks démontrent l'efficacité des systèmes fonctionnels élémentaires pour la vérification de modèles.

Garantir la fiabilité des systèmes informatiques exige des moyens de vérification rigoureux. Le model checking est une technique de vérification dont l’intérêt majeur est l’automatisation, et donc la facilité d’utilisation pour les ingénieurs. La récente attribution du prix Turing aux créateurs de cette technique atteste de sa viabilité. Le model checking explore exhaustivement les modèles analysés. Cela amène un problème majeur : l’explosion combinatoire liée aux espaces d'états des grands systèmes. Depuis plus de vingt ans, de nombreuses solutions ont été proposées pour repousser cette limite de taille afin d’être capable de traiter des espace d’états toujours plus grands dont les tailles peuvent atteindre très rapidement les 10^400 éléments. Les travaux présentés ici proposent deux types de solutions pour traiter plus efficacement de plus grands espaces d’états. La première s'appuie sur les ressources de calcul parallèle des machines multi-processeurs,omniprésentes aujourd’hui, et des grappes de calcul. La deuxième propose de traiter plus efficacement les diagrammes de décision en automatisant la technique dite de saturation, dont l’efficacité empiriquement montrée est très difficile à atteindre manuellement.

Les analyses de sûreté de fonctionnement standards sont basées sur la représentation des événements redoutés par des arbres de défaillances, qui les décrivent à l'aide de combinaison logiques d'événements plus basiques (formules Booléennes complexes). Les analyses quantitatives se font avec l'hypothèse que les probabilités d'occurrence de ces événements basiques sont connues. Le but de cette thèse est d'étudier l'impact de l'incertitude épistémique sur les événements élémentaires, ainsi que la propagation de cette incertitude à de plus hauts niveaux. Le problème soulevé est comment calculer l'intervalle de probabilité dans lequel se trouvera l'occurrence d'un événement redouté, lorsque les événements basiques qui le décrivent ont eux-mêmes une probabilité imprécise. Lorsque l'indépendance stochastique est supposée, on se retrouve avec un problème NP-hard. Nous avons donc développé un algorithme permettant de calculer l'intervalle exact dans lequel se trouvera la probabilité d'occurrence d'un événement redouté, grâce à des techniques d'analyse par intervalles. Cet algorithme a également été étendu dans le cas où les probabilités des événements basiques évolueraient en fonction du temps. Nous avons également utilisé une approche par fonctions de croyance pour étudier le cas où l'indépendance stochastique des événements ne peut pas être démontrée : on suppose alors que les probabilités viennent de différentes sources d'information Indépendantes. Dans ce cas, les mesures de plausibilité et de nécessité d'une formule Booléenne complexe sont difficiles à calculer, néanmoins nous avons pu dégager des situations pratiques dans le cadre de leur utilisation pour les Arbres de défaillances pour lesquelles elles se prêtent aux calculs
Standard approaches to reliability analysis relies on a probabilistic analysis of critical events based on fault tree representations. However in practice, and especially for preventive maintenance tasks, the probabilities ruling the occurrence of these events are seldom precisely known. The aim of this thesis is to study the impact of epistemic uncertainty on probabilities of elementary events such as failures over the probability of some higher level critical event. The fundamental problem addressed by the thesis is thus to compute the probability interval for a Boolean proposition representing a failure condition, given the probability intervals of atomic propositions. When the stochastic independence is assumed, we face a problem of interval analysis, which is NP-hard in general. We have provided an original algorithm that computes the output probability interval exactly, taking into account the monotonicity of the obtained function in terms of some variables so as to reduce the uncertainty. We have also considered the evolution of the probability interval with time, assuming parameters of the reliability function to be imprecisely known. Besides, taking advantage of the fact that a probability interval on a binary space can be modelled by a belief function, we have solved the same problem with a different assumption, namely information source independence. While the problem of computing the belief and plausibility of a Boolean proposition are even harder to compute, we have shown that in practical situations such as usual fault-trees, the additivity condition of probability theory is still valid, which simplifies this calculation. A prototype has been developed to compute the probability interval for a complex Boolean proposition

Dans un circuit asynchrone, la synchronisation entre les blocs est locale: on s'affranchit ainsi des contraintes liées à l'horloge. Ces circuits sont plus robustes, modulaires, moins bruités, et ont une consommation dynamique plus faible que les circuits synchrones. Cependant, le manque d'outils de conception de tels circuits freine leur développement. Cette thèse a permi de développer une technique de synthèse automatique de circuits asynchrones quasi insensibles aux délais (QDI), qui sont particulièrement robustes. La méthode de synthèse permet de synthétiser un circuit totalement décomposé en portes logiques élémentaires, ce qui permet d'effectuer une projection technologique. De plus, une étude formelle réalisée durant la thèse démontre que les circuits synthétisés respectent la contrainte de quasi insensibilité aux délais. Cette technique de synthèse a été développé au sein du projet TAST. Elle a été validée sur un ensemble de circuits de tests
In an asynchronous circuit, the synchronization between the blocs is local: the constraints due to the clock do not apply. These circuits are more robust, modular, have less noise and a lower dynamic power consumption that asynchronous circuits. However, the lack of design tools for such circuits prevents them from spreading widely. This thesis aimed at developping an automatic synthesis technique targeting asynchronous quasi delay insensitive (QDI) circuits, which are particularly robust. The technique synthesizes a circuit totally decomposed in elemetary logical gates, which allows a later technology mapping. Moreover, a formal study done during this thesis proves that the circuits synthesized respect the constraint of quasi delay insensitivity. This synthesis technique was developped in the TAST project. Is has been validated on a set of test circuits

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

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.

Dans un circuit asynchrone, la synchronisation entre les blocs est locale: on s'affranchit ainsi des contraintes liées à l'horloge. Ces circuits sont plus robustes, modulaires, moins bruités, et ont une consommation dynamique plus faible que les circuits synchrones. Cependant, le manque d'outils de conception de tels circuits freine leur développement. Cette thèse a permi de développer une technique de synthèse automatique de circuits asynchrones quasi insensibles aux délais (QDI), qui sont particulièrement robustes. La méthode de synthèse permet de synthétiser un circuit totalement décomposé en portes logiques élémentaires, ce qui permet d'effectuer une projection technologique. De plus, une étude formelle réalisée durant la thèse démontre que les circuits synthétisés respectent la contrainte de quasi insensibilité aux délais. Cette technique de synthèse a été développé au sein du projet TAST. Elle a été validée sur un ensemble de circuits de tests.

Cette thèse présente des méthodes et des algorithmes pour l'évaluation de performance de systèmes à grand espace d'états décrits par des formalismes de haut niveau. Parmi les différents formalismes de haut niveau normalement utilisés, nous nous sommes intéressés au formalisme des Réseaux d'Automates Stochastiques (SAN). Le formalisme SAN se caractérise par la modélisation de systèmes complexes, où un système est représenté par la composition de sous-systèmes (automates) qui interagissent entre eux. Cette interaction se réalise par l'occurrence des événements synchronisants ou des taux fonctionnels. Lorsqu'on calcule l'espace d'états atteignables de systèmes complexes, le principal problème qui surgit est l'explosion combinatoire de l'espace d'états du modèle. Dans la première partie de cette thèse, nous proposons des méthodes pour la génération de l'espace d'états atteignables de modèles compositionnels qui utilisent des taux fonctionnels. Nous utilisons les Diagrammes de Décision Multi-valués (MDD) pour représenter et manipuler les espaces d'états et le formalisme SAN pour la modélisation de systèmes. Un MDD est une structure de donnée arborescente qui permet de représenter et de manipuler de façon performante un très grand espace d'états. L'avancée par rapport à l'état de l'art a été de proposer de méthodes qui prennent en compte ces fonctions qui expriment des relations entre les composants des modèles. Des études d'exemples sont présentées afin d'illustrer les apports de ces méthodes. Dans la deuxième partie de cette thèse, nous nous sommes intéressés à la résolution d'un modèle SAN à temps discret dont la matrice de transition est représentée par une formule tensorielle (appelée descripteur discret). A cet effet, nous présentons l'Algèbre Tensorielle compleXe (ATX) adaptée à la composition parallèle des SAN à temps discret pour la représentation du descripteur et nous démontrons des propriétés qui servent de base aux méthodes itératives pour la résolution de la chaîne de Markov associée au modèle SAN. Un des avantages de représenter un modèle SAN par un descripteur est la façon compacte par laquelle on peut représenter les transitions du modèle: on remplace une description dans un espace produit par un unique produit tensoriel portant sur des facteurs qui décrivent ce qui se passe sur une seule dimension (une composante du modèle SAN). Afin de profiter de cette représentation, nous présentons une méthode de multiplication d'un vecteur de probabilité par un descripteur discret adaptée à cette algèbre. Cette méthode vise à exploiter des propriétés du produit tensoriel complexe de façon à ce que la multiplication par un opérateur sur l'espace produit soit remplacée par une suite d'opérations qui manipulent des données de la taille d'une composante (et pour toutes les composantes).