De plus en plus de recherches s'effectuent pour développer des systèmes de reconnaissance en se basant sur l'approche connexionniste. En grande partie, on tente de résoudre de cette manière les problèmes que l'on rencontre avec les approches statistiques plus conventionnelles (reconnaissance difficile dans des conditions bruités, quantité de données nécessaire pour l'apprentissage, ...). L'objectif de cette recherche est de tester la reconnaissance d'un signal vocal à l'aide d'un prototype inspiré par un excellent système de reconnaissance vocale qui a évolué depuis des milliers d'années. On fait évidemment allusion à celui de l'être humain qui est non seulement capable de comprendre rapidement les paroles prononcées par un individu dans des conditions adverses, mais aussi de deviner son sexe, son âge ainsi que son accent. Des réseaux de neurones ont déjà été développés pour effectuer la reconnaissance vocale, avec plus ou moins de succès. Cependant, nous ne commençons qu'à avoir une idée du potentiel offert par ces outils. Pour cette raison, nous poursuivons l'exploration des réseaux de neurones à décharges, car ils devraient nous permettre d'effectuer la reconnaissance vocale indépendamment du locuteur, sans avoir à exécuter une longue période d'apprentissage qui nécessite une importante quantité de données. De plus, certains types de réseaux à décharges se prêtent bien à la programmation événementielle. Nous avons donc tenté de conserver cette orientation pour obtenir une exécution plus efficace lors de la reconnaissance. La revue de certains articles jugés intéressants ou qui nous ont inspirés pour ce travail compose la première partie de cette recherche. Aussi, nous donnons une brève description des éléments théoriques amenés par ces articles ou ceux particulièrement intéressants rencontrés à travers le cheminement pédagogique de cette maîtrise. Parmi les domaines qui se rattachent à notre sujet, ceux qui nous viennent le plus rapidement en tête sont les domaines de l'intelligence artificielle (plus précisément les domaines portant sur les réseaux de neurones), des systèmes en temps réel et des processus aléatoires. Dans ce mémoire, on a exploré deux façons différentes d'effectuer la reconnaissance vocale à l'aide de neurones à décharges. Dans une première partie, un réseau composé d'oscillateurs a été utilisé avec un cepstrogramme. Malheureusement, il semble que ce type d'entrée ne soit pas compatible avec l'architecture présentée. De plus, l'implémentation des neurones oscillatoires dans un langage de programmation orienté événements, comme Rodin, risque à première vue d'être difficile. D'un autre côté, le prototype qui a été conçu en s'inspirant du fonctionnement du système auditif possède un potentiel intéressant. En effet, à l'aide du codage par ordre de rang et en modélisant le fonctionnement de l'oreille interne par un banc de filtre et des détecteurs de seuils, nous avons effectué efficacement la reconnaissance vocale avec un vocabulaire limité. Les résultats du prototype se comparent à ceux obtenus avec des chaînes de Markov et des coefficients cepstraux lorsqu'on limite le nombre de prononciations à l'apprentissage. De plus, l'approche développée est simple et peut facilement s'implémenter dans un langage de programmation orienté événements. Cet avantage va éventuellement nous permettre une exécution plus efficace du système de reconnaissance vocale. D'après les tests présentés dans ce mémoire, les efforts futurs devraient se concentrer sur le prototype qui utilise le codage par ordre de rang. En effet, ce prototype présente déjà un grand potentiel pour la reconnaissance vocale.

Les systèmes multi-agents actuels ne prennent pas en considération les problèmes de cohabitation entre un usager et son homologue agent virtuel agissant en son nom ?on behalf-, tels que l'intégration de l'utilisateur dans la même boucle de réalisation d'une tâche commune - usager dans la boucle - et les conflits terminologiques liés à l'utilisation de termes différents pour décrire leurs opinions (points de vue) à propos d'une situation de résolution d'un problème. La cohabitation usager-agent nécessite donc une compréhension mutuelle, ce qui signifie que les deux entités devront être aptes à comparer leurs points de vue respectifs avant la prise d'initiatives. Par conséquent, la question qui se pose est la suivante: dans quelle mesure les deux points de vue (utilisateur et agent) peuvent ou non se rapprocher? Ce travail de recherche vise à contribuer au processus général d'intégration d'un usager dans la boucle de réalisation d'une tâche conjointe. Il propose une approche de comparaison des points de vue dans un contexte de planification par initiatives mixtes. L'approche théorique proposée s'appuie sur la logique terminologique pour décrire les ontologies des points de vue de l'utilisateur et de l'agent. La méthode de comparaison des points de vue proposée dans ce mémoire permettra d'extraire une mesure de leur similarité, servant à prendre une décision sécuritaire. Ce mémoire se veut une première phase d'un projet de recherche beaucoup plus large, visant le développement d'une approche générique d'intégration des points de vue. Il doit donc être considéré comme un pas en avant vers la réalisation de ce projet d'envergure ainsi qu'une contribution au domaine de la coopération entre un usager et son agent artificiel.

L'évolution des moyens de communication, la puissance des outils disponibles et l'accessibilité des nouvelles technologies ont élargi les champs d'application des systèmes d'information. Auparavant réservées aux grandes entreprises et aux chercheurs, ces technologies sont maintenant accessibles à tous. Tous les domaines de la société sont touchés par ces développements technologiques. Qu'on pense seulement aux guichets automatiques, à la télévision interactive, aux tableaux de bord des voitures, à Internet ou au fonctionnement d'un téléphone cellulaire. Même si les premiers systèmes de communication comme le téléphone traditionnel ou la télévision ont réussi à atteindre l'ensemble des utilisateurs, les technologies informatiques demeurent encore trop complexes pour trop de personnes dans la société. Une des raisons du désintéressement des utilisateurs est le sentiment d'inutilité et la difficulté à comprendre le fonctionnement des systèmes. S'il est difficile de concevoir des systèmes conviviaux pour des utilisateurs chevronnés, concevoir des systèmes pour un large auditoire inexpérimenté s'avère une tâche encore plus complexe. Un problème majeur est de rendre les systèmes utilisables par des personnes qui, souvent, n'ont aucune connaissance des ordinateurs. Il faut notamment satisfaire les jeunes comme les plus vieux, les gens instruits comme ceux qui le sont moins, les travailleurs manuels, les communautés culturelles, les personnes souffrant d'un handicap temporaire ou permanent, et ainsi de suite. Le défi est de comprendre la diversité des utilisateurs afin de développer des systèmes simples et intuitifs qui n'exigeront pas un apprentissage laborieux. Dans le domaine des transports, les nouvelles technologies sont de plus en plus utilisées pour améliorer la gestion des déplacements et réduire les accidents sur le réseau routier. On recueille par divers moyens (boucles de détections, systèmes de caméras, patrouilleurs, etc.) des données sur les conditions de la circulation. Ces données sont par la suite traitées et retransmises à la population sous d'autres formes. On espère ainsi influencer les usagers afin qu'ils puissent prendre en considération ces renseignements dans la planification de leurs déplacements. Le défi est de taille compte tenu de la multitude de données à traiter qu'on espère rendre compréhensibles. La présente recherche porte sur l'utilisabilité des systèmes d'information grand public. Dans le cadre de cette recherche sont examinées les techniques pour rendre les systèmes plus facilement utilisables par la population. Une application qui permet de valider l'approche retenue est également présentée. Cette application a pour objectif d'améliorer la sécurité des personnes qui circulent sur le réseau routier. Elle vise à fournir des renseignements en temps réel ou quasi réel sur les conditions routières hivernales. Elle cherche à démontrer qu'il est possible, en suivant des règles de conception reconnues, de développer un système d'information intuitif qui se rapproche du langage naturel des usagers.

Un souci constant qui guide le développement de l'informatique est l'accélération des performances. Dans cette optique, une des solutions souvent utilisées réside en la mise en parallèle des traitements. L'émergence, depuis quelques années, des applications multimédia et l'augmentation incessante de la complexité des systèmes pouvant être intégrés sur un circuit motive et rend possible l'apparition et le développement de DSP1 de plus en plus complets, dédiés à certains traitements numériques intensifs. Les applications cibles traitent généralement une énorme quantité de données avec un nombre limité de fonctions. Ces traitements, souvent indépendants les uns des autres, peuvent être effectués en parallèle. Le but est d'exploiter le parallélisme dans les données de plusieurs algorithmes afin de les traiter nettement plus rapidement qu'avec un ordinateur séquentiel conventionnel. Pour obtenir des applications à traitement parallèle performantes il faut effectuer une partition des algorithmes étudiés en assignant une partie du traitement à chacun des processeurs. Le projet PULSE, issu d'un groupe de recherche de l'École Polytechnique de Montréal, travaille au développement d'une architecture multiprocesseur de type SIMD2 dédiée au traitement numérique en temps réel. Le circuit intégré cible possède quatre processeurs dans sa première version. La seconde version doit inclure seize processeurs à l'intérieur du même circuit intégré. Durant ce projet, sept applications numériques connues ont étés écrites en langage assembleur et optimisées sur la première version de PULSE. Les applications sont : multiplications vecteurs-matrice, algorithmes de cryptage RSA et IDEA, algorithme de Bresenham, modèle continu (poisson) et transformation binaire d'images (inclut érosion et dilatation d'images). Pour certaines de ces applications - multiplications vecteurs-matrice, algorithme de Bresenham et transformation binaire d'images - les résultats obtenus se comparent avantageusement avec les librairies déjà développées sur des circuits intégrés concurrents. En plus des applications numériques ce projet à permis d'améliorer les différents outils de PULSE - documentation et simulateur -, ainsi que le modèle VHDL3.

Les cadres interactionnels actuels pour les communications entre agents (protocoles, stratégies de conversation, jeux de dialogue, . . . ) garantissent la cohérence structurelle des conversations tenues. Pourtant, ce n'est pas tant l'habilité des agents à structurer leurs conversations qui nous intéresse que leurs aptitudes à tenir des conversations utiles quant à leurs objectifs individuels et collectifs. Pour traiter cette problématique, nous avons défini et implanté un modèle complet de la communication entre agents qui couvre les quatre dimensions classiques de la communication : syntaxe, structure, sémantique et pragmatique. Au niveau syntaxique, nous proposons le langage DIAGAL[DIAlogue Game based Agent communication Language] qui se présente comme un ensemble de jeux de dialogue qui permettent la manipulation conjointe d'engagements sociaux. Du point de vue de la structuration des dialogues, les jeux de dialogue que nous proposons offrent une alternative à la rigidité des protocoles tout en capturant les aspects conventionnels de la communication, absents des approches considérant des actes de langages isolés. Dans notre approche, le niveau sémantique de la communication repose, quant à lui, sur les engagements sociaux qui capturent les interdépendances contractées par les agents lors des communications. Dans ce contexte, notre contribution principale concerne les aspects cognitifs de la pragmatique. À cet effet, nous proposons une théorie cognitive de l'utilisation de ce cadre interactionnel basée sur la notion de cohérence cognitive et fondée sur des résultats non encore formalis és de sciences cognitives. Issue d'une unification de la théorie de la dissonance cognitive (une des théories majeures de psychologie cognitive) avec la théorie de cohérence cognitive (développée en philosophie de l'esprit), notre approche est formulée en termes d'éléments et de contraintes, notions familières en informatique. La théorie motivationnelle résultante est ensuite étendue afin de traiter la communication entre agents cognitifs. Sous les hypothèses de notre théorie, nous définissons alors une métrique de l'utilité des conversations entre agents. Nous montrons comment cette théorie permet de résoudre en pratique de nombreux problèmes fondamentaux des aspects cognitifs de la pragmatique des communications entre agents. En particulier, nous proposons une première application de notre théorie pour l'utilisation automatique par des agents de type BDI [Beliefs, Desires and Intentions] des jeux de dialogue du langage DIAGAL. Ce faisant, nous introduisons un certain nombre d'outils techniques pour l'automatisation des communications entre agents tout en précisant quels sont nos apports théoriques pour les SMAs et plus généralement pour les sciences cognitives. / Different approaches have investigated the syntax and semantics of agent communication languages. However, these approaches have not indicated how agents should dynamically use communications. Instead of filling this pragmatics gap, most approaches have mainly focused on the "structure" of dialogues even though developers are more interested in agents' capabilities of having "useful" automated conversations with respect to their goals rather than in their abilities to structure dialogues. We addressed this problem that requires re-inquiring the four main dimensions of (agent) communication : syntax, structure, semantics and pragmatics (the theory of the use of language). At the syntactic level, we have developed an agent communication language called DIAGAL [DIAlogue Game based Agent communication Language] which consists of a set of dialogue games that allows for the grounded manipulation of social commitments. At the structural level, DIAGAL dialogue games offer a good compromise between the lack of flexibility of protocols while taking into account the conventional aspects of dialogue which were missing in isolated speech acts approaches. At the semantics level, we provide a social commitments model that captures the inter-dependencies contracted by the agents toward each other during dialogues. In that context, our main contribution concerns the cognitive aspects of pragmatics. To this end, we develop in this thesis a motivational theory for the use of such a conventional and social agent communication framework. Our approach is based on cognitive science results that have not been formalized yet. Our theory consists of a formalisation and a unification of the cognitive dissonance theory (one of the major theories of cognitive psychology) with the coherence theory issuing from philosophy of mind. Our approach is formulated in terms of elements and constraints which allow making it computational. This theory allows formally defining and exploiting the notion of utility of dialogues. We show in this thesis how this approach allows solving many theoretical and practical problems in agent communication. As a validation of this approach, we extend classical BDI [Beliefs, Desires and Intentions] agents to allow them to automatically use DIAGAL dialogue games. The resulting framework provides the necessary theoretical and practical elements for implementing our theory. In doing so, it brings in a general scheme for automatizing agents' communicational behaviour.

L’objet principale de cette thèse est l’étude théorique et la conception d’algorithmes d’apprentissage concevant des classificateurs par vote de majorité. En particulier, nous présentons un théorème PAC-Bayes s’appliquant pour borner, entre autres, la variance de la perte de Gibbs (en plus de son espérance). Nous déduisons de ce théorème une borne du risque du vote de majorité plus serrée que la fameuse borne basée sur le risque de Gibbs. Nous présentons également un théorème permettant de borner le risque associé à des fonctions de perte générale. À partir de ce théorème, nous concevons des algorithmes d’apprentissage construisant des classificateurs par vote de majorité pondérés par une distribution minimisant une borne sur les risques associés aux fonctions de perte linéaire, quadratique, exponentielle, ainsi qu’à la fonction de perte du classificateur de Gibbs à piges multiples. Certains de ces algorithmes se comparent favorablement avec AdaBoost. / The main purpose of this thesis is the theoretical study and the design of learning algorithms returning majority-vote classifiers. In particular, we present a PAC-Bayes theorem allowing us to bound the variance of the Gibbs’ loss (not only its expectation). We deduce from this theorem a bound on the risk of a majority vote tighter than the famous bound based on the Gibbs’ risk. We also present a theorem that allows to bound the risk associated with general loss functions. From this theorem, we design learning algorithms building weighted majority vote classifiers minimizing a bound on the risk associated with the following loss functions : linear, quadratic and exponential. Also, we present algorithms based on the randomized majority vote. Some of these algorithms compare favorably with AdaBoost.

La société moderne est de plus en plus dépendante de l'informatique dont le rôle est devenu tellement vital au point que tout dysfonctionnement peut engendrer des pertes considérables voire des conséquences irréversibles telles que la perte de vies humaines. Pour minimiser les dégâts, plusieurs techniques et outils ont été mis en place au cours des dernières années. Leur objectif est de faire en sorte que nos systèmes informatiques fonctionnent <<~tout le temps~>>, et ce, tout en produisant les résultats escomptés. La duplication du matériel et les tests de logiciels sont parmi les techniques les plus utilisées. Cependant, sans méthodes formelles, rien n'est garanti et des problèmes peuvent surgir à tout moment. En contrepartie, l'utilisation de méthodes formelles n'est pas à la portée de tout le monde y compris les programmeurs chevronnés et la tâche reste subtile et complexe même pour les spécialistes. Quelques lignes de code nécessitent parfois des centaines de lignes de preuve difficiles à lire et à comprendre. Malgré tout, leur utilisation n'est plus un luxe, mais plutôt nécessaire afin d'éviter les dégâts engendrés par les mauvais fonctionnements de nos systèmes critiques. Le principal objectif de notre recherche est de développer un cadre formel et automatique pour le renforcement de politique de sécurité sur des systèmes concurrents. Plus précisément, l'idée consiste à ajouter dans un programme des tests à des endroits soigneusement calculés pour qu'une politique de sécurité soit respectée. La nouvelle version du programme préserve toutes les traces de la version originale respectant la politique de sécurité et bloque les traces qui ne peuvent plus respecter la politique de sécurité même si elles sont complétées par certains suffixes. Les principaux résultats ayant contribué à l'atteinte de cet objectif sont : 1. La définition d'une algèbre de processus [symbol] offrant un cadre purement algébrique pour le renforcement de politique de sécurité sur des systèmes concurrents. Plus précisément, nous avons défini un nouvel opérateur qui permet de renforcer, d'une manière intuitive, une politique de sécurité sur un système concurrent. 2. La définition d'une logique, dénotée par [symbol], inspirée des expressions régulières étendues. En effet, [symbol] est une logique linéaire qui exprime la classe de langage régulier, mais avec la possibilité d'exprimer des propriétés infinies. 3. La définition d'une algèbre [symbol] basée sur l'algèbre [symbol]. [symbol] définit un nouvel opérateur de renforcement qui tient compte de l'introduction de la logique. 4. Le développement d'une technique d'optimisation qui, pour une certaine classe de propriétés de sécurité, permet de réduire le nombre de tests insérés dans le programme renforcé. / One of the important goals of the software development process is proving that the produced systems always meet their requirements. However, establishing this goal is not only subtle and complex, but also requires high qualified persons. In addition, this operation is mostly omitted due to its high cost and the system is tested while trying to reduce the risk of errors as much as possible. The cost is, nevertheless, paid when this operation is required in order to avoid catastrophic consequences and major errors. In these cases, tools like theorem prover and those used for automatic generation of software are helpful to significantly reduce the cost of proof. Our aim is that this tool proves to be powerful and simple enough to generate benefits even to small companies and individuals with scarce budgets and limited theoretical skills . Many promising formal frameworks for automatic enforcement of security policies in programs have been proposed during the last years. Their goal is to ensure that a program respects a given security policy which generally specifies acceptable executions of the program and can be expressed in terms of access control problems, information flow, availability of resources, confidentiality, etc. The literature records various techniques for enforcing security policies belonging to mainly two principal classes: static approaches including typing theory, Proof Carrying Code, and dynamic approaches including reference monitors, Java stack inspection. Static analysis aims at enforcing properties before program execution. In dynamic analysis, however, the enforcement takes place at runtime by intercepting critical events during the program execution and halting the latter whenever an action is attempting to violate the property being enforced. Recently, several researchers have explored rewriting techniques in order to gather advantages of both static and dynamic methods. The idea consists in modifying a program statically, so that the produced version respects the requested requirements. The rewritten program is generated from the original one by adding, when necessary, some tests at some critical points to obtain the desired behaviors. This thesis aims to propose an algebraic and automatic approach that could generate from a given program, and a security policy, a new version of this program that respects the requested security policy. More precisely, we define an operator [symbol] that takes as input a process [symbol] and a security policy [symbol] and generates [symbol], a new process that respects the following conditions: [symbol] "satisfies" the security policy [symbol]. [symbol], behaviours of [symbol] are also behaviours of [symbol]. [symbol], all good behaviours of [symbol] are also behaviours [symbol]. The main results of our research are the following~: 1. The definition of a process algebra [symbol] offering an algebraic framework for the enforcement of security policies on concurrent systems. 2. The definition of a logic, denoted by [symbol], inspired from Kleene algebras and regular expressions. Basically, it allows to specify properties that can be checked on a trace-based model and properties related to infinite behavior (e.g. a server should not send the password of users). The choice of this logic is motivated by its syntax that is close to the one chosen for processes. In fact, this similarity is helpful to simplify the definition of our formal monitor. 3. The development of an optimization technique which, for a certain class of security properties, reduces the number of tests added in the target.

Depuis plusieurs années, nous constatons l'augmentation de l'utilisation des techniques d'agents et multiagent pour assister l'humain dans ses tâches. Ce travail de maîtrise se situe dans la même voie. Précisément, nous proposons d'utiliser les techniques multiagent de planification et de coordination pour la gestion de ressources dans les systèmes de commande et contrôle (C2) temps réel. Le problème particulier que nous avons étudié est la conception d'un système d'aide à la décision pour les opérations anti-aérienne sur les frégates canadiennes. Dans le cas où plusieurs frégates doivent se défendre contre des menaces, la coordination est un problème d'importance capitale. L'utilisation de mécanismes de coordination efficaces permet d'éviter les actions conflictuelles et la redondance dans les engagements. Dans ce mémoire, nous présentons quatre mécanismes de coordination basés sur le partage de tâche. Trois sont basés sur les communications : la coordination centrale, le Contract Net, la coordination similaire à celle proposée par Brown; tandis que la défense de zone est basée sur les lois sociales. Nous exposons enfin les résultats auxquels nous sommes arrivés en simulant ces différents mécanismes. / The use of agent and multiagent techniques to assist humans in their daily routines has been increasing for many years, notably in Command and Control (C2) systems. This thesis is is situated in this domain. Precisely, we propose to use multiagent planning and coordination techniques for resource management in real-time \acs{C2} systems. The particular problem we studied is the design of a decision-support for anti-air warfare on Canadian frigates. In the case of several frigates defending against incoming threats, multiagent coordination is a complex problem of capital importance. Better coordination mechanisms are important to avoid redundancy in engagements and inefficient defence caused by conflicting actions. In this thesis, we present four different coordination mechanisms based on task sharing. Three of these mechanisms are based on communications: central coordination, Contract Net coordination and Brown coordination, while the zone defence coordination is based on social laws. Finally, we expose the results obtained while simulating these various mechanisms.

Les progiciels de gestion intégrés (ERP) sont des applications fonctionnant à travers une organisation qui, grâce à leur intégration, automatisent les processus d’affaires de l’organisation. Les ERP se sont rapidement imposés dans l’industrie pour remplacer des applications patrimoniales. La pratique démontre que la majorité des déploiements de ERP dépassent leurs budgets et leurs échéances, par conséquent la recherche s’est mise à étudier les projets de migration pour fournir un cadre de déploiement optimal. Peu d’exemples de déploiement dans de grandes organisations sont documentés rigoureusement. Les applications ERP sont divisées en modules qui doivent être connectés à l’environnement patrimonial de l’organisation pour fournir des avantages concurrentiels. L’intégration des applications de l’entreprise (EAI) est définie comme le processus d’intégration d’applications avec l’environnement informatique. Le déploiement d’applications ERP peut être aisé lorsque les organisations possèdent une structure hiérarchique simple et réalisent des opérations dans un ou quelques lieux géographiques. Mais lorsque les organisations ont une structure hiérarchique complexe et sont géographiquement dispersés, le déploiement implique des choix, des défis techniques et de gestion uniques. Ce mémoire résume les stratégies de migration, les meilleures pratiques de réingénierie des processus d’affaires, l’analyse des applications patrimoniales et l’influence de la centralisation du pouvoir sur les processus d’une organisation. / Enterprise Resource Planning (ERP) systems are enterprise wide systems which, because of their integration, automate many business processes of a company. They have rapidly become the de facto industry standard for replacement of legacy systems. Because there is evidence that the overwhelming majority of ERP implementations exceed their budget and their time allocations, researchers have begun to analyse ERP implementation in case studies in order to provide an implementation framework which maximises efficiencies. Few examples of large organisation implementations are thoroughly documented. ERP applications are divided into modules that must be connected to an organisation's software environment to provide leverage. Enterprise Application Integration (EAI) is defined as the process of integrating enterprise systems with existing applications. Implementing ERP systems can be straightforward when organizations are simply structured and operate in one or a few locations. But when organizations are structurally complex and geographically dispersed, implementing ERP systems involves difficult, possibly unique, technical and managerial choices and challenges. This research summarises implementation strategies, best practices to reengineer business processes, analyse legacy software and the influence of centralisation of power on organisational processes.

Nous présentons une méthode symbolique pour représenter des modèles probabilistes à espace d’états continu (LMP). Ces modèles représentent des systèmes de transitions qui ont un nombre d’états non-dénombrable. L’objectif de l’utilisation d’une méthode symbolique est de consommer moins de mémoire lors de l’enregistrement du modèle. Notre technique pour enregistrer symboliquement les modèles est l’utilisation des diagrammes de décision binaire à terminaux multiples (MTBDD). Ces diagrammes offrent la possibilité d’enregistrer des fonctions à variables booléennes, ainsi que des graphes, de façon plus concise que les techniques plus fréquemment utilisées. Nous employons les MTBDD dans un vérificateur de modèles de type LMP nommé CISMO. La vérification de modèles est une technique entièrement automatique qui est utilisée pour vérifier si un modèle respecte ou non sa spécification. L’espace mémoire nécessaire pour faire la vérification dépend entre autres des structures utilisées pour enregistrer le modèle. Dans la première version de CISMO, le modèle était enregistré à l’aide de structures de données traditionnelles, comme des vecteurs. Cette façon de faire est qualifiée d’explicite. Nos modifications de CISMO lui permettent maintenant de faire la vérification de façon symbolique, à l’aide des MTBDD, en plus de la façon explicite. Nos principales contributions sont la description de deux heuristiques qui, dans certains contextes, réduisent la taille des diagrammes de décision binaire ordonnés, ainsi que la modification de CISMO. L’analyse de la mémoire consommée par CISMO après nos modifications nous montre que l’utilisation des diagrammes de décision permet de sauver de la mémoire.