OpenRaiser/Intern-Atlas huggingface dataset:
Decentralized Autonomous Navigation Strategies for Multi-Robot Search and Rescue
Venue: arXiv cs.RO 2016
Year: 2016

In this report, we try to improve the performance of existing approaches for search operations in multi-robot context. We propose three novel algorithms that are using a triangular grid pattern, i.e., robots certainly go through the vertices of a triangular grid during the search procedure. The main advantage of using a triangular grid pattern is that it is asymptotically optimal in terms of the minimum number of robots required for the complete coverage of an arbitrary bounded area. We use a new topological map which is made and shared by robots during the search operation. We consider an area that is unknown to the robots a priori with an arbitrary shape, containing some obstacles. Unlike many current heuristic algorithms, we give mathematically proofs of convergence of the algorithms. The computer simulation results for the proposed algorithms are presented using a simulator of real robots and environment. We evaluate the performance of the algorithms via experiments with real robots. We compare the performance of our own algorithms with three existing algorithms from other researchers. The results demonstrate the merits of our proposed solution. A further study on formation building with obstacle avoidance for a team of mobile robots is presented in this report. We propose a decentralized formation building with obstacle avoidance algorithm for a group of mobile robots to move in a defined geometric configuration. Furthermore, we consider a more complicated formation problem with a group of anonymous robots; these robots are not aware of their position in the final configuration and need to reach a consensus during the formation process. We propose a randomized algorithm for the anonymous robots that achieves the convergence to a desired configuration with probability 1. We also propose a novel obstacle avoidance rule, used in the formation building algorithm.
Finalizing tentative matches from truncated preference lists
Venue: arXiv cs.GT 2016
Year: 2016

Consider the standard hospitals/residents problem, or the two-sided many-to-one stable matching problem, and assume that the true preference lists of both sides are complete and strict. The lists actually submitted, however, are truncated. Let I be such a truncated instance. When we apply the resident-proposing deferred acceptance algorithm of Gale and Shapley to I, the algorithm produces a set of tentative matches (resident-hospital pairs). We say that a tentative match in this set is finalizable in I if it is in the resident-optimal stable matching for every completion of I (a complete instance of which I is a truncation). We study the problem we call FTM (Finalizability of Tentative Matches) of deciding if a given tentative match is finalizable in a given truncated instance. We first show that FTM is coNP-complete, even in the stable marriage case where the quota of each hospital is restricted to be 1. We then introduce and study a special case: we say that a truncated instance is resident-minimal, if further truncation of the preference lists of the residents inevitably changes the set of tentative matches. Resident-minimal instances are not only practically motivated but also useful in natural backtrack computations for the general case. We give a computationally useful characterization of negative instances of FTM in this special case, which, for instance, can be used to formulate an integer program for FTM. For the stable marriage case, in particular, this characterization yields a polynomial time algorithm to solve FTM for resident-minimal instances. On the other hand, we show that FTM remains coNP-complete for resident-minimal instances, if the maximum quota of the hospitals is 2 or larger. We also give a polynomial-time decidable sufficient condition for a tentative match to be finalizable in the general case.
From Query to Usable Code: An Analysis of Stack Overflow Code Snippets
Venue: arXiv cs.SE 2016
Year: 2016

Enriched by natural language texts, Stack Overflow code snippets are an invaluable code-centric knowledge base of small units of source code. Besides being useful for software developers, these annotated snippets can potentially serve as the basis for automated tools that provide working code solutions to specific natural language queries. With the goal of developing automated tools with the Stack Overflow snippets and surrounding text, this paper investigates the following questions: (1) How usable are the Stack Overflow code snippets? and (2) When using text search engines for matching on the natural language questions and answers around the snippets, what percentage of the top results contain usable code snippets? A total of 3M code snippets are analyzed across four languages: C\#, Java, JavaScript, and Python. Python and JavaScript proved to be the languages for which the most code snippets are usable. Conversely, Java and C\# proved to be the languages with the lowest usability rate. Further qualitative analysis on usable Python snippets shows the characteristics of the answers that solve the original question. Finally, we use Google search to investigate the alignment of usability and the natural language annotations around code snippets, and explore how to make snippets in Stack Overflow an adequate base for future automatic program generation.
Extended Hardness Results for Approximate Gröbner Basis Computation
Venue: arXiv cs.SC 2016
Year: 2016

Two models were recently proposed to explore the robust hardness of Gröbner basis computation. Given a polynomial system, both models allow an algorithm to selectively ignore some of the polynomials: the algorithm is only responsible for returning a Gröbner basis for the ideal generated by the remaining polynomials. For the $q$-Fractional Gröbner Basis Problem the algorithm is allowed to ignore a constant $(1-q)$-fraction of the polynomials (subject to one natural structural constraint). Here we prove a new strongest-parameter result: even if the algorithm is allowed to choose a $(3/10-ε)$-fraction of the polynomials to ignore, and need only compute a Gröbner basis with respect to some lexicographic order for the remaining polynomials, this cannot be accomplished in polynomial time (unless $P=NP$). This statement holds even if every polynomial has maximum degree 3. Next, we prove the first robust hardness result for polynomial systems of maximum degree 2: for the $q$-Fractional model a $(1/5-ε)$ fraction of the polynomials may be ignored without losing provable NP-Hardness. Both theorems hold even if every polynomial contains at most three distinct variables. Finally, for the Strong $c$-partial Gröbner Basis Problem of De Loera et al. we give conditional results that depend on famous (unresolved) conjectures of Khot and Dinur, et al.
Bounded Model Checking for Probabilistic Programs
Venue: arXiv cs.PL 2016
Year: 2016

In this paper we investigate the applicability of standard model checking approaches to verifying properties in probabilistic programming. As the operational model for a standard probabilistic program is a potentially infinite parametric Markov decision process, no direct adaption of existing techniques is possible. Therefore, we propose an on-the-fly approach where the operational model is successively created and verified via a step-wise execution of the program. This approach enables to take key features of many probabilistic programs into account: nondeterminism and conditioning. We discuss the restrictions and demonstrate the scalability on several benchmarks.
Boundary modeling in model-based calibration for automotive engines via the vertex representation of the convex hulls
Venue: arXiv cs.CG 2016
Year: 2016

When using the convex hull approach in the boundary modeling process, Model-Based Calibration (MBC) software suites -- such as Model-Based Calibration Toolbox from MathWorks -- can be computationally intensive depending on the amount of data modeled. The reason for this is that the half-space representation of the convex hull is used. We discuss here another representation of the convex hull, the vertex representation, which proves capable to reduce the computational cost. Numerical comparisons in this article are executed in MATLAB by using MBC Toolbox commands, and show that for certain conditions, the vertex representation outperforms the half-space representation.
Bitcoin Beacon
Venue: arXiv cs.CR 2016
Year: 2016

We examine a protocol $π_{\text{beacon}}$ that outputs unpredictable and publicly verifiable randomness, meaning that the output is unknown at the time that $π_{\text{beacon}}$ starts, yet everyone can verify that the output is close to uniform after $π_{\text{beacon}}$ terminates. We show that $π_{\text{beacon}}$ can be instantiated via Bitcoin under sensible assumptions; in particular we consider an adversary with an arbitrarily large initial budget who may not operate at a loss indefinitely. In case the adversary has an infinite budget, we provide an impossibility result that stems from the similarity between the Bitcoin model and Santha-Vazirani sources. We also give a hybrid protocol that combines trusted parties and a Bitcoin-based beacon.
Abnormal Subspace Sparse PCA for Anomaly Detection and Interpretation
Venue: arXiv cs.NA 2016
Year: 2016

The main shortage of principle component analysis (PCA) based anomaly detection models is their interpretability. In this paper, our goal is to propose an interpretable PCA-based model for anomaly detection and interpretation. The propose ASPCA model constructs principal components with sparse and orthogonal loading vectors to represent the abnormal subspace, and uses them to interpret detected anomalies. Our experiments on a synthetic dataset and two real world datasets showed that the proposed ASPCA models achieved comparable detection accuracies as the PCA model, and can provide interpretations for individual anomalies.
Joint Learning of Sentence Embeddings for Relevance and Entailment
Venue: arXiv cs.CL 2016
Year: 2016

We consider the problem of Recognizing Textual Entailment within an Information Retrieval context, where we must simultaneously determine the relevancy as well as degree of entailment for individual pieces of evidence to determine a yes/no answer to a binary natural language question. We compare several variants of neural networks for sentence embeddings in a setting of decision-making based on evidence of varying relevance. We propose a basic model to integrate evidence for entailment, show that joint training of the sentence embeddings to model relevance and entailment is feasible even with no explicit per-evidence supervision, and show the importance of evaluating strong baselines. We also demonstrate the benefit of carrying over text comprehension model trained on an unrelated task for our small datasets. Our research is motivated primarily by a new open dataset we introduce, consisting of binary questions and news-based evidence snippets. We also apply the proposed relevance-entailment model on a similar task of ranking multiple-choice test answers, evaluating it on a preliminary dataset of school test questions as well as the standard MCTest dataset, where we improve the neural model state-of-art.
An almost ideal coordination mechanism for unrelated machine scheduling
Venue: arXiv cs.GT 2016
Year: 2016

Coordination mechanisms aim to mitigate the impact of selfishness when scheduling jobs to different machines. Such a mechanism defines a scheduling policy within each machine and naturally induces a game among the selfish job owners. The desirable properties of a coordination mechanism includes simplicity in its definition and efficiency of the outcomes of the induced game. We present a broad class of coordination mechanisms for unrelated machine scheduling that are simple to define and we identify one of its members (mechanism \Dcoord) that is superior to all known mechanisms. \Dcoord\ induces potential games with logarithmic price of anarchy and only constant price of stability. Both bounds are almost optimal.
Formal Modelling, Testing and Verification of HSA Memory Models using Event-B
Venue: arXiv cs.LO 2016
Year: 2016

The HSA Foundation has produced the HSA Platform System Architecture Specification that goes a long way towards addressing the need for a clear and consistent method for specifying weakly consistent memory. HSA is specified in a natural language which makes it open to multiple ambiguous interpretations and could render bugs in implementations of it in hardware and software. In this paper we present a formal model of HSA which can be used in the development and verification of both concurrent software applications as well as in the development and verification of the HSA-compliant platform itself. We use the Event-B language to build a provably correct hierarchy of models from the most abstract to a detailed refinement of HSA close to implementation level. Our memory models are general in that they represent an arbitrary number of masters, programs and instruction interleavings. We reason about such general models using refinements. Using Rodin tool we are able to model and verify an entire hierarchy of models using proofs to establish that each refinement is correct. We define an automated validation method that allows us to test baseline compliance of the model against a suite of published HSA litmus tests. Once we complete model validation we develop a coverage driven method to extract a richer set of tests from the Event-B model and a user specified coverage model. These tests are used for extensive regression testing of hardware and software systems. Our method of refinement based formal modelling, baseline compliance testing of the model and coverage driven test extraction using the single language of Event-B is a new way to address a key challenge facing the design and verification of multi-core systems.
Self-Reflective Risk-Aware Artificial Cognitive Modeling for Robot Response to Human Behaviors
Venue: arXiv cs.RO 2016
Year: 2016

In order for cooperative robots ("co-robots") to respond to human behaviors accurately and efficiently in human-robot collaboration, interpretation of human actions, awareness of new situations, and appropriate decision making are all crucial abilities for co-robots. For this purpose, the human behaviors should be interpreted by co-robots in the same manner as human peers. To address this issue, a novel interpretability indicator is introduced so that robot actions are appropriate to the current human behaviors. In addition, the complete consideration of all potential situations of a robot's environment is nearly impossible in real-world applications, making it difficult for the co-robot to act appropriately and safely in new scenarios. This is true even when the pretrained model is highly accurate in a known situation. For effective and safe teaming with humans, we introduce a new generalizability indicator that allows a co-robot to self-reflect and reason about when an observation falls outside the co-robot's learned model. Based on topic modeling and two novel indicators, we propose a new Self-reflective Risk-aware Artificial Cognitive (SRAC) model. The co-robots are able to consider action risks and identify new situations so that better decisions can be made. Experiments both using real-world datasets and on physical robots suggest that our SRAC model significantly outperforms the traditional methodology and enables better decision making in response to human activities.
Viziometrics: Analyzing Visual Information in the Scientific Literature
Venue: arXiv cs.SI 2016
Year: 2016

Scientific results are communicated visually in the literature through diagrams, visualizations, and photographs. These information-dense objects have been largely ignored in bibliometrics and scientometrics studies when compared to citations and text. In this paper, we use techniques from computer vision and machine learning to classify more than 8 million figures from PubMed into 5 figure types and study the resulting patterns of visual information as they relate to impact. We find that the distribution of figures and figure types in the literature has remained relatively constant over time, but can vary widely across field and topic. Remarkably, we find a significant correlation between scientific impact and the use of visual information, where higher impact papers tend to include more diagrams, and to a lesser extent more plots and photographs. To explore these results and other ways of extracting this visual information, we have built a visual browser to illustrate the concept and explore design alternatives for supporting viziometric analysis and organizing visual information. We use these results to articulate a new research agenda -- viziometrics -- to study the organization and presentation of visual information in the scientific literature.
Accelerated Evaluation of Automated Vehicles Safety in Lane Change Scenarios Based on Importance Sampling Techniques
Venue: arXiv cs.RO 2016
Year: 2016

Automated vehicles (AVs) must be evaluated thoroughly before their release and deployment. A widely-used evaluation approach is the Naturalistic-Field Operational Test (N-FOT), which tests prototype vehicles directly on the public roads. Due to the low exposure to safety-critical scenarios, N-FOTs are time-consuming and expensive to conduct. In this paper, we propose an accelerated evaluation approach for AVs. The results can be used to generate motions of the primary other vehicles to accelerate the verification of AVs in simulations and controlled experiments. Frontal collision due to unsafe cut-ins is the target crash type of this paper. Human-controlled vehicles making unsafe lane changes are modeled as the primary disturbance to AVs based on data collected by the University of Michigan Safety Pilot Model Deployment Program. The cut-in scenarios are generated based on skewed statistics of collected human driver behaviors, which generate risky testing scenarios while preserving the statistical information so that the safety benefits of AVs in non-accelerated cases can be accurately estimated. The Cross Entropy method is used to recursively search for the optimal skewing parameters. The frequencies of occurrence of conflicts, crashes and injuries are estimated for a modeled automated vehicle, and the achieved accelerated rate is around 2,000 to 20,000. In other words, in the accelerated simulations, driving for 1,000 miles will expose the AV with challenging scenarios that will take about 2 to 20 million miles of real-world driving to encounter. This technique thus has the potential to reduce greatly the development and validation time for AVs.
Performance Characterization of a Commercial Video Streaming Service
Venue: arXiv cs.NI 2016
Year: 2016

Despite the growing popularity of video streaming over the Internet, problems such as re-buffering and high startup latency continue to plague users. In this paper, we present an end-to-end characterization of Yahoo's video streaming service, analyzing over 500 million video chunks downloaded over a two-week period. We gain unique visibility into the causes of performance degradation by instrumenting both the CDN server and the client player at the chunk level, while also collecting frequent snapshots of TCP variables from the server network stack. We uncover a range of performance issues, including an asynchronous disk-read timer and cache misses at the server, high latency and latency variability in the network, and buffering delays and dropped frames at the client. Looking across chunks in the same session, or destined to the same IP prefix, we see how some performance problems are relatively persistent, depending on the video's popularity, the distance between the client and server, and the client's operating system, browser, and Flash runtime.
Flexible Resource Allocation for Clouds and All-Optical Networks
Venue: arXiv cs.DS 2016
Year: 2016

Motivated by the cloud computing paradigm, and by key optimization problems in all-optical networks, we study two variants of the classic job interval scheduling problem, where a reusable resource is allocated to competing job intervals in a flexible manner. Each job, $J_i$, requires the use of up to $r_{max}(i)$ units of the resource, with a profit of $p_i \geq 1$ accrued for each allocated unit. The goal is to feasibly schedule a subset of the jobs so as to maximize the total profit. The resource can be allocated either in contiguous or non-contiguous blocks. These problems can be viewed as flexible variants of the well known storage allocation and bandwidth allocation problems. We show that the contiguous version is strongly NP-hard, already for instances where all jobs have the same profit and the same maximum resource requirement. For such instances, we derive the best possible positive result, namely, a polynomial time approximation scheme. We further show that the contiguous variant admits a $(\frac{5}{4} + \varepsilon)$-approximation algorithm, for any fixed $\varepsilon > 0$, on instances whose job intervals form a proper interval graph. At the heart of the algorithm lies a non-standard parameterization of the approximation ratio itself, which is of independent interest. For the non-contiguous case, we uncover an interesting relation to the paging problem that leads to a simple $O(n \log n)$ algorithm for uniform profit instances of n jobs. The algorithm is easy to implement and is thus practical.
Image stitching with perspective-preserving warping
Venue: arXiv cs.CV 2016
Year: 2016

Image stitching algorithms often adopt the global transformation, such as homography, and work well for planar scenes or parallax free camera motions. However, these conditions are easily violated in practice. With casual camera motions, variable taken views, large depth change, or complex structures, it is a challenging task for stitching these images. The global transformation model often provides dreadful stitching results, such as misalignments or projective distortions, especially perspective distortion. To this end, we suggest a perspective-preserving warping for image stitching, which spatially combines local projective transformations and similarity transformation. By weighted combination scheme, our approach gradually extrapolates the local projective transformations of the overlapping regions into the non-overlapping regions, and thus the final warping can smoothly change from projective to similarity. The proposed method can provide satisfactory alignment accuracy as well as reduce the projective distortions and maintain the multi-perspective view. Experiments on a variety of challenging images confirm the efficiency of the approach.
Speeding up Future Video Distribution via Channel-Aware Caching-Aided Coded Multicast
Venue: arXiv cs.IT 2016
Year: 2016

Future Internet usage will be dominated by the consumption of a rich variety of online multimedia services accessed from an exponentially growing number of multimedia capable mobile devices. As such, future Internet designs will be challenged to provide solutions that can deliver bandwidth-intensive, delay-sensitive, on-demand video-based services over increasingly crowded, bandwidth-limited wireless access networks. One of the main reasons for the bandwidth stress facing wireless network operators is the difficulty to exploit the multicast nature of the wireless medium when wireless users or access points rarely experience the same channel conditions or access the same content at the same time. In this paper, we present and analyze a novel wireless video delivery paradigm based on the combined use of channel-aware caching and coded multicasting that allows simultaneously serving multiple cache-enabled receivers that may be requesting different content and experiencing different channel conditions. To this end, we reformulate the caching-aided coded multicast problem as a joint source-channel coding problem and design an achievable scheme that preserves the cache-enabled multiplicative throughput gains of the error-free scenario,by guaranteeing per-receiver rates unaffected by the presence of receivers with worse channel conditions.