Dissertations / Theses: 'Modèles symboliques'

1

Cortier, Véronique. "Analyse des protocoles cryptographiques: des modèles symboliques aux modèles calculatoires." Habilitation à diriger des recherches, Institut National Polytechnique de Lorraine - INPL, 2009. http://tel.archives-ouvertes.fr/tel-00578816.

Full text

Abstract:

Les protocoles de sécurité sont des programmes informatiques qui définissent des règles d'échange entre les points d'un réseau et permettent de sécuriser les communications. Ils sont utilisés par exemple dans les distributeurs de billets, les abonnements aux chaînes de télévision payantes, la téléphonie mobile, le commerce électronique. Leur objectif est de garantir le secret d'une donnée, d'authentifier un des participants, de garantir l'anonymat ou la non-répudiation, etc. Ces programmes sont exécutés sur des réseaux ouverts facilement accessibles (comme internet). Aussi, pour démontrer qu'ils remplissent bien leurs objectifs, il est nécessaire de prendre en compte les attaques dont ils peuvent faire l'objet. L'objet de mon mémoire d'habilitation à diriger des recherches est de montrer que les méthodes formelles peuvent être utilisées avec succès pour entreprendre une analyse fine des protocoles cryptographiques, à travers une palette variée d'outils. Nous présentons des procédures pour déterminer de façon automatique si un protocole est sûr. Nous avons proposés différents algorithmes en fonction des propriétés de sécurité considérées ainsi que des primitives cryptographiques utilisées (chiffrement, signature, hachage, ou exclusif, etc.). D'autre part, nous caractérisons des conditions qui permettent de combiner les résultats précédents et de concevoir les protocoles de façon modulaire. Ces résultats se basent sur des modèles symboliques, très différents de ceux utilisés en cryptographie où la notion de sécurité est basée sur la théorie de la complexité. Cette notion de sécurité est mieux adaptée pour identifier toutes les attaques possibles dans la réalité mais, en contrepartie, les (lourdes) preuves de sécurité sont effectuées à la main et semblent difficilement automatisables. Nous avons identifié des hypothèses cryptographiques qui permettent de relier les approches cryptographiques et symboliques. Il est alors possible d'obtenir des preuves de sécurité à un niveau cryptographique, directement à partir des preuves établies (automatiquement) dans un cadre symbolique.

APA, Harvard, Vancouver, ISO, and other styles

2

Rodriguez-Rojas, Oldemar. "Classification et modèles linéaires en analyse des données symboliques." Paris 9, 2000. https://portail.bu.dauphine.fr/fileviewer/index.php?doc=2000PA090064.

Full text

Abstract:

Ce travail s'inscrit dans le cadre de l'analyse de données symboliques. Le but de ce travail est de généraliser au cas symbolique certaines techniques de la classification automatique, aussi bien que quelques modèles lineaux. Ces généralisations seront toujours faites d'après deux principes fondamentaux de l'analyse de données symbolique, à savoir : l'analyse de données classique devrait être toujours un cas particulier de l'analyse de données symbolique et dans une analyse de données symbolique, tant la sortie comme l'entrée devraient être symboliques. Nous présentons deux nouveaux algorithmes, qui généralisent au cas symbolique de l'algorithme cap, l'algorithme cap et l'algorithme capso. Nous généralisons, pour les variables de type intervalle, la moyenne, la médiane, la moyenne des valeurs extrèmes, l'écart type, la déviation quartile, boites de dispersion (boxplot) et la correlation. Trois nouvelles méthodes sont aussi présentées pour effectuer la regression simple pour les variables de type intervalle. Nous étendons la methode d'analyse en composantes principales pour données de type histogramme, nous généralisons le cercle des corrélations au cas des variables de type intervalle. Nous proposons une méthode pour l'analyse des tableaux de proximités (multidimensional scaling) pour des données de type intervalle, que nous avons dénommée interscal. Pour chacune des méthodes présentées dans cette thèse un outil de logiciel a été mis en application. Ce logiciel a été dénommé PIMAD symbolique (programme integré de méthodes d'analyse de données symbolique).

APA, Harvard, Vancouver, ISO, and other styles

3

Revault, d'Allonnes Adrien. "Evaluation sémantique d'informations symboliques : la cotation." Paris 6, 2011. http://www.theses.fr/2011PA066395.

Full text

APA, Harvard, Vancouver, ISO, and other styles

4

Sandel, Arnaud. "Outils symboliques pour l'écriture de modèles et l'étude de sensibilité des systèmes multicorps." Lyon, INSA, 2007. http://theses.insa-lyon.fr/publication/2007ISAL0081/these.pdf.

Full text

Abstract:

Tout d'abord, la théorie des Tenseurs d'Inertie Globaux (TIG), qui permet d'écrire le modèle dynamique sous forme algébrique (sans dérivation), est reformulée et étendue aux systèmes multicorps à liaisons complexes et pseudo-paramètres. Puis deux méthodes ana-lytiques d'étude de sensibilité, quantifiant l'influence de paramètres de construction sur les performances, sont adaptées aux systèmes de solides rigides ; la méthode de l'état-adjoint, en général moins rapide que la méthode directe, devient intéressante lorsque le critère est une intégrale sur un intervalle de temps unique et que les paramètres de construction sont nombreux. Enfin, les outils formels des TIG sont utilisés pour obtenir le système de sensibilité et le système adjoint sans dérivation, et ainsi des équations mieux ordonnées. Les méthodes proposées sont validées sur des exemples (double-pendule orthogonal, véhicule) utilisant Maple ou Matlab. Les perspectives concernent les chaînes fermées et les sensibilités secondes
Analytical tools for systems of rigid bodies are proposed. First of all, the Global Inertia Tensors (GITs) theory, which allows the dynamic model to be written in an algebraic form (without any derivation), is extended under a new presentation to complex joints and pseudo-parameters systems. Secondly, two sensitivity analysis methods, which quantify the influence of constructive parameters on the system performances, are adapted to multibody systems ; the adjoint-state method, generally slower than the direct method, becomes interesting in the case of an integrated constraint on a single time interval and a great number of constructive parameters. Thirdly, the GITs formal tools are used to obtain the sensitivity system and the adjoint system without any derivation, and thus better organized equations. The proposed methods are validated on examples (orthogonal double pendulum, vehicles) using Maple or Matlab. The perspectives concern closed loops and second-order sensitivities

APA, Harvard, Vancouver, ISO, and other styles

5

Janvier, Romain. "Lien entre modèles symboliques et computationnels pour les protocoles cryptographiques utilisant des hachages." Grenoble 1, 2006. http://www.theses.fr/2006GRE10106.

Full text

Abstract:

"Les protocoles cryptographiques sont utilisés pour assurer des communications sécurisées sur des canaux non sécurisés. Deux approches sont utilisées pour vérifier ces protocoles. L'approche symbolique suppose que la cryptographie est parfaite. Ainsi, il est impossible de déchiffrer un message sans la clef adéquate. Ce modèle a permis le développement d'outils automatiques pour la vérification des protocoles cryptographiques. L'approche computationnelle, au contraire, s'intéresse à la probabilité de "casser" les primitives cryptographiques. Ce modèle est mal adapté aux méthodes automatiques de part la difficulté des raisonnements sur les probabilités. Récemment, plusieurs travaux ont été entrepris pour relier ces deux approches et ainsi profiter de leurs avantages respectifs: automatisation dans le modèle symbolique et plus grand réalisme du modèle computationnel. Les travaux présentés dans cette thèse permettent de relier le modèle symbolique au modèle computationnel, dans le cas de protocoles utilisant des chiffrements asymétrique et symétrique, des signatures et des hachages. Nous montrons que tout ce qui peut se passer dans le modèle computationnel, avec une probabilité non négligeable, peut également se passer dans le modèle symbolique. Ainsi, les résultats des outils de vérification automatiques dans le modèle symboliques sont également valides dans le modèle computationnel. "
Cryptographic protocols are used for secure communications over unreliable channels. Two approaches are used for their verification. The symbolic approach assume perfect cryptography. Automatic verification of cryptographic protocols is common with this model. On the other hand, the computational approache focuses on the probability to break cryptographic primitives but is not well-suited for automatic verification. Recently, several works have attempted to link these two approaches and thus benefites of the advantage of each: automatic verification for symbolic model and greater realism for computational model. The works presented in this thesis allow to link the symbolic and the computationnel models for protocols using asymmetric and symmetric encryptions, signatures and hashes. We show that whatever can append in the computational model, with non negligible probability, can also happened in the symbolic model. Thus, results of automatic verification tools in the symbolic model also hold in the computational model

APA, Harvard, Vancouver, ISO, and other styles

6

Rondeau, Laurent. "Identification des systèmes par modèles flous linguistiques : prise en compte des aspects numériques et symboliques." Nancy 1, 1997. http://www.theses.fr/1997NAN10278.

Full text

Abstract:

L'élaboration de modèles à partir d'informations numériques et symboliques relatives au comportement du système constitue la problématique de ce mémoire. Dans le premier chapitre, nous confrontons l'approche suivie dans le domaine de l'identification, qui s'appuie principalement sur la prise en compte d'informations numériques, à l'approche système expert qui se fonde sur des informations symboliques. Nous proposons alors une stratégie de prise en compte de l'ensemble de ces informations reposant sur l'utilisation d'un modèle flou linguistique. L'estimation des paramètres de ce type de modèles à partir d'informations numériques conduit à deux approches possibles, classique ou floue. La seconde, que nous choisissons, possède l'avantage de faire apparaître des critères très précis quant au choix du modèle et de la méthode d'estimation paramétrique. Le deuxième chapitre est consacré à l'analyse des différentes modèles flous linguistiques et méthodes d'estimation paramétrique par rapport aux critères définis au chapitre 1. On constate que le seul modèle vérifiant ces critères est le modèle à règles graduelles mono-entrée mono-sortie. Parallèlement, on vérifie qu'aucune méthode d'estimation paramétrique ne répond aux conditions spécifiées. Au cours du troisième chapitre, le modèle à règles graduelles est étendu au cas multi-entrées mono-sortie. Une réécriture sous forme symbolique de ce modèle est proposée afin de définir une stratégie d'estimation paramétrique adaptée à notre contexte et fondée sur la résolution d'équations de relation floue. Une méthodologie d'identification permettant la prise en compte des informations numériques et symboliques est ensuite proposée. Elle est appliquée à la modélisation d'un système statique non linéaire, cette application mettant en évidence les caractéristiques essentielles de la méthode
Building models from numeric and symbolic information relating to system behavior is the subject of this thesis. In the first chapter, the approach used in the domain of identification which is mainly based upon numeric information is compared with the expert system approach which is based on symbolic information. Then, we propose a strategy which takes into account both types of information by using a linguistic fuzzy model. Parametric estimation of these kinds of models from numeric information leads to two possible methods, classical or fuzzy. The second, which is chosen for our development, has the advantage of highlighting two particular criteria for the choice of the model and the parametric estimation method. The second chapter presents the analysis of linguistic fuzzy models and parametric estimation methods, with respect to the criteria defined in chapter 1. We demonstrate that only one model verifies all criteria, the single-input single-output gradual rules model. We also emphasize that no parametric estimation method satisfies the specified conditions. In the third chapter, the gradual rules model is extended to the multi-inputs single-output case. A symbolic form of this model is then proposed in order to define a parametric estimation strategy which fulfills our criteria and is based on the resolution of fuzzy relational equations. A methodology of identification which takes into account numeric and symbolic information is proposed. This is applied to the modelling of a static non-linear system which showcases the main characteristics of the method

APA, Harvard, Vancouver, ISO, and other styles

7

Stouls, Nicolas. "Systèmes de transitions symboliques et hiérarchiques pour la conception et la validation de modèles B raffinés." Phd thesis, Grenoble INPG, 2007. http://tel.archives-ouvertes.fr/tel-00216026.

Full text

Abstract:

Cette thèse propose une approche d'aide à la conception et au développement de modèles formels B. Cette approche se base sur la construction d'un système de transitions symboliques décrivant les comportements du modèle. Cette seconde vue est complémentaire avec la description orientée données du modèle B et peut être utilisée pour le décrire, le documenter ou le valider. Le système de transitions est élaboré à partir d'un espace d'états fourni par l'utilisateur et les transitions sont construites par résolution d'obligations de preuve. Nous proposons également de prendre en compte le processus de raffinement B en introduisant la notion de hiérarchie dans les systèmes de transitions. Cette représentation permet de mettre en évidence le lien entre les données des différents niveaux de raffinement. De plus, la méthode que nous proposons se base sur la décomposition des états d'une représentation du modèle abstrait, permettant ainsi de conserver la structure générale du système. Enfin, nous terminons ce manuscrit en décrivant l'outil GénéSyst qui implante cette méthode, ainsi que son utilisation dans le cadre du projet GECCOO, pour la vérification de propriétés de sécurité.

APA, Harvard, Vancouver, ISO, and other styles

8

Stouls, Nicolas. "Systèmes de transitions symboliques et hiérarchiques pour la conception et la validation de modèles B raffinés." Phd thesis, Grenoble INPG, 2007. http://www.theses.fr/2007INPG0180.

Full text

Abstract:

Cette thèse propose une approche d'aide à la conception et au développement de modèles formels B. Cette approche se base sur la construction d'un système de transitions symboliques décrivant les comportements du modèle. Cette seconde vue est complémentaire avec la description orientée données du modèle B et peut être utilisée pour le décrire, le documenter ou le valider. Le système de transitions est élaboré à partir d'un espace d'états fourni par l'utilisateur et les transitions sont construites par résolution d'obligations de preuve. Nous proposons également de prendre en compte le processus de raffinement B en introduisant la notion de hiérarchie dans les systèmes de transitions. Cette représentation permet de mettre en évidence le lien entre les données des différents niveaux de raffinement. De plus, la méthode que nous proposons se base sur la décomposition des états d'une représentation du modèle abstrait, permettant ainsi de conserver la structure générale du système. Enfin, nous terminons ce manuscrit en décrivant l'outil GénéSyst qui implante cette méthode, ainsi que son utilisation dans le cadre du projet GECCOO, pour la vérification de propriétés de sécurité
This thesis presents a new approach to help in the design and development of B models. This approach is based on the construction of a symbolic labeled transition system which describes the models behaviors. This description completes the data oriented description provided by the B model. It can also be used to document it or to validate it. The transition system is constructed from a user-defined data space on which transition relation is computed by solving proof obligations. We also propose to take into account the B refinement process by introducing some hierarchy in the transition systems. This representation allows exhibiting the link between data from several refinement levels. Moreover, the proposed method works by partitioning the states space of the more abstract description. This makes it possible to keep the abstract system global structure. Finally, the manuscript ends with a description of the GénéSyst tool, which implements the proposed method. We describe its use in the framework of the GECCOO project, in order to verify some security properties

APA, Harvard, Vancouver, ISO, and other styles

9

El, Golli Aicha. "Extraction de données symboliques et cartes topologiques : Application aux données ayant une structure complexe." Paris 9, 2004. https://portail.bu.dauphine.fr/fileviewer/index.php?doc=2004PA090026.

Full text

Abstract:

Un des objectifs de l'analyse de données symboliques est de permettre une meilleure modélisation des variations et des imprécisions des données réelles. Ces données expriment en effet, un niveau de connaissance plus élevé, la modélisation doit donc offrir un formalisme plus riche que dans le cadre de l'analyse de données classiques. Un ensemble d'opérateurs de généralisation symbolique existent et permettent une synthèse et représentation des données par le formalisme des assertions, formalisme défini en analyse de données symboliques. Cette généralisation étant supervisée, est souvent sensible aux observations aberrantes. Lorsque les données que l'on souhaite généraliser sont hétérogènes, certaines assertions incluent des observations virtuelles. Face à ce nouveau formalisme et donc cette extension d'ordre sémantique que l'analyse de données symbolique a apporté, une nouvelle approche de traitement et d'interprétation s'impose. Notre objectif au cours de ce travail est d'améliorer tout d'abord cette généralisation et de proposer ensuite une méthode de traitement de ces données. Nous proposons donc une décomposition permettant d'améliorer la énéralisation tout en offrant le formalisme symbolique. Cette décomposition est basée sur un algorithme divisif de classification. Nous avons aussi proposé une méthode de généralisation symbolique non supervisée basée sur l'algorithme des cartes topologiques de Kohonen. L'avantage de cette méthode est de réduire les données d'une manière non supervisée et de modéliser les groupes homogènes obtenus par des données symboliques. Notre seconde contribution porte sur l'élaboration d'une méthode de classification traitant les données à structure complexe. Cette méthode est une adaptation de la version batch de l'algorithme des cartes topologiques de Kohonen aux tableaux de dissimilarités. En effet, seule la définition d'une mesure de dissimilarité adéquate, est nécessaire pour le bon déroulement de la méthode.

APA, Harvard, Vancouver, ISO, and other styles

10

Hördegen, Heinrich. "Vérification des protocoles cryptographiques : comparaison des modèles symboliques avec une application des résultats : étude des protocoles récursifs." Thesis, Nancy 1, 2007. http://www.theses.fr/2007NAN10083.

Full text

Abstract:

Cette thèse traite de la vérification des protocoles cryptographiques. Son sujet est la modélisation symbolique de protocoles avec pour objectif la preuve de propriétés de sécurité. La thèse comprend deux parties: La première partie définit quatre modèles symboliques différant par les moyens syntaxiques que les concepteur peuvent utiliser pour représenter les primitives cryptographiques. On a observé que les vérificateurs utilisent des astuces de codage dans des modèles peu riches pour représenter les primitives manquantes. Nous montrons que ces codages sont corrects dans le sens où un protocole qui satisfait une propriété dans un modèle peu expressif la satisfait aussi dans un modèle plus riche. Nous terminons cette partie par la description d'un module que nous avons implémenté pour la plate-forme de vérification AVISPA. Ce module est basé sur des résultats permettant le transfert des propriétés d'un protocole, prouvées dans un modèle symbolique, vers un modèle calculatoire. Dans la deuxième partie de cette thèse, nous développons un modèle symbolique pour représenter des protocoles récursifs. Ces protocoles sont difficiles à analyser et peu de résultats de décidabilité existent. Nous montrons que notre modèle symbolique permet de retrouver une attaque connue contre une propriété d'un protocole de commerce électronique. Nous proposons ensuite une modification de ce protocole et montrons que le protocole modifié satisfait cette propriété
This thesis deals with formal verification of cryptographic protocols. It is about symbolic modelling of protocols with the objective to prove security properties. The thesis is split in two parts: The first part defines four symbolic models which differ in the syntactic resources that protocol designers may use do model cryptographic primitives. We found that engineers employ coding dodges in order to model missing cryptographic primitives in simpler models. We showed that these codings are correct in that protocol properties that are proven in lean models also hold in more elaborated models. We finish this part with the description of a module implementation for the verification plate-form AVISPA. The module is based on results that allow to automatically translate protocol properties, proven in symbolic models, to computational models. In the second part of this thesis, we develop a symbolic model in order to represent ecursive protocols. This class of protocols is difficult to analyse and, so far, there are only few decidability results. We show that our symbolic model allows us to retrieve an previously known attack against a special security property of an e-commerce protocol. We then modify this protocol and show that the property holds for the modified protocol

APA, Harvard, Vancouver, ISO, and other styles

11

Hördegen, Heinrich. "Vérification des protocoles cryptographiques : Comparaison des modèles symboliques avec une application des résultats --- Etude des protocoles récursifs." Phd thesis, Université Henri Poincaré - Nancy I, 2007. http://tel.archives-ouvertes.fr/tel-00193300.

Full text

Abstract:

Cette thèse traite de la vérification des protocoles cryptographiques. Son sujet est la modélisation symbolique de protocoles avec pour objectif la preuve de propriétés de sécurité. La thèse comprend deux parties: La première partie définit quatre modèles symboliques différant par les moyens syntaxiques que les concepteur peuvent utiliser pour représenter les primitives cryptographiques. On a observé que les vérificateurs utilisent des astuces de codage dans des modèles peu riches pour représenter les primitives manquantes. Nous montrons que ces codages sont corrects dans le sens où un protocole qui satisfait une propriété dans un modèle peu expressif la satisfait aussi dans un modèle plus riche. Nous terminons cette partie par la description d'un module que nous avons implémenté pour la plate-forme de vérification AVISPA. Ce module est basé sur des résultats permettant le transfert des propriétés d'un protocole, prouvées dans un modèle symbolique, vers un modèle calculatoire. Dans la deuxième partie de cette thèse, nous développons un modèle symbolique pour représenter des protocoles récursifs. Ces protocoles sont difficiles à analyser et peu de résultats de décidabilité existent. Nous montrons que notre modèle symbolique permet de retrouver une attaque connue contre une propriété d'un protocole de commerce électronique. Nous proposons ensuite une modification de ce protocole et montrons que le protocole modifié satisfait cette propriété.

APA, Harvard, Vancouver, ISO, and other styles

12

Atkinson, Gordon. "Communication factuelle et évocations symboliques dans l'action du message publicitaire : une application au marché du vin." Dijon, 2000. http://www.theses.fr/2000DIJOE007.

Full text

Abstract:

Le marché du vin est extrêmement concurrentiel, ce qui rend les actions de communication particulièrement importantes. Le produit vin est empreint de symboles. Par conséquent, il semble légitime de s'interroger sur la pertinence d'une communication symbolique (qui insiste sur l'histoire et la richesse symbolique du vin) versus une communication factuelle (caractéristique des entreprises viticoles du nouveau monde) pour les producteurs de vins traditionnels. Ce travail se base sur deux études : - l'étude principale confirme l'existence de relations entre l'implication, la motivation intrinsèque / extrinsèque, le style de vie et l'orientation classique / romantique de la personnalité et l'attitude à l'égard de la marque, à l'égard de la communication et l'intention d'achat. Nous avons également pu démontrer qu'il existe non seulement une relation entre les évocations d'une communication symbolique et l'attitude à l'égard de la marque, la communication et l'intention d'achat, mais également entre la nature des évocations prédominantes d'une maison de vin et les variables attitudinales. - l'analyse des données issues de l'étude expérimentale confirment à la fois l'influence favorable de la communication symbolique et de la communication factuelle sur les dimensions affectives et conatives de l'attitude. L'interprétation des données est facilitée notamment par l'analyse factorielle, la classification ascendante hiérarchique, les nuées dynamiques, l'analyse discriminante, l'analyse de variance, des tests l et des tests de chi-deux. Ce travail nous conduit à émettre, entre autres, les préconisations suivantes : - pour les vins de terroir, l'élaboration de communications caractérisées par des évocations positives à l'égard du consommateur, à partir de l'histoire du vignoble et de l'entreprise viticole. - pour les vins de certaines régions de la France qui manquent de l'histoire, la création de cette histoire artificiellement, ceci pouvant renforcer l'image et la personnalité de l'entreprise et de la marque.

APA, Harvard, Vancouver, ISO, and other styles

13

Karam, Margot. "Génération de test de circuits intégrés fondée sur des modèles fonctionnels." Phd thesis, Grenoble INPG, 1991. http://tel.archives-ouvertes.fr/tel-00339935.

Full text

Abstract:

Cette thèse concerne l'utilisation de modèles fonctionnels dans le test de circuits intégrés complexes. Dans la première partie, des vecteurs de test sont générés pour les automates d'états finis a partir de leurs spécifications de synthèse. Un premier ensemble de vecteurs de test est calcule en parcourant tous les arcs du graphe de contrôle. Les valeurs d'entrées non spécifiées sur les transitions sont fixées afin d'accroitre la couverture. Il est montre que ce test a une excellente couverture par rapport a sa longueur. Les fautes résiduelles sont détectées par une methode de distinction sur les modèles machine juste machine fausse. La deuxième partie est consacrée au test hiérarchisé de circuits complexes. Les vecteurs de test locaux aux blocs sont justifies vers les entrées primaires et propages en avant vers les sorties primaires en utilisant des variables symboliques et des modèles fonctionnels pour les blocs traverses. Des techniques originale de propagation retardée permettent de restreindre le nombre d'échecs des propagations. Un prototype en prolog a été expérimenté

APA, Harvard, Vancouver, ISO, and other styles

14

Lestiennes, Grégory. "Contributions au test de logiciel basé sur des spécifications formelles." Paris 11, 2005. http://www.theses.fr/2005PA112164.

Full text

Abstract:

Dans cette thèse, nous nous intéressons au test de conformité qui vise à vérifier que l'implémentation d'un système satisfait à sa spécification selon une relation de conformité entre le modèle de la spécification et celui de l'implémentation. Nous avons défini le modèle RIOLTS signifiant Restrictive Input/Output Labeled Transition System et la relation de conformité rioco pour Restrictive Input/Output COnformance dont la spécificité est de permettre la description de systèmes dont certaines entrées sont interdites dans certains états. Dans la seconde partie de cette thèse nous nous intéressons à la génération de tests à partir de modèles infinis manipulant des types de données complexes, encore appelés modèles symboliques. La présence de types de données complexes rend plus difficile le problème de la sélection des tests: en effet, à la potentielle infinité des comportements d'un système s'ajoute celle des valeurs que peuvent prendre les symboles apparaissant dans les actions symboliques. De plus, des gardes peuvent conditionner les transitions ce qui nous confronte au fait que certaines traces symboliques ne sont pas faisables. Nous proposons ici une stratégie de sélection applicable sur tout modèle basé sur les systèmes de transitions symboliques. Nous utilisons un solveur de contraintes pour déterminer les chemins de l'automate de la spécification qui sont faisables. Les difficultés rencontrées pour obtenir de tels chemins de manière rapide nous ont conduit à optimiser l'utilisation du solveur. Ainsi plusieurs méthodes ont été proposées et expérimentées afin d'améliorer les temps de résolution et d'en assurer la terminaison
In this thesis, we get interested in conformance testing whose goal is to check that the implementation of a system conforms to its specification w. R. T. A conformance relation between the model of the specification and the one of the implementation. We have defined the RIOLTS model standing for Restrictive Input/Output Labeled Transition System and the conformance relation rioco standing for Restrictive Input/Output COnformance. The particularity of this model is that it makes it possible to describe systems in which some inputs are forbidden in some states. In the second part of this thesis, we have worked on test generation and selection from infinite models using complex data types. These models are called symbolic models. Complex data types makes it harder the test selection problem: we must not only deal with the possible unlimited number of behaviors of systems but also with the unlimited number of values possible for the symbols appearing in symbolic actions. Moreover as guards may condition transitions, some symbolic traces are unfeasible. We propose a selection strategy that can be applied on any model based on symbolic transition systems. We use a constraint solver to determine feasible paths of the specification automata. Such paths are difficult to calculate, and to get them faster, we have had to optimize the use of the solver. Though, we have proposed and carried out experiments on many methods to reduce solving time and ensure the termination of calculations

APA, Harvard, Vancouver, ISO, and other styles

15

Issa, Razanne. "Analyse symbolique et inférence de modèles métaboliques." Thesis, Bordeaux, 2015. http://www.theses.fr/2015BORD0100/document.

Full text

Abstract:

L’objectif de cette thèse est de proposer une nouvelle méthode de construction de modèles métaboliques dans le contexte de la génomique comparée. Nous avons développé un outil, ab-pantograph, permettant l’inférence de modèles métabolique se basant sur la logique abductive. Pour ce faire, nous avons introduit une représentation logique de modèles métaboliques minimaux enzymatiques, puis à partir d’un modèle métabolique dit de référence, nous avons dérivé un modèle minimal enzymatique explicite accompagné d’association de gènes. Enfin, en couplant ce modèle métabolique au génome d’un organisme cible, nous inférons par abduction un modèle enzymatique pour cet organisme cible accompagné d’un ensemble d’associations de gènes, modèle que l’on veut congruent à celui que l’on aurait pu obtenir en ayant toutes les informations pour l’organisme cible.L’outil proposé, ab-pantograph, a été développé en utilisant la programmation logique par contraintes et Hyprolog
The objective of this thesis is to propose a new method of constructing metabolic models in the context of comparative genomics. We have developed a tool, abpantograph, allowing the inference of metabolic models based on the Abductive logic. To do this, we have introduced a logical representation of minimal enzymatic metabolic models and from a metabolic model called reference, we derived an explicit enzymatic minimal model accompanied by gene association. Finally, by coupling this metabolic modele with the genome of a target organism, we infer abductively a model enzyme for this target organism accompanied by a set of gene associations, pattern one wants congruent to that which is could have obtained by having all the information to the target organism. The proposed tool, ab-pantograph, has been developed using constraint logic programming and Hyprolog

APA, Harvard, Vancouver, ISO, and other styles

16

Ivanova, Elena. "Efficient Synthesis of Safety Controllers using Symbolic Models and Lazy Algorithms." Electronic Thesis or Diss., université Paris-Saclay, 2021. http://www.theses.fr/2021UPASG088.

Full text

Abstract:

Cette thèse porte sur le développement d'approches efficaces de synthèse de contrôleurs basées sur l'abstraction pour les systèmes cyber-physiques (CPS). Alors que les méthodes basées sur l'abstraction pour la conception de CPS ont fait l'objet de recherches intensives au cours des dernières décennies, l'évolutivité de ces techniques reste un problème. Cette thèse se concentre sur le développement d'algorithmes de synthèse paresseuse pour les spécifications de sécurité. Les spécifications de sécurité consistent à maintenir la trajectoire du système à l'intérieur d'un ensemble sûr donné. Cette spécification est de la plus haute importance dans de nombreux problèmes d'ingénierie, souvent prioritaires par rapport à d'autres exigences de performance. Les approches paresseuses surpassent l'algorithme de synthèse classique [Tabuada, 2009] en évitant les calculs, qui ne sont pas essentiels pour les objectifs de synthèse. Le chapitre 1 motive la thèse et présente l'état de l'art. Le chapitre 2 structure les approches de synthèse paresseuses existantes et met l'accent sur trois sources d'efficacité : les informations sur les états contrôlables a priori, les priorités sur les entrées et les états non accessibles à partir de l'ensemble initial. Le chapitre 3 propose un algorithme, qui explore itérativement les états à la frontière du domaine contrôlable tout en évitant l'exploration des états internes, en supposant qu'ils sont contrôlables en toute sécurité a priori. Un contrôleur de sécurité en boucle fermée pour le problème d'origine est alors défini comme suit : nous utilisons le contrôleur abstrait pour repousser le système d'un état limite vers l'intérieur, tandis que pour les états internes, toute entrée admissible est valide. Le chapitre 4 présente un algorithme qui restreint les calculs de synthèse du contrôleur aux seuls états atteignables tout en privilégiant les transitions de plus longue durée. Le système original est abstrait par un modèle symbolique avec une grille adaptative. De plus, un nouveau type d'échantillonnage temporel est également envisagé. Au lieu d'utiliser des transitions de durée prédéterminée, la durée des transitions est contrainte par des intervalles d'état qui doivent contenir l'ensemble accessible. Le chapitre 5 est consacré aux systèmes de transition monotones. L'approche de synthèse paresseuse introduite bénéficie d'une propriété monotone des systèmes de transition et de la structure ordonnée de l'espace d'état (d'entrée), et du fait que des spécifications de sécurité dirigées sont prises en compte. La classe de spécifications considérée s'enrichit alors d'intersections d'exigences de sécurité supérieures et inférieures fermées. Le chapitre 6 conclut la discussion et soulève de nouvelles questions pour les recherches futures
This thesis focuses on the development of efficient abstraction-based controller synthesis approaches for cyber-physical systems (CPS). While abstraction-based methods for CPS design have been the subject of intensive research over the last decades, the scalability of these techniques remains an issue. This thesis focus on developing lazy synthesis algorithms for safety specifications. Safety specifications consist in maintaining the trajectory of the system inside a given safe set. This specification is of the utmost importance in many engineering problems, often prioritized over other performance requirements. Lazy approaches outperform the classical synthesis algorithm [Tabuada, 2009] by avoiding computations, which are non-essential for synthesis goals. Chapter 1 motivates the thesis and discusses the state of the art. Chapter 2 structures the existing lazy synthesis approaches and emphasizes three sources of efficiency: information about a priori controllable states, priorities on inputs, and non-reachable from initial set states. Chapter 3 proposes an algorithm, which iteratively explores states on the boundary of controllable domain while avoiding exploration of internal states, supposing that they are safely controllable a priory. A closed-loop safety controller for the original problem is then defined as follows: we use the abstract controller to push the system from a boundary state back towards the interior, while for inner states, any admissible input is valid. Chapter 4 presents an algorithm that restricts the controller synthesis computations to reachable states only while prioritizing longer-duration transitions. The original system is abstracted by a symbolic model with an adaptive grid. Moreover, a novel type of time sampling is also considered. Instead of using transitions of predetermined duration, the duration of the transitions is constrained by state intervals that must contain the reachable set. Chapter 5 is dedicated to monotone transition systems. The introduced lazy synthesis approach benefits from a monotone property of transition systems and the ordered structure of the state (input) space, and the fact that directed safety specifications are considered. The considered class of specifications is then enriched by intersections of upper and lower-closed safety requirements. Chapter 6 concludes the discussion and raises new issues for future research

APA, Harvard, Vancouver, ISO, and other styles

17

Hadjeres, Gaëtan. "Modèles génératifs profonds pour la génération interactive de musique symbolique." Thesis, Sorbonne université, 2018. http://www.theses.fr/2018SORUS027/document.

Full text

Abstract:

Ce mémoire traite des modèles génératifs profonds appliqués à la génération automatique de musique symbolique. Nous nous attacherons tout particulièrement à concevoir des modèles génératifs interactifs, c'est-à-dire des modèles instaurant un dialogue entre un compositeur humain et la machine au cours du processus créatif. En effet, les récentes avancées en intelligence artificielle permettent maintenant de concevoir de puissants modèles génératifs capables de générer du contenu musical sans intervention humaine. Il me semble cependant que cette approche est stérile pour la production artistique dans le sens où l'intervention et l'appréciation humaines en sont des piliers essentiels. En revanche, la conception d'assistants puissants, flexibles et expressifs destinés aux créateurs de contenus musicaux me semble pleine de sens. Que ce soit dans un but pédagogique ou afin de stimuler la créativité artistique, le développement et le potentiel de ces nouveaux outils de composition assistée par ordinateur sont prometteurs. Dans ce manuscrit, je propose plusieurs nouvelles architectures remettant l'humain au centre de la création musicale. Les modèles proposés ont en commun la nécessité de permettre à un opérateur de contrôler les contenus générés. Afin de rendre cette interaction aisée, des interfaces utilisateurs ont été développées ; les possibilités de contrôle se manifestent sous des aspects variés et laissent entrevoir de nouveaux paradigmes compositionnels. Afin d'ancrer ces avancées dans une pratique musicale réelle, je conclue cette thèse sur la présentation de quelques réalisations concrètes (partitions, concerts) résultant de l'utilisation de ces nouveaux outils
This thesis discusses the use of deep generative models for symbolic music generation. We will be focused on devising interactive generative models which are able to create new creative processes through a fruitful dialogue between a human composer and a computer. Recent advances in artificial intelligence led to the development of powerful generative models able to generate musical content without the need of human intervention. I believe that this practice cannot be thriving in the future since the human experience and human appreciation are at the crux of the artistic production. However, the need of both flexible and expressive tools which could enhance content creators' creativity is patent; the development and the potential of such novel A.I.-augmented computer music tools are promising. In this manuscript, I propose novel architectures that are able to put artists back in the loop. The proposed models share the common characteristic that they are devised so that a user can control the generated musical contents in a creative way. In order to create a user-friendly interaction with these interactive deep generative models, user interfaces were developed. I believe that new compositional paradigms will emerge from the possibilities offered by these enhanced controls. This thesis ends on the presentation of genuine musical projects like concerts featuring these new creative tools

APA, Harvard, Vancouver, ISO, and other styles

18

Hadjeres, Gaëtan. "Modèles génératifs profonds pour la génération interactive de musique symbolique." Electronic Thesis or Diss., Sorbonne université, 2018. http://www.theses.fr/2018SORUS027.

Full text

Abstract:

Ce mémoire traite des modèles génératifs profonds appliqués à la génération automatique de musique symbolique. Nous nous attacherons tout particulièrement à concevoir des modèles génératifs interactifs, c'est-à-dire des modèles instaurant un dialogue entre un compositeur humain et la machine au cours du processus créatif. En effet, les récentes avancées en intelligence artificielle permettent maintenant de concevoir de puissants modèles génératifs capables de générer du contenu musical sans intervention humaine. Il me semble cependant que cette approche est stérile pour la production artistique dans le sens où l'intervention et l'appréciation humaines en sont des piliers essentiels. En revanche, la conception d'assistants puissants, flexibles et expressifs destinés aux créateurs de contenus musicaux me semble pleine de sens. Que ce soit dans un but pédagogique ou afin de stimuler la créativité artistique, le développement et le potentiel de ces nouveaux outils de composition assistée par ordinateur sont prometteurs. Dans ce manuscrit, je propose plusieurs nouvelles architectures remettant l'humain au centre de la création musicale. Les modèles proposés ont en commun la nécessité de permettre à un opérateur de contrôler les contenus générés. Afin de rendre cette interaction aisée, des interfaces utilisateurs ont été développées ; les possibilités de contrôle se manifestent sous des aspects variés et laissent entrevoir de nouveaux paradigmes compositionnels. Afin d'ancrer ces avancées dans une pratique musicale réelle, je conclue cette thèse sur la présentation de quelques réalisations concrètes (partitions, concerts) résultant de l'utilisation de ces nouveaux outils
This thesis discusses the use of deep generative models for symbolic music generation. We will be focused on devising interactive generative models which are able to create new creative processes through a fruitful dialogue between a human composer and a computer. Recent advances in artificial intelligence led to the development of powerful generative models able to generate musical content without the need of human intervention. I believe that this practice cannot be thriving in the future since the human experience and human appreciation are at the crux of the artistic production. However, the need of both flexible and expressive tools which could enhance content creators' creativity is patent; the development and the potential of such novel A.I.-augmented computer music tools are promising. In this manuscript, I propose novel architectures that are able to put artists back in the loop. The proposed models share the common characteristic that they are devised so that a user can control the generated musical contents in a creative way. In order to create a user-friendly interaction with these interactive deep generative models, user interfaces were developed. I believe that new compositional paradigms will emerge from the possibilities offered by these enhanced controls. This thesis ends on the presentation of genuine musical projects like concerts featuring these new creative tools

APA, Harvard, Vancouver, ISO, and other styles

19

Daniel-Vatonne, Marie-Christine. "Les termes : un modèle de représentation et structuration de données symboliques." Montpellier 2, 1993. http://www.theses.fr/1993MON20031.

Full text

Abstract:

Nos travaux se situent dans le cadre de l'analyse conceptuelle des donnees. Notre objectif est de generaliser les representations par variables binaires ou nominales en y adjoignant la modelisation de structures internes. Le probleme est de ne pas perdre en complexite algorithmique ce qui est gagne en puissance de representation. Selon ces considerations, decrire les donnees et les classes de donnees par des structures arborescentes est un bon compromis. Le systeme de representation que nous proposons s'appuie sur un modele algebrique: les magmas. Il permet de construire des termes assimilables a des arborescences finies, etiquetees et typees. Leur interpretation est intuitive et ils autorisent les descriptions recursives. Une relation d'ordre naturel, la generalisation, induit un treillis sur les termes. Nous etudions ce treillis et montrons qu'il possede des proprietes proches de celles d'un treillis booleen. En particulier, nous montrons que l'on peut construire un treillis de galois mettant en correspondance des ensembles d'objets et leur description par des termes

APA, Harvard, Vancouver, ISO, and other styles

20

Mazaré, Laurent. "Protocoles cryptographiques : lien entre les vues symboliques et computationnelles." Grenoble INPG, 2006. http://www.theses.fr/2006INPG0118.

Full text

Abstract:

Les protocoles cryptographiques sont utilisés pour assurer des communications securisiées sur des canaux non securisés. Deux approches sont utilisées pour vérifier ces protocoles. L'approche symbolique suppose que la cryptographie est parfaite et a permis le développement d'outils automatiques pour la vérification des protocoles. L'approche computationnelle, au contraire, s'intéresse à la probabilité de "casser" les primitives cryptographiques. Les travaux présentés dans cette thèse permettent de relier le modèle symbolique au modèle computationnel, cela pour des protocoles utilisant les chiffrements asymétrique et symétrique ainsi que la signature numérique. De plus, nous étudions trois extensions possibles de ce résultat : l'ajout d'échanges de clés à la Diffie-Hellman (utilisant une exponentiation modulaire), le cas où l'adversaire est confronté à un nombre non borné de challenges et l'utilisation de propriétés plus complexes par le biais de l'opacité
Cryptographie protocols are used to ensure secure communications over insecure channels. Two approaches are used to verify protocols : the symbolic approach, more abstract, but for which many automatic tools exist and the computational approach, more realistic but harder to use. This document links the symbolic and computational views for protocols using asymmetric and symmetric cryptography as weil as digital signature. We also propose three extensions: adding DiffieHellman to handle key exchange protocols using modular exponentiation, considering adversary with access to an unbounded number of challenges and the case of more complex properties defined using opacity

APA, Harvard, Vancouver, ISO, and other styles

21

Nguyên, Duy-Tùng. "Vérification symbolique de modèles à l'aide de systèmes de ré-écriture dédiés." Phd thesis, Université d'Orléans, 2010. http://tel.archives-ouvertes.fr/tel-00579490.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

22

Maille, Nicolas. "Modèle logico-algébrique pour la fusion symbolique et l'analyse formelle." Toulouse, ENSAE, 1999. http://www.theses.fr/1999ESAE0021.

Full text

Abstract:

Dans cette thèse, nous nous intéressons aux formalismes de représentation et de manipulation de la connaissance dans des sytèmes nécessitant une représentation symbolique d'une réalité observée. Nous examinons plus particulièrement deux types de traitement de l'information : la fusion et la classification. Nous montrons le besoin d'un otuil algébrique pour structurer la connaissance. Puis nous nous penchons sur les structures de treillis et mettons en évidence leur adéquation pour caractériser un résultat de fusion. En nous fondant sur l'algèbre des treillis et la logique des prédicats nous construisons le modèle des cubes. Celui-ci définit, dans une optique mathématique, une théorie homogène pour la manipulation des conjonctions de propriétés. Le processus d'enrichissement du modèle est relancé par l'introduction des contraintes. Après un développement théorique conséquent la structure de treillis est retrouvée pour le modèle des cubes contraints. Celui-ci permet une représentation équilibrée des connaissances selon une composante logique et une composante numérique traduite par des intervalles. Parallèlement, les situations de fusion posent la question du choix des objets à fusionner. Nous nous intéressons à l'Analyse Formelle de Concepts qui permet de regrouper et structurer des objets en fonction de leur propriétés. Nous étendons cet outil formel pour prendre en compte une caractérisation des objets de la situation grâce à des cubes ou à des cubes contraints.

APA, Harvard, Vancouver, ISO, and other styles

23

Lozano, Aparicio Jose Martin. "Data exchange from relational databases to RDF with target shape schemas." Thesis, Lille 1, 2020. http://www.theses.fr/2020LIL1I063.

Full text

Abstract:

Resource Description Framework (RDF) est un modèle de graphe utilisé pour publier des données sur le Web à partir de bases de données relationnelles. Nous étudions l'échange de données depuis des bases de données relationnelles vers des graphes RDF avec des schémas de formes cibles. Essentiellement, échange de données modélise un processus de transformation d'une instance d'un schéma relationnel, appelé schéma source, en un graphe RDF contraint par un schéma cible, selon un ensemble de règles, appelé tuple source-cible générant des dépendances. Le graphe RDF obtenu est appelé une solution. Étant donné que les dépendances générant des tuple définissent ce processus de manière déclarative, il peut y avoir de nombreuses solutions possibles ou aucune solution du tout. Nous étudions le système d'échange de données relationnel avec RDF constructive avec des schémas de formes cibles, qui est composé d'un schéma source relationnel, un schéma de formes pour le schéma cible, un ensemble de mappages utilisant des constructeurs IRI. De plus, nous supposons que deux constructeurs IRI ne se chevauchent pas. Nous proposons un langage visuel pour la spécification des correspondances (VML) qui aide les utilisateurs non experts à spécifier des mappages dans ce système. De plus, nous développons un outil appelé ShERML qui effectue l'échange de données avec l'utilisation de VML et pour les utilisateurs qui souhaitent comprendre le modèle derrière les mappages VML, nous définissons R2VML, un langage texte, qui capture VML et présente une syntaxe succincte pour définition des mappages.Nous étudions le problème de la vérification de la consistance: un système d'échange de données est consistent si pour chaque instance de source d'entrée, il existe au moins une solution. Nous montrons que le problème de consistance est coNP-complet et fournissons un algorithme d'analyse statique du système qui permet de décider si le système est consistent ou non.Nous étudions le problème du calcul de réponses certaines. Une réponse est certaine si la réponse tient dans chaque solution. En générale, réponses certaines sont calculées en utilisant d'une solution universelle. Cependant, dans notre contexte, une solution universelle pourrait ne pas exister. Ainsi, nous introduisons la notion de solution de simulation universelle, qui existe toujours et permet de calculer certaines réponses à n'importe quelle classe de requêtes robustes sous simulation. Une de ces classes sont les expressions régulières imbriquées (NRE) qui sont forward c'est-à-dire qui n'utilisent pas l’opération inverse. L'utilisation d'une solution de simulation universelle rend traitable le calcul de réponses certaines pour les NRE (data-complexity).Enfin, nous étudions le problème d'extraction de schéma des formes qui consiste à construire un schéma de formes cibles à partir d'un système constructif d'échange de données relationnel vers RDF sans le schéma de formes cibles. Nous identifions deux propriétés souhaitables d'un bon schéma cible, qui sont la correction c'est-à-dire que chaque graphe RDF produit est accepté par le schéma cible; et la complétude c'est-à-dire que chaque graphe RDF accepté par le schéma cible peut être produit. Nous proposons un algorithme d'extraction qui convient à tout système d'échange de données sans schéma, mais qui est également complet pour une grande classe pratique de systèmes sans schéma
Resource Description Framework (RDF) is a graph data model which has recently found the use of publishing on the web data from relational databases. We investigate data exchange from relational databases to RDF graphs with target shapes schemas. Essentially, data exchange models a process of transforming an instance of a relational schema, called the source schema, to a RDF graph constrained by a target schema, according to a set of rules, called source-to-target tuple generating dependencies. The output RDF graph is called a solution. Because the tuple generating dependencies define this process in a declarative fashion, there might be many possible solutions or no solution at all. We study constructive relational to RDF data exchange setting with target shapes schemas, which is composed of a relational source schema, a shapes schema for the target schema, a set of mappings that uses IRI constructors. Furthermore, we assume that any two IRI constructors are non-overlapping. We propose a visual mapping language (VML) that helps non-expert users to specify mappings in this setting. Moreover, we develop a tool called ShERML that performs data exchange with the use of VML and for users that want to understand the model behind VML mappings, we define R2VML, a text-based mapping language, that captures VML and presents a succinct syntax for defining mappings.We investigate the problem of checking consistency: a data exchange setting is consistent if for every input source instance, there is at least one solution. We show that the consistency problem is coNP-complete and provide a static analysis algorithm of the setting that allows to decide if the setting is consistent or not. We study the problem of computing certain answers. An answer is certain if the answer holds in every solution. Typically, certain answers are computed using a universal solution. However, in our setting a universal solution might not exist. Thus, we introduce the notion of universal simulation solution, which always exists and allows to compute certain answers to any class of queries that is robust under simulation. One such class is nested regular expressions (NREs) that are forward i.e., do not use the inverse operation. Using universal simulation solution renders tractable the computation of certain answers to forward NREs (data-complexity).Finally, we investigate the shapes schema elicitation problem that consists of constructing a target shapes schema from a constructive relational to RDF data exchange setting without the target shapes schema. We identity two desirable properties of a good target schema, which are soundness i.e., every produced RDF graph is accepted by the target schema; and completeness i.e., every RDF graph accepted by the target schema can be produced. We propose an elicitation algorithm that is sound for any schema-less data exchange setting, but also that is complete for a large practical class of schema-less settings

APA, Harvard, Vancouver, ISO, and other styles

24

Cherifi, Dalila. "Utilisation d'un modèle symbolique pour l'interprétation d'images Radar à Ouverture Synthétique." Paris, ENST, 2005. http://www.theses.fr/2005ENST0036.

Full text

Abstract:

Au fil des années, l'imagerie radar à synthèse d'ouverture (RSO ) s'affirme comme une modalité fiable et pertinente en télédétection. En effet, la détection du réseau routier sur ce type d'images par des opérateurs de bas niveau tels que les détecteurs de lignes nous donne un taux de fausses détection élevé. Ceci est dû notamment à la présence du speckle. D'où la nécessité de faire suivre l'étape de bas-niveau par une étape de plus haut niveau, dans laquelle nous injectons des informations structurelles sur la forme des routes par l'intermédiaire d'un modèle symbolique. A cet effet, nous proposons dans cette thèse de traiter deux niveaux de modèles symboliques, par complexité croissante. Dans un premier temps nous traitons un modèle assez complet issu de données cartographiques, avec des informations spatiales relativement précises. Dans un second temps nous utilisons un modèle grossier correspondant à un schéma "manuel" représentant les objets à extraire avec des indications approximatives sur leurs formes et leurs positions relatives. Ainsi, nous proposons dans cette thèse deux approches pour intégrer au mieux cette information exogène. En effet, dans une première partie, nous proposons une méthode markovienne qui permet par l'intermédiaire du terme a priori d'introduire des connaissances sur les objets recherchés. Dans une second partie, nous proposons une méthode de recherche de chemin optimal basée sur la programmation dynamique. Enfin, nous présentons notre méthode d'extraction de réseau routier sur les images radar (RSO ) en utilisant des données symboliques ainsi que quelques applications de notre travail
Synthetic Aperture Radar (SAR) instruments are active microwave sensors that operate independently of time of day and weather conditions. SAR can achieve high resolution from long range and provide information about the physical structure and the electrical properties of remotely sensed objects. There has been a growing interest in SAR for automatic target recognition. We are interested in this thesis by road detection in spaceborne SAR (Synthetic Aperture Radar images. Several approaches have been proposed in the literature. They generally consist of two steps: in the first step they use a local operator like edge and line detectors and then they apply a global criterion which incorporates additional knowledge about the structure of the objects to be detected. The aim of this thesis is the detection of road on SAR images starting from a graphical sketch of road defined by a user which is considered as a model of road. To do this we propose to compare two methods. The first one combines both local and global criteria based on Markov Field(MRF). It is based on a previously published methods for road detection in SAR images. The second method uses a dynamic programming, it defines a cost, which depends on local information, and performs a summation minimization process in a graph. The results obtained with the two approaches applied to different SAR images are presented and evaluated with an objective criterion. Finnally, we applied our method based of dynamic programming to extract road network on the different SAR images and we present some applications of our work

APA, Harvard, Vancouver, ISO, and other styles

25

Dumitrescu, Emil. "Construction de modèles réduits et vérification symbolique de circuits industriels décrits au niveau RTL." Université Joseph Fourier (Grenoble), 2003. http://www.theses.fr/2003GRE10101.

Full text

APA, Harvard, Vancouver, ISO, and other styles

26

Faget, Zoé. "Un modèle pour la gestion des séquences temporelles synchronisées : Application aux données musicales symboliques." Phd thesis, Université Paris Dauphine - Paris IX, 2011. http://tel.archives-ouvertes.fr/tel-00676537.

Full text

Abstract:

La première partie de ma thèse est la description d'un modèle algébrique pour la gestion des séquences temporelles synchronisées. Ce modèle est une extension du modèle relationnel classique auquel on ajoute un type nouveau, le type séquence temporelle. L'algèbre relationnelle est augmentée de trois opérateurs dédiés à ce nouveau type. Ces opérateurs permettent de retrouver toutes les opérations classiquement conduites sur des séquences temporelles. Le langage utilisateur correspondant est exposé, ainsi que de nombreux exemples, puisés notamment dans le domaine de la gestion des partitions symboliques. La seconde partie est la description d'un index permettant de réaliser plusieurs types de recherches dans des partitions symboliques (exacte, transposée, avec ou sans rythme et approchée). Il repose notamment sur la notion de signature algébrique. Dans la dernière partie, je décris une plateforme dédiée à la gestion du contenu musical symbolique qui est une application des deux précédentes parties.

APA, Harvard, Vancouver, ISO, and other styles

27

Caillou, Philippe. "Modèle ARCO : Apprentissages multiples et Raisonnement réflexif sur des Connaissances homogènes." Paris 9, 2004. https://portail.bu.dauphine.fr/fileviewer/index.php?doc=2004PA090040.

Full text

Abstract:

Nous présentons un modèle d'agent qui s'adapte à son environnement. Il découvre et utilise efficacement de nouveaux concepts, objets, heuristiques, selon son expérience. Pour pouvoir créer, exécuter et analyser ses propres règles, les connaissances sont décrites de façon homogène dans un graphe orienté. Leur utilisation homogène et efficace se fait grâce à la transmission d'un flux d'activation dans le graphe. Seuls les concepts et règles les plus utiles en fonction de l'état mental de l'agent sont utilisés. La découverte de nouveaux concepts se fait par induction par l'analyse de données symboliques. Des règles de déduction permettent de créer les règles et liens associés aux nouveaux concepts. Le contrôle de l'agent par les émotions permet d'intégrer les nouveaux concepts en renforçant les liens utiles et de guider l'agent indépendamment de sa sémantique. Un agent utilisant le modèle décrit a été implanté afin de vérifier sa cohérence et son fonctionnement sur un exemple simple.

APA, Harvard, Vancouver, ISO, and other styles

28

Charrier, Tristan. "Complexité théorique du raisonnement en logique épistémique dynamique et étude d’une approche symbolique." Thesis, Rennes 1, 2018. https://ged.univ-rennes1.fr/nuxeo/site/esupversions/2a4b2a55-42ff-4768-9b9e-677421fef507.

Full text

Abstract:

Nous étudions la complexité théorique de tâches de raisonnement mettant en jeu la connaissance des agents dans les systèmes multi-agents. Nous considérons la logique épistémique dynamique (DEL) comme une façon naturelle d'exprimer la connaissance, qui permet d'exprimer la connaissance d'ordre supérieur des agents et des actions dynamiques partiellement observées. Nous montrons des résultats de complexité algorithmique pour la vérification de modèles et la satisfiabilité de formules de DEL, et définissons une approche symbolique pour ces mêmes problèmes. Nous étudions également la planification basée sur DEL ainsi que des quantifications sur certaines actions : les annonces publiques
We study the theoretical complexity of reasoning tasks involving knowledge in multi-agent systems. We consider dynamic epistemic logic (DEL) as a natural way of expressing knowledge, which allows to express nested knowledge of agents and partially observed dynamic actions. We show complexity results for model checking and satisfiability of DEL formulas, and define a symbolic approach for these problems. We also study DEL-based planning and quantification over specific actions: public announcements

APA, Harvard, Vancouver, ISO, and other styles

29

Sayed, Mazen El. "Une approche logico-symbolique des connaissances nuancées via des modificateurs linguistiques." Angers, 2001. http://www.theses.fr/2001ANGE0021.

Full text

Abstract:

Le traitement de la connaissance imprécise occupe une place centrale dans les recherches en Intelligence Artificielle. Parmi les approches proposées, on peut faire ressortir deux grandes catégories principales : 1. Celles numériques se basant sur la théorie des ensembles flous et la logique floue, 2. Celles symboliques dédiées au traitement de l'imprécision de nature qualitative. Ces approches se basent sur la théorie des multi-ensembles et des logiques symboliques multivalentes. Dans cette thèse, nous présentons une approche qualitative purement symbolique de représentation et d'exploitation des connaissances imprécises du langage naturel. Cette approche est construite sur le substrat d'une logique symbolique multivalente proposée par Pacholczyk. Dans un premier temps, nous proposons une modélisation multi-ensembliste pour les termes imprécis du langage. Dans cette modélisation, nous associons à chaque terme imprécis une " réglette " dont la géométrie représente le caractère imprécis et graduel de ce terme. La description de cette " réglette " est fournie par un expert dans un langage déclaratif et purement symbolique. En nous basant sur la nouvelle modélisation, nous définissons des modificateurs linguistiques (notamment les modificateurs de précision et ceux de translation) dans un contexte multi-ensembliste. Ensuite, nous proposons de nouvelles règles de Modus Ponens généralisé enrichissant ainsi le système d'exploitation symbolique de connaissances imprécises proposé par Pacholczyk. Dans ces généralisations, nous utilisons une relation de similarité multi-ensembliste et une relation de proximité. La première est une relation réflexive, symétrique et " faiblement transitive ". La deuxième est une relation réflexive et " faiblement transitive "

APA, Harvard, Vancouver, ISO, and other styles

30

Rebeuf, Xavier. "Un modèle de coût symbolique pour les programmes parallèles asynchrones à dépendances structurées." Orléans, 2000. http://www.theses.fr/2000ORLE2056.

Full text

Abstract:

L'objectif d'une parallélisation est souvent de minimiser en premier lieu le temps d'exécution. Il paraît donc indispensable de disposer d'un modèle permettant d'évaluer a priori les performances d'un algorithme. Or, l'évaluation repose sur l'identification des synchronisations pour chaque exécution (dépendances-écriture-lecture). Sans restriction de l'expression du parallélisme, un calcul exact conduit généralement à une explosion combinatoire. Pour pallier ce problème, les modèles de coût classiques, ne prennent généralement en compte qu'une partie du parallélisme possible, permettant ainsi de définir statiquement un surensemble cohérent des dépendances de toutes les exécutions d'un algorithme. Nous proposons un modèle intermédiaire fondé sur la structuration de la résolution dynamique des accès aux données. Nous montrons qu'il est possible de représenter symboliquement l'ensemble des dépendances effectives de chaque exécution, et d'obtenir ainsi une évaluation exacte du coût sans explosion combinatoire. Nous conditionnons l'existence de chaque dépendance en l'annotant par un prédicat. Le coût d'un programme est alors exprimé symboliquement en fonction de ces prédicats. Pour être capable de l'évaluer dans l'environnement initial, nous transformons les prédicats grâce à une méthode fondée sur le calcul des plus faibles préconditions. Le coût symbolique obtenu est paramétré par l'environnement initial et il intègre les indépendances dynamiques. Afin d'assurer la compositionalité des coûts symboliques, nous étendons le calcul des plus faibles préconditions aux expressions. Nous développons pour cela une sémantique permettant d'exprimer symboliquement ce que calcule le programme et de calculer son coût par induction sur la syntaxe. Nous montrons qu'il est possible d'intégrer au modèle des paramètres de l'architecture ainsi qu'une charge instantanée du réseau. Nous comparons les résultats obtenus sur plusieurs algorithmes avec des expérimentations sur Cray T3E.

APA, Harvard, Vancouver, ISO, and other styles

31

Paquette, Simon. "Évaluation symbolique de systèmes probabilistes à espace d'états continu." Thesis, Université Laval, 2005. http://www.theses.ulaval.ca/2005/22827/22827.pdf.

Full text

Abstract:

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.

APA, Harvard, Vancouver, ISO, and other styles

32

Lamirel, Jean-Charles. "Vers une approche systémique et multivues pour l'analyse de données et la recherche d'information : un nouveau paradigme." Habilitation à diriger des recherches, Université Nancy II, 2010. http://tel.archives-ouvertes.fr/tel-00552247.

Full text

Abstract:

Le sujet principal de notre travail d'habilitation concerne l'extension de l'approche systémique, initialement implantée dans le Système de Recherche d'Information NOMAD, qui a fait l'objet de notre travail de thèse, pour mettre en place un nouveau paradigme général d'analyse de données basé sur les points de vue multiples, paradigme que nous avons baptisé MVDA (Multi-View Data Analysis). Ce paradigme couvre à la fois le domaine de l'analyse de données et celui de la fouille de données. Selon celui-ci, chaque analyse de données est considérée comme une vue différente sur les données. Le croisement entre les vues s'opère par l'intermédiaire d'un réseau bayésien construit, de manière non supervisée, à partir des données ou des propriétés partagées entre ces dernières. Le paradigme MDVA repose également sur l'exploitation de méthodes spécifiques de visualisation, comme la visualisation topographique ou la visualisation hyperbolique. La mise en place de nouveaux estimateurs de qualité de type Rappel/Précision non supervisés basés sur l'analyse de la distribution des propriétés associées aux classes, et qui à la fois sont indépendants des méthodes de classification et des changements relatifs à leur mode opératoire (initialisation, distances utilisées ...), nous a permis de démontrer objectivement la supériorité de ce paradigme par rapport à l'approche globale, classique en analyse de données. Elle nous a également permis de comparer et d'intégrer dans le paradigme MVDA des méthodes de classification non supervisées (clustering) neuronales qui sont plus particulièrement adaptées à la gestion des données ultra-éparses et fortement multidimensionnelles, à l'image des données documentaires, ainsi que d'optimiser le mode opératoire de telles méthodes. Notre démarche a par ailleurs impliqué de développer la cohabitation entre le raisonnement neuronal et le raisonnement symbolique, ou entre des modèles de nature différente, de manière à couvrir l'ensemble des fonctions de la recherche et de l'analyse de l'information et à éliminer, sinon à réduire, les défauts inhérents à chacun des types d'approche. A travers de nombreuses applications, notamment dans le domaine de l'évaluation des sciences, nous montrons comment l'exploitation d'un tel paradigme peut permettre de résoudre des problèmes complexes d'analyse de données, comme ceux liés l'analyse diachronique à grande échelle des données textuelles polythématiques. Nous montrons également comment l'ensemble des outils développés dans le cadre de ce paradigme nous ont permis mettre en place de nouvelles méthodes très robustes et très performantes pour la classification supervisée et pour le clustering incrémental. Nous montrons finalement comment nous envisageons d'étendre leur application à d'autres domaines très porteurs, comme ceux du traitement automatique des langues ou de la bioinformatique.

APA, Harvard, Vancouver, ISO, and other styles

33

Ikoki, Bukoko. "Traitement symbolique des systèmes multicorps avec KINDA (Kinematics and Dynamics Analysis)." Thesis, Université Laval, 2008. http://www.theses.ulaval.ca/2008/25575/25575.pdf.

Full text

APA, Harvard, Vancouver, ISO, and other styles

34

Klai, Kais. "Réseaux de Petri : vérification symbolique et modulaire." Paris 6, 2003. http://www.theses.fr/2003PA066171.

Full text

APA, Harvard, Vancouver, ISO, and other styles

35

Melki, Michaël. "Etude d'un modèle de représentation symbolique multi-résolution d'une image à base de graphes." Lyon, INSA, 2006. http://theses.insa-lyon.fr/publication/2006ISAL0074/these.pdf.

Full text

Abstract:

Dans cette thèse, nous étudions un modèle de représentation symbolique et multi-résolution d'une image. Pour cela, nous distinguons les informations concernant la structure de l'image, c'est à dire les différents blocs, ou régions, qui la composent, des informations concernant le contenu de cette dernière, c'est à dire ce que représente chacun de ces blocs. Nous nous intéresserons alors tout particulièrement aux informations de structure : plutôt que de représenter de manière complète les différents blocs de l'image, nous nous focaliserons sur l'étude de certaines propriétés vérifiées par ces derniers. En imposant certaines contraintes sur la nature des blocs considérés, nous pouvons alors dégager quelques propriétés simples qui nous permettent de caractériser complètement la topologie d'une image. Il est alors possible de construire un modèle de représentation de la structure d'une image à base de graphes de manière à représenter ces propriétés, et donc en même temps la topologie de la structure de l'image. Dans ce modèle, chaque bloc est représenté par un sommet d'un graphe, et en lui associant un symbole, choisi dans un alphabet donné, pour représenter son contenu, nous obtenons un modèle de représentation symbolique de l'image. Nous définissons ensuite un processus pour construire une nouvelle image de plus faible résolution à partir d'une image donnée à l'aide de règles de réductions, prenant compte à la fois de la structure et du contenu symbolique de l'image. Ce processus est lui-même étudié de manière à proposer différentes techniques pour par exemple apprendre à paramétrer les règles, ou encore pour accélérer ou fiabiliser le processus. Il peut être utilisé pour construire des segmentations d'une image à différents niveaux de résolution en se basant sur des informations purement symboliques, ou encore pour extraire une information donnée dans une image, en appliquant le processus jusqu'à obtenir une image ne contenant qu'un unique bloc dont le symbole contient l'information recherchée
In this PhD, we present a symbolic, multi-resolution model for representing an image. To do that, we consider both the structure of the image, that is the blocs from which it is constituted, and its content. We first focus on the structural part of the image. Under some constraints, a few properties can be enough to fully characterize the topology of the structure. This leads us to a graph-based representation for the structure of an image, which can be completed by adding symbolic information to the nodes to represent the content part of the image. We then propose a process to build an lower resolution image from an input image. This process uses reduction rules that take into account both the structure and the content of the image, and could be used either to segment an image at different resolution levels or to extract some information from it. Then we study this process to define methods that can be used for learning some of the parameters of the rules, for speeding up the building process, or for making the whole process more reliable

APA, Harvard, Vancouver, ISO, and other styles

36

Letard, Vincent. "Apprentissage incrémental de modèles de domaines par interaction dialogique." Thesis, Université Paris-Saclay (ComUE), 2017. http://www.theses.fr/2017SACLS100/document.

Full text

Abstract:

L'intelligence artificielle est la discipline de recherche d'imitation ou de remplacement de fonctions cognitives humaines. À ce titre, l'une de ses branches s'inscrit dans l'automatisation progressive du processus de programmation. Il s'agit alors de transférer de l'intelligence ou, à défaut de définition, de transférer de la charge cognitive depuis l'humain vers le système, qu'il soit autonome ou guidé par l'utilisateur. Dans le cadre de cette thèse, nous considérons les conditions de l'évolution depuis un système guidé par son utilisateur vers un système autonome, en nous appuyant sur une autre branche de l'intelligence artificielle : l'apprentissage artificiel. Notre cadre applicatif est celui de la conception d'un assistant opérationnel incrémental, c'est-à-dire d'un système capable de réagir à des requêtes formulées par l'utilisateur en adoptant les actions appropriées, et capable d'apprendre à le faire. Pour nos travaux, les requêtes sont exprimées en français, et les actions sont désignées par les commandes correspondantes dans un langage de programmation (ici, R ou bash). L'apprentissage du système est effectué à l'aide d'un ensemble d'exemples constitué par les utilisateurs eux-mêmes lors de leurs interactions. Ce sont donc ces derniers qui définissent, progressivement, les actions qui sont appropriées pour chaque requête, afin de rendre le système de plus en plus autonome. Nous avons collecté plusieurs ensembles d'exemples pour l'évaluation des méthodes d'apprentissage, en analysant et réduisant progressivement les biais induits. Le protocole que nous proposons est fondé sur l'amorçage incrémental des connaissances du système à partir d'un ensemble vide ou très restreint. Cela présente l'avantage de constituer une base de connaissances très représentative des besoins des utilisateurs, mais aussi l'inconvénient de n'aquérir qu'un nombre très limité d'exemples. Nous utilisons donc, après examen des performances d'une méthode naïve, une méthode de raisonnement à partir de cas : le raisonnement par analogie formelle. Nous montrons que cette méthode permet une précision très élevée dans les réponses du système, mais également une couverture relativement faible. L'extension de la base d'exemples par analogie est explorée afin d'augmenter la couverture des réponses données. Dans une autre perspective, nous explorons également la piste de rendre l'analogie plus tolérante au bruit et aux faibles différences en entrée en autorisant les approximations, ce qui a également pour effet la production de réponses incorrectes plus nombreuses. La durée d'exécution de l'approche par analogie, déjà de l'ordre de la seconde, souffre beaucoup de l'extension de la base et de l'approximation. Nous avons exploré plusieurs méthodes de segmentation des séquences en entrée afin de réduire cette durée, mais elle reste encore le principal obstacle à contourner pour l'utilisation de l'analogie formelle dans le traitement automatique de la langue. Enfin, l'assistant opérationnel incrémental fondé sur le raisonnement analogique a été testé en condition incrémentale simulée, afin d'étudier la progression de l'apprentissage du système au cours du temps. On en retient que le modèle permet d'atteindre un taux de réponse stable après une dizaine d'exemples vus en moyenne pour chaque type de commande. Bien que la performance effective varie selon le nombre total de commandes considérées, cette propriété ouvre sur des applications intéressantes dans le cadre incrémental du transfert depuis un domaine riche (la langue naturelle) vers un domaine moins riche (le langage de programmation)
Artificial Intelligence is the field of research aiming at mimicking or replacing human cognitive abilities. As such, one of its subfields is focused on the progressive automation of the programming process. In other words, the goal is to transfer cognitive load from the human to the system, whether it be autonomous or guided by the user. In this thesis, we investigate the conditions for making a user-guided system autonomous using another subfield of Artificial Intelligence : Machine Learning. As an implementation framework, we chose the design of an incremental operational assistant, that is a system able to react to natural language requests from the user with relevant actions. The system must also be able to learn the correct reactions, incrementally. In our work, the requests are in written French, and the associated actions are represented by corresponding instructions in a programming language (here R and bash). The learning is performed using a set of examples composed by the users themselves while interacting. Thus they progressively define the most relevant actions for each request, making the system more autonomous. We collected several example sets for evaluation of the learning methods, analyzing and reducing the inherent collection biases. The proposed protocol is based on incremental bootstrapping of the system, starting from an empty or limited knowledge base. As a result of this choice, the obtained knowledge base reflects the user needs, the downside being that the overall number of examples is limited. To avoid this problem, after assessing a baseline method, we apply a case base reasoning approach to the request to command transfer problem: formal analogical reasoning. We show that this method yields answers with a very high precision, but also a relatively low coverage. We explore the analogical extension of the example base in order to increase the coverage of the provided answers. We also assess the relaxation of analogical constraints for an increased tolerance of analogical reasoning to noise in the examples. The running delay of the simple analogical approach is already around 1 second, and is badly influenced by both the automatic extension of the base and the relaxation of the constraints. We explored several segmentation strategies on the input examples in order to reduce reduce this time. The delay however remains the main obstacle to using analogical reasoning for natural language processing with usual volumes of data. Finally, the incremental operational assistant based on analogical reasoning was tested in simulated incremental condition in order to assess the learning behavior over time. The system reaches a stable correct answer rate after a dozen examples given in average for each command type. Although the effective performance depends on the total number of accounted commands, this observation opens interesting applicative tracks for the considered task of transferring from a rich source domain (natural language) to a less rich target domain (programming language)

APA, Harvard, Vancouver, ISO, and other styles

37

Missire, Régis. "Sémantique des textes et modèle morphosémantique de l'interprétation." Toulouse 2, 2005. http://www.theses.fr/2005TOU20047.

Full text

Abstract:

Le propos est de contribuer au développement d'un modèle morphosémantique de l'interprétation pour une sémantique des textes. On s'attache notamment à mesurer l'adéquation entre la théorie (sémantique interprétative) et un modèle s'inspirant de la gestaltthéorie et de la Théorie des Formes Sémantiques. On formule à cet effet des propositions : (i) théoriques, qui visent, en restituant la sémantique interprétative dans le cadre des sémantiques structurales européennes, tout particulièrement la lexématique, à accroître l'adéquation entre théories structurales et gestaltistes ; (ii) descriptives dans le cadre du modèle morphosémantique, en s'attachant particulièrement au concept d'isotopie et à la question de la temporalisation des parcours interprétatifs (rythmes sémantiques). Les propositions sont étayées de deux analyses, la première portant sur un sonnet de Baudelaire (Tristesses de la lune), la seconde sur un corpus de 113 définitions produites par autant de locuteurs auxquels a été soumis un texte dans lequel figure un mot à définir
The purpose is to contribute to the development of a morphosemantic model of interpretation for a textual semantics. We take interest in particular in the adequacy between the theory (Interpretative Semantics) and a model inspired by Gestalttheory and the Theory of Semantic Forms. To that end, we formulate several proposals :(i) Theoretical ones that aim, by restoring Interpretative Semantics within the scope of european structural semantics, and especially lexematics, at enhancing the adequacy between the structural and gestalt theories. (ii) Descriptive ones, within the scope of the morphosemantic model, focussing mainly on the " isotopy " concept and the question of temporalization of the interpretative paths (semantic rhythms). These proposals are supported by two analyses : the first one deals with a sonnet written by Baudelaire (Tristesses de la Lune), the second is about a corpus of 113 definitions produced by as many speakers to whom a text was submitted, text in wich a word was to be defined

APA, Harvard, Vancouver, ISO, and other styles

38

Kerbrat, Alain. "Méthodes symboliques pour la vérification de processus communicants : étude et mise en oeuvre." Université Joseph Fourier (Grenoble), 1994. http://tel.archives-ouvertes.fr/tel-00005100.

Full text

Abstract:

Ce travail porte sur la vérification formelle de programmes parallèles. Parmi les méthodes habituellement utilisées, nous nous intéressons aux méthodes basées sur la construction d'un modèle du programme à vérifier; la vérification proprement dite s'effectue sur ce modèle. Cette approche est limitée par l'explosion de la taille du modèle, dès que le programme traite est de complexité réaliste. Notre but est l'étude et la mise en œuvre de techniques permettant d'effectuer la vérification malgré cette explosion. Les techniques que nous présentons sont liées par une caractéristique commune : l'utilisation de méthodes symboliques de représentation du modèle. Nous étudions en premier lieu des techniques de réduction de modèles. Ces réductions s'opèrent par rapport à des relations d'équivalence basées sur la notion de bisimulation. Nous étudions en particulier un algorithme de minimisation de modèle pendant sa génération (Génération de Modèle Minimal). Dans une seconde partie, nous nous intéressons a deux techniques symboliques de représentation de modèles. Il s'agit d'une part de Graphes de Décision Binaires, qui permettent la manipulation efficace de formules booléennes, et d'autre part de systèmes d'inéquations linéaires, connus sous le nom de polyèdres convexes, pour la manipulation de variables entières. L'utilisation de ces techniques permet de représenter et manipuler des modèles de taille souvent prohibitive pour des méthodes énumératives classiques. Nous présentons la mise en œuvre de méthodes de comparaison et réduction de modèles aves les Graphes de Décision Binaires, avec en particulier l'algorithme de Génération de Modèle Minimal. L'application de l'outil correspondant à plusieurs exemples de programmes LOTOS a permis de montrer l'intérêt, mais aussi les limites de l'utilisation de cette représentation symbolique. Enfin, nous présentons une méthode d'analyse statique de protocoles, basée sur l'utilisation des polyèdres convexes. Cette analyse permet le calcul d'approximations supérieures d'invariants du programme et de vérifier la véracité de propriétés définies en termes de variables du programme.

APA, Harvard, Vancouver, ISO, and other styles

39

Theyssier, Guillaume. "Automates cellulaires : un modèle de complexités." Phd thesis, Ecole normale supérieure de lyon - ENS LYON, 2005. http://tel.archives-ouvertes.fr/tel-00166295.

Full text

Abstract:

Nous étudions le modèle des automates cellulaires en adoptant successivement deux points de vue --celui des représentations syntaxiques locales puis celui des dynamiques globales-- et en cherchant à établir des liens entre eux par différentes approches ou outils --algébrique, combinatoire, et de la théorie de la calculabilité. Au cours de notre étude de la structure des règles de transition locales, nous introduisons une nouvelle classe d'automates (appelés automates cellulaires captifs) définie par une contrainte locale très simple. Nous établissons une loi 0-1 sur cette classe qui a pour corollaire que presque tous les automates cellulaires captifs sont intrinsèquement universels. En revanche, nous montrons qu'il est indécidable de savoir si un automate cellulaire captif est intrinsèquement universel ou pas. Dans une seconde partie, nous poursuivons l'étude des automates cellulaires en cherchant au contraire à nous affranchir le plus possible de leur représentation syntaxique pour insister sur leurs propriétés dynamiques globales. Notre problématique devient celle de la classification et de l'étude de notions de complexité selon ce point de vue global. L'outil fondamental est celui de simulation. Nous étendons les résultats de N. Ollinger sur les structures de pré-ordre (nouvelles relations de simulations et nouvelles propriétés induisant des structures d'idéal ou de filtre) et étudions également l'effet du produit cartésien sur ces structures. Nous établissons une construction qui peut s'interpréter comme un produit cartésien limite et nous permet d'exhiber des chaînes infinies croissantes de longueur omega+omega dans l'un des pré-ordres étudiés. Enfin, nous nous intéressons aux dynamiques séquentielles et aux automates cellulaires universels pour le calcul Turing. Nous construisons un treillis infini d'automates cellulaires Turing-universels qui sont tous à distance infinie de tout automate cellulaire intrinsèquement universel.

APA, Harvard, Vancouver, ISO, and other styles

40

Kubiak, Philippe. "Analyse symbolique des systèmes physiques modélisés par bond graph et comportant des éléments multiports." Lille 1, 1996. http://www.theses.fr/1996LIL10218.

Full text

Abstract:

Toute etude d'un système dynamique nécessite une étape essentielle : celle de la modélisation. Bases sur la méthodologie bond graph, de récents travaux, menés au sein de l'équipe bond graph du l. A. I. L. , ont permis de dégager des méthodes de calcul permettant de déterminer formellement les modèles mathématiques associes au modèle bond graph (équation d'état, matrice de transfert dans le cas linéaire) du système étudié. Ils ont également permis de développer certains algorithmes qui depuis ont été utilises dans le cadre du projet archer (logiciel d'aide à la modélisation et à l'analyse des systèmes physiques modélisés par bond graph). Ces résultats s'appliquent aux bond graphs constitues uniquement d'éléments 1-port, caractérises par des lois scalaires. Les travaux présentés dans ce mémoire constituent une contribution à l'etude des systèmes physiques modélisés par bond graph et comportant des éléments multiports caractérises par des lois matricielles. Afin d'établir des méthodes de détermination formelle et automatique de la matrice de transfert ainsi que de l'équation d'état. Le premier chapitre de ce mémoire est consacré tout d'abord à certains rappels importants concernant la méthodologie bond graph. Ensuite, une extension de la définition de boucle causale est proposée. Une règle heuristique de simplification de l'application de la règle de mason dans le cas des bond graphs 1-port, est enfin présentée. Le deuxième chapitre traite de la détermination formelle de la matrice de transfert. Les modèles bond graphs ne comportant qu'un seul élément multiport à branches non connectées, puis connectées et enfin comportant plusieurs éléments multiports y sont abordés. Les résultats obtenus constituent une extension de la règle de mason jusqu'à présent utilisée dans le cas 1-port. La détermination formelle des matrices intervenant dans l'équation d'état fait l'objet du troisième chapitre. Basée sur de récents travaux menés au sein de notre équipe, cette etude se développe successivement sur les éléments multiports dynamiques à causalité unique puis sur les éléments multiports résistifs et enfin sur les éléments multiports dynamiques a causalité mixte. Nous proposons dans le quatrième et dernier chapitre, une nouvelle méthode de décomposition des éléments multiports. Cette méthode nommée méthode récurrente, permet de décomposer un élément multiport de dimension m en un élément multiport de dimension (m-1) associe à un élément 1-port, pour aboutir en m étapes, en m éléments 1-port.

APA, Harvard, Vancouver, ISO, and other styles

41

Benharrat, Nassim. "Model-Based Testing of Timed Distributed Systems : A Constraint-Based Approach for Solving the Oracle Problem." Thesis, Université Paris-Saclay (ComUE), 2018. http://www.theses.fr/2018SACLC021/document.

Full text

Abstract:

Le test à base de modèles des systèmes réactifs est le processus de vérifier si un système sous test (SUT) est conforme à sa spécification. Il consiste à gérer à la fois la génération des données de test et le calcul de verdicts en utilisant des modèles. Nous spécifions le comportement des systèmes réactifs à l'aide des systèmes de transitions symboliques temporisées à entrée-sortie (TIOSTS). Quand les TIOSTSs sont utilisés pour tester des systèmes avec une interface centralisée, l'utilisateur peut ordonner complètement les événements (i.e., les entrées envoyées au système et les sorties produites). Les interactions entre le testeur et le SUT consistent en des séquences d'entrées et de sortie nommées traces, pouvant être séparées par des durées dans le cadre du test temporisé, pour former ce que l'on appelle des traces temporisées. Les systèmes distribués sont des collections de composants locaux communiquant entre eux et interagissant avec leur environnement via des interfaces physiquement distribuées. Différents événements survenant à ces différentes interfaces ne peuvent plus être ordonnés. Cette thèse concerne le test de conformité des systèmes distribués où un testeur est placé à chaque interface localisée et peut observer ce qui se passe à cette interface. Nous supposons qu'il n'y a pas d’horloge commune mais seulement des horloges locales pour chaque interface. La sémantique de tels systèmes est définie comme des tuples de traces temporisées. Nous considérons une approche du test dans le contexte de la relation de conformité distribuée dtioco. La conformité globale peut être testée dans une architecture de test en utilisant des testeurs locaux sans communication entre eux. Nous proposons un algorithme pour vérifier la communication pour un tuple de traces temporisées en formulant le problème de message-passing en un problème de satisfaction de contraintes (CSP). Nous avons mis en œuvre le calcul des verdicts de test en orchestrant à la fois les algorithmes du test centralisé off-line de chacun des composants et la vérification des communications par le biais d'un solveur de contraintes. Nous avons validé notre approche sur un cas étude de taille significative
Model-based testing of reactive systems is the process of checking if a System Under Test (SUT) conforms to its model. It consists of handling both test data generation and verdict computation by using models. We specify the behaviour of reactive systems using Timed Input Output Symbolic Transition Systems (TIOSTS) that are timed automata enriched with symbolic mechanisms to handle data. When TIOSTSs are used to test systems with a centralized interface, the user may completely order events occurring at this interface (i.e., inputs sent to the system and outputs produced from it). Interactions between the tester and the SUT are sequences of inputs and outputs named traces, separated by delays in the timed framework, to form so-called timed traces. Distributed systems are collections of communicating local components which interact with their environment at physically distributed interfaces. Interacting with such a distributed system requires exchanging values with it by means of several interfaces in the same testing process. Different events occurring at different interfaces cannot be ordered any more. This thesis focuses on conformance testing for distributed systems where a separate tester is placed at each localized interface and may only observe what happens at this interface. We assume that there is no global clock but only local clocks for each localized interface. The semantics of such systems can be seen as tuples of timed traces. We consider a framework for distributed testing from TIOSTS along with corresponding test hypotheses and a distributed conformance relation called dtioco. Global conformance can be tested in a distributed testing architecture using only local testers without any communication between them. We propose an algorithm to check communication policy for a tuple of timed traces by formulating the verification of message passing in terms of Constraint Satisfaction Problem (CSP). Hence, we were able to implement the computation of test verdicts by orchestrating both localised off-line testing algorithms and the verification of constraints defined by message passing that can be supported by a constraint solver. Lastly, we validated our approach on a real case study of a telecommunications distributed system

APA, Harvard, Vancouver, ISO, and other styles

42

Rogacki, Rémy. "Simulation symbolique de descriptions comportementales de circuits digitaux." Montpellier 2, 1992. http://www.theses.fr/1992MON20222.

Full text

Abstract:

La simulation symbolique est une méthode de vérification dérivée de la simulation conventionnelle dans laquelle les valeurs numériques des entrées du modèle sont remplacées par des symboles. La simplification de ces valeurs symboliques constitue un point important d'une part, pour une mise en œuvre efficace de cette technique de simulation et, d'autre part, pour fournir des informations significatives au concepteur. Un simulateur symbolique de descriptions comportementales de circuits digitaux est présenté. Le mécanisme de simulation, adapté a la représentation interne de la description VHDL, est détaillé. Âpres une étude théorique du processus de simplification des expressions arithmétiques base sur un système de réécriture, les méthodes de représentation et de manipulation sont explicitées: diagrammes de décision binaire pour les expressions à valeur booléenne, formes normalisées pour les expressions arithmétiques

APA, Harvard, Vancouver, ISO, and other styles

43

Gravot, Fabien. "ASyMov : fondation d'un planificateur robotique intégrant le symbolique et le géométrique." Toulouse 3, 2004. http://www.theses.fr/2004TOU30018.

Full text

APA, Harvard, Vancouver, ISO, and other styles

44

Pavel, Sebastien. "Un modèle de composants hiérarchiques avec protocoles d'interaction." Phd thesis, Université de Nantes, 2008. http://tel.archives-ouvertes.fr/tel-00484788.

Full text

Abstract:

L'utilisation et la gestion des composants sont au coeur des nouvelles architectures logicielles. Les composants représentent les briques de bases des logiciels. Les efforts de recherche actuels se concentrent sur l'élaboration de modèles à base de composants qui intègrent des propriétés importantes comme, par exemple, la description et l'intégration des composants avec des comportements explicites (protocoles d'interaction). Ce sont ces descriptions plus complètes que les interfaces classiques (les points d'entrée et de sortie), qui ouvrent la voie vers la correction des assemblages. Comme aboutissement des travaux de cette thèse, nous proposons un modèle de composants qui utilise des Systèmes de Transitions Symboliques (STSs) pour décrire les comportements des composants. Les composants de notre modèle sont des boîtes noires communicant exclusivement par l'intermédiaire de leurs interfaces étendues avec des protocoles d'interaction. Le modèle spécifie aussi les règles de compatibilité, les algorithmes de vérification des assemblages des composants et de la substitution et un langage de description des composants. Nous proposons une implémentation dans le langage Java en suivant une approche générative ou le code Java est généré à partir des descriptions des composants de haut niveau. Le code est donc garanti a être conforme à la spécification.

APA, Harvard, Vancouver, ISO, and other styles

45

Midenet, Sophie. "Modèle connexionniste d'apprentissage d'associations par carte auto-organisatrice ; Contribution à l'étude d'une mise en correspondance des représentations connexionnistes et symboliques." Paris, ENST, 1991. http://www.theses.fr/1991ENST0019.

Full text

Abstract:

La complémentarité des propriétés attachées aux formalismes symbolique et connexionniste utilises en intelligence artificielle peut etre mise a profit par la spécification de systèmes hybrides disposant a la fois de facultés d'adaptation et de manipulation symbolique. Une telle coopération nécessite des échanges d'informations au moyen de transferts de représentations. Sa mise en place nous conduit a rechercher les conditions dans lesquelles pourrait se développer, pendant l'apprentissage d'un réseau connexionniste, une représentation orientée vers le symbolique, a caractère localise et structure. Ces propriétés permettent la détection de régularités dans les représentations internes, étape indispensable avant leur intégration effective dans un module symbolique. Le modèle des cartes auto-organisatrices de kohonen conduit au développement de telles représentations grâce a une compétition entre unités suivie d'une coopération entre voisins. Une analyse expérimentale de l'auto-organisation d'une carte met en évidence un traitement sélectif des dimensions d'entrée. Différents outils de description statistique ou topologique indiquent que les dimensions d'entrée les plus statistiquement informatives sont privilégiées par la carte et sont a l'origine de l'organisation topologique des unités. Le caractère privilégie accorde a certaines dimensions d'entrée pendant l'auto-organisation permet d'exercer un contrôle de l'adaptation au moyen des données présentées et de leur codage. Ce type de contrôle est utilise dans la spécification d'un modèle d'apprentissage d'associations base sur les cartes auto-organisatrices appelé lasso (learning associations by self-organization). Durant l'apprentissage, le système classifie des vecteurs composes d'une entrée et de la sortie désirée associée. Les poids ainsi appris sont utilises en phase d'exploitation pour déterminer le pattern associe a une entrée présentée. Ce modèle est appliqué a différents problèmes, dans le domaine de la reconnaissance des formes notamment. Les taux de reconnaissance obtenus valident le mode d'exploitation particulier des cartes auto-organisatrices que nous proposons. L'utilisation d'une carte topologiquement organisée confère au modèle des capacités spécifiques sur le plan de la représentation des connaissances, qui se développe dans la carte suivant un principe de localisation au niveau de groupes d'unités voisines

APA, Harvard, Vancouver, ISO, and other styles

46

Rousseaux, Francis. "Une contribution de l'intelligence artificielle et de l'apprentissage symbolique automatique à l'élaboration d'un modèle d'enseignement de l'écoute musicale." Phd thesis, Université Pierre et Marie Curie - Paris VI, 1990. http://tel.archives-ouvertes.fr/tel-00417579.

Full text

Abstract:

Pour un chercheur en apprentissage symbolique automatique amateur de musique, formaliser certains aspects de la représentation, de la pratique et de la pédagogie musicale est un thème séduisant. Mieux, ce thème peut prendre place au sein des préoccupations et des ambitions de l'intelligence artificielle. En effet, s'il est important que l'intelligence artificielle se renforce dans ses domaines de prédilection, il lui reste des références à élargir et des champs à gagner, comme ceux que lui soumet la problématique musicale.
C'est ainsi que ce thème devient un objectif d'études et de recherches : mais dans cette optique, il est nécessaire de prendre en compte l'état de l'art en informatique musicale, et d'écouter les besoins manifestés par les musiciens, afin de prendre pied sur une réelle communauté d'intérêts entre les deux disciplines.
En toute hypothèse, la musique est un objet abstrait dont il existe plusieurs représentations, aucune n'étant complète ni générale, et chacune possédant des propriétés spécifiques. Qui plus est, ces représentations ont tendance à évoluer, naître et mourir au gré des besoins des musiciens, même si la représentation sonore reste essentielle et par définition indissociable de l'objet abstrait : mais il faut bien admettre que le son musical n'est pas seul à évoquer la musique, et que si l'homme éprouve le besoin d'inventer des représentations pour mieux s'approprier le phénomène musical, il peut être enrichissant d'examiner la transposition de ce comportement aux machines.
On peut certes isoler une de ces représentations, la traduire informatiquement et lui dédier des outils : c'est ainsi que de nombreux systèmes informatiques abordent la musique. Mais il existe une approche plus typique de l'intelligence artificielle, qui consiste à chercher à atteindre l'objet abstrait à travers l'ensemble de ses représentations et de leurs relations : pour un système informatique, faire preuve d'intelligence dans ce contexte, c'est utiliser cette diversité et cette multiplicité de représentation; c'est savoir s'appuyer sur une réalité mouvante et se déplacer dans un univers d'abstractions.
Mais les représentations ne prennent leur sens qu'avec ceux qui communiquent à travers elles, qu'avec les activités qu'elles engendrent. On peut alors imaginer un système qui constituerait un véritable lieu de rencontre, de réflexion, de création, en un mot de communication : car la musique est avant tout un médium de communication. Mais quelle est la nature de ce qu'on pourra communiquer à travers un tel système ? Par exemple, on pourra s'exercer aux pratiques musicales, expérimenter de nouveaux rapports entre les représentations, en un mot s'approprier le médium musical lui-même.
Mais alors, on a besoin d'un système qui sache témoigner de ces rencontres, plus précisément qui apprenne à en témoigner; c'est là notre définition de l'apprentissage dans le contexte : on dira qu'un système apprend s'il témoigne, et éventuellement s'adapte à un univers de communication musicale. Sans cette exigence, la valeur de la communication est perdue : en effet les parties prenantes quittent le système avec leur nouvelle richesse, quelle que soit la réussite de la médiation. Aussi, l'enjeu pour un système apprenti consiste à retourner un témoignage aux musiciens, aux pédagogues et aux informaticiens, afin qu'ils puissent en tirer profit : bien entendu, on exigera de ce témoignage qu'il produise de la connaissance utile, sans se contenter de cumuls d'événements ou de faits ordonnés historiquement.
Ainsi, à travers un enseignement ouvert, il s'agira pour des élèves d'appréhender et d'expérimenter le médium musical, d'enrichir leurs connaissances et d'obtenir des explications. Pour des enseignants, il s'agira de créer et d'organiser cette médiation, et de rendre des oracles pédagogiques au système. Mais l'intelligence artificielle et l'apprentissage symbolique automatique sont les sciences de l'explication : il faut mettre en jeu la dimension cognitive qui permettra d'expertiser l'adéquation du lieu de rencontre; il faut se placer au cœur des besoins et des préoccupations des enseignants et des élèves, en tentant de formaliser les théories cognitives de la musique. On pourra même inventer des représentations à vocations cognitive et explicative : à terme, un système construit sur un tel modèle pourrait bien être capable de faire lui-même des découvertes dans ce domaine.

APA, Harvard, Vancouver, ISO, and other styles

47

Abdellatif, Chiboub. "Elaboration automatique et symbolique de modèles dynamiques inversés de robots à chaîne cinématique simple, arborescente ou fermée en vue deleur commande." Doctoral thesis, Universite Libre de Bruxelles, 1990. http://hdl.handle.net/2013/ULB-DIPOT:oai:dipot.ulb.ac.be:2013/213147.

Full text

APA, Harvard, Vancouver, ISO, and other styles

48

Dadeau, Frédéric. "Evaluation Symbolique à Contraintes pour la Validation - Application à Java/JML." Phd thesis, Université de Franche-Comté, 2006. http://tel.archives-ouvertes.fr/tel-00329891.

Full text

Abstract:

Mes travaux de thèse s'articulaient autour de la validation de modèles et de programmes. En ce sens, les modèles sont validés par animation, de manière à s'assurer qu'ils décrivent le bon comportement du système qu'ils représentent. Il s'agit d'un processus semi-automatique, car l'utilisateur sélectionne les actions du système à exécuter et effectue la comparaison entre les descriptions informelles données dans le cahier des charges et les résultats produits par le modèle. Un modèle validé est ensuite utilisé dans l'objectif de produire des cas de tests fonctionnels destinés à être joués sur une implantation ou un système sous test. Le modèle formel est ainsi utilisé à deux niveaux : d'une part, il permet de calculer de manière automatique les suites de tests, et, d'autre part, il sert d'oracle pour établir le verdict du test.
Au cours de ces travaux, nous nous sommes intéressés à la validation de programmes Java par l'intermédiaire de son langage de modélisation associé, nommé JML. Suite aux expériences et aux savoirs-faire accumulés au sein de l'équipe Techniques Formelles et à Contraintes du Laboratoire d'Informatique de Franche-Comté, nous avons choisi d'appliquer une représentation logico-ensembliste des modèles JML, reposant sur des solveurs de contraintes pour gérer les valeurs des variables des modèles objets que nous traitons. A partir de cette représentation symbolique, nous avons exprimé l'animation symbolique d'un modèle objet basé sur la sémantique de Java, utilisant les descriptions formelles contenues dans les pré- et postconditions des spécifications des méthodes.
Nous nous sommes ensuite appuyés sur la définition symbolique des états du système objet pour extraire des cibles de tests, liées aux comportements issus des méthodes, définies par un prédicat obtenu par conjonction de la condition d'activation du comportement et de la mise aux limites des attributs des objets du système et des paramètres de la méthode sous test. L'animation symbolique du modèle entre en jeu pour la construction des cas de tests. Un algorithme de parcours de l'espace d'états effectue la recherche d'un chemin d'exécution menant à la cible. Les cas de tests sont ensuite concrétisés pour produire un pilote de test Java. Une étude de cas a été menée sur une modélisation fonctionnelle d'un porte-monnaie électronique.
Ces travaux ont été implantés dans un prototype, nommé JML-Testing-Tools, qui permet l'animation symbolique d'un modèle JML et la génération de cas de tests pour l'implantation Java qui lui est associée. Ce prototype est composé d'un compilateur traduisant une spécification JML et des signatures de classes Java dans un format logico-ensembliste. Le modèle décrit dans ce format est ensuite animé par un interpréteur rétablissant la sémantique opérationnelle du Java/JML.

APA, Harvard, Vancouver, ISO, and other styles

49

Chazoule, Guy. "Représentations analogiques et représentations symboliques des quantités : leurs relations entre quatre et six ans." Phd thesis, Université Blaise Pascal - Clermont-Ferrand II, 2012. http://tel.archives-ouvertes.fr/tel-01063654.

Full text

Abstract:

Le modèle du triple code a été proposé par Dehaene (1992 ; Dehaene & Cohen, 2000)sur la base d'arguments neuro-anatomiques et neuropsychologiques pour rendre compte du traitement des nombres et des quantités. Le modèle postule l'existence de trois types de représentations correspondant chacune à un format de l'information numérique : une représentation analogique approximative préverbale, et deux représentations symboliques,l'une verbale, l'autre arabe. Si des études ont pu être mettre en évidence les caractéristiques de la dimension analogique tant chez le nouveau-né que chez l'adulte, la question de la" greffe " chez l'enfant des représentations symboliques sur la représentation analogique reste posée. L'objectif de cette thèse est de rechercher en suivant le développement comment s'effectue cette mise en relation. Nous avons élaboré un ensemble d'épreuves de comparaisons testant chacune une des représentations du modèle du triple code afin de déterminer chez des enfants dès 4 ans des indices de cette mise en relation. Si le lien entre dimensions analogique et symbolique est présent, un effet de rapport, " signature " de ce lien est attendu tant avec les comparaisons analogiques que symboliques. Cinq expérimentations ont été menées : avec des adultes, des enfants de 4 et 5 ans tout-venant, des enfants prématurés et des enfants atteints du syndrome de Down. Les résultats montrent que, dans toutes les populations, l'effet de rapport est présent avec la dimension analogique. Ensuite,entre 4 et 5 ans, avec l'acquisition du code verbal et indo-arabe la représentation symbolique change de nature. Enfin, les populations qui présentent des troubles du traitement du nombre sont affectées essentiellement sur la dimension verbale. Ces résultats sont discutés en regard de deux conceptions alternatives.

APA, Harvard, Vancouver, ISO, and other styles

50

Gagarina, Tatiana. "Modèle pseudo-rigide pour la simulation dynamique des mécanismes flexibles." Paris 6, 1999. http://www.theses.fr/1999PA066607.

Full text

APA, Harvard, Vancouver, ISO, and other styles

Dissertations / Theses on the topic 'Modèles symboliques'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles