OpenRaiser/Intern-Atlas huggingface dataset:
Towards Formal Interaction-Based Models of Grid Computing Infrastructures
Venue: arXiv cs.PL 2014
Year: 2014

Grid computing (GC) systems are large-scale virtual machines, built upon a massive pool of resources (processing time, storage, software) that often span multiple distributed domains. Concurrent users interact with the grid by adding new tasks; the grid is expected to assign resources to tasks in a fair, trustworthy way. These distinctive features of GC systems make their specification and verification a challenging issue. Although prior works have proposed formal approaches to the specification of GC systems, a precise account of the interaction model which underlies resource sharing has not been yet proposed. In this paper, we describe ongoing work aimed at filling in this gap. Our approach relies on (higher-order) process calculi: these core languages for concurrency offer a compositional framework in which GC systems can be precisely described and potentially reasoned about.
A Computational Framework for Boundary Representation of Solid Sweeps
Venue: arXiv cs.CG 2014
Year: 2014

This paper proposes a robust algorithmic and computational framework to address the problem of modeling the volume obtained by sweeping a solid along a trajectory of rigid motions. The boundary representation (simply brep) of the input solid naturally induces a brep of the swept volume. We show that it is locally similar to the input brep and this serves as the basis of the framework. All the same, it admits several intricacies: (i) geometric, in terms of parametrizations and, (ii) topological, in terms of orientations. We provide a novel analysis for their resolution. More specifically, we prove a non-trivial lifting theorem which allows to locally orient the output using the orientation of the input. We illustrate the framework by providing many examples from a pilot implementation.
Downlink Interference Estimation without Feedback for Heterogeneous Network Interference Avoidance
Venue: arXiv cs.NI 2014
Year: 2014

In this paper, we present a novel method for a base station (BS) to estimate the total downlink interference power received by any given mobile receiver, without information feedback from the user or information exchange between neighbouring BSs. The prediction method is deterministic and can be computed rapidly. This is achieved by first abstracting the cellular network into a mathematical model, and then inferring the interference power received at any location based on the power spectrum measurements taken at the observing BS. The analysis expands the methodology to a $\mathsf{K}$-tier heterogeneous network and demonstrates the accuracy of the technique for a variety of sampling densities. The paper demonstrates the methodology by applying it to an opportunistic transmission technique that avoids transmissions to channels which are overwhelmed by interference. The simulation results show that the proposed technique performs closely or better than existing interference avoidance techniques that require information exchange, and yields a 30% throughput improvement over baseline configurations.
Performance of Macro-Scale Molecular Communications with Sensor Cleanse Time
Venue: arXiv cs.NI 2014
Year: 2014

In this paper, we consider a molecular diffusion based communications link that conveys information on the macro-scale (several metres). The motivation is to apply molecular-based communications to challenging electromagnetic environments. We first derive a novel capture probability expression of a finite sized receiver. The paper then introduces the concept of time-aggregated molecular noise at the receiver as a function of the rate at which the sensor can self-cleanse. The resulting inter-symbol-interference is expressed as a function of the sensor cleanse time, and the performance metrics of bit error rate, throughput and round-trip-time are derived. The results show that the performance is very sensitive to the sensor cleanse time and the drift velocity. The paper concludes with recommendations on the design of a real communication link based on these findings and applies the concepts to a test-bed.
Information-Theoretic Bounds for Performance of Resource-Constrained Communication Systems
Venue: arXiv cs.IT 2014
Year: 2014

Resource-constrained systems are prevalent in communications. Such a system is composed of many components but only some of them can be allocated with resources such as time slots. According to the amount of information about the system, algorithms are employed to allocate resources and the overall system performance depends on the result of resource allocation. We do not always have complete information, and thus, the system performance may not be satisfactory. In this work, we propose a general model for the resource-constrained communication systems. We draw the relationship between system information and performance and derive the performance bounds for the optimal algorithm for the system. This gives the expected performance corresponding to the available information, and we can determine if we should put more efforts to collect more accurate information before actually constructing an algorithm for the system. Several examples of applications in communications to the model are also given.
Development of Wearable Systems for Ubiquitous Healthcare Service Provisioning
Venue: arXiv cs.OH 2014
Year: 2014

This paper reports on the development of a wearable system using wireless biomedical sensors for ubiquitous healthcare service provisioning. The prototype system is developed to address current healthcare challenges such as increasing cost of services, inability to access diverse services, low quality services and increasing population of elderly as experienced globally. The biomedical sensors proactively collect physiological data of remote patients to recommend diagnostic services. The prototype system is designed to monitor oxygen saturation level (SpO2), Heart Rate (HR), activity and location of the elderly. Physiological data collected are uploaded to a Health Server (HS) via GPRS/Internet for analysis.
Wear Minimization for Cuckoo Hashing: How Not to Throw a Lot of Eggs into One Basket
Venue: arXiv cs.DS 2014
Year: 2014

We study wear-leveling techniques for cuckoo hashing, showing that it is possible to achieve a memory wear bound of $\log\log n+O(1)$ after the insertion of $n$ items into a table of size $Cn$ for a suitable constant $C$ using cuckoo hashing. Moreover, we study our cuckoo hashing method empirically, showing that it significantly improves on the memory wear performance for classic cuckoo hashing and linear probing in practice.
The Complexity of Bounded Length Graph Recoloring
Venue: arXiv cs.CC 2014
Year: 2014

We study the following question: Given are two $k$-colorings $α$ and $β$ of a graph $G$ on $n$ vertices, and integer $\ell$. The question is whether $α$ can be modified into $β$, by recoloring vertices one at a time, while maintaining a $k$-coloring throughout, and using at most $\ell$ such recoloring steps. This problem is weakly PSPACE-hard for every constant $k\ge 4$. We show that it is also strongly NP-hard for every constant $k\ge 4$. On the positive side, we give an $O(f(k,\ell) n^{O(1)})$ algorithm for the problem, for some computable function $f$. Hence the problem is fixed-parameter tractable when parameterized by $k+\ell$. Finally, we show that the problem is W[1]-hard (but in XP) when parameterized only by $\ell$.
Mining Idioms from Source Code
Venue: arXiv cs.SE 2014
Year: 2014

We present the first method for automatically mining code idioms from a corpus of previously written, idiomatic software projects. We take the view that a code idiom is a syntactic fragment that recurs across projects and has a single semantic role. Idioms may have metavariables, such as the body of a for loop. Modern IDEs commonly provide facilities for manually defining idioms and inserting them on demand, but this does not help programmers to write idiomatic code in languages or using libraries with which they are unfamiliar. We present HAGGIS, a system for mining code idioms that builds on recent advanced techniques from statistical natural language processing, namely, nonparametric Bayesian probabilistic tree substitution grammars. We apply HAGGIS to several of the most popular open source projects from GitHub. We present a wide range of evidence that the resulting idioms are semantically meaningful, demonstrating that they do indeed recur across software projects and that they occur more frequently in illustrative code examples collected from a Q&A site. Manual examination of the most common idioms indicate that they describe important program concepts, including object creation, exception handling, and resource management.
Conjugate Gradient-based Soft-Output Detection and Precoding in Massive MIMO Systems
Venue: arXiv cs.IT 2014
Year: 2014

Massive multiple-input multiple-output (MIMO) promises improved spectral efficiency, coverage, and range, compared to conventional (small-scale) MIMO wireless systems. Unfortunately, these benefits come at the cost of significantly increased computational complexity, especially for systems with realistic antenna configurations. To reduce the complexity of data detection (in the uplink) and precoding (in the downlink) in massive MIMO systems, we propose to use conjugate gradient (CG) methods. While precoding using CG is rather straightforward, soft-output minimum mean-square error (MMSE) detection requires the computation of the post-equalization signal-to-interference-and-noise-ratio (SINR). To enable CG for soft-output detection, we propose a novel way of computing the SINR directly within the CG algorithm at low complexity. We investigate the performance/complexity trade-offs associated with CG-based soft-output detection and precoding, and we compare it to exact and approximate methods. Our results reveal that the proposed method outperforms existing algorithms for massive MIMO systems with realistic antenna configurations.
New Asymptotic Metrics for Relative Generalized Hamming Weight
Venue: arXiv cs.IT 2014
Year: 2014

It was recently shown that RGHW (relative generalized Hamming weight) exactly expresses the security of linear ramp secret sharing scheme. In this paper we determine the true value of the asymptotic metric for RGHW previously proposed by Zhuang et al. in 2013. Then we propose new asymptotic metrics useful for investigating the optimal performance of linear ramp secret sharing scheme constructed from a pair of linear codes. We also determine the true values of the proposed metrics in many cases.
From ADP to the Brain: Foundations, Roadmap, Challenges and Research Priorities
Venue: arXiv cs.NE 2014
Year: 2014

This paper defines and discusses Mouse Level Computational Intelligence (MLCI) as a grand challenge for the coming century. It provides a specific roadmap to reach that target, citing relevant work and review papers and discussing the relation to funding priorities in two NSF funding activities: the ongoing Energy, Power and Adaptive Systems program (EPAS) and the recent initiative in Cognitive Optimization and Prediction (COPN). It elaborates on the first step, vector intelligence, a challenge in the development of universal learning systems, which itself will require considerable new research to attain. This in turn is a crucial prerequisite to true functional understanding of how mammal brains achieve such general learning capabilities.
MBIS: Multivariate Bayesian Image Segmentation Tool
Venue: arXiv cs.CV 2014
Year: 2014

We present MBIS (Multivariate Bayesian Image Segmentation tool), a clustering tool based on the mixture of multivariate normal distributions model. MBIS supports multi-channel bias field correction based on a B-spline model. A second methodological novelty is the inclusion of graph-cuts optimization for the stationary anisotropic hidden Markov random field model. Along with MBIS, we release an evaluation framework that contains three different experiments on multi-site data. We first validate the accuracy of segmentation and the estimated bias field for each channel. MBIS outperforms a widely used segmentation tool in a cross-comparison evaluation. The second experiment demonstrates the robustness of results on atlas-free segmentation of two image sets from scan-rescan protocols on 21 healthy subjects. Multivariate segmentation is more replicable than the monospectral counterpart on T1-weighted images. Finally, we provide a third experiment to illustrate how MBIS can be used in a large-scale study of tissue volume change with increasing age in 584 healthy subjects. This last result is meaningful as multivariate segmentation performs robustly without the need for prior knowledge
The secretary returns
Venue: arXiv cs.DS 2014
Year: 2014

In the online random-arrival model, an algorithm receives a sequence of n requests that arrive in a random order. The algorithm is expected to make an irrevocable decision with regard to each request based only on the observed history. We consider the following natural extension of this model: each request arrives k times, and the arrival order is a random permutation of the kn arrivals; the algorithm is expected to make a decision regarding each request only upon its last arrival. We focus primarily on the case when k=2, which can also be interpreted as each request arriving at, and departing from the system, at a random time. We examine the secretary problem: the problem of selecting the best secretary when the secretaries are presented online according to a random permutation. We show that when each secretary arrives twice, we can achieve a competitive ratio of ~0.768 (compared to 1/e in the classical secretary problem), and that it is optimal. We also show that without any knowledge about the number of secretaries or their arrival times, we can still hire the best secretary with probability at least 2/3, in contrast to the impossibility of achieving a constant success probability in the classical setting. We extend our results to the matroid secretary problem, introduced by Babaioff et al., (2007) and show a simple algorithm that achieves a 2-approximation to the maximal weighted basis in the new model (for k=2). We show that this approximation factor can be improved in special cases of the matroid secretary problem; in particular, we give a 16/9-competitive algorithm for the returning edge-weighted bipartite matching problem.
Extraction of Projection Profile, Run-Histogram and Entropy Features Straight from Run-Length Compressed Text-Documents
Venue: arXiv cs.CV 2014
Year: 2014

Document Image Analysis, like any Digital Image Analysis requires identification and extraction of proper features, which are generally extracted from uncompressed images, though in reality images are made available in compressed form for the reasons such as transmission and storage efficiency. However, this implies that the compressed image should be decompressed, which indents additional computing resources. This limitation induces the motivation to research in extracting features directly from the compressed image. In this research, we propose to extract essential features such as projection profile, run-histogram and entropy for text document analysis directly from run-length compressed text-documents. The experimentation illustrates that features are extracted directly from the compressed image without going through the stage of decompression, because of which the computing time is reduced. The feature values so extracted are exactly identical to those extracted from uncompressed images.
Adaptability Checking in Multi-Level Complex Systems
Venue: arXiv cs.SE 2014
Year: 2014

A hierarchical model for multi-level adaptive systems is built on two basic levels: a lower behavioural level B accounting for the actual behaviour of the system and an upper structural level S describing the adaptation dynamics of the system. The behavioural level is modelled as a state machine and the structural level as a higher-order system whose states have associated logical formulas (constraints) over observables of the behavioural level. S is used to capture the global and stable features of B, by a defining set of allowed behaviours. The adaptation semantics is such that the upper S level imposes constraints on the lower B level, which has to adapt whenever it no longer can satisfy them. In this context, we introduce weak and strong adaptabil- ity, i.e. the ability of a system to adapt for some evolution paths or for all possible evolutions, respectively. We provide a relational characterisation for these two notions and we show that adaptability checking, i.e. deciding if a system is weak or strong adaptable, can be reduced to a CTL model checking problem. We apply the model and the theoretical results to the case study of motion control of autonomous transport vehicles.
Computational Optimization, Modelling and Simulation: Recent Trends and Challenges
Venue: arXiv cs.NE 2014
Year: 2014

Modelling, simulation and optimization form an integrated part of modern design practice in engineering and industry. Tremendous progress has been observed for all three components over the last few decades. However, many challenging issues remain unresolved, and the current trends tend to use nature-inspired algorithms and surrogate-based techniques for modelling and optimization. This 4th workshop on Computational Optimization, Modelling and Simulation (COMS 2013) at ICCS 2013 will further summarize the latest developments of optimization and modelling and their applications in science, engineering and industry. In this review paper, we will analyse the recent trends in modelling and optimization, and their associated challenges. We will discuss important topics for further research, including parameter-tuning, large-scale problems, and the gaps between theory and applications.
Pentago is a First Player Win: Strongly Solving a Game Using Parallel In-Core Retrograde Analysis
Venue: arXiv cs.DC 2014
Year: 2014

We present a strong solution of the board game pentago, computed using exhaustive parallel retrograde analysis in 4 hours on 98304 ($3 \times 2^{15}$) threads of NERSC's Cray Edison. At $3.0 \times 10^{15}$ states, pentago is the largest divergent game solved to date by two orders of magnitude, and the only example of a nontrivial divergent game solved using retrograde analysis. Unlike previous retrograde analyses, our computation was performed entirely in-core, writing only a small portion of the results to disk; an out-of-core implementation would have been much slower. Symmetry was used to reduce branching factor and exploit instruction level parallelism. Despite a theoretically embarrassingly parallel structure, asynchronous message passing was required to fit the computation into available RAM, causing latency problems on an older Cray machine. All code and data for the project are open source, together with a website which combines database lookup and on-the-fly computation to interactively explore the strong solution.
The Least Wrong Model Is Not in the Data
Venue: arXiv cs.LG 2014
Year: 2014

The true process that generated data cannot be determined when multiple explanations are possible. Prediction requires a model of the probability that a process, chosen randomly from the set of candidate explanations, generates some future observation. The best model includes all of the information contained in the minimal description of the data that is not contained in the data. It is closely related to the Halting Problem and is logarithmic in the size of the data. Prediction is difficult because the ideal model is not computable, and the best computable model is not "findable." However, the error from any approximation can be bounded by the size of the description using the model.
An Epistemic Strategy Logic (Extended Abstract)
Venue: arXiv cs.LO 2014
Year: 2014

The paper presents an extension of temporal epistemic logic with operators that quantify over strategies. The language also provides a natural way to represent what agents would know were they to be aware of the strategies being used by other agents. Some examples are presented to motivate the framework, and relationships to several variants of alternating temporal epistemic logic are discussed. The computational complexity of model checking the logic is also characterized.
Comprehensive Monitor-Oriented Compensation Programming
Venue: arXiv cs.SE 2014
Year: 2014

Compensation programming is typically used in the programming of web service compositions whose correct implementation is crucial due to their handling of security-critical activities such as financial transactions. While traditional exception handling depends on the state of the system at the moment of failure, compensation programming is significantly more challenging and dynamic because it is dependent on the runtime execution flow - with the history of behaviour of the system at the moment of failure affecting how to apply compensation. To address this dynamic element, we propose the use of runtime monitors to facilitate compensation programming, with monitors enabling the modeller to be able to implicitly reason in terms of the runtime control flow, thus separating the concerns of system building and compensation modelling. Our approach is instantiated into an architecture and shown to be applicable to a case study.
Implementing Anti-Unification Modulo Equational Theory
Venue: arXiv cs.LO 2014
Year: 2014

We present an implementation of E-anti-unification as defined in Heinz (1995), where tree-grammar descriptions of equivalence classes of terms are used to compute generalizations modulo equational theories. We discuss several improvements, including an efficient implementation of variable-restricted E-anti-unification from Heinz (1995), and give some runtime figures about them. We present applications in various areas, including lemma generation in equational inductive proofs, intelligence tests, diverging Knuth-Bendix completion, strengthening of induction hypotheses, and theory formation about finite algebras.
A Tutorial on Principal Component Analysis
Venue: arXiv cs.LG 2014
Year: 2014

Principal component analysis (PCA) is a mainstay of modern data analysis - a black box that is widely used but (sometimes) poorly understood. The goal of this paper is to dispel the magic behind this black box. This manuscript focuses on building a solid intuition for how and why principal component analysis works. This manuscript crystallizes this knowledge by deriving from simple intuitions, the mathematics behind PCA. This tutorial does not shy away from explaining the ideas informally, nor does it shy away from the mathematics. The hope is that by addressing both aspects, readers of all levels will be able to gain a better understanding of PCA as well as the when, the how and the why of applying this technique.