Les automates d'arbres et leurs applications à la vérification forment le tronc commun de cette thèse. Dans la première parie, nous définissons une plate forme de model-checking complète [...] La seconde partie se penche sur un aspect important des automates que nous utilisons: leur contraintes [...] Finalement, nous étudions également les automates d'arbres cheminants [...] Nous améliorons leur conversion en automates parallèles, et nous développons une procédure de semi décision de leur vacuité, à la fois efficace et précise / 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.

To the best of our knowledge, the only available implementations of FA-based string recognizers are the so-called conventional table-driven algorithm and, of course, its hardcoded counterpart suggested by Thompson, Penello, and DeRemer in 1967, 1986, and 2004 respectively. However, our early experiments have shown that the performance of both implementations is hampered by the random access nature of the automaton’s transition table in the case of table-driven, and also the random access nature of the directly executable instructions that make up each hardcoded state. Moreover, the problem of memory load and instruction load are also performance bottlenecks of these algorithms, since, as the automaton size grows, more space in memory is required to hold data/instructions relevant to the states. This thesis exploits the notion of cache optimization (that requires good data or instructions organization) in investigating various enhancements of both table-driven and hardcoding. Functions have been used to formally define the denotational semantics of string recognizers. These functions rely on various so-called strategy variables that are integrated into the formal definition of each recognizer. By appropriately selecting these variables, the conventional algorithms may be described, without loss of generality. By specializing these strategy variables, the new and enhanced recognizers can be denotationally described, and resulting algorithms can then be implemented. We first introduce the so-called Dynamic State Allocation (DSA) strategy regarded as a sort of Just-In-time (JIT) implementation of FA-based string recognizers whereby a predefined portion of the memory is reserved for acceptance testing. Then follows the State pre-Ordering (SpO) strategy that assumes some prior knowledge on the order in which states would be visited. In this case, acceptance testing takes place once each state have been allocated to its new position in memory. The last strategy referred to as the Allocated Virtual Caching (AVC) strategy is based on the premise that a portion of the memory originally occupied by the automaton’s states is virtually used as a sort of cache memory in which acceptance testing takes place, enabling therefore, the exploitation of the various performance enhancement notions on which hardware cache memory relies. It is shown that the algorithms can be classified in a taxonomy tree which is further mapped into a class-diagram that represents the design of a toolkit for FA-based string recognition. Also given in the thesis are empirical results that indicate that the algorithms suggested can, in general, outperform their conventional counterparts when recognizing large and appropriately chosen input strings. / Thesis (PhD (Computer Science))--University of Pretoria, 2007. / Computer Science / PhD / unrestricted

Apart from contributing to Computer Science, this research also contributes to Bioinformatics, a subset of the subject discipline Computational Biology. The main focus of this dissertation is the development of a data-analytical and theoretical algorithm to contribute to the analysis of DNA, and in particular, to detect microsatellites. Microsatellites, considered in the context of this dissertation, refer to consecutive patterns contained by genomic sequences. A perfect tandem repeat is defined as a string of nucleotides which is repeated at least twice in a sequence. An approximate tandem repeat is a string of nucleotides repeated consecutively at least twice, with small differences between the instances. The research presented in this dissertation was inspired by molecular biologists who were discovered to be visually scanning genetic sequences in search of short approximate tandem repeats or so called microsatellites. The aim of this dissertation is to present three algorithms that search for short approximate tandem repeats. The algorithms comprise the implementation of finite automata. Thus the hypothesis posed is as follows: Finite automata can detect microsatellites effectively in DNA. "Effectively" includes the ability to fine-tune the detection process so that redundant data is avoided, and relevant data is not missed during search. In order to verify whether the hypothesis holds, three theoretical related algorithms have been proposed based on theorems from finite automaton theory. They are generically referred to as the FireìSat algorithms. These algorithms have been implemented, and the performance of FireìSat2 has been investigated and compared to other software packages. From the results obtained, it is clear that the performance of these algorithms differ in terms of attributes such as speed, memory consumption and extensibility. In respect of speed performance, FireìSat outperformed rival software packages. It will be seen that the FireìSat algorithms have several parameters that can be used to tune their search. It should be emphasized that these parameters have been devised in consultation with the intended user community, in order to enhance the usability of the software. It was found that the parameters of FireìSat can be set to detect more tandem repeats than rival software packages, but also tuned to limit the number of detected tandem repeats. Copyright / Dissertation (MSc)--University of Pretoria, 2010. / Computer Science / unrestricted

Les systèmes digitaux jouent un rôle croissant dans le bon fonctionnement de notre société.Au delà de la grande diversité de leur domaines d'utilisations, on confie aujourd'hui destâches importantes à des algorithmes. Déjà largement utilisés dans des domaines aussi délicatque le transport, la chirurgie ou l'économie, il est aujourd'hui de plus en plus question defaire de la place aux systèmes digitaux dans les domaines sociaux et politiques :vote électronique, algorithmes de sélection, profilage électoraldotsPour les tâches confiées à des algorithmes, la responsabilité est déplacées de l'exécutantvers les concepteurs, développeurs et testeurs de ces algorithmes. Il incombe aussi auxchercheurs qui étudient ces algorithmes de proposer des techniques de vérifications fiablequi pourront être utilisées à tous les niveaux : conception, développement et test.Les méthodes de vérifications formelles donnent des outils mathématiques pourprévenir des erreurs à chaque niveaux. Parmi elle, le diagnostic d'erreur consiste en lacréation d'un diagnostiqueur basé sur un modèle formel du système à vérifier.Le diagnostiqueur est exécuté en parallèle du système qu'il doit surveiller et prévientun contrôleur si il détecte un comportement dangereux du système.Pour les systèmes modélisés par des automates temporisés, il n'est pas toujours possiblede construire un diagnostiqueur sous la forme d'un autre automate temporisé. En effetles automates temporisés, introduits par cite{AD94} dans les années 90 et largementétudiés et utilisés depuis pour modéliser des systèmes avec contraintes temporelles,ne sont pas déterminisable. Une machine plus puissante qu'un automate temporisé peutcependant être utilisée pour construire le diagnostiqueur d'un automate temporisé commele montre cite{Tripakis02}. L'aboutissement de ce travail de thèse est la constructionautomatique d'un diagnostiqueur pour les automates temporisés à une horloge.Ce diagnostiqueur, dans le même esprit que celui de cite{Tripakis02}, est une machineplus puissante qu'un automate temporisé. La partie~I du manuscrit introduit un cadreformel pour ce type de machine et plus généralement pour la modélisation et ladéterminisation de systèmes quantitatifs. Y est introduit le modèle des automates surstructures temporisés, qui apporte un nouveau point de vue sur la manière de modéliserles systèmes avec variables quantitatives. La partie~II étudie le problème de ladéterminisation des automates sur structures temporises, et plus spécifiquement celuides automates temporisés qui peuvent se traduire dans ce cadre nouveau cadre formel.La partie~III montre comment utiliser les automates sur structure temporisés pourconstruire de manière générique un diagnostiqueur pour les automate temporisés à unehorloge. Cette technique est implémentée dans un outils, DOTA , et comparée à lamachine construite par cite{Tripakis02}. / Digital system are now part of our society. They are used in a wide range of domainsand in particular they have to handle delicate tasks. Already used in domainssuch as transportation, surgery or economy, we speak now of using digital systemsfor social or political matters : electronic vote, selection algorithms, electoralprofilingdots For task handled by algorithm, the responsibility is moved from theexecutioner to the designer, developer and tester of those algorithms. It is alsothe responsibility of computer scientists who study those algorithms to proposereliable techniques of verification which will be applicable in the design, thedevelopment or the testing phase. Formal verification methods provide mathematicaltools to prevent executions error in all phases. Among them, fault-diagnosis consiston the construction of a diagnoser based on a formal model of the system we aim tocheck. The diagnoser runs in parallel with the real system and emit a warning anytime it detect a dangerous behavior. For systems modeled by timed automata, it isnot always possible to construct a timed automaton to diagnose it. Indeed timed automata,introduce in the nineties by cite{AD94} and widely studied and used since to modeltimed systems, are not determinizable. A machine, more powerful than a timed automaton,can still be used to construct the diagnoser of a timed automaton as it is done incite{Tripakis02}. This thesis work aim at constructing a diagnoser for any one-clocktimed automata. This diagnoser is constructed with the help of a machine more powerfulthan timed automata, following the idea of cite{Tripakis02}. Part~I of this thesisintroduce a formal framework for the modeling of quantitative systems and the study oftheir determinization. In this framework we introduce automata on timed structures,the model used to construct the diagnoser. Part~II study the determinization problemof automata on timed structures, and particularly the one of timed automatadeterminization in this framework. Part~III illustrate how automata on timed structurescan be used to construct in a generic way a diagnoser for one clock timed automata.This technique is implemented in a tool, DOTA , and is compared to the technique usedin cite{Tripakis02}.

The focus of this thesis is the fast network anomaly detection based on automata learning. It describes and compares several chosen automata learning algorithms including their adaptation for the learning of network characteristics. In this work, various network anomaly detection methods based on learned automata are proposed which can detect sequential as well as statistical anomalies in target communication. For this purpose, they utilize automata's mechanisms, their transformations, and statistical analysis. Proposed detection methods were implemented and evaluated using network traffic of the protocol IEC 60870-5-104 which is commonly used in industrial control systems.

Táto práca sa zaoberá redukciou veľkosti tzv. čítačových automatov. Čítačové automaty rozširujú klasické konečné automaty o čítače s obmedzeným rozsahom hodnôt. Umožňujú tým efektívne spracovať napr. regulárne výrazy s opakovaním: a{5,10}. V tejto práci sa zaoberáme reláciou simulácie v čítačových automatoch, pomocou ktorej sme schopní zredukovať ich veľkosť. Opierame sa pritom o klasickú simuláciu v konečných automatoch, ktorú netriviálnym spôsobom rozširujeme na čítačové automaty. Kľúčovým rozdielom je nutnosť simulovať okrem stavov taktiež čítače. Za týmto účelom zavádzame nový koncept parametrizovanej relácie simulácie, a navrhujeme metódy výpočtu tejto relácie a redukcie veľkosti čítačových automatov pomocou nej. Navrhnuté metódy sú tiež implementované a je vyhodnotená ich efektivita.

As the number of vehicles on our roads increases, the problems related to this phenomenon emerge more dramatically. These problems include car accidents, congestions and CO2 emissions production, increasing CO2 concentrations in the atmosphere. In order to minimize these impacts and to use the road infrastructure eff ectively, the use of traffic simulators can come in handy. Thanks to these tools, it is possible to evaluate the evolution of a traffic flow with various initial states of the simulation and thus know what to do and how to react in different states of the real-world traffic situations. This thesis deals with acceleration of microscopic urban traffic simulation using OpenCL. Supposing it is necessary to simulate a large network traffic, the need to accelerate the simulation is necessary. For this purpose, it is possible, for example, to use the graphics processing units (GPUs) and the technique of GPGPU for general purpose computations, which is used in this work. The results show that the performance gains of GPUs are significant compared to a parallel implementation on CPU.

Current computing hardware supports parallelism at various levels. Conventional programming techniques, however, do not utilise efficiently this growing resource. This thesis seeks a better fit between software and current hardware while following a hardware-agnostic software development approach. This allows the programmer to remain focussed on the problem domain. The thesis proposes process-based problem decomposition as a natural way to structure a concurrent implementation that may also improve multicore utilisation and, consequently, run-time performance. The thesis presents four algorithms as case studies from the domain of string pattern matching and finite automata. Each case study is conducted in the following manner. The particular sequential algorithm is decomposed into a number of communicating concurrent processes. This decomposition is described in the process algebra CSP. Hoare's CSP was chosen as one of the best known process algebras, for its expressive power, conciseness, and overall simplicity. Once the CSP-based process description has brought ideas to a certain level of maturity, the description is translated into a process-based implementation. The Go programming language was used for the implementation as its concurrency features were inspired by CSP. The performance of the process-based implementation is then compared against its conventional sequential version (also provided in Go). The goal is not to achieve maximal performance, but to compare the run-time performance of an ``ordinary'' programming effort that focussed on a process-based solution over a conventional sequential implementation. Although some implementations did not perform as well as others, some did significantly outperform their sequential counterparts. The thesis thus provides prima facie evidence that a process-based decomposition approach is promising for achieving a better fit between software and current multicore hardware. / Thesis (PhD)--University of Pretoria, 2017. / Computer Science / PhD / Unrestricted

This thesis is submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy (Ph.D) in the FASTAR group of the Department of Computer Science, University of Pretoria, South Africa. I present a number of algorithms for constructing minimal acyclic deterministic finite automata (MADFAs), most of which I originally derived/designed or co-discovered. Being acyclic, such automata represent finite languages and have proven useful in applications such as spellchecking, virus-searching and text indexing. In many of those applications, the automata grow to billions of states, making them difficult to store without using various compression techniques — the most important of which is minimization. Results from the late 1950’s show that minimization yields a unique automaton (for a given language), and later results show that minimization of acyclic automata is possible in time linear in the number of states. These two results make for a rich area of algorithmics research; automata and algorithmics research are relatively old fields of computing science and the discovery/invention of new algorithms in the field is an exciting result. I present both incremental and nonincremental algorithms. With nonincremental techniques, the unminimized acyclic deterministic finite automaton (ADFA) is first constructed and then minimized. As mentioned above, the unminimized ADFA can be very large indeed — often even too large to fit within the virtual memory space of the computer. As a result, incremental techniques for minimization (i.e. the ADFA is minimized during its construction) become interesting. Incremental algorithms frequently have some overhead: if the unminimized ADFA fits easily within physical memory, it may still be faster to use nonincremental techniques. The presentation used in this thesis has a few unusual characteristics: <ul><li> Few other presentations follow a correctness-by-construction style for presenting and deriving algorithms. The presentations given here include correctness arguments or sketches thereof. </li><li> The presentation is taxonomic — emphasizing the similarities and differences between the algorithms at a fundamental level. </li><li> While it is possible to present these algorithms in a formal-language-theoretic setting, this thesis remains somewhat closer to the actual implementation issues. </li><li> In several chapters, new algorithms and interesting new variants of existing algorithms are presented. </li><li> It gives new presentations of many existing algorithms — all in a common format with common examples. </li><li> There are extensive links to the existing literature. </li></ul> / Thesis (PhD)--University of Pretoria, 2010. / Computer Science / unrestricted

We introduce the notion of nested distance desert automata as a joint generalization and further development of distance automata and desert automata. We show that limitedness of nested distance desert automata is PSPACE-complete. As an application, we show that it is decidable in 22O(n2) space whether the language accepted by an n-state non-deterministic automaton is of a star height less than a given integer h (concerning rational expressions with union, concatenation and iteration). We also show some decidability results for some substitution problems for recognizable languages.