This thesis is a survey of the field of languages over infinite sequences. There is active research going on in this field, during the last year several new results where published. We investigate the language containment problem for infinite sequences, with focus on complementation of Büchi automata. Our main focus is on the approach with alternating automata by Kupferman&Vardi. The language containment problem has been proved to be in EXPSPACE. We identify some cases when we can avoid the exponential blow-up by taking advantage of properties of the input automaton. Some of the algorithms we explain are also implemented in a Sicstus Prolog library.

Reactive systems are computer systems that maintain continuous interaction with the environment in which they operate. Such systems are nowadays part of our daily life: think about common yet critical applications like engine control units in automotive, aircraft autopilots, medical aided- devices, or micro-controllers in mass production. Clearly, any flaw in such critical systems can have catastrophic consequences. However, they exhibit several characteristics, like resource limitation constraints, real-time responsiveness, concurrency that make them difficult to implement correctly. To ensure the design of reactive systems that are dependable, safe, and efficient, researchers and industrials have advocated the use of so-called formal methods, that rely on mathematical models to express precisely and analyze the behaviors of these systems.Automata theory provides a fundamental notion such as languages of program executions for which membership, emptiness, inclusion, and equivalence problems allow us to specify and verify properties of reactive systems. However, these Boolean notions yield the correctness of the system against a given property that sometimes, falls short of being satisfactory answers when the performances are prone to errors. As a consequence, a common engineering approach is not just to verify that a system satisfies a property, but whether it does so within a degree of quality and robustness.This thesis investigates the expressibility, recognition, and robustness of quantitative properties for program executions.• Firstly, we provide a survey on languages definable by regular automata with Presburger definable constraints on letter occurrences for which we provide descriptive complexity. Inspired by this model, we introduce an expression formalism that mixes formula and automata to define quantitative languages \ie function from words to integers. These expressions use Presburger arithmetic to combine values given by regular automata weighted by integers. We show that quantitative versions of the classical decision problems such as emptiness, universality, inclusion, and equivalence are computable. Then we investigate the extension of our expressions with a ''Kleene star'' style operator. This allows us to iterate an expression over smaller fragments of the input word, and to combine the results by taking their iterated sum. The decision problems quickly turn out to be not computable, but we introduce a new subclass based on a structural restriction for which algorithmic procedures exist.• Secondly, we consider a notion of robustness that places a distance on words, thus defining neighborhoods of program executions. A language is said to be robust if the membership satisfiability cannot differ for two ''close'' words, and that leads to robust versions of all the classical decision problems. Our contribution is to study robustness verification problems in the context of weighted transducers with different measures (sum, mean-payoff, and discounted sum). Here, the value associated by the transducer to rewrite a word into another denotes the cost of the noise that this rewriting induce. For each measure, we provide algorithms that determine whether a language is robust up to a given threshold of error and we solve the synthesis of the robust kernel for the sum measure. Furthermore, we provide case studies including modeling human control failures and approximate recognition of type-1 diabetes using robust detection of blood sugar level swings.• Finally, we observe that algorithms for structural patterns recognition of automata often share similar techniques. So, we introduce a generic logic to express structural properties of automata with outputs in some monoid, in particular, the set of predicates talking about the output values is parametric. Then, we consider three particular automata models (regular automata, transducers, and automata weighted by integers) and instantiate the generic logic for each of them. We give tight complexity results for the three logics with respect to the pattern recognition problem. We study the expressiveness of our logics by expressing classical structural patterns characterizing for instance unambiguity and polynomial ambiguity in the case of regular automata, determinizability, and finite-valuedness in the case of transducers and automata weighted by integers. As a consequence of our complexity results, we directly obtain that these classical properties can be decided in logarithmic space. / Doctorat en Sciences / info:eu-repo/semantics/nonPublished

Manual design of levels can be an expensive and time consuming process. Procedural content generation (PCG) entails methods to algorithmically generate game content such as levels. One such way is by using cellular automata (CA), and in particular evolved cellular automata. Existing research primarily considers specifically determined starting states, as opposed to randomly initialized ones. In this paper we investigate the current state of the art regarding using CA’s that have been evolved with a genetic algorithm (GA) for level generation purposes. Additionally, we create a level generator that uses a GA in order to evolve CA rules for the creation of maze-like 2d levels which can be used in video games. Specifically, we investigate if it is possible to evolve CA rules that, when applied to a set of random starting states, could transform these into game levels with long solution paths and a large number of dead ends. We generate 60 levels over 6 experiments, rendering 58 playable levels. Our analysis of the levels show some flaws in certain levels, such as large numbers of unreachable cells. Additionally, the results indicate that the designed GA can be further improved upon. Finally, we conclude that it is possible to evolve CA rules that can transform a set of random starting states into game levels.

La vérification est maintenant une branche très connue des sciences informatiques. Elle est cruciale lorsque l'on a affaire à des programmes informatiques dans des systèmes automatiques : on veut vérifier si un système donné est correct et s'il satisfait des propriétés nécessaires à son bon fonctionnement. Une façon d'analyser ces systèmes se fait par la modélisation mathématique. La question est alors : peut-on vérifier si le modèle satisfait les propriétés requises ? C'est ce que l'on appelle le problème du model-checking. Plusieurs modèles ont été étudiés dans la littérature. Nous portons notre intérêt sur des modèles qui peuvent mêler des aspects temporels et des aspects probabilistes. Dans cette thèse, nous étudions donc le modèle des automates temporisés et stochastiques (ATS). Les contributions de ce document sont divisées en deux parties. Tout d'abord, nous étudions les problèmes de model-checking qualitatifs et quantitatifs des ATS. Les ATS sont, en particulier, des systèmes probabilistes généraux et avec de tels modèles, on est intéressé par des questions du type : « Une propriété est-elle satisfaite, au sein d'un modèle donné, avec probabilité 1 ? » (qualitatif) ou bien « Peut-on calculer une approximation de la probabilité que le modèle satisfait une propriété donnée ? » (quantitatif).Nous étudions ces questions dans des systèmes probabilistes généraux en utilisant, entre autres, la notion de decisiveness utilisée dans les chaînes de Markov infinie dans le but d'obtenir d'importants résultats qualitatifs et que nous étendons ici dans notre contexte plus général. Nous prouvons plusieurs résultats pour les problèmes de model-checking qualitatifs et quantitatifs de ces systèmes probabilistes, certains d'entre eux étant des extensions de travaux antérieurs sur les chaînes de Markov, d'autres étant nouveaux, et nous montrons comment l'on peut appliquer ces résultats sur des sous-classes des ATS. Nous étudions ensuite la vérification compositionnelle des ATS. En général, un système est le résultat de plusieurs plus petits systèmes fonctionnant ensemble. La vérification compositionnelle permet alors de réduire l'analyse de gros systèmes aux analyses des plus petits systèmes qui le composent. Il est donc crucial d'avoir une bonne structure compositionnelle au sein des modèles mathématiques, et cela manque aux ATS. Dans cette thèse, nous définissons un opérateur de composition pour les ATS. Nous faisons d'abord l'hypothèse que les ATS composés fonctionnent complètement indépendamment l'un de l'autre, c'est-à-dire les ATS ne communiquent pas entre eux. Nous prouvons que notre définition satisfait bien cette hypothèse d'indépendance. Un tel opérateur de composition n'est pas très intéressant puisque, généralement, les systèmes interagissent entre eux. Mais c'est une première étape nécessaire. Nous introduisons donc le nouveau modèle des ATS interactifs (ATSI) qui vont permettre des interactions entre les systèmes. Nous définissons un opérateur de composition dans les ATSI qui va rendre possible des synchronisations entre les systèmes et qui est construit sur la précédente composition dans les ATS. Nous finissons cette thèse par l'identification d'une sous-classe de ATSI dans laquelle tous les résultats qualitatifs et quantitatifs fournis dans cette thèse peuvent être appliqués, et qui est donc accompagnée d'une bonne structure compositionnelle au sein du modèle. / Verification is now a well-known branch in computer science. It is crucial when dealing with computer programs in automatic systems: we want to check if a given system is correct and satisfies some specifications that should be met. One way to analyse those systems is to model them mathematically. The question is then: can we check if the model satisfies the required specifications ? This is called the model-checking problem. Several models have been studied in the literature. We have an interest for models that can mix both timing and randomized aspects. In this thesis we thus study the stochastic timed automaton model (STA). The contributions of this document are twofold. First, we study the qualitative and quantitative model-checking problems of STA. STA are, in particular, general probabilistic systems and with such model, one is thus interested in questions like « Is a property satisfied, within a given model, with probability 1 ? » (qualitative) or « Can we compute an approximation of the probability that the model satisfies a given property ? » (quantitative).We study those questions for general stochastic systems using, amongst other, the notion of decisiveness used in infinite Markov chains in order to get strong qualitative and quantitative results, and that we extend here in or more general context. We prove several results for the qualitative and quantitative model-checking problems of those probabilistic systems, some of them being extensions of previous work on Markov chains, others being new, and we show how it can be applied to subclasses of STA. Then we study the compositional verification in STA. In general, a system is the result of several smaller systems working together. Compositional verification allows then one to reduce the analysis of a big system to the analyses of the smaller systems which compose it. It is then crucial to have a good compositional framework in mathematical models, and this lacks in STA. In this thesis, we define an operator of composition for STA. We first make the assumption that the STA composed run completely independently from each other, i.e. they do not communicate between them. We prove that our definition satisfies indeed this independence assumption. Such an operator of composition is not very interesting as in general, systems do communicate. But it is a necessary first step. We then introduce the new model of interactive STA (ISTA) that will allow for interactions between the systems. We define an operator of composition in ISTA that will make synchronisations possible between the systems and that is built on the previous composition in STA. We end this thesis with the identification of a subclass of ISTA in which all the qualitative and quantitative results provided in this thesis can be applied, and which thus comes with the nice compositional framework defined in the model.

No description available.

No description available.

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.

This thesis investigates deep pushdown automata and introduces their modification called controlled deep pushdown automata. Distributed deep pushdown automata systems and parallel communicating deep pushdown automata systems are described. Their accepting power and properties are investigated and several variants are introduced. This thesis proves that the accepting power of one such variant of parallel communicating deep pushdown automata systems is equal to the accepting power of Turing machines. A method for syntactical analysis based on the previously introduced automata systems is described.

The goal of this master thesis is to examine possibilities of realizing comptutational structures in cellular automata. The work describes the fundamental principles of cellular automata and summarizes some ways of how to achive the specified goal. An overview of Turing-complete and other specialized computational tasks is proposed considering both 1D and 2D cellular automata. It is shown that different computational scenarios in cellular automata can be considered with various setups of the input and output arrangements. With regard to showed inputs and outputs arrangement, sets of tests is designed to find solutions of choosen computational structures on cellular automata with use of choosen evolutionary algorithm. Found solutions are compared by computational resources consumption and difficulty of discovery later.

This thesis elaborates the Büchi automata theory and introduces a library that enables working with them. Basics of the automata theory is explained. The main part of this work is focused on Büchi automata, which belong to finite automata. The main properties of Büchi automata are explained and proved. The knowledge of those properties is important for understanding the algorithms mentioned in this work. The next part describes those algorithms and explains their principles in details. The design of library is described in the next part of this work. Main part is aimed at the implementation of the library and auxiliary scripts. The most interesting and important parts of methods are described in detail. Closing part describes testing of library functionality.