Langages formels : Quelques aspects quantitatifs

Formal languages are sequences of symbols in some discrete set called alphabet. They are often specified by formulas in some logic, by rational expressions or else by discrete automata of various types. Current theory is mostly qualitative, in the sense that its objects are sequences over a discrete, non-metric, time, that acceptation of a sequence over an automaton depends on whether an accepting state is visited or not, and that, for language comparison, one will most often consider inclusion than quantitative measures. This thesis contributes to the study of these often neglected aspects by presenting fundamental results in three new quantitative problem classes about formal languages. In the first chapter, we study a class of scheduling problems which combines structural aspects related to dependencies between tasks with dynamical aspects of online scheduling. We show that some task request streams in this class of problems, however admissible in the sense that they do not require more raw resource utilization than available machines can provide, cannot be scheduled with bounded latency. However, we develop a scheduling policy which can guarantee a bounded backlog accumulation for all admissible streams even without knowledge of the stream content prior to execution. We show that if the streams actually are sub-critical, then the same policy also guarantees a bounded latency. In quantitative verification, states and transitions of a system can be endowed with costs, which can be used to associate average costs to infinite behaviors. In this second part, we propose to define omega-languages thanks to Boolean queries concerning average costs. Specifications dealing with averages, such as "average message loss is under some threshold" are not omega-regular, but can be expressed in our model. Hence we study expressive power and Borel complexity of such specifications. We show that in order to ensure closure by intersection, multi-dimensional costs have to be considered. In the general case, we show that accepting conditions can be defined on the set of accumulation points of the sequence of the average costs of the prefixes of a run. We accurately characterize such sets. Last, we also propose a class of multi-threshold mean-payoff languages, in which extremal values of coordinates of points of the accumulation set are compared to constants. We show this class is closed under Boolean operations and analyzable. In the last chapter, we define two measures for a timed language: the volume of its sub-languages of words having a fixed number of discrete events, and entropy, which is the asymptotic logarithmic growth of volumes. These measures can be used to compare languages quantitatively and entropy can be seen as information content of a typical event of a typical word of in a language. For languages accepted by deterministic timed automata, we give an exact formula for the volume. Next we characterize entropy, thanks to functional analysis techniques, as the logarithm of the spectral radius of some positive integral operator. We give several methods to compute entropy: a symbolical one for the special case of "one clock and a half" automata, and two numerical ones: one using functional analysis, the other using discretization techniques. Last we establish an interpretation of this entropy in information theory by showing its relation with Kolmogorov complexity.Les langages formels sont des séquences sur un ensemble discret de symboles appelé alphabet. On les spécifie souvent par des formules dans une certaine logique, par des expressions rationnelles ou bien par des automates discrets de types variés. La théorie actuelle est principalement qualitative, dans le sens où ses objets sont des séquence sur un temps discret, non-métrique, dans le sens où l'acceptation d'une séquence sur un automate dépend du fait que l'on visite ou non un état accepteur, et enfin dans le sens où la comparaison de langages est plus souvent considérée en termes d'inclusion, plutôt qu'en termes de mesures quantitatives. Cette thèse contribue à l'étude de ces aspects souvent négligés en présentant des résultats fondamentaux dans trois nouvelles classes de problèmes quantitatifs sur les langages formels. Dans la première partie, nous étudions une classe de problèmes d'ordonnancement qui combine les aspects structurels associés aux dépendances entre tâches avec les aspects dynamiques liés au fait qu'un flux de requêtes arrive en continu pendant l'exécution. Nous montrons que, dans cette classe de problèmes, certains flux, pourtant admissibles dans le sens que les requêtes ne représentent pas plus de travail que ce que les machines peuvent traiter, ne peuvent pas être ordonnancé avec une latence bornée. Cependant nous développons une politique d'ordonnancement que peut garantir une accumulation de retard bornée pour tout flux de requêtes admissible, même sans le connaître à l'avance. Nous montrons que si les flux sont sous-critiques, alors cette même politique peut garantir une latence bornée. En vérification quantitative, les états et transitions d'un système peuvent être associés à des coûts, et ceux-ci utilisés pour associer des coûts moyens aux comportements infinis. Dans cette seconde partie, nous proposons de définir des omega-langages par des requêtes booléennes sur les coûts moyens. Des spécifications concernant des moyennes, tels que " le taux de perte moyen de messages est inférieur à un certain seuil " ne sont pas omega-régulières, mais exprimables dans notre modèle. Ainsi, nous étudions l'expressivité et la complexité de Borel de telles spécifications. Nous montrons que pour la clôture par intersection, il est nécessaire de considérer des coûts multi-dimensionnels. Nous mettons en évidence que dans le cas général, les conditions d'acceptation portent sur l'ensemble des points d'accumulation de la séquence des coûts moyens des préfixes d'une exécution, et nous donnons une caractérisation précise de tels ensembles. Nous proposons une classe de langages de coût moyen à seuils multiples, comparant les coordonnées minimales et minimales des points de cet ensemble à des constantes. Nous montrons enfin que cette classe est close par opérations booléennes et analysable. Enfin, dans le dernier volet, nous définissons deux mesures pour un langage temporisé : le volume de ses sous-langages de mots à nombre d'événements fixe et l'entropie (vitesse de croissance), mesure asymptotique pour un nombre non borné d'événements. Ces mesures peuvent être utilisées pour la comparaison quantitative de langages, et l'entropie peut être vue comme la quantité d'information par événement dans un mot typique du langage temporisé. Pour les langages acceptés par des automates temporisés déterministes, nous donnons une formule exacte pour le volume. Ensuite, nous caractérisons l'entropie, en utilisant des méthodes d'analyse fonctionnelle, en tant que logarithme du rayon spectral d'un opérateur intégral positif. Nous établissons plusieurs méthodes pour calculer l'entropie : une symbolique pour les automates que nos appelons " à une horloge et demie ", et deux numériques : une utilisant les techniques d'analyse fonctionnelle, l'autre basée sur la discrétisation. Nous donnons une interprétation de l'entropie en théorie de l'information en termes de complexité de Kolmogorov