This thesis defines and studies two new types of automata, cooperating distributed pushdown automata systems (CDPDAS) and parallel communicating pushdown automata systems (PCPDAS).  CDPDAS and PCPDAS adapt the main concept of cooperating distributed grammar systems (CDGS) and parallel communicating automata systems (PCPDAS), respectively.  CDPDAS are proven to have the same power as PDA and this thesis further explores the reason why CDPDAS do not increase power while CDGS do and introduces an automata system inspired by CDPDAS that does increase the power.  PCGS have similar power as CDGS, but PCPDAS are equvalent with TM, which is proven by creating a communication protocol to access a second stack.

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.

A problem in computer security is identification of attack signatures in network packets. An attack signature is a pattern of bits that characterizes a particular attack. Because there are many kinds of attacks, there are potentially many attack signatures. Furthermore, attackers may seek to avoid detection by altering the attack mechanism so that the bit pattern presented differs from the known signature. Thus, recognizing attack signatures is a problem in approximate string matching. The time to perform an approximate string match depends upon the length of the string and the number of patterns. For constant string length, the time to matchnpatterns is approximatelyO(n); the time increases approximately linearly as the number of patterns increases. A binary cellular automaton is a discrete, deterministic system of cells in which each cell can have one of two values. Cellular automata have the property that the next state of each cell can be evaluated independently of the others. If there is a processing element for each cell, the next states of all cells in a cellular automaton can be computed simultaneously. Because there is no programming paradigm for cellular automata, cellular automata to perform specific functions are createdad hocby hand or discovered using search methods such as genetic algorithms. This research has identified, through evolution by genetic algorithm, cellular automata that can perform approximate string matching for more than one pattern while operating in constant time with respect to the number of patterns, and in the presence of noise. Patterns were recognized by using the bits of a network packet payload as the initial state of a cellular automaton. After a predetermined number of cycles, the ones density of the cellular automaton was computed. Packets for which the ones density was below an experimentally determined threshold were identified as target packets. Six different cellular automaton rules were tested against a corpus of 7.2 million TCP packets in the IDEval data set. No rule produced false negative results, and false positive results were acceptably low.

<p>Regular inference is a research direction in machine learning. The goal of regular inference is to construct a representation of a regular language in the form of deterministic finite automaton (DFA) based on the set of positive and negative examples. DFAs take strings of symbols (words) as input, and produce a binary classification as output, indicating whether the word belongs to the language or not. There are two types of learning algorithms for DFAs: passive and active learning algorithms. In passive learning, the set of positive and negative examples is given and not chosen by inference algorithm. In contrast, in active learning, the learning algorithm chooses examples from which a model is constructed.</p><p>Active learning was introduced in 1987 by Dana Angluin. She presented the L* algorithm for learning DFAs by asking membership and equivalence queries to a teacher who knows the regular language accepted by DFA to be learned. A membership query checks whether a word belongs to the language or not. An equivalence query checks whether a hypothesized model is equivalent to the DFA to be learned.The L* algorithm has been found to be useful in different areas, including black box checking, compositional verification and integration testing. There are also other algorithms similar to L* for regular inference. However, the learning of timed systems has not been studied before. This thesis presents algorithms for learning timed systems in an active learning framework.</p><p>As a model of timed system we choose event-recording automata (ERAs), a determinizable subclass of the widely used timed automata. The advantages of ERA in comparison with timed automata, is that it is known priori the set of clocks of an ERA and when clocks are reset. The contribution of this thesis is four algorithms for learning deterministic event-recording automaton (DERA). Two algorithms learn a subclass of DERA, called event-deterministic ERA (EDERA) and two algorithms learn general DERA.</p><p>The problem with DERAs that they do not have canonical form. Therefore we focus on subclass of DERAs that have canonical representation, EDERA, and apply the L* algorithm to learn EDERAs. The L* algorithm in timed setting requires a procedure that learns clock guards of DERAs. This approach constructs EDERAs which are exponentially bigger than automaton to be learned. Another procedure can be used to lean smaller EDERAs, but it requires to solve NP-hard problem.</p><p>We also use the L* algorithm to learn general DERA. One drawback of this approach that inferred DERAs have a form of region graph and there is blow-up in the number of transitions. Therefore we introduce an algorithm for learning DERA which uses a new data structure for organising results of queries, called a timed decision tree, and avoids region graph construction. Theoretically this algorithm can construct bigger DERA than the L* algorithm, but in the average case we expect better performance.</p>

Real-time Embedded Systems (RTESs) have an increasing role in controlling society infrastructures that we use on a day-to-day basis. RTES behaviour is not based solely on the interactions it might have with its surrounding environment, but also on the timing requirements it induces. As a result, ensuring that an RTES behaves correctly is non-trivial, especially after adding time as a new dimension to the complexity of the testing process. This research addresses the problem of testing RTESs from Timed Automata (TA) specification by the following. First, a new Priority-based Approach (PA) for testing RTES modelled formally as UPPAAL timed automata (TA variant) is introduced. Test cases generated according to a proposed timed adequacy criterion (clock region coverage) are divided into three sets of priorities, namely boundary, out-boundary and in-boundary. The selection of which set is most appropriate for a System Under Test (SUT) can be decided by the tester according to the system type, time specified for the testing process and its budget. Second, PA is validated in comparison with four well-known timed testing approaches based on TA using Specification Mutation Analysis (SMA). To enable the validation, a set of timed and functional mutation operators based on TA is introduced. Three case studies are used to run SMA. The effectiveness of timed testing approaches are determined and contrasted according to the mutation score which shows that our PA achieves high mutation adequacy score compared with others. Third, to enhance the applicability of PA, a new testing tool (GeTeX) that deploys PA is introduced. In its current version, GeTeX supports Control Area Network (CAN) applications. GeTeX is validated by developing a prototype for that purpose. Using GeTeX, PA is also empirically validated in comparison with some TA testing approaches using a complete industrial-strength test bed. The assessment is based on fault coverage, structural coverage, the length of generated test cases and a proposed assessment factor. The assessment is based on fault coverage, structural coverage, the length of generated test cases and a proposed assessment factor. The assessment results confirmed the superiority of PA over the other test approaches. The overall assessment factor showed that structural and fault coverage scores of PA with respect to the length of its tests were better than the others proving the applicability of PA. Finally, an Analytical Hierarchy Process (AHP) decision-making framework for our PA is developed. The framework can provide testers with a systematic approach by which they can prioritise the available PA test sets that best fulfils their testing requirements. The AHP framework developed is based on the data collected heuristically from the test bed and data collected by interviewing testing experts. The framework is then validated using two testing scenarios. The decision outcomes of the AHP framework were significantly correlated to those of testing experts which demonstrated the soundness and validity of the framework.

The focus of this thesis is finitely generated subgroups of the automorphism group of an infinite spherically homogeneous rooted tree (regular or irregular). The first chapter introduces the topic and outlines the main results. The second chapter provides definitions of the terminology used, and also some preliminary results. The third chapter introduces a group that appears to be a promising candidate for a finitely generated group of infinite upper rank with finite upper $p$-rank for all primes $p$. It goes on to demonstrate that in fact this group has infinite upper $p$-rank for all primes $p$. As a by-product of this construction, we obtain a finitely generated branch group with quotients that are virtually-(free abelian of rank $n$) for arbitrarily large $n$. The fourth chapter gives a complete classification of ternary automata with $C_2$-action at the root, and a partial classification of ternary automata with $C_3$-action at the root. The concept of a `windmill automaton' is introduced in this chapter, and a complete classification of binary windmill automata is given. The fifth chapter contains a detailed study of the non-abelian ternary automata with $C_3$-action at the root. It also contains some conjectures about possible isomorphisms between these groups.

Finite-state automata are a central computational model in computer science, with numerous and diverse applications. In one such application, viz. model-checking, automata over infinite words play a central rˆole. In this thesis, we concentrate on B¨uchi automata (BA), which are arguably the simplest finite-state model recognizing languages of infinite words. Two algorithmic problems are paramount in the theory of automata: language inclusion and automata minimization. They are both PSPACE-complete, thus under standard complexity-theoretic assumptions no deterministic algorithm with worst case polynomial time can be expected. In this thesis, we develop techniques to tackle these problems. In automata minimization, one seeks the smallest automaton recognizing a given language (“small” means with few states). Despite PSPACE-hardness of minimization, the size of an automaton can often be reduced substantially by means of quotienting. In quotienting, states deemed equivalent according to a given equivalence are merged together; if this merging operation preserves the language, then the equivalence is said to be Good for Quotienting (GFQ). In general, quotienting cannot achieve exact minimization, but, in practice, it can still offer a very good reduction in size. The central topic of this thesis is the design of GFQ equivalences for B¨uchi automata. A particularly successful approach to the design of GFQ equivalences is based on simulation relations. Simulation relations are a powerful tool to compare the local behavior of automata. The main contribution of this thesis is to generalize simulations, by relaxing locality in three perpendicular ways: by fixing the input word in advance (fixed-word simulations, Ch. 3), by allowing jumps (jumping simulations, Ch. 4), and by using multiple pebbles (multipebble simulations for alternating BA, Ch. 5). In each case, we show that our generalized simulations induce GFQ equivalences. For fixed-word simulation, we argue that it is the coarsest GFQ simulation implying language inclusion, by showing that it subsumes a natural hierarchy of GFQ multipebble simulations. From a theoretical perspective, our study significantly extends the theory of simulations for BA; relaxing locality is a general principle, and it may find useful applications outside automata theory. From a practical perspective, we obtain GFQ equivalences coarser than previously possible. This yields smaller quotient automata, which is beneficial in applications. Finally, we show how simulation relations have recently been applied to significantly optimize exact (exponential) language inclusion algorithms (Ch. 6), thus extending their practical applicability.

Phase change devices in both optical and electrical formats have been subject of intense research since their discovery by Ovshinsky in the early 1960’s. They have revolutionized the technology of optical data storage and have very recently been adopted for non-volatile semiconductor memories. Their great success relies on their remarkable properties enabling high-speed, low power consumption and stable retention. Nevertheless, their full potential is still yet to be realized. Operations in electrical phase change devices rely on the large resistivity contrast between the crystalline (low resistance) and amorphous (high resistance) structures. The underlying mechanisms of phase transformations and the relation between structural and electrical properties in phase change materials are quite complex and need to be understood more deeply. For this purpose, we compare different approaches to mathematical modelling that have been suggested to realistically simulate the crystallization and amorphization of phase change materials. In this thesis the recently introduced Gillespie Cellular Automata (GCA) approach is used to obtain direct simulation of the structural phases and the electrical states of phase change materials and devices. The GCA approach is a powerful technique to understand the nanostructure evolution during the crystallization (SET) and amorphization (RESET) processes in phase change devices over very wide length scales. Using this approach, a detailed study of the electrical properties and nanostructure dynamics during SET and RESET processes in a PCRAM cell is presented. Besides the possibility of binary storage in phase change memory devices, there is a wider and far-reaching potential for using them as the basis for new forms of arithmetic and cognitive computing. The origin of such potential lies in a previously under-explored property, namely accumulation which has the potential to implement basic arithmetic computations. We exploit and explore this accumulative property in films and devices. Furthermore, we also show that the same accumulation property can be used to mimic a simple integrate and fire neuron. Thus by combining both a phase change cell operating in the accumulative regime for the neural body and a phase change cell in the multilevel regime for the synaptic weighting an artificial neuromorphic system can be obtained. This may open a new route for the realization of phase change based cognitive computers. This thesis also examines the relaxation oscillations observed under suitable bias conditions in phase change devices. The results presented are performed through a circuit analysis in addition with a generation and recombination mechanism driven by the electric field and carrier densities. To correctly model the oscillations we show that it is necessary to include a parasitic inductance. Related to the electrical states of phase change materials and devices is the threshold switching of the amorphous phase at high electric fields and recent work has suggested that such threshold switching is the result of field-induced nucleation. An electric field induced nucleation mechanism is incorporated into the GCA approach by adding electric field dependence to the free energy of the system. Using results for a continuous phase change thin films and PCRAM devices we show that a purely electronic explanation of threshold switching, rather than field-induced nucleation, provides threshold fields closer to experimentally measured values.

Pitting corrosion is a form of highly localized corrosion that can lead to crack and failure of a structure. Study on pitting corrosion is necessary in order to predict and prevent the risk of failure of structure susceptible to corrosion. In this thesis, a combination of Cellular Automata (CA) and Boundary Element Method (BEM) was developed to simulate pitting corrosion growth under certain environment. It is assumed that pitting corrosion can be simplified to electrochemical corrosion cell. The distribution of potential around this corrosion cell can then be simulated by BEM. This distribution potential represents cathodic and anodic reactions around the corrosion cell. A CA model was developed that uses transition rules reflecting mechanism of pitting corrosion. The CA model has two types of cell states, one reflecting BEM simulation results and the other reflecting the status of corrosion cell (anode, cathode, and passive metal’s surface). For every CA iteration, the CA decides the state of the corrosion cells (the location and size of anode, cathode) while BEM simulate the level of electrochemical activity at discrete location on the surface (represented by potential distribution). In order to demonstrate the methodology, a simple case of rectangular corrosion cell with varied dimensions and under different polarization functions is considered. Results show certain shapes tend to grow at certain type environment and these pits are comparable to commonly observed pit shapes. In addition, stress analysis was carried out to investigate the severity of corrosion pits of varying shapes and sizes. Results show that certain pits induced highly varying stress concentration as it grows over time, while others have more steady increase of stress concentration.

Biological systems exhibit complex behaviors through coordinated responses of individual biological components. With the advent of genome-scale techniques, one focus has been to develop methods to model interactions between components to accurately describe intact system function. Mathematical modeling techniques such as constraint-based modeling, agent-based modeling, cellular automata (CA) modeling and differential equation modeling are employed as computational tools to study biological phenomenon. We have shown that cellular automata simulations can be used as a computational tool for 12 predicting the dynamics of biological systems with stochastic behavior. The basic premise for the research was the observations made during a study of biologically important feed-forward motifs where CA simulations were compared with differential equation simulations. It was shown for classes of structural motifs with feed-forward architecture that network topology affects the overall rate of a process in a quantitatively predictable manner. The study which comprised of CA simulations compared with differential equation modeling show reasonable agreement in the predictability of system dynamics, which provided enough support to model biological systems at cellular level to observe dynamic system evolution. The great promise shown by CA simulations to model biochemical systems was then employed to elucidate evolutionary clues as to why biological networks show preference for certain types of motifs and preserve them with higher frequency during evolution. It was followed by modeling apoptotic networks to shed light on the efficacy of inhibitors and to model cellulose hydrolysis to evaluate efficiency of different enzyme systems used by cellulytic bacteria.