L’étude des automates est un sujet fondamental de l’informatique. Ce modèle apporte des solutions pratiques à divers problèmes en compilation et en vérification notamment. Dans ce travail nous proposons l'extension aux automates à pile visible de résultats existants pour les automates. Nous proposons une définition d'automate à pile visible émondé et donnons un algorithme s’exécutant en temps polynomial émondant un automate en préservant son langage. Nous donnons aussi un algorithme de complexité exponentielle qui, pour un automate à pile visible donné, construit un automate équivalent à la fois émondé et déterministe. Cette complexité exponentielle se révèle optimale. Étant donné un automate à pile visible, nous pouvons associer à ses transitions des coûts pris dans un semi-anneau S. L’automate associe ainsi un mot d’entrée à un élément de S. Le coût d’un automate est le supremum des coûts associés aux mots d'entrée. Pour les semi-anneaux des entiers naturels et Max-plus, nous donnons des caractérisations et des algorithmes polynomiaux pour décider si le coût d’un automate est fini. Puis, nous étudions pour les entiers naturels la complexité du problème de la majoration du coût par un entier k. Les transducteurs à pile visibles produisent des sorties sur chaque mot accepté. Un problème classique est de décider s'il existe une borne sur le nombre de sorties de chaque mot accepté. Pour une sous-classe des transducteurs à pile visible, nous proposons des propriétés caractérisant les instances positives de ce problème. Nous montrons leur nécessité et discutons d’approches possibles afin de montrer leur suffisance. / The study of automata is a central subject of computer science. This model provides practical solutions to several problems including compilation and verification. In this work we extend existing results of automata to visibly pushdown automata. We give a definition of trimmed visibly pushdown automata and a polynomial time algorithm to trim an automata while preserving its language. We also provide an exponential time algorithm which, given a visibly pushdown automaton, produces an equivalent automaton, both deterministic and trimmed. We prove the optimality of the complexity. Given a visibly pushdown automaton, we can equip its transitions with a cost taken from a semiring S, and thus associate each input word to an element of S. The cost of the automaton is the supremum of the input words cost. For the semiring of natural integers and Max-plus, we give characterisations and polynomial time algorithms to decide if the cost of a visibly pushdown automaton is finite. Then in the case of natural integers we study the complexity of deciding if the cost is bounded by a given integer k. Visibly pushdown transducers produce output on each accepted word. A classical problem is to decide if there exists a bound on the number of outputs of each accepted word. In the case of a subclass of visibly pushdown transducers, we give properties characterizing positive instances of this problem. We show their necessity and discuss of possible approaches to prove their sufficiency.

Dans cette thèse, on s'intéresse aux automates cellulaires en tant que modèle de calcul permettant de reconnaître des langages. Dans un tel domaine, il est toujours difficile d'établir des résultats négatifs, typiquement de prouver qu'un langage donné n'est pas reconnu en une certaine fonction de temps par une certaine classe d'automates. On se focalisera en particulier sur les classes de faible complexité comme le temps réel, au sujet desquelles de nombreuses questions restent ouvertes.Dans une première partie, on propose plusieurs manières d'affaiblir encore les classes de langages étudiées, permettant ainsi d'obtenir des exemples de résultats négatifs. Dans une seconde partie, on montre un théorème d'accélération par automate cellulaire d'un modèle séquentiel, les automates finis oublieux. Ce modèle est une version a priori affaiblie, mais non triviale, des automates finis à plusieurs têtes de lecture. / This document deals with cellular automata as a model of computation used to recognise languages. In such a domain, it is always difficult to provide negative results, that is, typically, to prove that a given language is not recognised in some function of time by some class of automata. The document focuses in particular on the low-complexity classes such as real time, about which a lot of questions remain open since several decades.In a first part, several techniques to weaken further still these classes of languages are investigated, thereby bringing examples of negative results. A second part is dedicated to the comparison of cellular automata with another model language recognition, namely multi-head finite automata. This leads to speed-up theorem when finite automata are oblivious, which makes them a priori weaker than in the general case but leaves them a nontrivial power.

Le sujet de cette thèse se divise en trois parties: les deux premières traitent chacune d'une extension du modèle utilisé en théorie des automates, tandis que la dernière aborde une partie plus concrète qui consiste à générer des automates avec des propriétés particulières. Tout d'abord, nous donnons une extension du concept d'automate universel, défini sur les mots finis, aux omega-langages. Pour cela, nous avons défini une forme normale pour tenir compte de la spécificité du mode d'acceptation des automates de Büchi qui nous permettent de reconnaître les omega-langages. Ensuite nous avons défini deux types d'omega-factorisations, "classiques" et "pures", qui sont des extensions du concept de factorisation d'un langage, ce qui nous a permis de définir l'automate universel d'un omega-langage. Nous avons prouvé que ce dernier dispose bien des différentes propriétés attendues: il est le plus petit automate de Büchi reconnaissant l'omega-langage et qui possède la propriété d'universalité (moyennant la forme normale). Nous présentons également une méthode pour calculer efficacement les omega-factorisations maximales d'un langage à partir d'un automate prophétique reconnaissant le dit langage. Dans la seconde partie, nous traitons le cas des automates bidirectionnels à multiplicité dans un semi-anneau. Dans un premier temps, nous donnons une version légérement différente de la construction permettant de passer d'un automate bidirectionnel à multiplicité à un automate unidirectionnel à multiplicité et nous prouvons qu'elle préserve la non-ambiguïté mais pas le déterminisme. Nous montrons, également à l'aide d'une construction, que les automates bidirectionnels à multiplicité non-ambigus sont équivalents aux automates unidirectionnels à multiplicité déterministes. Dans un second temps, nous nous concentrons sur les semi-anneaux tropicaux (ou min-+). Nous montrons que sur N-min-+, les automates bidirectionnels sont équivalents aux automates unidirectionnels. Nous montrons également que sur Z-min-+, les automates bidirectionnels n'ont pas toujours un comportement défini et que cette propriété est décidable tandis qu'il n'est pas décidable s'il existe un mot pour lequel le comportement est défini. Dans la dernière partie, nous proposons un algorithme de génération aléatoire d'automate acycliques, accessibles et déterministes ainsi que d'automates acycliques minimaux avec une distribution qui est quasiment uniforme, tout cela à l'aide de chaîne de Markov. Nous prouvons l'exactitude de chacun de ces deux algorithmes et nous expliquons comment adapter en tenant compte de contraintes sur l'ensemble des états finals / The subject of this thesis is decided into three parts: two of them are about extensions of the classical model in automata theory, whereas the third one is about a more concrete aspect which consists in randomly generate automata with specific properties. We first give an extension of the universal automaton on finite words to infinite words. To achieve this, we define a normal form in order to take account of the specific acceptance mode of Büchi automata which recognize omega-langages. Then we define two kinds of omega-factorizations, a "regular" one and the "pure" kind, which are both extensions of the classical concept of factorization of a language. This let us define the universal automaton of an omega-language. We prove that it has all the required properties: it is the smallest Buchi automaton, in normal form, that recognizes the omega-language and which has the universal property. We also give an effective way to compute the "regular" omega-factorizations of a language using a prophetic automaton recognizing the language. In the second part, we deal with two-way automata weighted over a semi ring. First, we give a slightly different version of the computation of a weighted one-way automaton from a weighted two-way automaton and we prove that it preserves the non-ambiguity but not the determinism. We prove that non-ambiguous weighted two-way automata are equivalent to deterministic weighted one-way automata. In a later part, we focus on tropical semi rings (or min-+). We prove that two-way automata on N-min-+ are equivalent to one-way automata on N-min-+. We also prove that the behavior of two-way automata on Z-min-+ are not always defined and that this property is decidable whereas it is undecidable whether or not there exists a word on which the behavior is defined. In the last section, we propose an algorithm in order to randomly generate acyclic, accessible and determinist automata and minimal acyclic automata with an almost uniform distribution using Morkov chains. We prove the reliability of both algorithms and we explain how to adapt them in order to fit with constraints on the set of final states

La recherche de solutions analytiques pour l'évaluation de la fiabilité en contexte dynamique n'est pas résolue dans le cas général. Un état de l'art présenté dans le chapitre 1 montre que des approches partielles relatives à des hypothèses particulières existent. La simulation de Monte Carlo serait le seul recours, mais il n'existait pas d'outils performants permettant la simulation simultanée de l'évolution discrète du système et de son évolution continue prenant en compte les aspects probabilistes. Dans ce contexte, dans le chapitre 2, nous introduisons le concept d'automate stochastique hybride capable de prendre en compte tous les problèmes posés par la fiabilité dynamique et d'accéder à l'évaluation des grandeurs de la sûreté de fonctionnement par une simulation de Monte Carlo implémentée dans l'environnement Scilab-Scicos. Dans le chapitre 3, nous montrons l'efficacité de notre approche de simulation pour l'évaluation de la sûreté de fonctionnement en contexte dynamique sur deux cas test dont un est un benchmark de la communauté de la Sûreté de Fonctionnement. Notre approche permet de répondre aux problèmes posés, notamment celui de la prise en compte de l'influence de l'état discret, de l'état continu et de leur interaction dans l'évaluation probabiliste des performances d'un système dans lequel en outre, les caractéristiques fiabilistes des composants dépendent eux-mêmes des états continu et discret. Dans le chapitre 4, nous donnons une idée de l'intérêt du contrôle par supervision comme moyen de la sûreté de fonctionnement. Les concepts d'automate observateur et de contrôleur ont été introduits et illustrés sur notre cas test afin de montrer leur potentialité.

La vérification et la validation des composants logiciels des systèmes temps réel est un des enjeuxmajeurs pour le développement de systèmes automatisés. Les modèles de tels systèmes doiventêtre vérifiés, et la conformité de leur implémentation par rapport à leur modèle doit être validée. Nous nous plaçons dans le cadre des systèmes récursifs temps réels modélisables par des automates à pile temporisés avec deadlines (TPAIO). Les deadlines imposent des conditions de progression du temps. L’objectif de cette thèse est de proposer des méthodes de génération de tests pour les TPAIO.Nos contributions sont les suivantes. Premièrement, une relation de conformité pour les TPAIO est introduite. Deuxièmement, une méthode polynomiale de génération de tests à partir d’un TPAIO déterministe avec deadline lazy est définie. Elle consiste à définir un algorithme de calcul d’un automate temporisé d’accessibilité incomplet en respectant les contraintes de pile. Cette méthode est incomplète. L’incomplétude n'étant pas un problème car l’activité de test est par essence incomplète. Troisièmement, nous définissons une méthode générant des cas de tests à partir d’un TPAIO déterministe avec sorties seulement et deadline delayable seulement. Elle d’applique aux abstractions de programmes récursifs temporisés. Elle consiste à générer des cas de tests en calculant un testeur sur-approximé. Finalement, nous avons proposé une généralisation du processus de génération de tests à partir d’un TPAIO général avec entrées/sorties et avec deadlines quelconques. La capacité de cette dernière méthode à détecter des implémentations non conformes est évaluée par une technique de mutation. / The verification and validation of software components for real-time systems is a major challenge for the development of automated systems. The models of such systems must be verified and the conformance of their implementation w.r.t their model must be validated. Our framework is that of real-time recursive systems modelled by timed pushdown automata with deadlines (TPAIO). The deadlines impose time progress conditions. The objective of this thesis is to propose test generation methods from TPAIO.Our contributions are as follows. Firstly, a conformance relation for TPAIO is introduced. Secondly, a polynomial method of test generation from a deterministic TPAIO with only lazy deadlines is defined. It consists of defining a polynomial algorithm that computes a partial reachability timed automaton by removing the stack constraints. This method is incomplete. The incompleteness is not a problem because software testing is an incomplete activity by nature. Thirdly, we define a method for generating test cases from a deterministic TPAIO with only outputs and delayable deadlines. It applies to the abstractions of timed recursive programs. It consists of generating test cases by computing an over-approximated tester. Finally, we propose a generalization of the test generation process from a non deterministic TPAIO with any deadlines. Its ability to detect non conform implementation is assessed by a mutation technique.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Cette thèse traite de l'identification des systèmes à événements discrets (SED) automatisés dans un contexte industriel. En particulier, le travail aborde les systèmes formés par un processus et un automate programmable (AP) fonctionnant en boucle fermée - l'identification a pour but d’obtenir un modèle approximatif exprimé en réseaux de Petri interprétés (RPI) à partir du comportement externe observé sous la forme d'une seule séquence de vecteurs d’entrée-sortie de l’AP. Tout d'abord, une analyse des méthodes d'identification est présentée, ainsi qu’une étude comparative des méthodes récentes pour l'identification des SED. Puis le problème abordé est décrit - des importantes caractéristiques technologiques dans les systèmes automatisés par l’AP sont détaillées. Ces caractéristiques doivent être prises en compte dans la résolution du problème, mais elles ne peuvent pas être traitées par les méthodes existantes d’identification. La contribution principale de cette thèse est la création de deux méthodes d’identification complémentaires. La première méthode permet de construire systématiquement un modèle RPI à partir d'une seule séquence entrée-sortie représentant le comportement observable du SED. Les modèles RPI décrivent en détail l’évolution des entrées et sorties pendant le fonctionnement du système. La seconde méthode considère des SED grands et complexes - elle est basée sur une approche statistique qui permettre la construction des modèles en RPI compactes et expressives. Elle est composée de deux étapes - la première calcule à partir de la séquence entrée-sortie, la partie réactive du modèle, constituée de places observables et de transitions. La deuxième étape fait la construction de la partie non-observable, en rajoutant des places pour permettre la reproduction de la séquence entrée-sortie. Les méthodes proposées, basées sur des algorithmes de complexité polynomiale, ont été implémentées en outils logiciels, lesquels ont été testés avec des séquences d’entrée-sortie obtenues à partir des systèmes réels en fonctionnement. Les outils sont décrits et leur application est illustrée à travers deux cas d’étude. / This thesis deals with the identification of automated discrete event systems (DES) operating in an industrial context. In particular the work focuses on the systems composed by a plant and a programmable logic controller (PLC) operating in a closed loop- the identification consists in obtaining an approximate model expressed in interpreted Petri nets (IPN) from the observed behaviour given under the form of a single sequence of input-output vectors of the PLC. First, an overview of previous works on identification of DES is presented as well as a comparative study of the main recent approaches on the matter. Then the addressed problem is stated- important technological characteristics of automated systems and PLC are detailed. Such characteristics must be considered in solving the identification problem, but they cannot be handled by previous identification techniques. The main contribution in this thesis is the creation of two complementary identification methods. The first method allows constructing systematically an IPN model from a single input-output sequence representing the observable behaviour of the DES. The obtained IPN models describe in detail the evolution of inputs and outputs during the system operation. The second method has been conceived for addressing large and complex industrial DES- it is based on a statistical approach yielding compact and expressive IPN models. It consists of two stages- the first one obtains, from the input-output sequence, the reactive part of the model composed by observable places and transitions. The second stage builds the non observable part of the model including places that ensure the reproduction of the observed input-output sequence. The proposed methods, based on polynomial-time algorithms, have been implemented in software tools, which have been tested with input-output sequences obtained from real systems in operation. The tools are described and their application is illustrated through two case studies.

Cette thèse revisite les problèmes d'accessibilité et de vivacité pour les au-tomates temporisés.L'accessibilité est couramment résolue par le calcul d'un arbre de recherche abstrait. L'abstraction est paramétrée par des bornes provenant des gardes de l'automate. Nous montrons que l'abstraction a 4LU de Behrmann et al. est la plus grande abstraction saine et complète pour les bornes LU. N' étant pas convexe, elle n'est pas mise en oeuvre dans les outils. Nous introduisons une méthode qui permet son utilisation éfficace. Finalement, nous proposons une optimisation des bornes à la volée exploitant le calcul de l'arbre.Le problème de vivacité requiert de détecter les exécutions Zenon/non-Zenon. Une solution standard ajoute une horloge à l'automate. Nous montrons qu'elle conduit a une explosion combinatoire. Nous proposons une solution qui évite ce problème pour une grande classe d'abstractions. Pour les abstractions LU nous montrons que détecter ces exécutions est un problèmeNP-complet. / We consider the classic model of timed automata introduced by Alurand Dill. Two fundamental properties one would like to check in this modelare reachability and liveness. This thesis revisits these classical problems.The reachability problem for timed automata asks if there exists a run ofthe automaton from the initial state to a given final state. The standard solutionto this problem constructs a search tree whose nodes are abstractionsof zones. For effectiveness, abstractions are parameterized by maximal lowerand upper bounds (LU-bounds) occurring in the guards of the automaton.Such abstractions are also termed as LU-abstractions. The a4LU abstractiondefined by Behrmann et al is the coarsest known LU-abstraction. Althoughit is potentially most productive to use the a4LU abstraction, it has not beenused in implementations as it could lead to non-convex sets. We show howone could use the a4LU abstraction efficiently in implementations. Moreover,we prove that a4LU abstraction is optimal: given only the LU-bound information,it is the coarsest possible abstraction that is sound and completefor reachability. We then concentrate on ways to get better LU-bounds. Inthe standard procedure the LU-bounds are obtained from a static analysisof the automaton. We propose a new method to obtain better LU-boundson-the-fly during exploration of the zone graph. The potential gains of proposedimprovements are validated by experimental results on some standardverification case studies.The liveness problem deals with infinite executions of timed automata.An infinite execution is said to be Zeno if it spans only a finite amountof time. Such runs are considered unrealistic. While considering infiniteexecutions, one has to eliminate Zeno runs or dually, find runs that arenon-Zeno. The B¨uchi non-emptiness problem for timed automata asks ifthere exists a non-Zeno run visiting an accepting state infinitely often. Thestandard solution to this problem adds an extra clock to take care of non-Zenoness. We show that this solution might lead to an exponential blowupin the search space. We propose a method avoiding this blowup for a wideclass of abstractions weaker than LU-abstractions. We show that such amethod does not exist for LU-abstractions unless P=NP. Another questionrelated to infinite executions of timed automata is to decide the existenceof Zeno runs. We provide the first complete solution to this problem. Itworks for a wide class of abstractions weaker than LU. Yet again, we showthe solution could lead to a blowup for LU-abstractions, unless P=NP.

La modélisation dans le domaine de l'agro-écologie est importante car elle permet de mieux comprendre les interactions entre l'environnement et les activités humaines. Des travaux basés sur la simulation ont été développés depuis des années. Cependant, non seulement ces outils restent difficiles à utiliser par les utilisateurs non experts, mais aussi le coût des modèles rend leur utilisation difficile à case de la complexité élevée en cas d'application réelle. Nous proposons une approche qui consiste à représenter le système étudié dans un formalisme de système à événements discrets qui est bien adapté quand la dynamique du système est liée à des interactions entre les entités concernés. Ceci permet de profiter l'efficacité du model-checking pour étudier le comportement du système modélisé et d'utiliser la synthèse de contrôleur pour générer automatiquement des stratégies optimales. Nous présentons deux contributions dans cette thèse. La première contribution concerne le projet EcoMata. Cette modélisation qualitative en automates temporisés pour un réseau trophique marin de type proie-prédateur permet d'analyser l'écosystème à l'aide de model-checking sans avoir à faire des simulations. Des scénarios de requête prédéfinis ont été développés dans un langage naturel pour que les utilisateurs non expert puissent faire des requêtes sur les réseaux trophiques sans avoir des connaissances sur la langage TCTL. Nous avons amélioré la génération automatique d'automates temporisés à partir d'une description des équation Lotka-Votera. Nous avons aussi proposé une approche de synthèse de contrôleur pour générer automatiquement des stratégies optimales de gestion de pêche. Le prototype logiciel EcoMata implémente l'ensemble des propositions incluant la recherche de stratégies optimales. Dans la seconde contribution, nous proposons une modélisation hybride en automates temporisés d'une exploitation de pâturage. Cette modélisation hybride combine un modèle numérique de la croissance d'herbe et un modèle qualitatif des activités de pâturage. Une structure hiérarchique organise les modèles dans quatre couches: la couche biologique, la couche activité, la couche décisionnelle et la couche d'horloge. Nous proposons quatre méthodes pour générer des stratégies optimales des activités de pâturage. La première méthode est appliquée à la recherche de stratégies optimales de la mise au pâturage. Trois méthodes sont dédiées à la recherche de stratégies optimales de la fertilisation. Une d'entre elles utilise la synthèse de contrôleur alors que les deux autres combinent la synthèse de contrôleur et l'apprentissage supervisé pour générer des stratégies génériques par type d'exploitation. Un prototype logiciel PaturMata a été développé implémentant cette modélisation, permettant aux utilisateurs de simuler des scénarios de pâturage et rechercher des stratégies optimales de mise au pâturage. / The modeling in the domain of agro-ecology is important since it helps us to better understand the interactiosn between the environment and the human activities. Some research works based on simulation has been carried out during the recent years. Mainwhile, not only these simulation tools are difficult to use by the non expert users, but also the high complexity of models makes interactive uses impossible. We propose an approch in which we represent the system to be studied in a discret event system formalism. This kind of representation benefits the efficiency of model-checking and makes it possible to use controller synthesis to generate strategies. We present two contributions in this thesis. The first one concerns the project EcoMata. This project proposes a qualitative modelling which represents a marine prey-predator type food chain in timed automata. Predifined query patterns in natural langurage are also proposed which allow users to investigate easiy the food chain. We have improved the efficiency of the algorithm of timed automata generation and also developped a strategy synthesis method to generate best fishing management strategy. The prototype software EcoMata implements all these propositions including the best strategy synthesis. In the second contribution, we propose a hybrid modelling which represents grazing activities in timed automata. This hybrid modelling combines a numerical grass model and a qualitative grazing model. These sub models are organized in a hierarchical struture of four layers: the biological layer, the activity layer, the decision layer and the clock. We propose four methods to generate best grazing management strategy. One of these methods is applied to the movement of herd. The other three methods are applied to fertilization among which one of them use controller synthesis on timed automata and the other two combine controller synthesis and machine learning to generate generic strategy for a exploitation type. A prototype software PaturMata has been developped which implements this modelling method and the generation of the best strategy of herd movement.