OpenRaiser/Intern-Atlas huggingface dataset:
Optimal Index Coding with Min-Max Probability of Error over Fading Channels
Venue: arXiv cs.IT 2015
Year: 2015

An index coding scheme in which the source (transmitter) transmits binary symbols over a wireless fading channel is considered. Index codes with the transmitter using minimum number of transmissions are known as optimal index codes. Different optimal index codes give different performances in terms of probability of error in a fading environment and this also varies from receiver to receiver. In this paper we deal with optimal index codes which minimizes the maximum probability of error among all the receivers. We identify a criterion for optimal index codes that minimizes the maximum probability of error among all the receivers. For a special class of index coding problems, we give an algorithm to identify optimal index codes which minimize the maximum error probability. We illustrate our techniques and claims with simulation results leading to conclude that a careful choice among the optimal index codes will give a considerable gain in fading channels.
Verifying linearizability: A comparative survey
Venue: arXiv cs.LO 2015
Year: 2015

Linearizability has become the key correctness criterion for concurrent data structures, ensuring that histories of the concurrent object under consideration are consistent, where consistency is judged with respect to a sequential history of a corresponding abstract data structure. Linearizability allows any order of concurrent (i.e., overlapping) calls to operations to be picked, but requires the real-time order of non-overlapping to be preserved. Over the years numerous techniques for verifying linearizability have been developed, using a variety of formal foundations such as refinement, shape analysis, reduction, etc. However, as the underlying framework, nomenclature and terminology for each method differs, it has become difficult for practitioners to judge the differences between each approach, and hence, judge the methodology most appropriate for the data structure at hand. We compare the major of methods used to verify linearizability, describe the main contribution of each method, and compare their advantages and limitations.
Canonical Polyadic Decomposition with Auxiliary Information for Brain Computer Interface
Venue: arXiv cs.CV 2015
Year: 2015

Physiological signals are often organized in the form of multiple dimensions (e.g., channel, time, task, and 3D voxel), so it is better to preserve original organization structure when processing. Unlike vector-based methods that destroy data structure, Canonical Polyadic Decomposition (CPD) aims to process physiological signals in the form of multi-way array, which considers relationships between dimensions and preserves structure information contained by the physiological signal. Nowadays, CPD is utilized as an unsupervised method for feature extraction in a classification problem. After that, a classifier, such as support vector machine, is required to classify those features. In this manner, classification task is achieved in two isolated steps. We proposed supervised Canonical Polyadic Decomposition by directly incorporating auxiliary label information during decomposition, by which a classification task can be achieved without an extra step of classifier training. The proposed method merges the decomposition and classifier learning together, so it reduces procedure of classification task compared with that of respective decomposition and classification. In order to evaluate the performance of the proposed method, three different kinds of signals, synthetic signal, EEG signal, and MEG signal, were used. The results based on evaluations of synthetic and real signals demonstrated that the proposed method is effective and efficient.
Observation of the Kibble-Zurek Mechanism in Microscopic Acoustic Cracking Noises
Venue: arXiv cs.CE 2015
Year: 2015

The fast evolution of microstructure is key to understanding crackling phenomena. It has been proposed that formation of a nonlinear zone around a moving crack tip controls the crack tip velocity. Progress in understanding the physics of this critical zone has been limited due to the lack of hard data describing the detailed complex physical processes that occur within. For the first time, we show that the signature of the non-linear elastic zone around a microscopic dynamic crack maps directly to generic phases of acoustic noises, supporting the formation of a strongly weak zone near the moving crack tips. We additionally show that the rate of traversing to non-linear zone controls the rate of weakening, i.e. speed of global rupture propagation. We measure the power-law dependence of nonlinear zone size on the traversing rate, and show that our observations are in agreement with the Kibble-Zurek mechanism (KZM) .
Random Sampling in an Age of Automation: Minimizing Expenditures through Balanced Collection and Annotation
Venue: arXiv cs.CY 2015
Year: 2015

Methods for automated collection and annotation are changing the cost-structures of sampling surveys for a wide range of applications. Digital samples in the form of images or audio recordings can be collected rapidly, and annotated by computer programs or crowd workers. We consider the problem of estimating a population mean under these new cost-structures, and propose a Hybrid-Offset sampling design. This design utilizes two annotators: a primary, which is accurate but costly (e.g. a human expert) and an auxiliary which is noisy but cheap (e.g. a computer program), in order to minimize total sampling expenditures. Our analysis gives necessary conditions for the Hybrid-Offset design and specifies optimal sample sizes for both annotators. Simulations on data from a coral reef survey program indicate that the Hybrid-Offset design outperforms several alternative sampling designs. In particular, sampling expenditures are reduced 50% compared to the Conventional design currently deployed by the coral ecologists.
Efficient implementation of elementary functions in the medium-precision range
Venue: arXiv cs.MS 2015
Year: 2015

We describe a new implementation of the elementary transcendental functions exp, sin, cos, log and atan for variable precision up to approximately 4096 bits. Compared to the MPFR library, we achieve a maximum speedup ranging from a factor 3 for cos to 30 for atan. Our implementation uses table-based argument reduction together with rectangular splitting to evaluate Taylor series. We collect denominators to reduce the number of divisions in the Taylor series, and avoid overhead by doing all multiprecision arithmetic using the mpn layer of the GMP library. Our implementation provides rigorous error bounds.
Repairable Threshold Secret Sharing Schemes
Venue: arXiv cs.CR 2015
Year: 2015

In this paper, we propose a class of threshold secret sharing schemes with repairing function between shares without the help of the dealer, that we called repairable threshold secret sharing schemes. Specifically, if a share fails, such as broken or lost, it will be repaired just by some other shares. A construction of such repairable threshold secret sharing schemes is designed by applying linearized polynomials and regenerating codes in distributed storage systems. In addition, a new repairing rate is introduced to characterize the performance and efficiency of the repairing function. Then an achievable upper bound on the repairing rate is derived, which implies the optimality of the repair and describes the security between different shares. Under this optimality of the repair, we further discuss traditional information rate and also indicate its optimality, that can describe the efficiency of secret sharing schemes in the aspect of storage. Finally, by applying the minimum bandwidth regenerating (MBR) codes, our construction designs repairable threshold secret sharing schemes achieving both optimal repairing and information rates simultaneously.
Interactive Consistency in practical, mostly-asynchronous systems
Venue: arXiv cs.DC 2015
Year: 2015

Interactive consistency is the problem in which n nodes, where up to t may be byzantine, each with its own private value, run an algorithm that allows all non-faulty nodes to infer the values of each other node. This problem is relevant to critical applications that rely on the combination of the opinions of multiple peers to provide a service. Examples include monitoring a content source to prevent equivocation or to track variability in the content provided, and resolving divergent state amongst the nodes of a distributed system. Previous works assume a fully synchronous system, where one can make strong assumptions such as negligible message delivery delays and/or detection of absent messages. However, practical, real-world systems are mostly asynchronous, i.e., they exhibit only some periods of synchrony during which message delivery is timely, thus requiring a different approach. In this paper, we present a thorough study on practical interactive consistency. We leverage the vast prior work on broadcast and byzantine consensus algorithms to design, implement and evaluate a set of algorithms, with varying timing assumptions and message complexity, that can be used to achieve interactive consistency in real-world distributed systems. We provide a complete, open-source implementation of each proposed interactive consistency algorithm by building a multi-layered stack of protocols that include several broadcast protocols, as well as a binary and a multi-valued consensus protocol. Most of these protocols have never been implemented and evaluated in a real system before. We analyze the performance of our suite of algorithms experimentally by engaging in both single instance and multiple parallel instances of each alternative.
The Hegselmann-Krause dynamics on the circle converge
Venue: arXiv cs.SY 2015
Year: 2015

We consider the Hegselmann-Krause dynamics on a one-dimensional torus and provide the first proof of convergence of this system. The proof requires only fairly minor modifications of existing methods for proving convergence in Euclidean space.
Integral Control on Lie Groups
Venue: arXiv cs.SY 2015
Year: 2015

In this paper, we extend the popular integral control technique to systems evolving on Lie groups. More explicitly, we provide an alternative definition of "integral action" for proportional(-derivative)-controlled systems whose configuration evolves on a nonlinear space, where configuration errors cannot be simply added up to compute a definite integral. We then prove that the proposed integral control allows to cancel the drift induced by a constant bias in both first order (velocity) and second order (torque) control inputs for fully actuated systems evolving on abstract Lie groups. We illustrate the approach by 3-dimensional motion control applications.
ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems
Venue: arXiv cs.LO 2015
Year: 2015

We present ProbReach, a tool for verifying probabilistic reachability for stochastic hybrid systems, i.e., computing the probability that the system reaches an unsafe region of the state space. In particular, ProbReach will compute an arbitrarily small interval which is guaranteed to contain the required probability. Standard (non-probabilistic) reachability is undecidable even for linear hybrid systems. In ProbReach we adopt the weaker notion of delta-reachability, in which the unsafe region is overapproximated by a user-defined parameter (delta). This choice leads to false alarms, but also makes the reachability problem decidable for virtually any hybrid system. In ProbReach we have implemented a probabilistic version of delta-reachability that is suited for hybrid systems whose stochastic behaviour is given in terms of random initial conditions. In this paper we introduce the capabilities of ProbReach, give an overview of the parallel implementation, and present results for several benchmarks involving highly non-linear hybrid systems.
Cost Preserving Bisimulations for Probabilistic Automata
Venue: arXiv cs.FL 2015
Year: 2015

Probabilistic automata constitute a versatile and elegant model for concurrent probabilistic systems. They are equipped with a compositional theory supporting abstraction, enabled by weak probabilistic bisimulation serving as the reference notion for summarising the effect of abstraction. This paper considers probabilistic automata augmented with costs. It extends the notions of weak transitions in probabilistic automata in such a way that the costs incurred along a weak transition are captured. This gives rise to cost-preserving and cost-bounding variations of weak probabilistic bisimilarity, for which we establish compositionality properties with respect to parallel composition. Furthermore, polynomial-time decision algorithms are proposed, that can be effectively used to compute reward-bounding abstractions of Markov decision processes in a compositional manner.
Codes for DNA Storage Channels
Venue: arXiv cs.IT 2015
Year: 2015

We consider the problem of assembling a sequence based on a collection of its substrings observed through a noisy channel. The mathematical basis of the problem is the construction and design of sequences that may be discriminated based on a collection of their substrings observed through a noisy channel. We explain the connection between the sequence reconstruction problem and the problem of DNA synthesis and sequencing, and introduce the notion of a DNA storage channel. We analyze the number of sequence equivalence classes under the channel mapping and propose new asymmetric coding techniques to combat the effects of synthesis and sequencing noise. In our analysis, we make use of restricted de Bruijn graphs and Ehrhart theory for rational polytopes.
Uplink User-Assisted Relaying in Cellular Networks
Venue: arXiv cs.IT 2015
Year: 2015

We use stochastic geometry to analyze the performance of a partial decode-and-forward (PDF) relaying scheme applied in a user-assisted relaying setting, where an active user relays data through another idle user in uplink cellular communication. We present the geometric model of a network deploying user-assisted relaying and propose two geometric cooperation policies for fast and slow fading channels. We analytically derive the cooperation probability for both policies. This cooperation probability is further used in the analytical derivation of the moments of inter-cell interference power caused by system-wide deployment of this user-assisted PDF relaying. We then model the inter-cell interference power statistics using the Gamma distribution by matching the first two moments analytically derived. This cooperation and interference analysis provides the theoretical basis for quantitatively evaluating the performance impact of user-assisted relaying in cellular networks. We then numerically evaluate the average transmission rate performance and show that user-assisted relaying can significantly improve per-user transmission rate despite of increased inter-cell interference. This transmission rate gain is significant for active users near the cell edge and further increases with higher idle user density, supporting user-assisted relaying as a viable solution to crowded population areas.
Algorithms for Mapping Parallel Processes onto Grid and Torus Architectures
Venue: arXiv cs.DS 2015
Year: 2015

Static mapping is the assignment of parallel processes to the processing elements (PEs) of a parallel system, where the assignment does not change during the application's lifetime. In our scenario we model an application's computations and their dependencies by an application graph. This graph is first partitioned into (nearly) equally sized blocks. These blocks need to communicate at block boundaries. To assign the processes to PEs, our goal is to compute a communication-efficient bijective mapping between the blocks and the PEs. This approach of partitioning followed by bijective mapping has many degrees of freedom. Thus, users and developers of parallel applications need to know more about which choices work for which application graphs and which parallel architectures. To this end, we not only develop new mapping algorithms (derived from known greedy methods). We also perform extensive experiments involving different classes of application graphs (meshes and complex networks), architectures of parallel computers (grids and tori), as well as different partitioners and mapping algorithms. Surprisingly, the quality of the partitions, unless very poor, has little influence on the quality of the mapping. More importantly, one of our new mapping algorithms always yields the best results in terms of the quality measure maximum congestion when the application graphs are complex networks. In case of meshes as application graphs, this mapping algorithm always leads in terms of maximum congestion AND maximum dilation, another common quality measure.
Probabilistic verification of partially observable dynamical systems
Venue: arXiv cs.SY 2015
Year: 2015

The construction and formal verification of dynamical models is important in engineering, biology and other disciplines. We focus on non-linear models containing a set of parameters governing their dynamics. The value of these parameters is often unknown and not directly observable through measurements, which are themselves noisy. When treating parameters as random variables, one can constrain their distribution by conditioning on observations and thereby constructing a posterior probability distribution. We aim to perform model verification with respect to this posterior. The main difficulty in performing verification on a model under the posterior distribution is that in general, it is difficult to obtain \emph{independent} samples from the posterior, especially for non-linear dynamical models. Standard statistical model checking methods require independent realizations of the system and are therefore not applicable in this context. We propose a Markov chain Monte Carlo based statistical model checking framework, which produces a sequence of dependent random realizations of the model dynamics over the parameter posterior. Using this sequence of samples, we use statistical hypothesis tests to verify whether the model satisfies a bounded temporal logic property with a certain probability. We use sample size bounds tailored to the setting of dependent samples for fixed sample size and sequential tests. We apply our method to a case-study from the domain of systems biology, to a model of the JAK-STAT biochemical pathway. The pathway is modeled as a system of non-linear ODEs containing a set of unknown parameters. Noisy, indirect observations of the system state are available from an experiment. The results show that the proposed method enables probabilistic verification with respect to the parameter posterior with specified error bounds.
The Limitations of Standardized Science Tests as Benchmarks for Artificial Intelligence Research: Position Paper
Venue: arXiv cs.AI 2015
Year: 2015

In this position paper, I argue that standardized tests for elementary science such as SAT or Regents tests are not very good benchmarks for measuring the progress of artificial intelligence systems in understanding basic science. The primary problem is that these tests are designed to test aspects of knowledge and ability that are challenging for people; the aspects that are challenging for AI systems are very different. In particular, standardized tests do not test knowledge that is obvious for people; none of this knowledge can be assumed in AI systems. Individual standardized tests also have specific features that are not necessarily appropriate for an AI benchmark. I analyze the Physics subject SAT in some detail and the New York State Regents Science test more briefly. I also argue that the apparent advantages offered by using standardized tests are mostly either minor or illusory. The one major real advantage is that the significance is easily explained to the public; but I argue that even this is a somewhat mixed blessing. I conclude by arguing that, first, more appropriate collections of exam style problems could be assembled, and second, that there are better kinds of benchmarks than exam-style problems. In an appendix I present a collection of sample exam-style problems that test kinds of knowledge missing from the standardized tests.
Random Linear Network Coding for Wireless Layered Video Broadcast: General Design Methods for Adaptive Feedback-free Transmission
Venue: arXiv cs.IT 2015
Year: 2015

This paper studies the problem of broadcasting layered video streams over heterogeneous single-hop wireless networks using feedback-free random linear network coding (RLNC). We combine RLNC with unequal error protection (UEP) and our main purpose is twofold. First, to systematically investigate the benefits of UEP+RLNC layered approach in servicing users with different reception capabilities. Second, to study the effect of not using feedback, by comparing feedback-free schemes with idealistic full-feedback schemes. To these ends, we study `expected percentage of decoded frames' as a key content-independent performance metric and propose a general framework for calculation of this metric, which can highlight the effect of key system, video and channel parameters. We study the effect of number of layers and propose a scheme that selects the optimum number of layers adaptively to achieve the highest performance. Assessing the proposed schemes with real H.264 test streams, the trade-offs among the users' performances are discussed and the gain of adaptive selection of number of layers to improve the trade-offs is shown. Furthermore, it is observed that the performance gap between the proposed feedback-free scheme and the idealistic scheme is very small and the adaptive selection of number of video layers further closes the gap.
A totally unimodular view of structured sparsity
Venue: arXiv cs.LG 2015
Year: 2015

This paper describes a simple framework for structured sparse recovery based on convex optimization. We show that many structured sparsity models can be naturally represented by linear matrix inequalities on the support of the unknown parameters, where the constraint matrix has a totally unimodular (TU) structure. For such structured models, tight convex relaxations can be obtained in polynomial time via linear programming. Our modeling framework unifies the prevalent structured sparsity norms in the literature, introduces new interesting ones, and renders their tightness and tractability arguments transparent.