Abstract

Software is finding place in deeply embedded systems to large scale distributed systems of cloud service providers such as Amazon and Google. Due to concurrent and distributed nature of this software, it is hard to test for correctness of such systems in a foolproof manner. Model checking is now a standard technology for verifying large and complex systems. Explicit state model checking is an approach in which we build a model of the system and specify the properties it should hold. Then we construct a state transition system from the model and check if it satisfies the specified properties. There are two kinds of properties of interest: safety and liveness. The scaling of model checking, however, remains a significant challenge. Distributed model checking is an important and promising approach to tackle the problem of scale. In this thesis, we focus our attention on safety properties verification, which involves checking if the states that are generated in the transition system satisfies some predicate formulae specified in the form of assertions. The main problem here is that the number of states in the transition system grows exponentially with the number of bits required to store the state of a model at any given point of time. So the available main memory even in a server class machine is not sufficient to model check non-trivial practical models. One approach to address this problem is by using resources from a distributed collection of machines. We use two different distributed models in order to achieve the above mentioned. Our first implementation is based on vertex centric programming model. It is uses the concept of bulk synchronous parallel computing to synchronize. The second implementation uses Actor Model. We propose asynchronous algorithms for the verification and a simple reduction strategy in this implementation. The main advantage of Actor model is that it comes with a transparent way to scale from a single node to multiple nodes, without having to change any of the implementation.

Abstract

Historically, row store has been the most popular storage layout to store relational data in commercial databases. With the advent of column store, it became possible to improve the efficiency of real world queries by storing and operating on each attribute separately. Traditional row store has the disadvantage of reading irrelevant attributes into main memory, when only a few attributes are queried. Whereas, column store suffers from large “stitching” costs if the number of attributes queried are large. Moreover, traditional row store suffers from a large amount of cache misses whereas column store is cache-efficient since irrelevant attributes are not brought into the cache. Recent years have also witnessed an in-memory revolution in databases, wherein a large part of the data is majorly stored in RAM thereby removing the I/O overhead. Although the concept of in-memory databases has been around for a long time, commercial and practical implementations have been feasible only recently due to the falling prices of RAM coupled with its increasing capacity. However, research has shown that most of the time in such systems is lost due to the cache misses. Most commercial row and column storage systems do not optimize for the layout of data in the available main memory to improve performance. In this thesis, we introduce an intuitive, hybrid combination of row and column storage mechanisms to reduce the I/O cost and cache misses for ad-hoc read-only queries. Our system acts as a commercial off-the-shelf (COTS) solution on top of existing databases. We leverage the concept of vertical fragmentation by analyzing the historical query load and grouping certain related attributes together to form vertical fragments. The attributes within a particular fragment are selected on the basis of their co-occurrence over all queries. These generated fragments are then stored as materialized views in the main memory buffer. The more ”valuable” fragments are given priority when allocating space in the main memory. We also present algorithms to optimally select the required data from these fragments for a given query so as to reduce the total I/O calls to the secondary storage. Moreover, this placement of data in main memory is cache-efficient, thereby improving the performance. We show that on average, FAST executes queries up-to an order of magnitude faster than row storage and as much as twice as fast than column storage for an ad-hoc workload. We demonstrate the superior performance of FAST on TPC-H benchmark queries as well. Our results show superior performance of FAST on multiple TPC- H queries. We also present techniques to automatically adapt the main memory layout to a changing workload Although the framework described by this thesis largely focuses on the main memory and the secondary storage for data layout, our algorithms and techniques have been designed to work for any generic multi-level data storage system. For example, we can leverage our approach in a three level storage model consisting of the main memory, an intermediate SSD layer and the secondary storage. This is possible because we deal with the logical database layer rather than modifying the physical layer to achieve performance gains. Moreover, our storage model is designed to support both OLAP (online analytical processing) and OLTP (online transaction processing) workloads. In fact, one of the advantages of our framework is the ease of implementation on top of existing databases systems. To this end, we apply FAST in the context of distributed databases. We also discuss an in-grained applica- tion of FAST for distributed databases which would result in larger query efficiency gains at the cost of implementation. We hope this discussion to open up new areas of systems research in this direction.

Abstract

Real world images depict varying scenes, actions and multiple objects interacting with each other. We consider the fundamental Computer Vision problem of image annotation, where an image needs to be automatically tagged with a set of discrete labels that best describe its semantics. As more and more digital images become available, image annotation can help in the automatic archival and retrieval of large image collections. Being at the heart of image understanding, image annotation can also assist in other visual learning tasks, such as image captioning, scene recognition, multi-object recognition, etc.. With the advent of deep neural networks, recent research has achieved ground-breaking results in single-label image classification. However, for images representing the real world, containing different objects in varying scales and viewpoints, modelling the semantic relationship between images and all of their associated labels continues to remain a challenging problem. Additional challenges are posed from class-imbalance, incomplete labelling, label-ambiguity and several other issues that are commonly observed in the image annotation datasets. In this thesis, we study the image annotation task from two aspects. First, we bring to attention some of the core issues in the image annotation domain related to dataset properties and evaluation metrics that inherently affect the annotation performance of existing approaches to a significant extent. To examine these key aspects, we evaluate ten benchmark image annotation techniques on five popular datasets using the same baseline features, and perform thorough empirical analyses. With novel experiments, we explore possible reasons behind variations in per-label versus per-image evaluation criteria and discuss when each one of these should be used. We investigate dataset specific biases and propose new quantitative measures to quantify the degree of image and label diversity in a dataset, that can also be useful in developing new image annotation datasets. We believe the conclusions derived in this analysis would be helpful in making systematic advancements in this domain. Second, we attempt to address the annotation task by a CNN-RNN framework that jointly models label dependencies in an image while annotating it. We base our approach on the premise that labels corresponding to different visual concepts in an image share rich semantic relationships among them (e.g., “sky” is related to “cloud”). We follow recent works that have explored the CNN-RNN style models due to RNN’s capacity to model higher-order dependencies, but are limited in their approach to train the RNN in a pre-defined label order sequence. We overcome this limitation and propose a new method to learn multiple label prediction paths. We evaluate our proposed method on a number of popular and relevant datasets and achieve superior results compared to existing CNN-RNN based approaches. We also discuss the scope of the CNN-RNN framework in the context of image annotation.

Abstract

The advent of indoor personal mobile robots has clearly demonstrated their utility in assisting humans at various places such as workshops, offices, homes, etc. One of the most important cases in such autonomous scenarios is where the robot has to search for certain objects in large rooms. Exploring the whole room would prove to be extremely expensive in terms of both computing power and time. To address this issue, we demonstrate a fast algorithm to reduce the search space by identifying possible object locations as two classes, namely - Support Structures and Clutter. Support Structures are plausible object containers in a scene, such as tables, chairs, sofas, etc. Clutter refers to places where there seem to be several objects but cannot be clearly distinguished. In this thesis, we propose an algorithm to identify potential object locations using a Support Vector Machine(SVM) learned over the features extracted from the depth map and the RGB image of the scene, which further culminates into a densely connected Conditional Random Field(CRF) formulated over the image of the scene. The inference over the CRF leads to the assignment of the labels - support structure, clutter, others to each pixel. Further to this, we also explore deep neural network-based algorithms for detecting objects from far off spaces. Small object detection plays an important role in robot navigation, scene understanding, etc as most of the objects observed are generally small until observed from close. Although current object detection algorithms show state-of-the-art accuracy on multiple datasets, they fail to accurately detect small objects. We propose a deep neural network architecture which is a variant of the SSD network. The proposed architecture uses spatial context to efficiently detect small objects without much reduction in the speed. This is close to mimicking human behavior where we search for small objects in the vicinity of larger related objects. The architecture proposed shows a better accuracy for small object detection compared to the conventional SSD. We also explore the use of a context network-based method to improve the accuracy of small object detection. We formulate this as a label space learning method compared to an end-to-end learning algorithm. We use the state-of-the-art YOLO network and train a context network as an auxiliary task for better localization of the small objects in an image. We demonstrate improvements in the object detection accuracy for small objects compared to the YOLO v2 method.

Abstract

Heme, the second most abundant tetrapyrrole, serves as the cofactor for proteins involved in respiration and metabolism. Heme is synthesized through a well conserved and established heme biosynthetic pathway in all eukaryotes and most prokaryotes. Hydroxymethylbilane synthase (HMBS), also known as porphobilinogen deaminase (HMBS; EC 2.5.1.61), is the third enzyme in the heme biosynthetic pathway. It catalyzes the stepwise polymerization of four molecules of porphobilinogen (PBG) into the linear tetrapyrrole, 1-hydroxymethylbilane (HMB). In yeast, apart from 5-aminolevulinic acid dehydratase (ALAD), HMBS has been proposed to play a rate limiting role in the heme biosynthetic pathway. In humans, mutations of HMBS have been linked to acute intermittent porphyria (AIP). In vitro studies on HMBS have suggested certain residues with catalytic importance, but their specific role in the catalysis and the chain elongation is unclear. In the current thesis, classical and quantum mechanical calculations have been used to understand the structural dynamics and catalytic mechanism of HMBS. Molecular dynamics (MD) simulations of the E. coli HMBS through the different stages of pyrrole chain elongation suggested the importance of domain movements and the active site loop movement in the polymerization of four units of PBG. However, in the human HMBS (hHMBS), an additional 29-residue insert wedged between domains 1 and 3 prevents the domain motions. In hHMBS, the cofactor turn movement along with minor domain motions provides space for the addition of first two PBG moieties to the dipyrromethane cofactor, while the movement of the active-site loop away from the active-site region facilitates the accommodation of the next two PBG moieties. Residues R26, D99 and R167 are proposed to be important for the catalysis based on MD simulations and earlier hypothesis. The findings from MD simulations provide a basis to study the catalytic mechanism using quantum mechanical (QM) and QM/MM calculations. The QM calculations were performed on a cluster model consisting of the active site of hHMBS enzyme. The addition of one molecule of PBG to the cofactor is carried out in four steps: (1) protonation of the PBG substrate; (2) deamination of PBG; (3) electrophilic addition of the deaminated substrate to the terminal pyrrole ring of the enzyme-bound cofactor and (4) deprotonation at the carbon atom at the α-position of the penultimate ring. The rate limiting step for the complete mechanism was found to be the deamination of the PBG moiety. The QM/MM calculations demonstrated the significance of protein environment in obtaining accurate energies for the catalytic mechanism. The findings from this study provide a detailed understanding of the chain elongation mechanism using multi-scale modeling and would assist in future work aimed at modulating the activity of HMBS.

Abstract

Color Fundus (CF) imaging and Optical Coherence Tomography (OCT) are widely used by ophthalmologists to visualize the retinal surface and the intra-retinal tissue layers respectively. An accurate segmentation of the anatomical structures in these images is necessary to visualize and quantify the structural deformations that characterize retinal diseases such as Glaucoma, Diabetic Macular Edema (DME) and Age-related Macular Degeneration (AMD). In this thesis, we propose different frameworks for the automatic extraction of the boundaries of relevant anatomical structures in CF and OCT images. First, we address the problem of the segmentation of Optic Disc (OD) and Optic Cup (OC) in CF images to aid in the detection of Glaucoma. We propose a novel boundary-based Conditional Random Field (CRF) framework to jointly extract both the OD and OC boundaries in a single optimization step. Although OC is characterized by the relative drop in depth from the OD boundary, the 2D CF images lack explicit depth information. The proposed method estimates depth from CF images in a supervised manner using a coupled, sparse dictionary trained on a set of image-depth map (derived from OCT) pairs. Since our method requires a single CF image per eye during testing it can be employed in the large-scale screening of glaucoma where expensive 3D imaging is unavailable. Next, we consider the task of the intra-retinal tissue layer segmentation in cross-sectional OCT images which is essential to quantify the morphological changes in specific tissue layers caused by AMD and DME. We propose a supervised CRF framework to jointly extract the eight layer boundaries in a single optimization step. In contrast to the existing energy mini-mization based segmentation methods that employ handcrafted energy cost terms, we linearly parameterize the total CRF energy to allow the appearance features for each layer and the relative weights of the shape priors to be learned in a joint, end-to-end manner by employing the Structural Support Vector Machine formulation. The proposed method can aid the oph-thalmologists in the quantitative analysis of structural changes in the retinal tissue layers for clinical practice and large-scale clinical studies. Next, we explore the Level Set based Deformable Models (LDM) which is a popular energy minimization framework for medical image segmentation. We model the LDM as a novel Recurrent Neural Network (RNN) architecture called the Recurrent Active Contour Evolution Network (RACE-net). In contrast to the existing LDMs, RACE-net allows the curve evolution velocities to be learned in an end-to-end manner while minimizing the number of network parameters, computation time and memory requirements. Consistent performance of RACE-net on a diverse set of segmentation tasks such as the extraction of OD and OC in CF images, cell nuclei in histopathological images and left atrium in cardiac MRI volumes demonstrates its utility as a generic, off-the-shelf architecture for biomedical segmentation. Segmentation has many clinical applications especially in the area of computer aided diagnostics. We close this dissertation with some illustrative applications of the segmentation information. We consider the case of disease detection in CF and OCT images. We explore and benchmark two classification strategies for the detection of glaucoma from CF images based on deep learning and handcrafted features respectively. Both the methods use a combination of appearance features directly derived from the CF image and structural features derived from the OD and OC segmentation. We also construct a Normative Atlas for the macular OCT volumes to aid in the detection of AMD. The irregularities in the Bruch’s membrane caused by the deposit of drusen are modeled as deviations from the normal anatomy represented by the Atlas Mean Template

Abstract

The process of imaging converts a 3D world into a 2D image. This process is inherently lossy, making the problem of understanding the world, ill-posed. During the imaging process, a light ray emanating from a source bounces of different surfaces, interacting with them according to the surface properties (albedo, color, specularity) before reaching the camera. The structure that we see in an image is primarily based on the final surface from which the light was reflected, except when that surface is highly specular (mirror-like). In this work, we explore imaging techniques the recover both the structure and surface properties of a scene. For structure recovery, we extend the idea of stereo imaging and present a practical solution to capture a complete 360◦ panorama using a single camera. Current approaches either use a moving camera for capturing multiple images of a scene, which are then stitched together to form the final panorama, or use multiple cameras that are synchronized. A moving camera limits the solution to static scenes, while multi-camera solutions require dedicated calibrated setups. Our approach improves upon the existing solutions in two significant ways: It solves the problem using a single camera, thus minimizing the calibration problem and providing us the ability to convert any digital camera into a stereo panoramic capture device. It captures all the light rays required for stereo panoramas in a single frame using a compact custom designed mirror, thus making the design practical to manufacture and easier to use. We analyze the optimality of the design as well as present panoramic stereo and depth estimation results. The methods for structure recovery, including stereo are often fooled when the surface is highly specular. To alleviate this, we propose an active-illumination based method to detect and segment mirror-like surfaces in a scene. In computer vision, many active illumination techniques employ Projector-Camera systems to extract useful information from the scenes. Known illumination patterns are projected onto the scene and their deformations in the captured images are then analyzed. We observe that the local frequencies in the captured pattern for the mirror-like surfaces is different from the projected pattern. This property allows us to design a custom Projector-Camera system to segment mirror-like surfaces by analyzing the local frequencies in the captured images. The system projects a sinusoidal pattern and capture the images from projector’s point of view. We present segmentation results for the scenes including multiple reflections and inter-reflections from the mirror-like surfaces. The method can further be used in the separation of direct and global components for the mirror-like surfaces by illuminating the non-mirror-like objects separately. We show how our method is also useful for accurate estimation of shape of the non-mirror-like regions in the presence of mirror-like regions in a scene.

Abstract

Among the extreme climate events, droughts are the most widespread and slowly developing atmo-spheric hazards which remain for a long duration affecting natural resources, environment, and people.Drought is a temporary deviation from normal weather conditions. It corresponds to the failure of spa-tial and temporal precipitation and water availability and therefore consequent impact on agriculture,ecosystem and socioeconomic activities of human being. Understanding the drought characteristics in the context of climate change is critical for water resources management in water stressed countries such as India. The frequency of severe and widespread multi-year droughts has increased in India during the recent decades due to the erratic summer monsoon and increase in air temperature and thereby creating a huge damage to crops and society. India has experienced 23 large-scale droughts starting from 1891 to 2009 and the frequency of droughts is increasing. In this context, several drought indices have been developed, which evaluate the deviation of climate variables in a given year from the normal conditions. These drought indices serve as monitoring tools and operational indicators for regional water resources management. The Standardized Precipitation and Evapotranspiration Index (SPEI) became one of the popular drought indices in the context of increasing temperatures under global warming conditions in recent periods. The SPEI is estimated by fitting a probability distribution to the difference between Precipita- tion (P) and Potential Evapotranspiration (PET) (P-PET), which represents the climatic water balance. SPEI has been widely used in the drought characterization for the Indian context but none of the drought studies analyzed the applicability of SPEI in the Indian context. So, in this study, the applicability of the SPEI over India has been evaluated and modified to account for the spatio-temporal heterogeneity of rainfall and seasonality present due to the monsoon rainfall variability. The choice of an inappropriate probability distribution may lead to bias in the index values leading to distorted drought severity. Further, application of SPEI with a single probability distribution all over India may not be a meaningful index due to the large spatial heterogeneity in the rainfall patterns at various temporal scales of Indian monsoon rainfall. So, the ability of a group of candidate probability distributions over seven meteorological homogeneous zones of India has been evaluated. The results suggested that the Log-Logistic distribution which was used in the original formulation of SPEI was not the best distribution to fit the water balance series for the Indian context. Pearson type III distribution for shorter time scales (3 and 6 months) and GEV distribution for longer time scales (12 and 24 months) have been identified as the best distributions for fitting SPEI for Indian case study. India being a country associated with strong seasonal rainfall (80% rain in June-September) it is important for any drought index to represent the seasonality in the index values. The study analyzed the strength of SPEI in capturing the seasonality in the drought assessment. The results of the study revealed that SPEI in its original formulation was unable to capture the seasonal aspect of the rainfall in the Indian context. The study makes use water balance deficits instead of water balance values itself to capture the seasonality of Indian monsoon rainfall in the drought estimation. Furthermore, suitability of Actual Evapotranspiration (AET), which can account for both water and energy based evaporative demands, in drought characterization using SPEI is unexplored for Indian context. In this study we have divided India into water and energy limited zones and compared the drought characteristics with PET and AET. The research findings of the study reveal that use of AET in the drought categorisation provides more insight towards the drought assessment for water-limited zones. The proposed modified SPEI has been identified as a better drought index in characterisation of various drought characteristics with better agreement with remote sensing-based drought indices, which accounts for the energy budget, canopy transpiration, soil evaporation and open water evaporation of a region. The global land surface in extreme drought is predicted to increase from 1-3% for the present day to 30% by the 2090s (International Panel on Climate Change (IPCC), Assessment Report 4). More intense droughts and increased precipitation variability lead to increased stresses to water, agriculture and economic activities (IPCC AR5 WG2 Ch26 Exec. Summary). The severity of droughts has been reported to be increasing in many parts of the Indian sub-continental basins under climate change. The present study used the projections of precipitation and temperatures based on General Circulation Models (GCMs) outputs to study the climate change i

Abstract

Finding whether a graph is k-connected, and identifying its k-connected components is a fundamental problem in graph theory. For this reason, there have been several algorithm for this problem in both sequential and parallel settings. Several recent sequential and parallel algorithms for k-connectivity rely on one or more breadth-first traversals of the input graph. It can be also noticed that the time spent by the algorithms on BFS operations is usually a significant portion of the overall runtime of the algorithm. While BFS can be made very efficient in a sequential setting, the same cannot be said in the case of parallel environments. A major factor in this difficulty is due to the inherent requirement to use a shared a queue, balance work among multiple threads in every round, synchronization, and the like. Optimizing the execution of BFS on many current parallel architectures is therefore quite challenging. In this thesis, we present the first GPU algorithms and implementations for 2- and 3-connectivity. We improve upon them through the use of certificates to reduce the size of the input graph and provide the fastest implementations yet. We also study how one can, in the context of algorithms for graph connectivity, mitigate the practical inefficiency of BFS operations in parallel. Our technique suggests that such algorithms may not require a BFS of the input graph but actually can work with a sparse spanning subgraph of the input graph. The incorrectness introduced by not using a BFS spanning tree can then be offset by further post-processing steps on suitably defined small auxiliary graphs. We apply our technique to our GPU implementations for 2- and 3- connectivity and improve upon them further by a factor of 2.2x and 2.1x respectively

Abstract

Model Predictive Control(MPC) is a powerful optimization strategy for feedback control which is being used increasingly for Motion planning in autonomous driving. However there are two key restrictions on using MPC. One is the requirement of high performance computational resources as it performs full optimization for every time step. The other is requirement of an accurate predictive model which is less variant to various initializations in multiple scenarios.In this thesis, We propose a new model predictive control formulation for autonomous driving. The novelty of our MPC stems from the following results. Firstly, we adopt an alternating minimization approach wherein linear velocities and angular accelerations are alternately optimized. We show that in contrast to the joint optimization, the alternating minimization exploits the structure of the problem better, which in turn translates to a reduction in computation time. Secondly, our MPC explicitly incorporates the time-dependent non-linear actuator dynamics that captures the transient response of the vehicle for a given commanded velocity. This added complexity improves the predictive component of MPC, resulting in an improved margin of inter-vehicle distance during complex urban scenarios like occlusion during overtaking, lane-change, etc. Although past works have also incorporated actuator dynamics within MPC, there have been very few attempts towards coupling actuator dynamics to collision avoidance constraints through the non-holonomic motion model of the vehicle and analyzing the resulting behavior. We use a high fidelity simulator to benchmark our actuator dynamics augmented MPC with other related approaches in terms of metrics like inter-vehicle distance, trajectory smoothness, and velocity overshoot. Planning frameworks for autonomous vehicles must be robust and computationally efficient for realtime realization. At the same time, they should accommodate the unpredictable behavior of the other participants and produce safe trajectories. In this thesis, we also present a computationally, the efficient hierarchical planning framework for autonomous vehicles. This framework can generate safe trajectories in complex driving scenarios, which are commonly encountered in urban traffic settings. The first level of the proposed framework constructs a Model Predictive Control(MPC) routine using an efficient difference of convex programming approach, that generates smooth and collision-free trajectories. The constraints on curvature and road boundaries are seamlessly integrated into this optimization routine. The second layer is mainly responsible for handling the unpredictable behaviors that are typically exhibited by the other participants of traffic. It is built along the lines of time scaled collision cone(TSCC) which optimize for the velocities along the trajectory to handle such disturbances. We additionally show that our framework maintains an optimal balance between temporal and path deviations while executing safe trajectories. To demonstrate the efficacy of the presented framework, we validated it in extensive simulations in different driving scenarios like overtaking, lane merging and jaywalking amongst many dynamic obstacles.