Büchi, Elgot and Trakhtenbrot provided a seminal connection between monadic second-order logic and finite automata for both finite and infinite words. This BET- Theorem has been extended by Lautemann, Schwentick and Thérien to context-free languages by introducing a monadic second-order logic with an additional existentially quantified second-order variable. This new variable models the stack of pushdown au- tomata. A fundamental study by Cohen and Gold extended the context-free languages to infinite words. Our first main result is a second-order logic in the sense of Lautemann, Schwentick and Thérien with the same expressive power as ω-context-free languages. For our argument, we investigate Greibach normal forms of ω-context-free grammars as well as a new type of Büchi pushdown automata, the simple pushdown automata. Simple pushdown automata do not use e-transitions and can change the stack only by at most one symbol. We show that simple pushdown automata of infinite words suffice to accept all ω-context-free languages. This enables us to use Büchi-type results recently developed for infinite nested words. In weighted automata theory, many classical results on formal languages have been extended into a quantitative setting. Weighted context-free languages of finite words trace back already to Chomsky and Schützenberger. Their work has been extended to infinite words by Ésik and Kuich. As in the theory of formal grammars, these weighted ω-context-free languages, or ω-algebraic series, can be represented as solutions of mixed ω-algebraic systems of equations and by weighted ω-pushdown automata. In our second main result, we show that (mixed) ω-algebraic systems can be trans- formed into Greibach normal form. We then investigate simple pushdown automata in the weighted setting. Here, we give our third main result. We prove that weighted simple pushdown automata of finite words recognize all weighted context-free languages, i.e., generate all algebraic series. Then, we show that weighted simple ω-pushdown automata generate all ω-algebraic series. This latter result uses the former result together with the Greibach normal form that we developed for ω-algebraic systems. As a fourth main result, we prove that for weighted simple ω-pushdown automata, Büchi-acceptance and Muller-acceptance are expressively equivalent. In our fifth main result, we derive a Nivat-like theorem for weighted simple ω- pushdown automata. This theorem states that the behaviors of our automata are precisely the projections of very simple ω-series restricted to ω-context-free languages. The last result, our sixth main result, is a weighted logic with the same expressive power as weighted simple ω-pushdown automata. To prove the equivalence, we use a similar result for weighted nested ω-word automata and apply our present result of expressive equivalence of Muller and Büchi acceptance.

This thesis is concerned with automata over infinite trees. They are given a labeled infinite tree and accept or reject this tree based on its labels. A generalization of these automata with binary decisions are weighted automata. They do not just decide 'yes' or 'no', but rather compute an arbitrary value from a given algebraic structure, e.g., a semiring or a lattice. When passing from unweighted to weighted formalisms, many problems can be translated accordingly. The purpose of this work is to determine the feasibility of solving the inclusion problem for automata on infinite trees and its generalization to weighted automata, the infimum aggregation problem.

Cette thèse porte sur certaines extensions des automates pondérés, et étudie les séries qu’ils réalisent en fonction de la nature des poids.Ces extensions se distinguent par les mouvements supplémentaires autorisés à la tête de lecture de l’automate : retour au début du mot pour les automates circulaires, changement de sens de lecture pour les automates boustrophédons.Dans le cas général, les automates pondérés circulaires sont plus puissants que les automates unidirectionnels classiques, et moins puissants que les boustrophédons.On introduit de plus les expressions de Hadamard, qui sont une extension des expressions rationnelles et qui permettent de dénoter le comportement des automates circulaires. Les aspects algorithmiques de cette conversion sont étudiés dans le cas où les poids appartiennent à un semi-anneau rationnellement additif.On montre que lorsque les poids sont des nombres rationnels, réels ou complexes, les automates circulaires sont aussi expressifs que les boustrophédons.Enfin, si les poids forment un bi-monoïde localement fini, les automates boustrophédons ne sont pas plus expressifs que les automates pondérés classsiques. / This thesis deals with some extensions of weighted automata,and studies the series they can realisedepending on the nature of their weigths.These extensions are characterised by howthe input head of the automaton is allowed to move:rotating automata can go back at the beginning of the word,and two-way automata can change the reading direction.In the general setting, weigthed rotating automata are morepowerful than classical one-way automata, and less powerfulthan two-way ones.Moreover, we introduce Hadamard expressions,which are an extension of rational expressions and can denotethe behaviour of rotating automata.The algorithms for this conversion are studied when the weights belong toa rationally additive semiring.Then, rotating automata are shown as expressive as two-way automatain the case of rational, real or complex numbers.It is also proved that two-way and one-way automataare equivalent when weighted on a locally finite bimonoid.

L'objectif principal de cette thèse est de proposer une approche efficace de modélisation et de résolution pour le problème d’ordonnancement, en mettant l’accent sur le partage multi-ressources et sur l’incertitude potentielle d’occurrence de certains événements. L'ordonnancement a pour objectif de réaliser un ensemble de tâches à la fois en respectant des contraintes prédéfinies et en optimisant le temps. Ce travail s’intéresse en particulier à la minimisation du temps total d’exécution. La plupart des approches existantes préconisent une modélisation mathématique exprimant des équations et des contraintes pour décrire et résoudre des problèmes d’ordonnancement. De telles démarches ont une complexité inhérente. Cependant dans l’industrie, la tâche de planification est récurrente et peut requérir des changements fréquents des contraintes. Outre cela, la prise en compte d’événements incertains est peu supportée par les approches existantes; cela peut toutefois augmenter la robustesse d’un ordonnancement. Pour répondre à ces problématiques, après une introduction, le chapitre 2 aborde le problème de l’ordonnancement à travers une démarche de modélisation visuelle, expressive et formelle, s’appuyant sur les automates pondérés et sur la théorie des automates temporisés. L’originalité des modèles proposés réside aussi dans leur capacité de décrire le partage de ressources multiples et proposer une approche de résolution efficace. Ces modèles ont l’avantage d’être directement exploitables par des outils de vérification formelle, à travers une démarche de preuve par contradiction vis-à-vis de l’existence d’une solution. Les résultats effectifs sont obtenus grâce à l’outil UPPAAL. La complexité inhérente à la production d’une solution optimale est abordée à travers un algorithme de recherche et d’amélioration itérative de solutions, offrant une complexité très prometteuse sur la classe de problèmes étudiés. Dans le chapitre 3, une composition synchrone est d’automates pondérés est proposée dans le but de résoudre le problème d’ordonnancement en effectuant une analyse d’atteignabilité optimale directement sur les modèles automates pondérés. Dans le quatrième chapitre, divers comportements incontrôlables tels que le temps de début, la durée de la tâche et l'occurrence d’échec dans un problème d‘ordonnancement sont modélisés par des automates de jeu temporisés. Ensuite, le problème est résolu en effectuant une synthèse de stratégie optimale dans le temps dans l'outil de synthèse TIGA. / The objective of scheduling problems is to find the optimal performing sequence for a set of tasks by respecting predefined constraints and optimizing a cost: time, energy, etc. Despite classical approaches, automata models are expressive and also robust against changes in the parameter setting and against changes in the problem specification. Besides, few studies have used formal verification approaches for addressing scheduling problems; yet none of them considered challenging and practical issues such as multi-resource sharing aspect, uncontrollable environment and reaching the optimal schedule in a reasonable time for industrializing the model. The main objective of this thesis is to propose an efficient modeling and solving approach for the scheduling problem, considering multi-resource sharing and potential uncertainty in occurrence of certain events. For this purpose, after an introduction in Chapter 1, Chapter 2 addresses the problem of scheduling through a visual, expressive and formal modeling approach, based on weighted automata and the theory of timed automata. The originality of the proposed approach lies in ability of handling the sharing of multiple resources and proposing an efficient solving approach. The proposed models have the advantage of being directly exploitable by means of formal verification tools. The results are obtained using the UPPAAL tool. To solve the problem, an algorithm is developed based on iterating reachability analysis to obtain sub-optimal makespan. Results show the proposed model and solving approach provides a very promising complexity on the class of studied problems and can be applied to industrial cases. In Chapter 3, a synchronous composition of weighted automata is proposed to solve the scheduling problem by performing an optimal reachability analysis directly on the weighted automata models. In the fourth chapter, various uncontrollable behaviors such as the start time, the duration of the task and the failure occurrence in a scheduling problem are modeled by timed game automata. Then, the problem is solved by performing an optimal strategy synthesis over time in TIGA as a synthesis tool.

The focus of this thesis is the comparison of languages and the reduction of automata used in network traffic monitoring. In this work, several approaches for approximate (language non-preserving) reduction of automata and comparison of their languages are proposed. The reductions are based on either under-approximating the languages of automata by pruning their states, or over-approximating the language by introducing new self-loops (and pruning redundant states later). The proposed approximate reduction methods and the proposed probabilistic distance utilize information from a network traffic. Formal guarantees with respect to a model of network traffic, represented using a probabilistic automaton are provided. The methods were implemented and evaluated on automata used in network traffic filtering.

In this thesis, we investigate weighted tree automata with storage theoretically. This model generalises finite state automata in three dimensions: (i) from words to trees, (ii) by using an arbitrary storage type in addition to a finite-state control, and (iii) by considering languages in a quantitative setting using a weight structure.

Automata theory, one of the main branches of theoretical computer science, established its roots in the middle of the 20th century. One of its most fundamental concepts is that of a finite automaton, a basic yet powerful model of computation. In essence, finite automata provide a method to finitely represent possibly infinite sets of strings. Such a set of strings is also called a language, and the languages which can be described by finite automata are known as regular languages. Owing to their versatility, regular languages have received a great deal of attention over the years. Other formalisms were shown to be expressively equivalent to finite automata, most notably regular grammars, regular expressions, and monadic second order (MSO) logic. To increase expressiveness, the fundamental idea underlying finite automata and regular languages was also extended to describe not only languages of strings, or words, but also of infinite words by Büchi and Muller, finite trees by Doner and Thatcher and Wright, infinite trees by Rabin, nested words by Alur and Madhusudan, and pictures by Blum and Hewitt, just to name a few examples. In a parallel line of development, Schützenberger introduced weighted automata which allow the description of quantitative properties of regular languages. In subsequent works, many of these descriptive formalisms and extensions were combined and their relationships investigated. For example, weighted regular expressions and weighted logics have been developed as well as regular expressions for trees and pictures, regular grammars for trees, pictures, and nested words, and logical characterizations for regular languages of trees, pictures, and nested words. In this work, we focus on two of these extensions and their relationship, namely weighted automata and weighted logics. Just as the classical Büchi-Elgot-Trakhtenbrot Theorem established the coincidence of regular languages with languages definable in monadic second order logic, weighted automata have been shown to be expressively equivalent to a specific fragment of a weighted monadic second order logic by Droste and Gastin. We explore several aspects of weighted automata and of this weighted logic. More precisely, the thesis considers the following topics. In the first part, we extend the classical Feferman-Vaught Theorem to the weighted setting. The Feferman-Vaught Theorem is one of the fundamental theorems in model theory. The theorem describes how the computation of the truth value of a first order sentence in a generalized product of relational structures can be reduced to the computation of truth values of first order sentences in the contributing structures and the evaluation of an MSO sentence in the index structure. The theorem itself has a long-standing history. It builds upon work of Mostowski, and was shown in subsequent works to hold true for MSO logic. Here, we show that under appropriate assumptions, the Feferman-Vaught Theorem also holds true for a weighted MSO logic with arbitrary commutative semirings as weight structure. In the second part, we lift four decidability results from max-plus word automata to max-plus tree automata. Max-plus word and tree automata are weighted automata over the max-plus semiring and assign real numbers to words or trees, respectively. We show that, like for max-plus word automata, the equivalence, unambiguity, and sequentiality problems are decidable for finitely ambiguous max-plus tree automata, and that the finite sequentiality problem is decidable for unambiguous max-plus tree automata. In the last part, we develop a logic which is expressively equivalent to quantitative monitor automata. Introduced very recently by Chatterjee, Henzinger, and Otop, quantitative monitor automata are an automaton model operating on infinite words. Quantitative monitor automata possess several interesting features. They are expressively equivalent to a subclass of nested weighted automata, an automaton model which for many valuation functions has decidable emptiness and universality problems. Also, quantitative monitor automata are more expressive than weighted Büchi-automata and their extension with valuation functions. We introduce a new logic which we call monitor logic and show that it is expressively equivalent to quantitative monitor automata.

L'un des problèmes fondamentaux de test pour les systèmes à événements discrets (SEDs) est l'identification d'un état final, c'est-à-dire, étant donné un système dont l'état courant est inconnu, trouver une séquence d'événements d'entrée pouvant le conduire à un état connu. Les séquences de synchronisation (SS), sans information de sortie, sont une solution classique à ce problème. Dans cette thèse, nous étudions la détermination des SS pour des systèmes modélisés par des réseaux de Petri synchronisés (SynPN) non bornés, une classe de réseaux de Petri avec des entrées. Dans la première partie de cette thèse, nous développons deux méthodes: 1) construction d'une représentation finie, appelée improved modified coverability graph (IMCG), pour d'écrire exactement l'espace d'états infini d'un 1-place-unbounded SynPN; 2) conversion d'un 1-place-unbounded SynPN en un automate pondéré (WA) fini et sauf équivalent. Les deux graphes sont ainsi potentiellement des outils puissants pour déterminer les SS pour une telle sous-classe de réseaux de Petri. Dans la seconde partie de cette thèse, nous développons des algorithmes de calcul pour deux problèmes de synchronisation de localisation dans le cas où l'IMCG ou le WA sont déterministes : synchronisation sur un seul nœud et synchronisation sur un sous-ensemble de nœuds de ces deux graphes. L'avantage de ces algorithmes de calcul est de réduire le calcul sur les graphes globaux (IMCG ou WA) à celui du plus petit sous-graphe: la composante fortement connectée ergodique peut réduire l'effort de calcul mais peut également être appliquée lorsque le IMCG ou le WA équivalent déterministes ne sont pas fortement connexes / One of the fundamental testing problems for discrete event systems (DESs) is the identification of a final state, i.e., given a system whose current state is unknown, find an input sequence that can drive it to a known state. Synchronizing sequences (SSs), without output information, are one conventional solution to this problem. In this thesis, we address the computation of SSs for systems modeled by unbounded synchronized Petri nets (SynPNs), a class of Petri nets with inputs. In the first part of this thesis, we utilize two methods: 1) construct a finite representation, called improved modified coverability graph (IMCG), to exactly describe the infinite state space of a 1-place-unbounded SynPN; 2) convert a 1-place-unbounded SynPN into an equivalent finite location weighted automaton (WA) with safety conditions. Both graphs are thus, potentially, useful tools to compute SSs for such subclass of nets. In the second part of this thesis, we develop computation algorithms for two location synchronization problems in the case either the IMCG or the WA is deterministic: synchronization into a single node and synchronization into a subset of nodes of these two graphs. The advantage of these computation algorithms consists in reducing the computation on the global graphs (IMCGs or WAs) to the one on the smaller subgraph: the ergodic strongly connected component (SCC), which can reduce the computational effort and furthermore can also be applied when the converted deterministic IMCG or WA is not strongly connected

Recently, multi-priced timed automata have received much attention for real-time systems. These automata extend priced timed automata by featuring several price parameters. This permits to compute objectives like the optimal ratio between rewards and costs. Arising from the model of timed automata, the multi-weighted setting has also attracted much notice for classical nondeterministic automata. The present thesis develops multi-weighted MSO-logics on finite, infinite and timed words which are expressively equivalent to multi-weighted automata, and studies decision problems for them. In addition, a Nivat-like theorem for weighted timed automata is proved; this theorem establishes a connection between quantitative and qualitative behaviors of timed automata. Moreover, a logical characterization of timed pushdown automata is given.

Ce manuscrit regroupe différents travaux explorant les interactions entre les tenseurs et l'apprentissage automatique. Le premier chapitre est consacré à l'extension des modèles de séries reconnaissables de chaînes et d'arbres aux graphes. Nous y montrons que les modèles d'automates pondérés de chaînes et d'arbres peuvent être interprétés d'une manière simple et unifiée à l'aide de réseaux de tenseurs, et que cette interprétation s'étend naturellement aux graphes ; nous étudions certaines propriétés de ce modèle et présentons des résultats préliminaires sur leur apprentissage. Le second chapitre porte sur la minimisation approximée d'automates pondérés d'arbres et propose une approche théoriquement fondée à la problématique suivante : étant donné un automate pondéré d'arbres à n états, comment trouver un automate à m<n états calculant une fonction proche de l'originale. Le troisième chapitre traite de la régression de faible rang pour sorties à structure tensorielle. Nous y proposons un algorithme d'apprentissage rapide et efficace pour traiter un problème de régression dans lequel les sorties des tenseurs. Nous montrons que l'algorithme proposé est un algorithme d'approximation pour ce problème NP-difficile et nous donnons une analyse théorique de ses propriétés statistiques et de généralisation. Enfin, le quatrième chapitre introduit le modèle de mélanges algébriques de distributions. Ce modèle considère des combinaisons affines de distributions (où les coefficients somment à un mais ne sont pas nécessairement positifs). Nous proposons une approche pour l'apprentissage de mélanges algébriques qui étend la méthode tensorielle des moments introduite récemment. . / This thesis tackles several problems exploring connections between tensors and machine learning. In the first chapter, we propose an extension of the classical notion of recognizable function on strings and trees to graphs. We first show that the computations of weighted automata on strings and trees can be interpreted in a natural and unifying way using tensor networks, which naturally leads us to define a computational model on graphs: graph weighted models; we then study fundamental properties of this model and present preliminary learning results. The second chapter tackles a model reduction problem for weighted tree automata. We propose a principled approach to the following problem: given a weighted tree automaton with n states, how can we find an automaton with m<n states that is a good approximation of the original one? In the third chapter, we consider a problem of low rank regression for tensor structured outputs. We design a fast and efficient algorithm to address a regression task where the outputs are tensors. We show that this algorithm generalizes the reduced rank regression method and that it offers good approximation, statistical and generalization guarantees. Lastly in the fourth chapter, we introduce the algebraic mixture model. This model considers affine combinations of probability distributions (where the weights sum to one but may be negative). We extend the recently proposed tensor method of moments to algebraic mixtures, which allows us in particular to design a learning algorithm for algebraic mixtures of spherical Gaussian distributions.