OpenRaiser/Intern-Atlas huggingface dataset:
Adaptive Convex Combination of APA and ZA-APA algorithms for Sparse System Identification
Venue: arXiv cs.SY 2015
Year: 2015

In general, one often encounters the systems that have sparse impulse response, with time varying system sparsity. Conventional adaptive filters which perform well for identification of non-sparse systems fail to exploit the system sparsity for improving the performance as the sparsity level increases. This paper presents a new approach that uses an adaptive convex combination of Affine Projection Algorithm (APA) and Zero-attracting Affine Projection Algorithm (ZA-APA)algorithms for identifying the sparse systems, which adapts dynamically to the sparsity of the system. Thus works well in both sparse and non-sparse environments and also the usage of affine projection makes it robust against colored input. It is shown that, for non-sparse systems, the proposed combination always converges to the APA algorithm, while for semi-sparse systems, it converges to a solution that produces lesser steady state EMSE than produced by either of the component filters. For highly sparse systems, depending on the value of the proportionality constant ($ρ$) in ZA-APA algorithm, the proposed combined filter may either converge to the ZA-APA based filter or produce a solution similar to the semi-sparse case i.e., outerperforms both the constituent filters.
Sharing HOL4 and HOL Light proof knowledge
Venue: arXiv cs.AI 2015
Year: 2015

New proof assistant developments often involve concepts similar to already formalized ones. When proving their properties, a human can often take inspiration from the existing formalized proofs available in other provers or libraries. In this paper we propose and evaluate a number of methods, which strengthen proof automation by learning from proof libraries of different provers. Certain conjectures can be proved directly from the dependencies induced by similar proofs in the other library. Even if exact correspondences are not found, learning-reasoning systems can make use of the association between proved theorems and their characteristics to predict the relevant premises. Such external help can be further combined with internal advice. We evaluate the proposed knowledge-sharing methods by reproving the HOL Light and HOL4 standard libraries. The learning-reasoning system HOL(y)Hammer, whose single best strategy could automatically find proofs for 30% of the HOL Light problems, can prove 40% with the knowledge from HOL4.
A comparative analysis of progressive multiple sequence alignment approaches using UPGMA and neighbor joining based guide trees
Venue: arXiv cs.CE 2015
Year: 2015

Multiple sequence alignment is increasingly important to bioinformatics, with several applications ranging from phylogenetic analyses to domain identification. There are several ways to perform multiple sequence alignment, an important way of which is the progressive alignment approach studied in this work. Progressive alignment involves three steps: find the distance between each pair of sequences; construct a guide tree based on the distance matrix; finally based on the guide tree align sequences using the concept of aligned profiles. Our contribution is in comparing two main methods of guide tree construction in terms of both efficiency and accuracy of the overall alignment: UPGMA and Neighbor Join methods. Our experimental results indicate that the Neighbor Join method is both more efficient in terms of performance and more accurate in terms of overall cost minimization.
Towards Detecting Compromised Accounts on Social Networks
Venue: arXiv cs.CR 2015
Year: 2015

Compromising social network accounts has become a profitable course of action for cybercriminals. By hijacking control of a popular media or business account, attackers can distribute their malicious messages or disseminate fake information to a large user base. The impacts of these incidents range from a tarnished reputation to multi-billion dollar monetary losses on financial markets. In our previous work, we demonstrated how we can detect large-scale compromises (i.e., so-called campaigns) of regular online social network users. In this work, we show how we can use similar techniques to identify compromises of individual high-profile accounts. High-profile accounts frequently have one characteristic that makes this detection reliable -- they show consistent behavior over time. We show that our system, were it deployed, would have been able to detect and prevent three real-world attacks against popular companies and news agencies. Furthermore, our system, in contrast to popular media, would not have fallen for a staged compromise instigated by a US restaurant chain for publicity reasons.
Some Supplementaries to The Counting Semantics for Abstract Argumentation
Venue: arXiv cs.AI 2015
Year: 2015

Dung's abstract argumentation framework consists of a set of interacting arguments and a series of semantics for evaluating them. Those semantics partition the powerset of the set of arguments into two classes: extensions and non-extensions. In order to reason with a specific semantics, one needs to take a credulous or skeptical approach, i.e. an argument is eventually accepted, if it is accepted in one or all extensions, respectively. In our previous work \cite{ref-pu2015counting}, we have proposed a novel semantics, called \emph{counting semantics}, which allows for a more fine-grained assessment to arguments by counting the number of their respective attackers and defenders based on argument graph and argument game. In this paper, we continue our previous work by presenting some supplementaries about how to choose the damaging factor for the counting semantics, and what relationships with some existing approaches, such as Dung's classical semantics, generic gradual valuations. Lastly, an axiomatic perspective on the ranking semantics induced by our counting semantics are presented.
DeepSat - A Learning framework for Satellite Imagery
Venue: arXiv cs.CV 2015
Year: 2015

Satellite image classification is a challenging problem that lies at the crossroads of remote sensing, computer vision, and machine learning. Due to the high variability inherent in satellite data, most of the current object classification approaches are not suitable for handling satellite datasets. The progress of satellite image analytics has also been inhibited by the lack of a single labeled high-resolution dataset with multiple class labels. The contributions of this paper are twofold - (1) first, we present two new satellite datasets called SAT-4 and SAT-6, and (2) then, we propose a classification framework that extracts features from an input image, normalizes them and feeds the normalized feature vectors to a Deep Belief Network for classification. On the SAT-4 dataset, our best network produces a classification accuracy of 97.95% and outperforms three state-of-the-art object recognition algorithms, namely - Deep Belief Networks, Convolutional Neural Networks and Stacked Denoising Autoencoders by ~11%. On SAT-6, it produces a classification accuracy of 93.9% and outperforms the other algorithms by ~15%. Comparative studies with a Random Forest classifier show the advantage of an unsupervised learning approach over traditional supervised learning techniques. A statistical analysis based on Distribution Separability Criterion and Intrinsic Dimensionality Estimation substantiates the effectiveness of our approach in learning better representations for satellite imagery.
Morpheus: Safe and Flexible Dynamic Updates for SDNs
Venue: arXiv cs.NI 2015
Year: 2015

SDN controllers must be periodically modified to add features, improve performance, and fix bugs, but current techniques for implementing dynamic updates are inadequate. Simply halting old controllers and bringing up new ones can cause state to be lost, which often leads to incorrect behavior-e.g., if the state represents hosts blacklisted by a firewall, then traffic that should be blocked may be allowed to pass through. Techniques based on record and replay can reconstruct state automatically, but they are expensive to deploy and can lead to incorrect behavior. Problematic scenarios are especially likely to arise in distributed controllers and with semantics-altering updates. This paper presents a new approach to implementing dynamic controller updates based on explicit state transfer. Instead of attempting to infer state changes automatically-an approach that is expensive and fundamentally incomplete-our framework gives programmers effective tools for implementing correct updates that avoid major disruptions. We develop primitives that enable programmers to directly (and easily, in most cases) initialize the new controller's state as a function of old state and we design protocols that ensure consistent behavior during the transition. We also present a prototype implementation called Morpheus, and evaluate its effectiveness on representative case studies.
HAPPY: Hybrid Address-based Page Policy in DRAMs
Venue: arXiv cs.AR 2015
Year: 2015

Memory controllers have used static page closure policies to decide whether a row should be left open, open-page policy, or closed immediately, close-page policy, after the row has been accessed. The appropriate choice for a particular access can reduce the average memory latency. However, since application access patterns change at run time, static page policies cannot guarantee to deliver optimum execution time. Hybrid page policies have been investigated as a means of covering these dynamic scenarios and are now implemented in state-of-the-art processors. Hybrid page policies switch between open-page and close-page policies while the application is running, by monitoring the access pattern of row hits/conflicts and predicting future behavior. Unfortunately, as the size of DRAM memory increases, fine-grain tracking and analysis of memory access patterns does not remain practical. We propose a compact memory address-based encoding technique which can improve or maintain the performance of DRAMs page closure predictors while reducing the hardware overhead in comparison with state-of-the-art techniques. As a case study, we integrate our technique, HAPPY, with a state-of-the-art monitor, the Intel-adaptive open-page policy predictor employed by the Intel Xeon X5650, and a traditional Hybrid page policy. We evaluate them across 70 memory intensive workload mixes consisting of single-thread and multi-thread applications. The experimental results show that using the HAPPY encoding applied to the Intel-adaptive page closure policy can reduce the hardware overhead by 5X for the evaluated 64 GB memory (up to 40X for a 512 GB memory) while maintaining the prediction accuracy.
Solving underdetermined systems with error-correcting codes
Venue: arXiv cs.IT 2015
Year: 2015

In an underdetermined system of equations $Ax=y$, where $A$ is an $m\times n$ matrix, only $u$ of the entries of $y$ with $u < m$ are known. Thus $E_jw$, called `measurements', are known for certain $j\in J \subset \{0,1,\ldots,m-1\}$ where $\{E_i, i=0,1,\ldots, m-1\}$ are the rows of $A$ and $|J|=u$. It is required, if possible, to solve the system uniquely when $x$ has at most $t$ non-zero entries with $u\geq 2t$. Here such systems are considered from an error-correcting coding point of view. The unknown $x$ can be shown to be the error vector of a code subject to certain conditions on the rows of the matrix $A$. This reduces the problem to finding a suitable decoding algorithm which then finds $x$. Decoding workable algorithms are shown to exist, from which the unknown $x$ may be determined, in cases where the known $2t$ values are evenly spaced (that is, when the elements of $J$ are in arithmetic progression) for classes of matrices satisfying certain row properties. These cases include Fourier $n\times n $ matrices where the arithmetic difference $k$ satisfies $\gcd(n,k)=1$, and classes of Vandermonde matrices $V(x_1,x_2,\ldots,x_n)$ (with $x_i\neq 0$) with arithmetic difference $k$ where the ratios $x_i/x_j$ for $i\neq j$ are not $k^{th}$ roots of unity. The decoding algorithm has complexity $O(nt)$ and in some cases, including the Fourier matrix cases, the complexity is $O(t^2)$. Matrices which have the property that the determinant of any square submatrix is non-zero are of particular interest. Randomly choosing rows of such matrices can then give $t$ error-correcting pairs to generate a `measuring' code $C^\perp=\{E_j | j\in J\}$ with a decoding algorithm which finds $x$. This has applications to signal processing and compressed sensing.
HFR Code: A Flexible Replication Scheme for Cloud Storage Systems
Venue: arXiv cs.IT 2015
Year: 2015

Fractional repetition (FR) codes are a family of repair-efficient storage codes that provide exact and uncoded node repair at the minimum bandwidth regenerating point. The advantageous repair properties are achieved by a tailor-made two-layer encoding scheme which concatenates an outer maximum-distance-separable (MDS) code and an inner repetition code. In this paper, we generalize the application of FR codes and propose heterogeneous fractional repetition (HFR) code, which is adaptable to the scenario where the repetition degrees of coded packets are different. We provide explicit code constructions by utilizing group divisible designs, which allow the design of HFR codes over a large range of parameters. The constructed codes achieve the system storage capacity under random access repair and have multiple repair alternatives for node failures. Further, we take advantage of the systematic feature of MDS codes and present a novel design framework of HFR codes, in which storage nodes can be wisely partitioned into clusters such that data reconstruction time can be reduced when contacting nodes in the same cluster.
Attack on a classical analogue of the Dunjko, Wallden, Kent and Andersson quantum digital signature protocol
Venue: arXiv cs.CR 2015
Year: 2015

A quantum digital signature (QDS) protocol is investigated in respect of an attacker who can impersonate other communicating principals in the style of Lowe's attack on the Needham-Schroeder public-key authentication protocol. A man-in-the-middle attack is identified in respect of a classical variant of the protocol and it is suggested that a similar attack would be effective against the QDS protocol. The attack has been confirmed through initial protocol modelling using a automated theorem prover, ProVerif.
Improving Lower Bound on Opaque Set for Equilateral Triangle
Venue: arXiv cs.CG 2015
Year: 2015

An opaque set (or a barrier) for $U \subseteq \mathbb{R}^2$ is a set $B$ of finite-length curves such that any line intersecting $U$ also intersects $B$. In this paper, we consider the lower bound for the shortest barrier when $U$ is the unit equilateral triangle. The known best lower bound for triangles is the classic one by Jones [Jones,1964], which exhibits that the length of the shortest barrier for any convex polygon is at least the half of its perimeter. That is, for the unit equilateral triangle, it must be at least $3/2$. Very recently, this lower bounds are improved for convex $k$-gons for any $k\geq 4$ [Kawamura et al. 2014], but the case of triangles still lack the bound better than Jones' one. The main result of this paper is to fill this missing piece: We give the lower bound of $3/2 + 5 \cdot 10^{-13}$ for the unit-size equilateral triangle. The proof is based on two new ideas, angle-restricted barriers and a weighted sum of projection-cover conditions, which may be of independently interest.
Dpush: A scalable decentralized spam resistant unsolicited messaging protocol
Venue: arXiv cs.CR 2015
Year: 2015

Herein this paper is presented a novel invention - called Dpush - that enables truly scalable spam resistant uncensorable automatically encrypted and inherently authenticated messaging; thus restoring our ability to exert our right to private communication, and thus a step forward in restoring an uncorrupted democracy. Using a novel combination of a distributed hash table[1] (DHT) and a proof of work[2] (POW), combined in a way that can only be called a synergy, the emergent property of a scalable and spam resistant unsolicited messaging protocol elegantly emerges. Notable is that the receiver does not need to be online at the time the message is sent. This invention is already implemented and operating within the package that is called MORPHiS - which is a Sybil[3] resistant enhanced Kademlia[1] DHT implementation combined with an already functioning implementation of Dpush, as well as a polished HTTP Dmail interface to send and receive such messages today. MORPHiS is available for free (GPLv2) at the https://morph.is website.
An Information Theoretic Approach Towards Assessing Perceptual Audio Quality using EEG
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we propose a novel information theoretic model to interpret the entire "transmission chain" comprising stimulus generation, brain processing by the human subject, and the electroencephalograph (EEG) response measurements as a nonlinear, time-varying communication channel with memory. We use mutual information (MI) as a measure to assess audio quality perception by directly measuring the brainwave responses of the human subjects using a high resolution EEG. Our focus here is on audio where the quality is impaired by time varying distortions. In particular, we conduct experiments where subjects are presented with audio whose quality varies with time between different possible quality levels. The recorded EEG measurements can be modeled as a multidimensional Gaussian mixture model (GMM). In order to make the computation of the MI feasible, we present a novel low-complexity approximation technique for the differential entropy of the multidimensional GMM. We find the proposed information theoretic approach to be successful in quantifying subjective audio quality perception, with the results being consistent across different music sequences and distortion types.
Parametric Maxflows for Structured Sparse Learning with Convex Relaxations of Submodular Functions
Venue: arXiv cs.LG 2015
Year: 2015

The proximal problem for structured penalties obtained via convex relaxations of submodular functions is known to be equivalent to minimizing separable convex functions over the corresponding submodular polyhedra. In this paper, we reveal a comprehensive class of structured penalties for which penalties this problem can be solved via an efficiently solvable class of parametric maxflow optimization. We then show that the parametric maxflow algorithm proposed by Gallo et al. and its variants, which runs, in the worst-case, at the cost of only a constant factor of a single computation of the corresponding maxflow optimization, can be adapted to solve the proximal problems for those penalties. Several existing structured penalties satisfy these conditions; thus, regularized learning with these penalties is solvable quickly using the parametric maxflow algorithm. We also investigate the empirical runtime performance of the proposed framework.
Natural scene statistics mediate the perception of image complexity
Venue: arXiv cs.AI 2015
Year: 2015

Humans are sensitive to complexity and regularity in patterns. The subjective perception of pattern complexity is correlated to algorithmic (Kolmogorov-Chaitin) complexity as defined in computer science, but also to the frequency of naturally occurring patterns. However, the possible mediational role of natural frequencies in the perception of algorithmic complexity remains unclear. Here we reanalyze Hsu et al. (2010) through a mediational analysis, and complement their results in a new experiment. We conclude that human perception of complexity seems partly shaped by natural scenes statistics, thereby establishing a link between the perception of complexity and the effect of natural scene statistics.
An uniform data replication algorithm in wireless micro-sensor network for communicating materials application
Venue: arXiv cs.NI 2015
Year: 2015

Wireless sensor networks (WSN) have recently gained a great deal of attention as a topic of research, with a wide range of applications being explored such as communicating materials. Data dissemination and storage are very important issues for sensor networks. The problem of designing data dissemination protocols for communicating material needs different analyses related to storage density and uniformity which has not been addressed sufficiently in the literature. This paper details storage protocol on the material by systematic dissemination through integrated wireless micro-sensors nodes. The performances of our solutions are evaluated through simulation using Castalia/OMNeT++. The results show that our algorithm provides uniform data storage in communicating material for different density level.
Massive MIMO versus Small-Cell Systems: Spectral and Energy Efficiency Comparison
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we study the downlink performance of two important 5G network architectures, i.e. massive multiple-input multiple-output (M-MIMO) and small-cell densification. We propose a comparative modeling for the two systems, where the user and antenna/base station (BS) locations are distributed according to Poisson point processes (PPPs). We then leverage both the stochastic geometry results and large-system analytical tool to study the SIR distribution and the average Shannon and outage rates of each network. By comparing these results, we observe that for user-average spectral efficiency, small-cell densification is favorable in crowded areas with moderate to high user density and massive MIMO with low user density. However, small-cell systems outperform M-MIMO in all cases when the performance metric is the energy efficiency. The results of this paper are useful for the optimal design of practical 5G networks.
Multiversion Conflict Notion for Transactional Memory Systems
Venue: arXiv cs.DC 2015
Year: 2015

In recent years, Software Transactional Memory systems (STMs) have garnered significant interest as an elegant alternative for addressing concurrency issues in memory. STM systems take optimistic approach. Multiple transactions are allowed to execute concurrently. On completion, each transaction is validated and if any inconsistency is observed it is aborted. Otherwise it is allowed to commit. In databases a class of histories called as conflict-serializability (CSR) based on the notion of conflicts have been identified, whose membership can be efficiently verified. As a result, CSR is the commonly used correctness criterion in databases. Similarly, using the notion of conflicts, a correctness criterion, conflict-opacity (co-opacity) which is a sub-class of can be designed whose membership can be verified in polynomial time. Using the verification mechanism, an efficient STM implementation can be designed that is permissive w.r.t co-opacity. By storing multiple versions for each transaction object, multi-version STMs provide more concurrency than single-version STMs. But the main drawback of co-opacity is that it does not admit histories that are uses multiple versions. This has motivated us to develop a new conflict notions for multi-version STMs. In this paper, we present a new conflict notion multi-version conflict. Using this conflict notion, we identify a new subclass of opacity (a popular correctness-criterion), mvc-opacity that admits multi-versioned histories and whose membership can be verified in polynomial time. We show that co-opacity is a proper subset of this class. The proposed conflict notion mv-conflict can be applied on non-sequential histories as well unlike traditional conflicts. Further, we believe that this conflict notion can be easily extended to other correctness-criterion as well.