.

Thèse de doctorat : Informatique : Nice : 2006. / Bibliogr. p. 87-89. Index. Résumés en français et en anglais.

Thèse doctorat : Informatique : Rennes 1 : 2006. / Bibliogr. p. 221-229.

Thèse doctorat : Informatique. Bioinformatique : Rennes 1 : 2005. / Bibliogr. p. 107-129.

Thèse de doctorat : Informatique : University of Twente, Netherlands : 1997. / Bibliogr. p. 311-326 et index.

Reproduction de : Thèse de doctorat : mathématiques appliquées : Grenoble 1 : 1986. / Titre provenant de l'écran-titre.

Nous étudions des classes d'automates à états finis calculant sur les arbres, étendus par des contraintes permettant de tester des égalités et diségalités entre sous-arbres. Nous nous concentrons sur des automates d'arbres à contraintes globales où les tests sont opérés en fonction des états que l'automate atteint lors de ses calculs. De tels automates ont été introduit dans le cadre de travaux sur les documents semi-structurés. Nous procédons ici à une comparaison détaillée en expressivité entre ces automates et d'autres modèles permettant de réaliser des tests similaires, comme les automates à contraintes entre frères ou les automates d'arbres avec une mémoire auxiliaire. Nous montrons comment de tels automates peuvent être utilisés pour vérifier des propriétés de sécurité sur les protocoles cryptographiques. Les automates d'arbres ont déjà été utilisés pour modéliser les messages échangés lors d'une session d'un protocole. En ajoutant des contraintes d'égalité, nous pouvons décrire précisement des sessions qui utilisent à plusieurs reprises un même message, évitant ainsi une approximation trop grande. Nous répondons ensuite positivement au problème de la décision du vide des langages reconnus par les automates à contraintes globales. En montrant que leur expressivité est très proche de celle des automates opérant sur des représentations de termes par des graphes orientés acycliques, nous en déduisons une procédure de décision du vide en temps non-déterministe doublement exponentiel. Finalement, nous étudions le problème de la décision du vide pour des automates à contraintes globales pour lesquels on autorise des contraintes dites de clé, exprimant intuitivement que tous les sous arbres d'un certain type dans un arbre en entrée sont distincts deux à deux. Le type des clés est classiquement utilisé pour représenter un identifiant unique, comme un numéro de sécurité sociale.Nous décrivons alors une procédure de décision du vide de complexité non-élementaire. Nous montrons que cette procédure est très robuste, et qu'il est possible d'étendre les automates avec des contraintes supplémentaires, comme des contraintes de comptage ou des tests locaux, tout en préservant la décidabilité du vide.

Le présent travail a pour but d'étudier la densité spectrale de puissance de différents systèmes de communication digitaux. Le premier chapitre expose les propriétés principales du système duobinaire, en insistant plus particulièrement sur la densité spectrale de puissance. L'influence, sur la forme du spectre, d'une généralisation du concept duobinaire, généralisation qui conduit à la notion de duobinaire modifié d'ordre r, est considérée au chapitre deux. Enfin, le troisième chapitre s'intéresse aux techniques diphasés, ainsi qu'a leurs combinaisons avec les techniques duobinaire et duobinaire modifié d'ordre r. De plus, les différents signaux étudiés étant stationnaires, leur fonction d'autocorrélation et leur densité spectrale de puissance constituent une paire de transformées de Fourier, si bien qu'un corrélateur permet la vérification expérimentale des calculs de spectres.

Dans la première partie de ce manuscrit nous étudions les fonctions rationnelles, c'est-à-dire définies par des transducteurs unidirectionnels. Notre objectif est d'étendre aux transductions les nombreuses correspondances logique-algèbre qui ont été établies concernant les langages, notamment le célèbre théorème de Schützenberger-McNaughton-Papert. Dans le cadre des fonctions rationnelles sur les mots finis, nous obtenons une caractérisation à la Myhill-Nerode en termes de congruences d'indice fini. Cette caractérisation nous permet d'obtenir un résultat de transfert, à partir d'équivalences logique-algèbre pour les langages vers des équivalences pour les transductions. En particulier nous montrons comment décider si une fonction rationnelle est définissable en logique du premier ordre. Sur les mots infinis, nous pouvons également décider la définissabilité en logique du premier ordre, mais avec des résultats moins généraux.Les fonctions rationnelles sur les mots infinis sont plus difficiles à caractériser et nous obtenons un résultat plus faible: étant donné un transducteur nous montrons comment calculer un transducteur canonique, c'est-à-dire indépendant du transducteur initial, réalisant la même fonction.Cependant cette machine canonique nous permet tout de même de décider si une fonction est définissable en logique du premier ordre.Dans la seconde partie nous introduisons une logique pour les transductions et nous résolvons le problème de synthèse régulière: étant donnée une formule de la logique, peut-on obtenir un transducteur bidirectionnel déterministe satisfaisant la formule ?Dans la seconde partie nous considérons un problème de synthèse: étant donné une relation (spécification) peut-on obtenir une fonction (un programme) qui est inclus dans (qui satisfait) la relation. Les fonctions réalisées par des transducteurs bidirectionnels déterministes sont caractérisés par plusieurs modèles différents, y compris par les transducteurs MSO, et ont ainsi été nommées transductions régulières.Nous introduisons une logique expressive pour les transduction et nous résolvons le problème de synthèse régulière pour cette logique.Plus précisément nous fournissons un algorithme qui produit toujours une fonction régulière satisfaisant une spécification donnée en entrée.Nous exposons également un lien intéressant entre les transductions et les mots avec données.Par conséquent nous obtenons une logique expressive pour les mots avec données, pour laquelle le problème de satisfiabilité est décidable. / Option Informatique du Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Cette thèse propose une nouvelle approche pour la synthèse de valeurs temporelles dans les systèmes temporisés. Notre approche est basée sur la méthode inverse suivante : à partir d’une instance de référence des paramètres, nous synthétisons une contrainte sur les paramètres, garantissant le même comportement que pour l’instance de référence, abstraction faite du temps. Il en résulte un critère de robustesse pour le système. En itérant cette méthode sur des points dans un domaine paramétrique borné, nous sommes alors à même de partitionner l’espace des paramètres en bonnes et mauvaises zones par rapport à une propriété à vérifier. Ceci nous donne une cartographie comportementale du système. Cette méthode s’étend aisément aux systèmes probabilistes. Nous présentons également des variantes de la méthode inverse pour les graphes orientés valués et les processus de décision markoviens. Parmi les prototypes implémentés, IMITATOR II implémente la méthode inverse et la cartographie pour les automates temporisés. Ce prototype nous a permis de synthétiser de bonnes valeurs pour les paramètres temporels de plusieurs études de cas, dont un modèle abstrait d’une mémoire commercialisée par le fabricant de puces STMicroelectronics, ainsi que plusieurs protocoles de communication. / This thesis proposes a novel approach for the synthesis of delays for timed systems, in particular in the framework oftimed automata, a model for verifying real-time systems. Our approach relies on the following inverse method: given a reference valuation of the parameters, we synthesize a constraint on the parameters, guaranteeing the same timeabstract linear behavior as for the reference valuation. This gives a criterion of robustness to the system. By iterating this inverse method on various points of a bounded parameter domain, we are then able to partition the parametric space into good and bad zones, with respect to a given property one wants to verify. This gives a behavioral cartography of the system. This method extended to probabilistic systems allows to preserve minimum and maximum probabilities of reachability properties. We also present variants of the inverse method for directed weighted graphs and Markov Decision Processes. Several prototypes have been implemented; in particular, IMITATOR II implements the inverse method and the cartography for timed automata. It allowed us to synthesize parameter values for several case studies such as an abstract model of a memory circuit sold by the chipset manufacturer ST-Microelectronics, and various communication protocols.