In the thesis we discuss binary hyperstructures of linear differential operators of the second order both in general and (inspired by models of specific time processes) in a special case of the Jacobi form. We also study binary hyperstructures constructed from distributive lattices and suggest transfer of this construction to n-ary hyperstructures. We use these hyperstructures to construct multiautomata and quasi-multiautomata. The input sets of all these automata structures are constructed so that the transfer of information for certain specific modeling time functions is facilitated. For this reason we use smooth positive functions or vectors components of which are real numbers or smooth positive functions. The above hyperstructures are state-sets of these automata structures. Finally, we investigate various types of compositions of the above multiautomata and quasi-multiautomata. In order to this we have to generalize the classical definitions of Dörfler. While some of the concepts can be transferred to the hyperstructure context rather easily, in the case of Cartesian composition the attempt to generalize it leads to some interesting results.

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.

On considère des jeux stochastiques joués sur un graphe fini. La première partie s’intéresse aux jeux stochastiques à deux joueurs et information parfaite. Dans de tels jeux, les joueurs choisissent des actions dans ensemble fini, tour à tour, pour une durée infinie, produisant une histoire infinie. Le but du jeu est donné par une fonction d’utilité qui associe un réel à chaque histoire, la fonction est bornée et Borel-mesurable. Le premier joueur veut maximiser l’utilité espérée, et le deuxième joueur veut la minimiser. On démontre que si la fonction d’utilité est à la fois shift-invariant et submixing alors le jeu est semi-positionnel. C’est-à-dire le premier joueur a une stratégie optimale qui est déterministe et sans mémoire. Les deux joueurs ont information parfaite: ils choisissent leurs actions en ayant une connaissance parfaite de toute l’histoire. Dans la deuxième partie, on étudie des jeux de durée fini où le joueur protagoniste a zéro information. C’est-à-dire qu’il ne reçoit aucune information sur le déroulement du jeu, par conséquent sa stratégie est un mot fini sur l’ensemble des actions. Un automates probabiliste peut être considéré comme un tel jeu qui a un seul joueur. Tout d’abord, on compare deux classes d’automates probabilistes pour lesquelles le problème de valeur 1 est décidable: les automates leaktight et les automates simples. On prouve que la classe des automates simples est un sous-ensemble strict de la classe des automates leaktight. Puis, on considère des jeux semi-aveugles, qui sont des jeux à deux joueurs où le maximiseur a zéro information, et le minimiseur est parfaitement informé. On définit la classe des jeux semi-aveugles leaktight et on montre que le problème d’accessibilité maxmin est décidable sur cette classe. / We consider stochastic games that are played on finite graphs. The subject of the first part are two-player stochastic games with perfect information. In such games the two players take turns choosing actions from a finite set, for an infinite duration, resulting in an infinite play. The objective of the game is given by a Borel-measurable and bounded payoff function that maps infinite plays to real numbers. The first player wants to maximize the expected payoff, and the second player has the opposite objective, that of minimizing the expected payoff. We prove that if the payoff function is both shift-invariant and submixing then the game is half-positional. This means that the first player has an optimal strategy that is at the same time pure and memoryless. Both players have perfect information, so the actions are chosen based on the whole history. In the second part we study finite-duration games where the protagonist player has zero information. That is, he gets no feedback from the game and consequently his strategy is a finite word over the set of actions. Probabilistic finite automata can be seen as an example of such a game that has only a single player. First we compare two classes of probabilistic automata: leaktight automata and simple automata, for which the value 1 problem is known to be decidable. We prove that simple automata are a strict subset of leaktight automata. Then we consider half-blind games, which are two player games where the maximizer has zero information and the minimizer is perfectly informed. We define the class of leaktight half-blind games and prove that it has a decidable maxmin reachability problem.

The topic of this paper is the determinization problem of ω-automata under the transition-based Emerson-Lei acceptance (called TELA), which generalizes all standard acceptance conditions and is defined using positive Boolean formulas. Such automata can be determinized by first constructing an equivalent generalized Büchi automaton (GBA), which is later determinized. The problem of constructing an equivalent GBA is considered in detail, and three new approaches of solving it are proposed. Furthermore, a new determinization construction is introduced which determinizes several GBA separately and combines them using a product construction. An experimental evaluation shows that the product approach is competitive when compared with state-of-the-art determinization procedures. The second part of the paper studies limit-determinization of TELA and we show that this can be done with a single-exponential blow-up, in contrast to the known double-exponential lower-bound for determinization. Finally, one version of the limit-determinization procedure yields good-for-MDP automata which can be used for quantitative probabilistic model checking.

Pushdown systems equip a finite state system with an unbounded stack memory, and are thus infinite state. By recording the call history on the stack, these systems provide a natural model for recursive procedure calls. Model-checking for pushdown systems has been well-studied. Tools implementing pushdown model-checking (e.g. Moped) are an essential back-end component of high-profile software model checkers such as SLAM, Blast and Terminator. Higher-order pushdown systems define a more complex memory structure: a higher-order stack is a stack of lower-order stacks. These systems form a robust hierarchy closely related to the Caucal hierarchy and higher-order recursion schemes. This latter connection demonstrates their importance as models for programs with higher-order functions. We study the global model-checking problem for (higher-order) pushdown systems. In particular, we present a new algorithm for computing the winning regions of a parity game played over an order-1 pushdown system. We then show how to compute the winning regions of two-player reachability games over order-n pushdown systems. These algorithms extend the saturation methods of Bouajjani, Esparza and Maler for order-1 pushdown systems, and Bouajjani and Meyer for higher-order pushdown systems with a single control state. These techniques begin with an automaton recognising (higher-order) stacks, and iteratively add new transitions until the automaton becomes saturated. The reachability result, presented at FoSSaCS 2007 and in the LMCS journal, is the main contribution of the thesis. We break the saturation paradigm by adding new states to the automaton during the iteration. We identify the fixed points required for termination by tracking the updates that are applied, rather than by observing the transition structure. We give a number of applications of this result to LTL model-checking, branching-time model-checking, non-emptiness of higher-order pushdown automata and Büchi games. Our second major contribution is the first application of the saturation technique to parity games. We begin with a mu-calculus characterisation of the winning region. This formula alternates greatest and least fixed point operators over a kind of reachability formula. Hence, we can use a version of our reachability algorithm, and modifications of the Büchi techniques, to compute the required result. The main advantages of this approach compared to existing techniques due to Cachat, Serre and Vardi et al. are that it is direct and that it is not immediately exponential in the number of control states, although the worst-case complexity remains the same.

This thesis reports on new music technology research which investigates the use of cellular automata (CA) for the digital synthesis of dynamic sounds. The research addresses the problem of the sound design limitations of synthesis techniques based on CA. These limitations fundamentally stem from the unpredictable and autonomous nature of these computational models. Therefore, the aim of this thesis is to develop a sound synthesis technique based on CA capable of allowing a sound design process. A critical analysis of previous research in this area will be presented in order to justify that this problem has not been previously solved. Also, it will be discussed why this problem is worthwhile to solve. In order to achieve such aim, a novel approach is proposed which considers the output of CA as digital signals and uses DSP procedures to analyse them. This approach opens a large variety of possibilities for better understanding the self-organization process of CA with a view to identifying not only mapping possibilities for making the synthesis of sounds possible, but also control possibilities which enable a sound design process. As a result of this approach, this thesis presents a technique called Histogram Mapping Synthesis (HMS), which is based on the statistical analysis of CA evolutions by histogram measurements. HMS will be studied with four different automatons, and a considerable number of control mechanisms will be presented. These will show that HMS enables a reasonable sound design process. With these control mechanisms it is possible to design and produce in a predictable and controllable manner a variety of timbres. Some of these timbres are imitations of sounds produced by acoustic means and others are novel. All the sounds obtained present dynamic features and many of them, including some of those that are novel, retain important characteristics of sounds produced by acoustic means.

Formal verification techniques are growing increasingly vital for the development of safety-critical software and hardware in practice. Techniques such as requirements-based design and model checking for system verification have been successfully used to verify systems for air traffic control, airplane separation assurance, autopilots, CPU logic designs, life-support, medical equipment, and other functions that ensure human safety. Formal behavioral specifications written early in the system-design process and communicated across all design phases increase the efficiency, consistency, and quality of the system under development. We argue that to prevent introducing design or verification errors, it is crucial to test specifications for satisfiability. We advocate for the adaptation of a new sanity check via satisfiability checking for property assurance. Our focus here is on specifications expressed in Linear Temporal Logic (LTL). We demonstrate that LTL satisfiability checking reduces to model checking and satisfiability checking for the specification, its complement, and a conjunction of all properties should be performed as a first step to LTL model checking. We report on an experimental investigation of LTL satisfiability checking. We introduce a large set of rigorous benchmarks to enable objective evaluation of LTL-to-automaton algorithms in terms of scalability, performance, correctness, and size of the automata produced. For explicit model checking, we use the Spin model checker; we tested all LTL-to-explicit automaton translation tools that were publicly available when we conducted our study. For symbolic model checking, we use CadenceSMV, NuSMV, and SAL-SMC for both LTL-to-symbolic automaton translation and to perform the satisfiability check. Our experiments result in two major findings. First, scalability, correctness, and other debilitating performance issues afflict most LTL translation tools. Second, for LTL satisfiability checking, the symbolic approach is clearly superior to the explicit approach. Ironically, the explicit approach to LTL-to-automata had been heavily studied while only one algorithm existed for LTL-to-symbolic automata. Since 1994, there had been essentially no new progress in encoding symbolic automata for BDD-based analysis. Therefore, we introduce a set of 30 symbolic automata encodings. The set consists of novel combinations of existing constructs, such as different LTL formula normal forms, with a novel transition-labeled symbolic automaton form, a new way to encode transitions, and new BDD variable orders based on algorithms for tree decomposition of graphs. An extensive set of experiments demonstrates that these encodings translate to significant, sometimes exponential, improvement over the current standard encoding for symbolic LTL satisfiability checking. Building upon these ideas, we return to the explicit automata domain and focus on the most common type of specifications used in industrial practice: safety properties. We show that we can exploit the inherent determinism of safety properties to create a set of 26 explicit automata encodings comprised of novel aspects including: state numbers versus state labels versus a state look-up table, finite versus infinite acceptance conditions, forward-looking versus backward-looking transition encodings, assignment-based versus BDD-based alphabet representation, state and transition minimization, edge abbreviation, trap-state elimination, and determinization either on-the-fly or up-front using the subset construction. We conduct an extensive experimental evaluation and identify an encoding that offers the best performance in explicit LTL model checking time and is constantly faster than the previous best explicit automaton encoding algorithm.

Tree automata, and their applications to verification from the common thread of this thesis In the first part, we definie a complete model-cheking framework.[...] The second part focus on an important aspect of the automata involved: constraints.[...] Finaly, we also study the very different variety of tree-walking automata which have tight connections with navigational languages on semi-structured documents.

L'apprentissage de langages réguliers est un sous-ensemble de l'apprentissage automatique qui s'est révélé utile dans de nombreux domaines tels que l'intelli-gence artificielle, les réseaux de neurones, l'exploration de données, la vérification, etc. De plus, l'intérêt dans les langages définis sur des alphabets infinis ou de grande taille est croissant au fil des années. Même si plusierurs propriétés et théories se généralisent à partir du cas fini, l'apprentissage de tels langages est une tâche difficile.En effet, dans ce contexte, l'application naïve des algorithmes d'apprentissage traditionnel n'est pas possible.Dans cette thèse, nous présentons un schéma algorithmique général pour l'ap-prentissage de langages définis sur des alphabets infinis ou de grande taille, comme par exemple des sous-ensembles bornés de N or R ou des vecteurs booléens de grandes dimensions. Nous nous restreignons aux classes de langages qui sont acceptés par des automates déterministes symboliques utilisant des prédicats pour définir les transitions, construisant ainsi une partition finie de l'alphabet pour chaque état.Notre algorithme d'apprentissage, qui est une adaptation du L* d'Angluin, combine l'apprentissage classique d'un automate par la caractérisation de ses états, avec l'apprentissage de prédicats statiques définissant les partitions de l'alphabet. Nous utilisons l'apprentissage incrémental avec la propriété que deux types de requêtes fournissent une information suffisante sur le langage cible. Les requêtes du premier type sont les requêtes d'adhésions, qui permettent de savoir si un mot proposé appartient ou non au langage cible. Les requêtes du second type sont les requêtes d'équivalence, qui vérifient si un automate proposé accepte le langage cible; dans le cas contraire, un contre-exemple est renvoyé.Nous étudions l'apprentissage de langages définis sur des alphabets infinis ou de grande tailles dans un cadre théorique et général, mais notre objectif est de proposer des solutions concrètes pour un certain nombre de cas particuliers. Ensuite, nous nous intéressons aux deux principaux aspects du problème. Dans un premier temps, nous supposerons que les requêtes d'équivalence renvoient toujours un contre-exemple minimal pour un ordre de longueur-lexicographique quand l'automate proposé est incorrect. Puis dans un second temps, nous relâchons cette hypothèse forte d'un oracle d'équivalence, et nous la remplaçons avec une hypothèse plus réaliste où l'équivalence est approchée par un test sur les requêtes qui utilisent un échantillonnage sur l'ensemble des mots. Dans ce dernier cas, ce type de requêtes ne garantit pas l'obtention de contre-exemples, et par conséquent de contre-exemples minimaux. Nous obtenons alors une notion plus faible d'apprent-issage PAC (Probably Approximately Correct), permettant l'apprentissage d'une approximation du langage cible.Tout les algorithmes ont été implémentés, et leurs performances, en terme de construction d'automate et de taille d'alphabet, ont été évaluées empiriquement. / Learning regular languages is a branch of machine learning, which has been proved useful in many areas, including artificial intelligence, neural networks, data mining, verification, etc. On the other hand, interest in languages defined over large and infinite alphabets has increased in recent years. Although many theories and properties generalize well from the finite case, learning such languages is not an easy task. As the existing methods for learning regular languages depends on the size of the alphabet, a straightforward generalization in this context is not possible.In this thesis, we present a generic algorithmic scheme that can be used for learning languages defined over large or infinite alphabets, such as bounded subsets of N or R or Boolean vectors of high dimensions. We restrict ourselves to the class of languages accepted by deterministic symbolic automata that use predicates to label transitions, forming a finite partition of the alphabet for every state.Our learning algorithm, an adaptation of Angluin's L*, combines standard automaton learning by state characterization, with the learning of the static predicates that define the alphabet partitions. We use the online learning scheme, where two types of queries provide the necessary information about the target language. The first type, membership queries, answer whether a given word belongs or not to the target. The second, equivalence queries, check whether a conjectured automaton accepts the target language, a counter-example is provided otherwise.We study language learning over large or infinite alphabets within a general framework but our aim is to provide solutions for particular concrete instances. For this, we focus on the two main aspects of the problem. Initially, we assume that equivalence queries always provide a counter-example which is minimal in the length-lexicographic order when the conjecture automaton is incorrect. Then, we drop this ``strong'' equivalence oracle and replace it by a more realistic assumption, where equivalence is approximated by testing queries, which use sampling on the set of words. Such queries are not guaranteed to find counter-examples and certainly not minimal ones. In this case, we obtain the weaker notion of PAC (probably approximately correct) learnability and learn an approximation of the target language. All proposed algorithms have been implemented and their performance, as a function of automaton and alphabet size, has been empirically evaluated.

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.