Search

Reachability and shortest distance query processing are important research problems among the key graph operations. These problems have been widely studied due to their numerous applications. Most of the existing works focus on creating an index and answering reachability/shortest distance query from that index. It is very challenging to keep the index size smaller while creating an index with all the reachability/shortest distance information. We aim to reduce the index size of existing techniques by doing compression while keeping the index construction time and query time sufficiently faster. In this thesis, we first focus on the reachability problem. We introduce a multilevel graph compression scheme that can reduce the graph size significantly. We also propose an algorithm to answer reachability queries using the compressed graph. Extensive experiments with real-world and synthetic datasets confirm the efficiency of our approach. We then study the shortest distance problem. One of the state-of-the-art shortest distance labeling approaches is Pruned Landmark Labeling (PLL). Another well-known distance labeling approach is Pruned Highway Labeling (PHL) which is specifically designed for undirected road networks. Both PLL and PHL constructs large index for large graphs. To address this problem, we propose two approaches. One is to compress the PLL index for directed graphs; the other is to do a path compression to compress undirected road networks. We aim to reduce the index size and index construction time without significantly compromising query performance. We verify the effectiveness of our approach by extensive experiments with real-world datasets. This thesis finally provides a comprehensive experimental evaluation of the state-of-the-art algorithms for shortest distance queries on road networks. We also evaluate the effect of path compression on these algorithms. Our evaluation provides several important insights on the advantage/disadvantages of these algorithms, and it enables us to recommend the most suitable algorithm for some application scenarios.

Autonomous mobile robots (AMRs) can transform a wide variety of industries including transportation, shipping and goods delivery, and defense. AMRs must match or exceed human performance in metrics for task completion and safety. Motion plans for AMRs are generated by solving an optimization program where collision avoidance and the trajectory obeying a dynamic model of the robot are enforced as constraints. This dissertation focuses on three main challenges associated with trajectory planning. First, collision checks are typically performed at discrete time steps. Second, there can be a nontrivial gap between the planning model used and the actual system. Finally, there is inherent uncertainty in the motion of other agents or robots. This dissertation first proposes a receding-horizon planning methodology called Reachability-based Trajectory Design (RTD) to address the first and second challenges, where uncertainty is dealt with robustly. Sums-of-Squares (SOS) programming is used to represent the forward reachable set for a dynamic system plus uncertainty, over an interval of time, as a polynomial level set. The trajectory optimization is a polynomial optimization program over a space of trajectory parameters. Hardware demonstrations are implemented on a Segway, rover, and electric vehicle. In a simulation of 1,000 trials with static obstacles, RTD is compared to Rapidly-exploring Random Tree (RRT) and Nonlinear Model Predictive Control (NMPC) planners. RTD has success rates of 95.4% and 96.3% for the Segway and rover respectively, compared to 97.6% and 78.2% for RRT and 0% for NMPC planners. RTD is the only successful planner with no collisions. In 10 simulations with a CarSim model, RTD navigates a test track on all trials. In 1,000 simulations with random dynamic obstacles RTD has success rates of 96.8% and 100% respectively for the electric vehicle and Segway, compared to 77.3% and 92.4% for a State Lattice planner. In 100 simulations performing left turns, RTD has a success rate of 99% compared to 80% for an MPC controller tracking the lane centerline. The latter half of the dissertation treats uncertainty with the second and/or third challenges probabilistically. The Chance-constrained Parallel Bernstein Algorithm (CCPBA) allows one to solve the trajectory optimization program from RTD when obstacle states are given as probability functions. A comparison for an autonomous vehicle planning a lane change with one obstacle shows an MPC algorithm using Cantelli's inequality is unable to find a solution when the obstacle's predictions are generated with process noise three orders of magnitude less than CCPBA. In environments with 1-6 obstacles, CCPBA finds solutions in 1e-3 to 1.2 s compared to 1 to 16 s for an NMPC algorithm using the Chernoff bound. A hardware demonstration is implemented on the Segway. The final portion of the dissertation presents a chance-constrained NMPC method where uncertain components of the robot model are estimated online. The application is an autonomous vehicle with varying road surfaces. In the first study, the controller uses a linear tire force model. Over 200 trials of lane changes at 17 m/s, the chance-constrained controller has a cost 86% less than a controller using fixed coefficients for snow, and only 29% more than an oracle controller using the simulation model. The chance-constrained controller also has 0 lateral position constraint violations, while an adaptive-only controller has minor violations. The second study uses nonlinear tire models on a more aggressive maneuver and provides similar results.

Graphs are widely used to represent interactions (i.e., edges) between entities (i.e., nodes/vertices) in a large spectrum of applications, including social networks, biological protein-protein networks, and e-commerce networks. One fundamental task in graph analysis is to explore node-to-node relationships such as "how similar two proteins are in biological networks'' and "whether or not a user can influence another user in social networks''. In this thesis, we study the following three problems, which are of great importance in exploring these relationships. Firstly, we study the problem of role similarity computation. As one of the structural node similarity metrics, role similarity has the merit of indicating automorphism. However, existing algorithms cannot handle large-scale graphs. In this thesis, we propose an efficient algorithm StructSim, which admits a pre-computed index to query a node pair in O(k log D) time, where k is a small user-defined parameter, and D is the maximum node degree. To build the index efficiently, we further devise an FM-sketch-based technique that can handle billion-scale graphs. Secondly, we study how to quantify approximate simulation. Simulation and its variants are useful binary relations among nodes. However, all simulation variants are coarse "yes-or-no'' indicators that simply confirm or refute whether one node simulates another, which limits the scope of their utility. Therefore, it is meaningful to develop a fractional simulation measure to quantify the extent that a node simulates another. To this end, we propose a general fractional simulation computation framework that can be configured to quantify the extent of different simulation variants. Thirdly, we study the reachability problem on temporal bipartite graphs. Reachability, which studies if a node can reach the other node, has been extensively studied on (temporal) unipartite graphs, while it remains largely unexplored on temporal bipartite graphs. In this thesis, we study the temporal bipartite reachability problem. Specifically, a vertex u reaches a vertex w in a temporal bipartite graph if they are connected through a series of consecutive wedges with time constraints. We propose an index-based method to support fast reachability queries, and we also devise effective techniques to accelerate the index construction process.

We are captivated by the promise of autonomous systems in our everyday life. However, ensuring that these systems act safely is an immense challenge: introducing complex systems into real-world uncertain environments while guaranteeing safety at all times is impossible in applications like self-driving vehicles, collaborative factory robots, and assistive robots. These systems will inevitably need to make real-time decisions with limited computational resources, and incomplete knowledge of the environment and other agents. This dissertation is an effort towards achieving trustworthy real-world autonomy by enabling autonomous systems to: (1) make theoretical safety guarantees efficiently based on known information, and(2) bridge the safety gap between this theory and the real world by reasoning about uncertainty in the environment and other agents.Towards this goal this dissertation covers various methods for scalable safety and real-time decision-making that draw from control theory, cognitive science, and learning, and are backed by both rigorous theory and physical testing on robotic platforms. We begin with an overview of reachability analysis and its applications for optimal control with safety guarantees. We then tackle the curse of dimensionality associated with reachability computation by decomposing systems or updating previous solutions in a warm-starting fashion. Next we explore planning in a simplified, low-dimensional space online with precomputed safety guarantees and tracking controls offline. This is extended to meta-planning, in which the online algorithm switches between faster/conservative modes and slower/accurate modes. Then we apply all of these tools towards navigating in uncertain environments among hard-to-predict agents such as human pedestrians. We use Bayesian machine learning methods to reason about human intention and navigate in a probabilistically safe manner. Finally, the dissertation ends with information about code bases and reachability tutorial examples.

Stochastic reachability is an important verification tool that provides probabilistic assurances of safety in a variety of contexts. In engineered systems, safety may be synonymous with the ability of the system to avoid "bad" constraints on the state space, that constitute collision, departure from a flight envelope, or other undesirable phenomenon. In biomedical systems, assurance of safety (such as the mandate to ``do no harm'') are considerably complicated by the fact that there is a lack of physics-driven models, extensive signal processing is needed to capture the underlying state of the system, and the stochasticity inherent to the system may be quite large. However, assurances of safety are no less paramount. Stochastic reachability analysis is a framework that is well suited to address safety problems in biomedical systems. We are particularly motivated by the problem of circadian regulation, which is not only critical for those with diagnosed sleep disorders, e.g. Delayed Sleep-Wake Phase disorder, but also for shift workers, people traveling across multiple time zones, and those in regulated lighting environments that do not account for circadian regulation, e.g. hospitals. The primary focus of this thesis is on the development software systems and algorithms that can address some of the most significant challenges associated with safety guarantees in biomedical systems. Specifically, I focus on linear time-varying dynamical systems (which are a common approximation of nonlinear dynamical systems) with unstructured, non-Gaussian disturbances. The theoretical methods I develop provide conservative assurances of safety, despite a potentially unbounded disturbance input, in a computable manner. I have implemented these methods in a new MATLAB toolbox for stochastic reachability, SReachTools, that I have jointly developed. This toolbox is open-source and has been repeatability verified. Implementation of such methods in a clinical environment requires rigorous development, design, and testing of software, as well as integration with methods for signal processing, fault handling, and error reporting. As part of a collaboration on smart lighting, I created a software implementation of a smart lighting testbed, which provides the necessary functionality to implement feedback-based circadian control, such as those provided by stochastic reachability algorithms. The testbed software was validated in a pilot experiment, in which the testbed successfully ran continuously for 5 days for each of 3 subjects. Estimates of circadian phase are necessary for control, hence signal processing techniques to infer phase from circadian-regulated biometrics are important. We developed a method to infer circadian phase from invasively gathered brain temperature data, in collaboration with UNM neurosurgeons in the UNM Neurotrauma intensive care unit. A similar technique would be necessary to someday fully close the loop in the smart lighting clinical testbed.

A solution to the terminal-hitting and first-hitting stochastic reach-avoid problem for a Markov control process is presented. This solution takes advantage of a nonparametric representation of the stochastic kernel as a conditional distribution embedding within a reproducing kernel Hilbert space (RKHS). Because the disturbance is modeled as a data-driven stochastic process, this representation avoids intractable integrals in the dynamic recursion of the reach-avoid problem since the expectations can be calculated as an inner product within the RKHS. An example using a high-dimensional chain of integrators is presented, as well as for Clohessy-Wiltshire-Hill (CWH) dynamics.

Systems of nonlinear ordinary differential equations (ODEs) are used to model an incredible variety of dynamic phenomena in chemical, oil and gas, and pharmaceutical industries. In reality, such models are nearly always subject to significant uncertainties in their initial conditions, parameters, and inputs. This dissertation provides new theoretical and numerical techniques for rigorously enclosing the set of solutions reachable by a given systems of nonlinear ODEs subject to uncertain initial conditions, parameters, and time-varying inputs. Such sets are often referred to as reachable sets, and methods for enclosing them are critical for designing systems that are passively robust to uncertainty, as well as for optimal real-time decision-making. Such enclosure methods are used extensively for uncertainty propagation, robust control, system verification, and optimization of dynamic systems arising in a wide variety of applications. Unfortunately, existing methods for computing such enclosures often provide an unworkable compromise between cost and accuracy. For example, interval methods based on differential inequalities (DI) can produce bounds very efficiently but are often too conservative to be of any practical use. In contrast, methods based on more complex sets can achieve sharp bounds, but are far too expensive for real-time decision-making and scale poorly with problem size. Recently, it has been shown that bounds computed via differential inequalities can often be made much less conservative while maintaining high efficiency by exploiting redundant model equations that are known to hold for all trajectories of interest (e.g., linear relationships among chemical species in a reaction network that hold due to the conservation of mass or elements). These linear relationships are implied by the governing ODEs, and can thus be considered redundant. However, these advances are only applicable to a limited class of system in which pre-existing linear redundant model equations are available. Moreover, the theoretical results underlying these algorithms do not apply to redundant equations that depend on time-varying inputs and rely on assumptions that prove to be very restrictive for nonlinear redundant equations, etc. This dissertation continues a line of research that has recently achieved very promising bounding results using methods based on differential inequalities. In brief, the major contributions can be divided into three categories: (1) In regard to algorithms, this dissertation significantly improves existing algorithms that exploit linear redundant model equations to achieve more accurate and efficient enclosures. It also develops new fast and accurate bounding algorithms that can exploit nonlinear redundant model equations. (2) Considering theoretical contributions, it develops a novel theoretical framework for the introduction of redundant model equations into arbitrary dynamic models to effectively reduce conservatism. The newly developed theories have more generality in terms of application. For example, complex nonlinear constraints that involve states, time derivatives of the system states, and time- varying inputs are allowed to be exploited. (3) A new differential inequalities method called Mean Value Differential Inequalities (MVDI) is developed that can automatically introduce redundant model equations for arbitrary dynamic systems and has a second-order convergence rate reported the first time among DI-based methods.

For many manufacturing tasks, such as welding and cutting, the task trajectory, or path, is known a priori in the object's reference frame. What is not known is whether or not the robot can reach the entirety of the trajectory given the relative location of the object frame to the robot's base frame and its reachable and/or dexterous workspace. The problem increases in complexity with each additional object in the robot's workspace. Some robots need to perform tasks in cluttered or confined environments, such as a glovebox, and the ability to know if and where the manipulator can perform a certain task is crucial for both design and operation. This thesis describes the development, design, and implementation of a Task-Trajectory Analysis Package (T-TAP) within the Robot Operating System (ROS) framework. Reachability has been extensively discussed in the literature, but current reachability visualization tools do not account for task data, and instead describe the robot's global workspace and thus take a long time to compute. Such tools may be useful for designing robotic systems, but their value diminishes when analyzing a specific task and environment. T-TAP focuses on the task space and is capable of producing real-time or near real-time feedback about the validity of a path. The results are shown in an easy-to-interpret visualization of the path points and their relative quality as measured using selected performance metrics. T-TAP contains several capabilities. The first, and simplest, validates reachability for discrete points along the trajectory. An inverse kinematic (IK) solver is used to plan from one trajectory point to the next. The user can use standard ROS IK solvers or utilize their own IK solver. Next, T-TAP uses the Jacobian to analyze the system's performance as it completes the proposed trajectory. It ensures that joint and velocity limits are not violated, singularities are avoided, and is extensible to include additional user-defined performance metrics. T-TAP requires no prior computations, is hardware agnostic, and can be run entirely in simulation. It can reduce the time required to place and plan a trajectory by an order of magnitude. It is designed to work seamlessly with existing ROS path-planning packages. The operator needs only to send the path to T-TAP and T-TAP will analyze the trajectory. This information will allow the operator to intelligently adjust the path so that it is reachable and viable.

To integrate renewable energy, converter-interfaced sources (CISs) keep penetrating into power systems and degrade the grid frequency response. Control synthesis towards guaranteed performance is a challenging task. Meanwhile, the potentials of highly controllable converters are far from fully developed. With properly designed controllers the CISs can not only eliminate the negative impacts on the grid, but also provide performance guarantees.First, the wind turbine generator (WTG) is chosen to represent the CISs. An augmented system frequency response (ASFR) model is derived, including the system frequency response model and a reduced-order model of the WTG representing the supportive active power due to the supplementary inputs.Second, the framework for safety verification is introduced. A new concept, region of safety (ROS), is proposed, and the safe switching principle is provided. Two different approaches are proposed to estimate the largest ROS, which can be solved using the sum of squares programming.Third, the critical switching instants for adequate frequency response are obtained through the study of the ASFR model. A safe switching window is discovered, and a safe speed recovery strategy is proposed to ensure the safety of the second frequency dip due to the WTG speed recovery.Fourth, an adaptive safety supervisory control (SSC) is proposed with a two-loop configuration, where the supervisor is scheduled with respect to the varying renewable penetration level. For small-scale system, a decentralized fashion of the SSC is proposed under rational approximations and verified on the IEEE 39-bus system.Fifth, a two-level control diagram is proposed so that the frequency of a microgrid satisfies the temporal logic specifications (TLSs). The controller is configured into a scheduling level and a triggering level. The satisfaction of TLSs will be guaranteed by the scheduling level, and triggering level will determine the activation instant.Finally, a novel model reference control based synthetic inertia emulation strategy is proposed. This novel control strategy ensures precise emulated inertia by the WTGs as opposed to the trial and error procedure of conventional methods. Safety bounds can be easily derived based on the reference model under the worst-case scenario.

Take a blank page, draw some small circles, and connect them with a few arrows, and voilà you created a directed graph, a digraph for short. Now let us ask an algorithmic question: If I point out two of those circles to you, one as the start and one as the target, can you find a way to go from the start to the target by only using the arrows in their one-way direction? While this reachability question is well-studied, we found new algorithms for the following slight variations of the reachability problem: - What if we ask this questions for many starts and many targets while we also add and remove arrows in between answering these questions? - What if we want to find two ways from the start to the target that use completely different arrows? Or can we even find three disjoint paths? And how fast can we compute the answer for all combinations of starts and targets? For the dynamic reachability problem, we review the link-cut tree data structure for dynamic rooted forests before we extend it to a new class of dynamic graphs: partial-function graphs. We provide algorithms for arbitrarily interleaved queries and updates to the graph in time O(log n). In the generalized reachability problem, we ask about the existence of multiple arc-disjoint paths between the query vertices. The all-pairs k-reachability problem asks for the number of arc-disjoint paths between all vertex pairs, where one can answer 'at least k', whenever there are k or more arc-disjoint paths. 2-reachability answers basic resilience of paths, i.e., is there an arc that can not be avoided on the path from u to v. As our main result, we present an algorithm running in time O(n^ω log n) to compute all-pairs 2-reachability of any digraph, where ω is the matrix multiplication exponent. This result comes in three steps: first, we develop a path algebra with binary encodings for acyclic graphs, second, we use dominator trees to build auxiliary graphs that represent the answer for strongly connected graphs, and third, we carefully combine the two on arbitrary digraphs. Finally, we look at the general k-reachability problem restricted to acyclic graphs. We develop a framework dealing with the structure of extremal cuts and encoding and handling those cuts efficiently to come up with two algorithms for DAGs: one running in time O(mn^{1+o(1)}) for k = o(√{log n}) and one in time O(n^{ω + o(1)}) for k = o(log log n). One nice side effect of these algorithms is that they do not only report the size of the minimum cut but also provide a cut as a witness.

Guaranteeing safety and performance are crucial components in any control system, and particularly relevant in light of growing interest in reliable autonomy. In safety-critical applications like biomedical devices, spacecraft applications, and self-driving cars, the cost of failure can be severe. Verification provides these guarantees by characterizing the ``good'' initial states or configurations from which a state can be driven to remain within a collection of pre-specified safe sets, while respecting the system dynamics, bounds on control authority, and additive uncertainties. We also wish to design controllers to achieve this objective. This dissertation proposes novel theory and scalable algorithms for tractable solutions to the stochastic reachability problems. We treat the verification problems as backward stochastic reachability problems, since we wish to ascertain a set of initial states (back in time) that satisfy the pre-specified safety constraints in future and determine the associated admissible controllers. Current approaches to this problem are restricted to low dimensional systems since they rely on grids over the state space. In contrast, we have developed several approaches which avoid gridding, scale well with time and system dimension, and may be terminated at any time without compromising on the solution integrity (anytime algorithms). Additionally, our approaches enable controller synthesis that is open-loop or affine feedback. We design these algorithms by characterizing the sufficient conditions for the convexity and compactness of the sets. This enables verification of high-dimensional systems using convex optimization, stochastic programming, and Fourier transforms. We apply our methods to verification of spacecraft rendezvous, as well as to automated anesthesia delivery. We also discuss a related problem of predicting the stochasticity of the state of the system at a future time, given an initial state --- the problem of forward stochastic reachability. We address this problem using Fourier transforms and computational geometry. Using forward stochastic reachability, we also introduce probabilistic occupancy functions to reason about collision probability and characterize keep-out sets for probabilistic safety. The applications include autonomous surveillance and stochastic motion planning problems. We present an open-source MATLAB toolbox, SReachTools, that implements all the algorithms presented in this dissertation in an easily-accessible code base.

Modern aircraft with nonlinear flight envelopes predominately utilize gain scheduled controllers to provide stability of flight. Using gain scheduled control techniques, nonlinear envelopes can be linearized into collections of linear systems that operate under various system dynamics.Linear controllers approximate the nonlinear response over setpoints of operating conditions which allow traditional linear theory to be applied to maintain stability. Techniques to prove linear stability are well understood and realized in control systems, but when controllers are switched, interpolation methods must be used. Interpolation is necessary as gain scheduled systems do not have foundational switching paradigms as part of their realization and therefore can not naturally guarantee smooth (or stable) transitions. To ensure stability between linear controllers, empirical data must be obtained through test and simulation which adds significant time and fiscal cost to development. This work examines if fuzzy controllers can provide similar response to that of gain scheduled controllers. By representing controllers as fuzzy representations, transitions between the designed linear setpoints can be smoothed by adding membership functions between defined linear controllers. However, fuzzy control lacks analytical tools to find the stability margins to test the stability of fuzzy systems.In order to provide assurance of stability and performance concerns, fuzzy controllers are translated into hybrid automata representations. Hybrid Automata (HA) theory, which is gaining popularity to represent cyber-physical systems (CPS), is an extension of finite state machines (finite automata) which blends continuous dynamics with discrete switching conditions. The hybrid representation of the fuzzy system allows reachability tools and formal methods to examine stability and desired performance characteristics. This provides evidence that a fuzzy controller can produce, at a minimum, an equally effective controller.The goal of this effort is to establish a process to use fuzzy controller design and reachability tools to provide evidence of control system key attributes. The work primarily focuses on using two reachability tools which capture flow-pipe construction in linear models. The first, SpaceEx, uses representations of continuous sets to compute an overapproximation of the reachable states. The second, HyLAA, provides a simulation-equivalent reachability representation. Through reachability evidence generated by these tools, the tested fuzzy systems show that they maintain stability over the entire range of normalized input signal.

Inspired by the Open mHealth application architecture, which emphasizes user-controlled data security, reusable common modules and inter-operability among different mHealth applications, this dissertation introduces NDNFit, a mobile health (mHealth) application built on the Named Data Networking (NDN) architecture, while offer users the familiar user experience as traditional mHealth applications. An equally important motivation for NDNFit is NDN's application-driven architecture development philosophy -- NDNFit serves as a use case to experiment with integrating multiple NDN components into one coherent application ecosystem, as well as drive the design and development of NDN architecture and protocol.During the design and implementation process of NDNFit, we identified and solved five problems. First, because NDN mandates that all data packets be authenticated, NDNFit builds a namespace and certificate management system to manage identity and certificate, and defines trust policies for consumers to verify data packets; to protect confidentiality, it employs NAC to encrypt Data content, and makes the first effort to obscure Data names. Second, NDNFit employs Named Function Networking (NFN) to implement data processing services, defines name conversion services to enable sharing of named functions across multiple mHealth applications, and designs key delegation mechanisms for named functions to properly secure processed data. Third, to provide reliable data storage service, NDNFit designs DSU command protocol for users to communication with the storage, and designs mechanisms to employ State Vector Synchronization (SVS) protocol to replicate data in a distributed data storage system. Fourth, NDNFit introduces catalog and denial of existence packets for efficient data transferring among different components. Last, NDNFit recognizes the issue of application mobility and refine forwarding hint to enable data reachability and support producer application mobility.The NDNFit design illustrates that NDN's data-centric approach to networking -- naming and securing data directly, and sharing namespace between application layer and network layer -- provides a superior solution over the existing TCP/IP based solution for Open mHealth application architecture, as NDN network primitives enable users' control over their own data and facilitate interoperability among multiple applications, without relying on underlying transport layers and other third party services. The NDNFit design also demonstrates the power of NDN naming conventions -- how Data packets are named, and what is the relationship between different Data names -- in simplifying application design, that good naming conventions can help in many aspects: enable data-centric security, speed up data dissemination, or even improve data reachability.At the end of this dissertation, we present the initial implementation of NDNFit as well as its demonstration on NDN testbed. Experimental results show that NDNFit design works well, and the lessons we learned from NDNFit design and development can benefit those of future NDN-based applications.

This Thesis presents modeling and analysis framework for video games design. Using the hybrid system framework, we tackle the problem of designing the game parameters that achieve the best compromise between the difficulty level and the winnablility of the game. Although there exist iterative processes for game design, they are often regarded as time consuming and qualitative. Moreover, changes in the game environment usually involves a series of redesigns and re-tests. Our proposed method is novel as we model a video game as a hybrid dynamical system and we apply existing tools within this framework. In particular, we solve problems such as reachability, feasibility and optimality that allow us to quantify the game attributes. In addition, the later analysis promote the use of automatic game design procedures.

The prevalence of location tracking systems has resulted in large volumes of spatiotemporal data generated every day. Addressing reachability queries on such datasets is important for a wide range of applications, such as security monitoring, surveillance, public health, epidemiology, social networks, etc. While traditional graph reachability queries have been studied extensively, little work exists on processing reachability queries on large disk-resident trajectory datasets. What makes spatiotemporal reachability queries different and challenging is that the associated graph is dynamic and space-time dependent. As the spatiotemporal dataset becomes very large over time, a solution needs to be I/O-efficient.Given two objects OS and OT, and a time interval I, a spatiotemporal reachability query identifies whether information (or physical item etc.) could have been transferred from OS to OT during I (typically indirectly through a chain of intermediate transfers). In the previous research on spatiotemporal reachability queries, it is assumed that information can be passed from one object to another instantaneously, which may not always be the case. In this dissertation, we introduce several novel reachability-based queries. For all our problems, we assume that ‘instant transfer’ is not possible, and consider reachability queries with different types of delays (processing and transfer delays), as well as queries with information decay. First, we propose the RICC (Reachability Index Construction by Contraction) framework for processing spatiotemporal reachability queries with processing delays. Next, using this framework, we address reachability queries with transfer delays (or meetings). For this purpose we design two algorithms, RICCmeetMin that precomputes some reachability events considering the shortest valid meetings duration, and RICCmeetMax which uses the longest possible meeting duration.Our next work considers reachability queries under the scenario of information decay. Such queries arise when the value of information that travels through the chain of intermediate objects decreases with each transfer. This leads to an interesting extension: if there are many different sources of information, the aggregate value of information an object can obtain varies. As a result, we examine a top-k reachability problem, identifying the k objects with the highest accumulated information. All proposed algorithms consist of two stages: preprocessing and query processing. To prune the search space during query time, they precompute and store some reachability information. This approach allows for efficient reachability query processing on large disk-resident datasets.

In the first half of this thesis, a novel approach for k-induction bounded model checking using signal domain constraints and property partitioning for proving unreachability of branches in Verilog RTL code is presented. To do this, it approach uses program slicing with respect to the variables of the property under test to generate small-sized SMT formulas that describe the change of variable values between consecutive cycles. Variable substitution is then used on these variables to generate the formula for the subsequent cycles without traversing the abstract syntax tree of the entire design. To reduce the approximation on the induction step, an addition of signal domain constraints is proposed. Moreover, we present the technique for splitting up the property in question to get a better model of the system. The later half of the thesis is concerned with presenting a technique for doing sequential vector compaction on test set generated during simulation based ATPG. Starting with a compaction framework for storing metadata and about the test vectors during generation, this work presented to methods for findind the solution of this compaction problem. The first of these two methods generate the optimum solution by converting the problem appropriate for an optimization solver. The latter method utilizes a heuristics based approach for solving the same problem which generates a comparable but sub-optimal solution while having magnitudes better time and computational efficiency.

The ability to guarantee the safety of autonomously controlled space vehicles is of great importance to help avoid accidents and ensure mission success. In this paper we investigate the safety verification of a satellite attempting to maneuver to a new position while avoiding multiple pieces of debris. We assume that the satellite, desired rendezvous point, and all debris are near the same circular orbit with dynamics modeled by Clohessy-Wiltshire-Hill (CWH) equations. We will use reachability methods to guarantee the satellite is able to reach a desired point while avoiding all debris. We will first develop a computationally efficient method for computing the Reach-Avoid set for a system modeled by CWH dynamics, and then extend this method to the minimal and maximal reach calculations. We then review a system decomposition method for computing reach sets in large dimensions and apply the methods to the debris avoidance problem. Finally, we develop computationally efficient methods to compute an under-approximation of the Reach-Avoid set and present numerical examples for single and multiple debris scenarios.

The archetype of rechargeable technology, Li-ion batteries have over the last decade benefited from improvements in material science through increased energy and power density. Although widely adopted, these batteries suffer from significant performance degradation at low temperatures, posing a challenge for automotive applications, especially during vehicle start-up. This begs the question: if one was to seek an energy optimal warm-up strategy, how would it look? Moreover, if as much as 22% of reduction in range of electric vehicles is attributable to onboard battery heating systems, would an optimal heating strategy alleviate this energy drain and at what drawback? This thesis addresses these questions. To that end, we pose and solve two energy-optimal warm-up strategies in addition to developing tools that will enable one to make prudent decisions on whether warm-up is feasible if the battery energy state falls too low. In this dissertation, we address the four main aspects of control design modeling, control, verification and adaptation. There are two primary control strategies that are designed in this dissertation and tools to analyze them are developed. The first warm-up scenario involves a receding horizon optimal control problem whose objective trades-offs increase in battery's temperature by self-heating against energy expended. The shape of battery current is restricted to be bi-directional pulses that charge and discharge the cell at relatively high frequencies via an external capacitor. The optimal control problem solves for the amplitude of the pulse train and the results clarify issues associated with capacitor size, time and lost energy stored. The second control policy is deduced by solving an optimal discharge control problem for the trajectory of power that could self-heat the cell and at the same time feed an external heater whilst minimizing the loss in state of charge. Batteries inevitably age as they are used and consequently their dynamics also change. Since both proposed methods are model based, the last of part of this dissertation proposes a novel augmented-state-space partitioning technique which can be used to design cascaded nonlinear estimators. Using this partitioning technique, the relative average estimability of the different states of the electrical and thermal model is studied and Dual Extended Kalman Filters are built and validated in simulations. All the methods developed are demonstrated via a combination of simulation and experiments on Iron Phosphate or Nickel Manganese Cobalt Li-ion battery cell which have high power capability and could be used in replacement of 12V starter batteries or 48V start-stop applications.

One of the fundamental problems in runtime verification of parallel program is to check if a predicate could become true in any global state of the system. The problem is challenging because of the nondeterministic process or thread scheduling of the system. Predicate detection alleviates this problem by analyzing the computation of the program and predicting whether the predicate could become true by exercising an alternative process schedule. The technique was first introduced by Cooper et al. and Garg et al. for distributed debugging. Later, jPredictor applies this technique for concurrent debugging. We improve the technique of predicate detection in three ways. The first part of this dissertation presents the first online-and-parallel predicate detector for general-purpose predicate detection, named ParaMount. ParaMount partitions the set of consistent global states and each subset can be enumerated in parallel using existing sequential enumeration algorithms. Our experimental results show that ParaMount speeds up the existing sequential algorithms by a factor of 6 with 8 threads. Moreover, Paramount can run along with the execution of users’ program and hence it is applicable even to non-terminating programs. The second part develops a fast enumeration algorithm, named QuickLex, for consistent global states. In comparison with the original lexical algorithm (Lex), QuickLex uses an additional O(n2) space to reduce the time complexity from O(n2) to O(n·∆(P)), where n is the number of processes or threads in the computation and ∆(P) is the maximal number of incoming edges of any event. The third part introduces Loset — a new model for parallel computations with locking constraints. We show that the reachability problem in a loset is NP-complete. To tackle the NP-completeness, we present several useful properties. Specifically, if the final global state is reachable, then all lock-free feasible global states are reachable. In addition, we show that the reachability of a global state G can be determined using a sub-computation instead of the entire computation. Moreover, we introduce the strong feasibility of a global state, which is an upper approximation of reachability that can be calculated efficiently. Our experiments show that the property accurately models the reachability for all 11 benchmarks.

Software controllers of reactive systems are ubiquitous in situations where incorrectness has a high cost. In order to place trust in the software, strong guarantees of its functional correctness are required. Reactive synthesis can be used to automatically construct software to a specification and ensure correctness. The drawback is that synthesis is computationally hard and it is infeasible to synthesise a controller for many specifications. Synthesis is formalised as a game between the controller and its environment. In this thesis we consider safety specifications that define the winning condition of the game for the controller as never allowing the game to visit an error state. The usual approach for solving controller synthesis is to compute the set of all winning states in the system and construct a controller that never deviates from this set. The set may be very large so it is standard practice to represent sets of states symbolically as a relation over the variables of the system. Binary decision diagrams (BDDs) are an efficient data structure used to store and manipulate sets of states for synthesis. The drawback of this approach is that a set of states has only one representation as a BOD and in some cases it may be exponentially large in the number of variables. The state explosion of BDDs causes controller synthesis to be infeasible on specifications with no compact representation of the set of winning states. In this thesis I propose a synthesis algorithm that constructs an approximation of the set of safe states that is sufficient to show correctness of the controller. The algorithm constructs an abstraction of the game and searches for a candidate strategy for the controller. Counterexamples are used to refine the strategy until it is winning for the game abstraction. Similar to bounded model checking, a SAT solver is used to efficiently implement the search for a counterexample trace. When a strategy is found to be winning in the abstraction of the game an approximation of the states for which the strategy wins is extracted from the strategy via interpolation. The search continues by refining the abstraction until the approximation of winning states converges on a fixed point that is sufficient to prove that the specification is realisable.

Every year, 2.5 million people visit the emergency department accounting for $34 billion in hospital visits, stays and treatment. Financial considerations aside, falling once results in the fear of falling further increasing the likelihood of falling. For the past few decades, much work has gone into identifying those likely of falling or those who are stable by determining features that distinguish fallers from non-fallers. The holy grail of such an identification scheme would inform how much perturbation the subject can reject, which is also known as the basin of stability. The more perturbation that can be rejected, the larger the basin of stability is and the more stable the individual is. However, determining this basin of stability experimentally is an impractical task. Rather than performing perturbation experiments, recent advances in control theory and reachability analysis allow us to compute this basin of stability in simulation.In this thesis, we present a personalized and automated framework for computing the basin of stability for human motion. To do this, we first develop a tool to compute the basin of stability for dynamical systems and apply this to human motion. The utility of this framework is illustrated on the Sit-to-Stand task, though it can handle more general motions such as gait. The framework is broken down into three components. First, a representative hybrid model is chosen for the standing motion. Second, a controller is constructed to track the motion using optimal control and PD control. Third, using recent advances in hybrid occupation measures, an outer-approximation of the basin of stability is computed. We study the Sit-to-Stand action of 15 subjects (10 young and 5 older) and the computed basin of stability can differentiate between less and more stable Sit-to-Stand strategies. The contributions are the first steps towards developing a numerical method for determining the basin of stability of human motion.

Considerable research has been directed towards efficient test stimuli generation for Register Transfer Level (RTL) circuits. However, stimuli generation frameworks are still not capable of generating effective stimuli for all circuits. Some of the limiting factors are 1) It is hard to ascertain if a branch in the RTL code is reachable, and 2) Some hard-to-reach branches require intelligent algorithms to reach them. Since unreachable branches cannot be reached by any test sequence, we propose a method to deduce unreachability of a branch by looking for the possible values which a signal can take in an RTL code without explicit unrolling of the design. To the best of our knowledge, this method has been able to identify more unreachable branches than any method published in this domain, while being computationally less expensive. Moreover, some branches require very specific values on input signals in specific cycles to reach them. Conventional symbolic execution can generate those values but is computationally expensive. We propose a cycle-by-cycle restrictive symbolic execution that analyzes only a selected subset of program statements to reduce the computational cost. Our proposed method gathers information from an initial execution trace generated by any technique, to intelligently decide specific cycles where the application of this method will be helpful. This method can hybrid with simulation-based test stimuli generation methods to reduce the cost of formal verification. With this method, we were able to reach some previously unreached branches in ITC99 benchmark circuits.

As automated control systems grow in prevalence and complexity, there is an increasing demand for verification and controller synthesis methods to ensure these systems perform safely and to desired specifications. In addition, uncertain or stochastic behaviors are often exhibited (such as wind affecting the motion of an aircraft), making probabilistic verification desirable. Stochastic reachability analysis provides a formal means of generating the set of initial states that meets a given objective (such as safety or reachability) with a desired level of probability, known as the reachable (or safe) set, depending on the objective. However, the applicability of reachability analysis is limited in the scope and size of system it can address. First, generating stochastic reachable or viable sets is computationally intensive, and most existing methods rely on an optimal control formulation that requires solving a dynamic program, and which scales exponentially in the dimension of the state space. Second, almost no results exist for extending stochastic reachability analysis to systems with incomplete information, such that the controller does not have access to the full state of the system. This thesis addresses both of the above limitations, and introduces novel computational methods for generating stochastic reachable sets for both perfectly and partially observable systems. We initially consider a linear system with additive Gaussian noise, and introduce two methods for computing stochastic reachable sets that do not require dynamic programming. The first method uses a particle approximation to formulate a deterministic mixed integer linear program that produces an estimate to reachability probabilities. The second method uses a convex chance-constrained optimization problem to generate an under-approximation to the reachable set. Using these methods we are able to generate stochastic reachable sets for a four-dimensional spacecraft docking example in far less time than it would take had we used a dynamic program. We then focus on discrete time stochastic hybrid systems, which provide a flexible modeling framework for systems that exhibit mode-dependent behavior, and whose state space has both discrete and continuous components. We incorporate a stochastic observation process into the hybrid system model, and derive both theoretical and computational results for generating stochastic reachable sets subject to an observation process. The derivation of an information state allows us to recast the problem as one of perfect information, and we prove that solving a dynamic program over the information state is equivalent to solving the original problem. We then demonstrate that the dynamic program to solve the reachability problem for a partially observable stochastic hybrid system shares the same properties as for a partially observable Markov decision process (POMDP) with an additive cost function, and so we can exploit approximation strategies designed for POMDPs to solve the reachability problem. To do so, however, we first generate approximate representations of the information state and value function as either vectors or Gaussian mixtures, through a finite state approximation to the hybrid system or using a Gaussian mixture approximation to an indicator function defined over a convex region. For a system with linear dynamics and Gaussian measurement noise, we show that it exhibits special properties that do not require an approximation of the information state, which enables much more efficient computation of the reachable set. In all cases we provide convergence results and numerical examples.

Constraint answer set programming (CASP) is a declarative problem solving paradigm that combines the strengths of answer set programming (ASP) and constraint programming (CP). ASP solvers provide good computational performance by conflict-driven nogood learning (CDNL) and exploiting unfounded sets. To model features like finite domain variables and global constraints, which are naturally dealt with in CP, hybrid CASP systems have been developed that delegate CP constructs to a CP solver. While this achieved some success, hybrid systems do not seamlessly integrate with CDNL. We address this deficiency by devising two alternative approaches that accommodate CDNL. For one, we introduce a translation-based approach. The idea is to enhance ASP with CP constructs through translation to ASP. Implemented as preprocessing, this allows us to apply existing CDNL-enabled ASP systems to CASP solving. Our contributions include various generic translations that work for any constraint, and specialised encodings for important global constraints such as ALL-DIFFERENT, GRAMMAR, and REACHABILITY. We show that the inference of ASP solvers can simulate the effect of complex CP algorithms in many cases. Propagation of REACHABILITY, however, can be hindered because ASP systems disregard some consequences from unfounded sets for performance reasons. We tackle this weakness by providing more efficient methods using a reduction to the problem of finding dominators in a flowgraph. For another, we devise an extension to CDNL-based ASP solving that can integrate CP constructs via lazy nogood generation (LNG). Rather than a-priori translations into ASP, the idea of LNG is to make necessary parts of an encoding explicit on demand and only when new information can be propagated. We introduce external propagators to facilitate LNG and incorporate them into a decision procedure for ASP solving that is centred around CDNL. We then demonstrate how to seamlessly integrate constraint propagation with this framework, resulting in a novel approach to CASP solving. We have implemented a prototypical CASP system to demonstrate some key principles of our approaches. In 2013, it has successfully participated in a model and solve competition, outperforming hybrid systems.

Flapping-winged flight is very complex, and it is difficult to efficiently model the unsteady airflow and nonlinear dynamics for online control. While steady state flight is well understood, transitions between flight regimes are not readily modeled or controlled. Maneuverability in non-equilibrium flight, which birds and insects readily exhibit in nature, is necessary to operate in the types of cluttered environments that small-scale flapping-winged robots are best suited for. The advantages of flapping wings over quadrotors and fixed-wing fliers are realized in the ability to transition from forward flight to hover to gliding. Flight in the transitions between these regimes necessitates the development of novel modeling techniques and online control techniques to accurately complete these types of maneuvers.In this thesis, methods for modeling and controlling the transitions between takeoff and diving maneuvers are developed for a flapping-winged micro aerial vehicle (MAV), the H2Bird. To transition into takeoff and steady state flight, a cooperative launching system is developed for the H2Bird by carrying it on the back of a 32 gram hexapedal millirobot, the VelociRoACH. The necessary initial velocity and pitch angle are determined for take off using force data collected in a wind tunnel, and the VelociRoACH is used to reach these initial conditions for successful launch. The models for the diving maneuver are generated using an automatic piece-wise affine identification technique. The flight conditions during the maneuver are segmented into separate regions and least-squares is used to estimate affine linear models for each modeling region. These models are used to compute the reachability sets for the recovery conditions for safe diving, and linear quadratic regulator controllers are used to maintain stable conditions before and after the dive. The data-driven automatic modeling techniques and controller design processes can be extended to additional flight maneuvers.

Current generation teleoperated human-robot systems remain difficult to operate. Understanding the properties of a distant environment through the sensors on a robot is much more difficult and error prone as compared to the same perceptual judgments when the human observer is directly present in that environment. In other words, human observers have difficulty perceiving the affordances of the environment such as passability, traversability, and reachability when a robot mediates their access to the environment. This thesis presents the results of a study that measures the ability of human observers to perceive the affordance reachability using simulations of three different robots that vary in their camera configurations. Two are based on robots currently in use, and the third is a novel approach to human-robot systems that considers them a perceptual system. Observer perception of reachability varied across the three systems. Measuring the ability to perceive affordances provides a means to assess a robot as a human-sensor system. This approach contrasts with current methods, which focus on evaluating human-robot systems in search tasks (e.g., counts of targets, areas visited).

This dissertation focuses on developing novel techniques to help understand, analyze, and query large graphs by utilizing backbone structures. Network backbone depicts a core substructure which not only offers concise and highlighted topological view of original graph, but also carries a large amount of essential information, such as information flow. In this dissertation, we introduce a novel backbone structure “gate graph” to provide a simplified topological view of original graph while preserving its distance measure. A graph simplification algorithm based on set cover framework is proposed to extract gate graph. We show theoretically and empirically that both approaches considerably reduce the complexity of original graph in terms of the number of vertices.In addition, we also examine how to efficiently answer reachability query and shortest path (distance) query on large graphs, by utilizing tailored backbone structures: 1) first, to address scalability challenge in reachability query answering on massive graphs, we extract a “reachability backbone” and then leverage it to help scale the existing reachability indexing algorithms and speed up online query processing approaches; 2) secondly, to efficiently answer distance queries on large directed graphs, we present a novel labeling scheme, referred to as Highway-Centric Labeling, utilizing a directed spanning tree as highway structure. We build an interesting connection between our labeling problem and Bipartite Set Cover problem and propose an elegant algorithm with non-trivial logarithmic bound to solve it; 3) finally, we introduce a novel Hub2-Labeling approach to compute the exact shortest path between two vertices with distance no more than 6 in large social networks. Our approach significantly extends the existing landmark approach by utilizing a large number of hubs to help estimate the distance and to help reduce the search space. We demonstrate these approaches using synthetic datasets and real-world datasets to show that they achieve much better performance than existing methods, in terms of either scalability or query efficiency.

Our world today is generating huge amounts of graph data such as social networks, biological networks, and the semantic web. Many of these real-world graphs are edge-labeled graphs, i.e., each edge has a label that denotes the relationship between the two vertices connected by the edge. A fundamental research problem on these labeled graphs is how to handle the label-constraint reachability query: Can vertex u reach vertex v through a path whose edge labels are constrained by a set of labels? In this work, we introduce a novel tree-based index framework which utilizes the directed maximal weighted spanning tree algorithm and sampling techniques to maximally compress the generalized transitive closure for the labeled graphs . An extensive experimental evaluation on both real and synthetic datasets demonstrates the efficiency of our approach in answering label-constraint reachability queries.

With the increasing complexity of systems found in practical applications, the problem of controller design is often approached in a hierarchical fashion, with discrete abstractions and design methods used to satisfy high level task specifications, and continuous abstractions and design techniques used to satisfy low level control objectives. Although such a separation allows the application of mature theoretical and computational tools from the realms of computer science and control theory, the task of ensuring desired closed-loop behaviors, which results from the composition between discrete and continuous designs, often requires costly and time consuming verification and validation. This problem becomes especially acute in safety-critical applications, in which design specifications are often subject to rigorous industry standards and government regulations. Hybrid systems, which feature state trajectories evolving on a combination of discrete and continuous state spaces, have been proposed as a possible approach to reconcile the analysis and design techniques from the discrete and continuous domains under a rigorous theoretical framework. However, designing controllers for general classes of hybrid systems is a highly nontrivial task, as such a design problem inherits both the difficulty of nonlinear control, as well as the range of theoretical and computational issues introduced by the consideration of discrete switching.This dissertation describes several efforts aimed towards the development of theoretical analysis tools and computational synthesis techniques to facilitate the systematic design of feedback control policies satisfying safety and target attainability specifications with respect to subclasses of hybrid system models. The main types of problems we consider are safety/invariance problems, which involve keeping the closed-loop state trajectory within a safe set in the hybrid state space, and reach-avoid problems, which involve driving the state trajectory into a target set subject to a safety constraint. These problems are addressed within the context of continuous time switched nonlinear systems and discrete time stochastic hybrid systems, as motivated by application scenarios arising in autonomous vehicle control and air traffic management. First, we provide several design techniques and synthesis algorithms for deterministic reachability problems formulated in the setting of switched nonlinear systems, with controlled switches between discrete modes, and bounded continuous disturbances. For scenarios in which the mode transitions proceed in a known sequence, a method is discussed for designing controllers to satisfy sequential reachability specifications, consisting of a temporally ordered sequence of invariance and reach-avoid objectives. In particular, we use continuous time reachable sets to inform choices of feedback control policies within each discrete mode to satisfy both individual reachability objectives and compatibility conditions between successive modes. This technique is illustrated through an example of maneuver sequence design for automated aerial refueling of unmanned aerial vehicles. For scenarios in which the modes of a switched system can be freely selected, we describe an approach for the automated synthesis of feedback control policies achieving safety and reach-avoid objectives, under a sampled data setting. This synthesis technique proceeds by a structured reachability computation which retains information about the choice of switching controls at each discrete time instant, resulting in a set-valued policy represented in terms of a finite collection of reachable sets. Experimental results from the implementation of such control policies on a quadrotor platform to track a moving ground target show strong robustness properties in the presence of significant disturbances.Second, we provide theoretical and computational results on stochastic game and partial information formulations of probabilistic reachability problems. In the setting of a discrete time stochastic hybrid game model, zero-sum dynamic game formulations of probabilistic safety and reach-avoid problems are considered. Under an asymmetric information pattern favoring the adversary, we prove dynamic programming results for the computation of finite horizon max-min safety and reach-avoid probabilities and synthesis of deterministic max-min control policies. The implications of alternative information patterns and infinite horizon formulations are also discussed. In particular, it is shown that under a symmetric information pattern, equilibrium solutions are in general found within the class of randomized policies. The utility of this approach is illustrated through an example of pairwise aircraft conflict resolution, with a probabilistic model of wind effects. In the setting of a partially observable discrete time stochastic hybrid system, we provide a characterization of the optimal solution to partial information probabilistic safety and reach-avoid problems, which have nonstandard multiplicative and sum-multiplicative cost structures. In particular, these problems are shown to be equivalent to terminal cost and additive cost problems, by augmenting the hybrid state space with a binary random variable capturing the safety of past state evolution. Using this result, we derive a sufficient statistic in terms of a set of Bayesian filtering equations, along with an abstract dynamic programming algorithm for computing the optimal safety and reach-avoid probabilities. The practical implementation of the estimation and control algorithms, however, will depend on the existence of finite dimensional representations or approximations of the hybrid probability distribution.

Three fundamental and related problems, with applications in networks and graph databases, are the focus of this dissertation. They are: how to answer quickly whether a vertex can reach another vertex in a directed graph, using a succinct representation of the reachability information; how to route a message efficiently from a source vertex to a destination vertex and how to calculate or estimate quickly the distance between any two vertices, using very limited information stored locally at those vertices.To efficiently answer reachability queries, we introduce a novel path-tree structure to assist with the compression of transitive closure and answering reachability queries. Our path-tree generalizes the traditional tree cover approach and can produce a better compression rate for the transitive closure. We also propose a 3-hop indexing scheme with high compression rate targeting the directed graphs with higher edge-vertex ratio. In addition, we show how to effectively summarize reachability information.To efficiently route messages in a graph, we investigate three strategies of how to use a spanning tree T of a graph G to navigate in G, i.e., to move from a current vertex x towards a destination vertex y via a path close to optimal. We investigate advantages and limitations of these strategies on several families of graphs such as graphs with locally connected spanning trees, graphs with bounded length of largest induced cycle, graphs with bounded tree-length, and graphs with bounded hyperbolicity. For most of these families of graphs, the ancestry information from a Breadth-First-Search-tree guarantees short enough routing paths. In many cases, the obtained results are optimal up to a constant factor.Finally, we propose distance and routing labeling schemes for circle graphs and polygon graphs by constructing collective additive tree spanners. We show that the family of n-vertex circle graphs admits a 2-additive distance labeling scheme with O(log3n)-bit labels and O(log n) time distance decoder, and the family of n-vertex k-polygon graphs admits a 2-additive distance labeling scheme with O(log k log2n)-bit labels and O(log k) time distance decoder. Similar routing labeling schemes are also designed for these families of graphs.

Reachability routing is a newly emerging paradigm in networking, where the goal is to determine all paths between a sender and a receiver. It is becoming relevant with the changing dynamics of the Internet and the emergence of low-bandwidth wireless/ad hoc networks. This thesis presents the case for reinforcement learning (RL) as the framework of choice to realize reachability routing, within the confines of the current Internet backbone infrastructure. The setting of the reinforcement learning problem offers several advantages, including loop resolution, multi-path forwarding capability, cost-sensitive routing, and minimizing state overhead, while maintaining the incremental spirit of the current backbone routing algorithms. We present the design and implementation of a new reachability algorithm that uses a model-based approach to achieve cost-sensitive multi-path forwarding. Performance assessment of the algorithm in various troublesome topologies shows consistently superior performance over classical reinforcement learning algorithms. Evaluations of the algorithm based on different criteria on many types of randomly generated networks as well as realistic topologies are presented.