Positive kernels and their associated reproducing kernel Hilbert spaces have played a key role in the development of complex analysis and Hilbert-space operator theory, and they have recently been extended to the setting of free noncommutative function theory. In this paper, we develop the subject further in a number of directions. We give a characterization of completely positive noncommutative kernels in the setting of Hilbert C*-modules and Hilbert W*-modules. We prove an Arveson-type extension theorem for completely positive noncommutative kernels, and we show that a uniformly bounded noncommutative kernel can be decomposed into a linear combination of completely positive noncommutative kernels. / Ph. D.

For a compact, nowhere dense set X in the complex plane, C, define Rp(X) as the closure of the rational functions with poles off X in Lp(X, dA). It is well known that for 1 ≤ p < 2, Rp(X) = Lp(X) . Although density may not be achieved for p > 2, there exists a set X so that Rp(X) = Lp(X) for p up to a given number greater than 2 but not after. Additionally, when p > 2 we shall establish that the support of the annihiliating and representing measures for Rp(X) lies almost everywhere on the set of bounded point evaluations of X.

When the primary measurement sensor is passive in nature--by which we mean that it does not directly measure range or range rate--there are well-documented challenges for target state estimation. Most estimation schemes rely on variations of the Extended Kalman Filter (EKF), which, in certain situations, suffer from divergence and/or covariance collapse. For this and other reasons, we believe that the Kalman filter is fundamentally ill-suited to the problems that are inherent in target state estimation using passive sensors. As an alternative, we propose a bounded-error (or set-membership) approach to the target state estimation problem. Such estimators are nearly as old as the Kalman filter, but have enjoyed much less attention. In this study we develop a practical estimator that bounds the target states, and apply it to the two-dimensional case of a submarine tracking a surface vessel, which is commonly referred to as Target Motion Analysis (TMA). The estimator is robust in the sense that the true target state does not escape the determined bounds; and the estimator is not unduly pessimistic in the sense that the bounds are not wider than the situation dictates. The estimator is--as is the problem itself--nonlinear and geometric in nature. In part, the simplicity of the estimator is maintained by using redundant states to parameterize the target's velocity. These redundant states also simplify the incorporation of other measurements that are frequently available to the system. The estimator's performance is assessed in a series of simulations and the results are analyzed. Extensions of the algorithm are considered.

Since its introduction in 1999, bounded model checking (BMC) has quickly become a serious and indispensable tool for the formal verification of hardware designs and, more recently, software. By leveraging propositional satisfiability (SAT) solvers, BMC overcomes some of the shortcomings of more conventional model checking methods. In model checking we automatically verify whether a state transition system (STS) describing a design has some property, commonly expressed in linear temporal logic (LTL). BMC is the restriction to only checking the looping and non-looping runs of the system that have bounded descriptions. The conventional BMC approach is to translate the STS runs and LTL formulae into propositional logic and then conjunctive normal form (CNF). This CNF expression is then checked by a SAT solver. In this thesis we study the effect on the performance of BMC of changing the translation to propositional logic. One novelty is to use a normal form for LTL which originates in resolution theorem provers. We introduce the normal form conversion early on in the encoding process and examine the simplifications that it brings to the generation of propositional logic. We further enhance the encoding by specialising the normal form to take advantage of the types of runs peculiar to BMC. We also improve the conversion from propositional logic to CNF. We investigate the behaviour of the new encodings by a series of detailed experimental comparisons using both hand-crafted and industrial benchmarks from a variety of sources. These reveal that the new normal form based encodings can reduce the solving time by a half in most cases, and up to an order of magnitude in some cases, the size of the improvement corresponding to the complexity of the LTL expression. We also compare our method to the popular automata-based methods for model checking and BMC.

Model checking is a fully-automatic formal verification method that has been extremely successful in validating and verifying safety-critical systems in the past three decades. In the past fifteen years, there has been a lot of work in extending many model checking algorithms over finite-state systems to finitely representable infinitestate systems. Unlike in the case of finite systems, decidability can easily become a problem in the case of infinite-state model checking. In this thesis, we present generic and specific techniques that can be used to derive decidability with near-optimal computational complexity for various model checking problems over infinite-state systems. Generic techniques and specific techniques primarily differ in the way in which a decidability result is derived. Generic techniques is a “top-down” approach wherein we start with a Turing-powerful formalismfor infinitestate systems (in the sense of being able to generate the computation graphs of Turing machines up to isomorphisms), and then impose semantic restrictions whereby the desired model checking problem becomes decidable. In other words, to show that a subclass of the infinite-state systems that is generated by this formalism is decidable with respect to the model checking problem under consideration, we will simply have to prove that this subclass satisfies the semantic restriction. On the other hand, specific techniques is a “bottom-up” approach in the sense that we restrict to a non-Turing powerful formalism of infinite-state systems at the outset. The main benefit of generic techniques is that they can be used as algorithmic metatheorems, i.e., they can give unified proofs of decidability of various model checking problems over infinite-state systems. Specific techniques are more flexible in the sense they can be used to derive decidability or optimal complexity when generic techniques fail. In the first part of the thesis, we adopt word/tree automatic transition systems as a generic formalism of infinite-state systems. Such formalisms can be used to generate many interesting classes of infinite-state systems that have been considered in the literature, e.g., the computation graphs of counter systems, Turing machines, pushdown systems, prefix-recognizable systems, regular ground-tree rewrite systems, PAprocesses, order-2 collapsible pushdown systems. Although the generality of these formalisms make most interesting model checking problems (even safety) undecidable, they are known to have nice closure and algorithmic properties. We use these nice properties to obtain several algorithmic metatheorems over word/tree automatic systems, e.g., for deriving decidability of various model checking problems including recurrent reachability, and Linear Temporal Logic (LTL) with complex fairness constraints. These algorithmic metatheorems can be used to uniformly prove decidability with optimal (or near-optimal) complexity of various model checking problems over many classes of infinite-state systems that have been considered in the literature. In fact, many of these decidability/complexity results were not previously known in the literature. In the second part of the thesis, we study various model checking problems over subclasses of counter systems that were already known to be decidable. In particular, we consider reversal-bounded counter systems (and their extensions with discrete clocks), one-counter processes, and networks of one-counter processes. We shall derive optimal complexity of various model checking problems including: model checking LTL, EF-logic, and first-order logic with reachability relations (and restrictions thereof). In most cases, we obtain a single/double exponential reduction in the previously known upper bounds on the complexity of the problems.

A mobile ad hoc network (MANET) is a collection of mobile platforms or nodes that come together to form a network capable of communicating with each other, without the help of a central controller. To avail the maximum potential of a MANET, it is of great importance to devise a routing scheme, which will optimize upon the performance of a MANET, given the high rate of random mobility of the nodes. In a MANET individual nodes perform the routing functions like route discovery, route maintenance and delivery of packets from one node to the other. Existing routing protocols flood the network with broadcasts of route discovery messages, while attempting to establish a route. This characteristic is instrumental in deteriorating the performance of a MANET, as resource overhead triggered by broadcasts is directly proportional to the size of the network. Bounded-dynamic source routing (B-DSR), is proposed to curb this multitude of superfluous broadcasts, thus enabling to reserve valuable resources like bandwidth and battery power. B-DSR establishes a bounded region in the network, only within which, transmissions of route discovery messages are processed and validated for establishing a route. All route discovery messages reaching outside of this bounded region are dropped, thus preventing the network from being flooded. In addition B-DSR also guarantees loop-free routing and is robust for a rapid recovery when routes in the network change.

The purpose of this paper is to investigate the integrability, measurability, and summability of certain set functions. The paper is divided into four chapters. The first chapter contains basic definitions and preliminary remarks about set functions and absolute continuity. In Chapter i, the integrability of bounded set functions is investigated. The chapter culminates with a theorem that characterizes the transmission of the integrability of a real function of n bounded set functions. In Chapter III, measurability is defined and a characterization of the transmission of measurability by a function of n variables is provided, In Chapter IV, summability is defined and the summability of set functions is investigated, Included is a characterization of the transmission of summability by a function of n variables.

The first chapter gives basic definitions and theorems concerning set functions and set function integrals. The lemmas and theorems are presented without proof in this chapter. The second chapter deals with absolute continuity and Lipschitz condition. Particular emphasis is placed on the properties of max and min integrals. The third chapter deals with approximating absolutely continuous functions with bounded functions. It also deals with the existence of the integrals composed of various combinations of bounded functions and finitely additive functions. The concluding theorem states if the integral of the product of a bounded function and a non-negative finitely additive function exists, then the integral of the product of the bounded function with an absolutely continuous function exists over any element in a field of subsets of a set U.

A series of experimental studies was performed to investigate two separate fluid impingement flow systems intended for removal of particles from a surface or deposition of particles onto a surface. One of these flow systems is generated using a nozzle that incorporates both tilted jets and suction to create what we call a "bounded vortex flow", consisting of an annular swirling jet and a wall-normal vortex with axial upflow into a suction outlet. The other flow system is generated by a combination of acoustic streaming and substrate heating from an ultrasonic source. The primary methods used in the study for flow field measurements included laser-induced fluorescence (LIF) and particle-image velocimetry (PIV). Thermocouples are utilized for gathering temperature information from the ultrasonic induced flow. For the bounded vortex flow, different jet/suction flow rates and different nozzle-substrate separation distances were examined. In the acoustic-generated flow system, different acoustic intensities and transducer-substrate separation distances and different choices of substrate material were examined. Both flow systems achieve high levels of shear stress on the impingement surface via a combination of flow oriented toward and/or away from the surface and via formation of vortex structures near the impingement surface. In the bounded flow configuration, the vortex flow is oriented with axis normal to the impingement surface, whereas in the acoustic-generated flow a series of vortex rings form with axes parallel to the impingement surface. For both flow fields, conditions are observed with high impingement surface shear stress that are well suited to particle removal from the impingement surface. However, as the variables controlling the flows are varied, other conditions are observed in which the flow fields become unstable, leading to oscillatory flows that generally have much smaller shear stress values on the impingement surface. The rate of fluid mixing, as characterized by upward and downward flows normal to the impingement surface, is also generally decreased after these flow transitions have occurred, implying that the unstable flows will be less suited for both particle deposition on and particle removal from the impingement surface.

Primary objective of the thesis is proof of the statement that if for ∈ ℕ a ≥ 1 a bilipschitz mapping belongs to +1, loc ∩ ,∞ loc then also its inverse −1 belongs to +1, loc . We prove a similar statement also for spaces loc . For this purpose we construct a new ordering of -th partial derivatives to generalized Jacobian matrix. Thanks to this matrix we are able to differentiate matrices in an applicable way. Generalized Jacobian matrix is projected so that there still holds the Chain rule and, in some way, also rules for matrices product differentiation. 1