One of today's most serious social, economical and environmental problems is traffic congestion. In addition to the financial cost of the problem, the number of traffic related injuries and casualties is very high. A recently considered approach to increase safety while reducing congestion and improving driving conditions is Automated Highway Systems (AHS). The AHS will evolve from the present highway system to an intelligent vehicle/highway system that will incorporate communication, vehicle control and traffic management techniques to provide safe, fast and more efficient surface transportation. A key factor in AHS deployment is intelligent vehicle control. While the technology to safely maneuver the vehicles exists, the problem of making intelligent decisions to improve a single vehicle's travel time and safety while optimizing the overall traffic flow is still a stumbling block. We propose an artificial intelligence technique called stochastic learning automata to design an intelligent vehicle path controller. Using the information obtained by on-board sensors and local communication modules, two automata are capable of learning the best possible (lateral and longitudinal) actions to avoid collisions. This learning method is capable of adapting to the automata environment resulting from unmodeled physical environment. Simulations for simultaneous lateral and longitudinal control of an autonomous vehicle provide encouraging results. Although the learning approach taken is capable of providing a safe decision, optimization of the overall traffic flow is also possible by studying the interaction of the vehicles. The design of the adaptive vehicle path planner based on local information is then carried onto the interaction of multiple intelligent vehicles. By analyzing the situations consisting of conflicting desired vehicle paths, we extend our design by additional decision structures. The analysis of the situations and the design of the additional structures are made possible by the study of the interacting reward-penalty mechanisms in individual vehicles. The definition of the physical environment of a vehicle as a series of discrete state transitions associated with a "stationary automata environment" is the key to this analysis and to the design of the intelligent vehicle path controller. This work was supported in part by the Center for Transportation Research and Virginia DOT under Smart Road project, by General Motors ITS Fellowship program, and by Naval Research Laboratory under grant no. N000114-93-1-G022. / Ph. D.

Recent advances in VLSI technology have stimulated research efforts in the area of highly reliable fault tolerant, general purpose computing systems, notably, parallel systems. An automatically reconfigurable, fault-tolerant, parallel architecture is suited to VLSI technology. The architecture, a uniformly interconnected array of identical cells, is capable of functional reconfiguration as well as fault reconfiguration. Microprocessor cells are suggested as the "fabric" for implementation of the array. This thesis also introduces an I/O algorithm as an extension to the reconfiguration process, and outlines the steps by which the array cells construct paths from the active-array to the cellular array I/O ports. Path reconfiguration is presented as the method by which fault-free paths replace faulty paths. A testing algorithm is described for use in the self-testing operation of the array. The types of tests that are conducted on cells are outlined, and the basis by which a cell determines the faulty or fault-free status of a cell is described. / M.S.

What do you do if a computational object fails a specification? An obvious approach is to repair it, namely, to modify the object minimally to get something that satisfies the constraints. In this thesis we study foundational problems of repairing regular specifications over strings and trees. Given two regular specifications R and T we aim to understand how difficult it is to transform an object satisfying R into an object satisfying T. The setting is motivated by considering R to be a restriction -- a constraint that the input object is guaranteed to satisfy -- while T is a target -- a constraint that we want to enforce. We first study which pairs of restriction and target specifications can be repaired with a ``small'' numbers of changes. We formalize this as the bounded repair problem -- to determine whether one can repair each object satisfying R into T with a uniform number of edits. We provide effective characterizations of the bounded repair problem for regular specifications over strings and trees. These characterizations are based on a good understanding of the cyclic behaviour of finite automata. By exploiting these characterizations, we give optimal algorithms to decide whether two specifications are bounded repairable or not. We also consider the impact of limitations on the editing process -- what happens when we require the repair to be done sequentially over serialized objects. We study the bounded repair problem over strings and trees restricted to this streaming setting and show that this variant can be characterized in terms of finite games. Furthermore, we use this characterization to decide whether one can repair a pair of specifications in a streaming fashion with bounded cost and how to obtain a streaming repair strategy in this case. The previous notion asks for a uniform bound on the number of edits, but having this property is a strong requirement. To overcome this limitation, we study how to calculate the maximum number of edits per character needed to repair any object in R into T. We formalize this as the asymptotic cost -- the limit of the number of edits divided by the length of the input in the worst case. Our contribution is an algorithm to compute the asymptotic cost for any pair of regular specifications over strings. We also consider the streaming variant of this cost and we show how to compute it by reducing this problem to mean-payoff games.

Este trabalho é um estudo inicial sobre a integração de duas áreas da engenharia da computação, as tecnologias adaptativas e os algoritmos genéticos. Para tanto, foi realizada a aplicação de algoritmos genéticos na inferência de autômatos adaptativos. Várias tácnicas foram estudas e propostas para a implementação do algoritmo, visando µa obtenção de resultados cada vez mais satisfatórios. Ambas as tecnologias, algoritmos genéticos e tecnologia adaptativa, possuem caráter fortemente adaptativo, porém com características bastante diferentes na forma que são implementadas e executadas. As inferências, propostas neste trabalho, foram realizadas com sucesso, de maneira que as técnicas descritas podem ser empregadas em ferramentas de auxílio para projetistas desses tipos de dispositivos. Ferramentas que podem vir a ser úteis devido µa complexidade envolvida no desenvolvimento de um autômato adaptativo. Através desta aplicação dos algoritmos genéticos, observando como os autômatos evoluíram durante a execução dos ensaios realizados, acredita-se que foi obtido um entendimento melhor da estrutura e funcionamento dos autômatos adaptativos e de como essas duas tecnologias, tão importantes, podem ser combinadas. / This work is an initial study about the integration of two computing engineering areas, the adaptive technologies and the genetic algorithms. For that, it was per- formed the application of genetic algorithms for the adaptive automata inference. Several techniques were studied and proposed along the algorithm implementation, always seeking for more satisfying results. Both technologies, genetic algorithm and adaptive technology, hold very strong adaptive features, however, with very di®erent characteristics in the way they are implemented and executed. The inferences, proposed in this work, were performed with success, so that the techniques described may be employed in aid tools for designers of such de- vices. Tools that may be useful due to the complexity involved in the development of an adaptive automaton. Through this genetic algorithm application, observing how automata evolved during the algorithm execution, we believe that it was obtained a better under- standing about the adaptive automaton structure and how those two, so impor- tant, technologies can be integrated.

Este trabalho é um estudo inicial sobre a integração de duas áreas da engenharia da computação, as tecnologias adaptativas e os algoritmos genéticos. Para tanto, foi realizada a aplicação de algoritmos genéticos na inferência de autômatos adaptativos. Várias tácnicas foram estudas e propostas para a implementação do algoritmo, visando µa obtenção de resultados cada vez mais satisfatórios. Ambas as tecnologias, algoritmos genéticos e tecnologia adaptativa, possuem caráter fortemente adaptativo, porém com características bastante diferentes na forma que são implementadas e executadas. As inferências, propostas neste trabalho, foram realizadas com sucesso, de maneira que as técnicas descritas podem ser empregadas em ferramentas de auxílio para projetistas desses tipos de dispositivos. Ferramentas que podem vir a ser úteis devido µa complexidade envolvida no desenvolvimento de um autômato adaptativo. Através desta aplicação dos algoritmos genéticos, observando como os autômatos evoluíram durante a execução dos ensaios realizados, acredita-se que foi obtido um entendimento melhor da estrutura e funcionamento dos autômatos adaptativos e de como essas duas tecnologias, tão importantes, podem ser combinadas. / This work is an initial study about the integration of two computing engineering areas, the adaptive technologies and the genetic algorithms. For that, it was per- formed the application of genetic algorithms for the adaptive automata inference. Several techniques were studied and proposed along the algorithm implementation, always seeking for more satisfying results. Both technologies, genetic algorithm and adaptive technology, hold very strong adaptive features, however, with very di®erent characteristics in the way they are implemented and executed. The inferences, proposed in this work, were performed with success, so that the techniques described may be employed in aid tools for designers of such de- vices. Tools that may be useful due to the complexity involved in the development of an adaptive automaton. Through this genetic algorithm application, observing how automata evolved during the algorithm execution, we believe that it was obtained a better under- standing about the adaptive automaton structure and how those two, so impor- tant, technologies can be integrated.

Proceedings with the revised papers of the FSMNLP (Finite-state Methods and Natural Language Processing) 2007 Workshop in Potsdam / Tagungsband mit den Beiträgen der FSMNLP (Finite-state Methods and Natural Language Processing) 2007 in Potsdam

The proper composition of independently developed components of an embedded real- time system is complicated due to the fact that besides the functional behavior also the non-functional properties and in particular the timing have to be compatible. Nowadays related compatibility problems have to be addressed in a cumbersome integration and configuration phase at the end of the development process, that in the worst case may fail. Therefore, a number of formal approaches have been developed, which try to guide the upfront decomposition of the embedded real-time system into components such that integration problems related to timing properties can be excluded and that suitable configurations can be found. However, the proposed solutions require a number of strong assumptions that can be hardly fulfilled or the required analysis does not scale well. In this paper, we present an approach based on timed automata that can provide the required guarantees for the later integration without strong assumptions, which are difficult to match in practice. The approach provides a modular reasoning scheme that permits to establish the required guarantees for the integration employing only local checks, which therefore also scales. It is also possible to determine potential configuration settings by means of timed game synthesis. / Die korrekte Komposition individuell entwickelter Komponenten von eingebetteten Realzeitsystemen ist eine Herausforderung, da neben funktionalen Eigenschaften auch nicht funktionale Eigenschaften berücksichtigt werden müssen. Ein Beispiel hierfür ist die Kompatibilität von Realzeiteigenschaften, welche eine entscheidende Rolle in eingebetteten Systemen spielen. Heutzutage wird die Kompatibilität derartiger Eigenschaften in einer aufwändigen Integrations- und Konfigurationstests am Ende des Entwicklungsprozesses geprüft, wobei diese Tests im schlechtesten Fall fehlschlagen. Aus diesem Grund wurde eine Zahl an formalen Verfahren Entwickelt, welche eine frühzeitige Analyse von Realzeiteigenschaften von Komponenten erlauben, sodass Inkompatibilitäten von Realzeiteigenschaften in späteren Phasen ausgeschlossen werden können. Existierenden Verfahren verlangen jedoch, dass eine Reihe von Bedingungen erfüllt sein muss, welche von realen Systemen nur schwer zu erfüllen sind, oder aber, die verwendeten Analyseverfahren skalieren nicht für größere Systeme. In dieser Arbeit wird ein Ansatz vorgestellt, welcher auf dem formalen Modell des Timed Automaton basiert und der keine Bedingungen verlangt, die von einem realen System nur schwer erfüllt werden können. Der in dieser Arbeit vorgestellte Ansatz enthält ein Framework, welches eine modulare Analyse erlaubt, bei der ausschließlich miteinender kommunizierende Komponenten paarweise überprüft werden müssen. Somit wird eine skalierbare Analyse von Realzeiteigenschaften ermöglicht, die keine Bedingungen verlangt, welche nur bedingt von realen Systemen erfüllt werden können.

In this thesis we will introduce multioperator weighted monadic datalog (mwmd), a formal model for specifying tree series, tree transformations, and tree languages. This model combines aspects of multioperator weighted tree automata (wmta), weighted monadic datalog (wmd), and monadic datalog tree transducers (mdtt). In order to develop a rich theory we will define multiple versions of semantics for mwmd and compare their expressiveness. We will study normal forms and decidability results of mwmd and show (by employing particular semantic domains) that the theory of mwmd subsumes the theory of both wmd and mdtt. We conclude this thesis by showing that mwmd even contain wmta as a syntactic subclass and present results concerning this subclass.

This thesis concerns decision procedures for fragments of linear arithmetic and their application to model-checking one-counter automata. The first part of this thesis covers the complexity of decision problems for different types of linear arithmetic, namely the existential subset of the first-order linear theory over the p-adic numbers and the existential subset of Presburger arithmetic with divisibility, with all integer constants and coefficients represented in binary. The most important result of this part is a new upper complexity bound of <b>NEXPTIME</b> for existential Presburger arithmetic with divisibility. The best bound that was known previously was <b>2NEXPTIME</b>, which followed directly from the original proof of decidability of this theory by Lipshitz in 1976. Lipshitz also gave a proof of <b>NP</b>-hardness of the problem in 1981. Our result is the first improvement of the bound since this original description of a decision procedure. Another new result, which is both an important building block in establishing our new upper complexity bound for existential Presburger arithmetic with divisibility and an interesting result in its own right, is that the decision problem for the existential linear theory of the p-adic numbers is in the Counting Hierarchy <b>CH</b>, and thus within <b>PSPACE</b>. The precise complexity of this problem was stated as open by Weispfenning in 1988, who showed that it is in <b>EXPTIME</b> and <b>NP</b>-hard. The second part of this thesis covers two problems concerning one-counter automata. The first problem is an LTL synthesis problem on one-counter automata with integer-valued and parameterised updates and with equality tests. The decidability of this problem was stated as open by G&ouml;ller et al. in 2010. We give a reduction of this problem to the decision problem of a subset of Presburger arithmetic with divisibility with one quantifier alternation and a restriction on existentially quantified variables. A proof of decidability of this theory is currently under review. The final result of this thesis concerns a type of one-counter automata that differs from the previous one in that it allows parameters only on tests, not actions, and it includes both equality and disequality tests on counter values. The decidability of the basic reachability problem on such one-counter automata was stated as an open problem by Demri and Sangnier in 2010. We show that this problem is decidable by a reduction to the decision problem for Presburger arithmetic.

Problems in formal verification are often stated in terms of finite automata and extensions thereof. In this thesis we investigate several such algorithmic problems. In the first part of the thesis we develop a theory of completeness thresholds in Bounded Model Checking. A completeness threshold for a given model M and a specification &phi; is a bound k such that, if no counterexample to &phi; of length k or less can be found in M, then M in fact satisfies &phi;. We settle a problem of Kroening et al. [KOS⁺11] in the affirmative, by showing that the linearity problem for both regular and &omega;-regular specifications (provided as finite automata and Buchi automata respectively) is PSPACE-complete. Moreover, we establish the following dichotomies: for regular specifications, completeness thresholds are either linear or exponential, whereas for &omega;-regular specifications, completeness thresholds are either linear or at least quadratic in the recurrence diameter of the model under consideration. Given a formula in a temporal logic such as LTL or MTL, a fundamental problem underpinning automata-based model checking is the complexity of evaluating the formula on a given finite word. For LTL, the complexity of this task was recently shown to be in NC [KF09]. In the second part of the thesis we present an NC algorithm for MTL, a quantitative (or metric) extension of LTL, and give an AC¹ algorithm for UTL, the unary fragment of LTL. We then establish a connection between LTL path checking and planar circuits which, among others, implies that the complexity of LTL path checking depends on the Boolean connectives allowed: adding Boolean exclusive or yields a temporal logic with P-complete path-checking problem. In the third part of the thesis we study the decidability of the reachability problem for parametric timed automata. The problem was introduced over 20 years ago by Alur, Henzinger, and Vardi [AHV93]. It is known that for three or more parametric clocks the problem is undecidable. We translate the problem to reachability questions in certain extensions of parametric one-counter machines. By further reducing to satisfiability in Presburger arithmetic with divisibility, we obtain decidability results for several classes of parametric one-counter machines. As a corollary, we show that, in the case of a single parametric clock (with arbitrarily many nonparametric clocks) the reachability problem is NEXP-complete, improving the nonelementary decision procedure of Alur et al. The case of two parametric clocks is open. Here, we show that the reachability is decidable in this case of automata with a single parameter.