OpenRaiser/Intern-Atlas huggingface dataset:
Abstract interpretation as anti-refinement
Venue: arXiv cs.PL 2014
Year: 2014

This article shows a correspondence between abstract interpretation of imperative programs and the refinement calculus: in the refinement calculus, an abstract interpretation of a program is a specification which is a function. This correspondence can be used to guide the design of mechanically verified static analyses, keeping the correctness proof well separated from the heuristic parts of the algorithms.
Signal Reconstruction from Rechargeable Wireless Sensor Networks using Sparse Random Projections
Venue: arXiv cs.NI 2014
Year: 2014

Due to non-homogeneous spread of sunlight, sensing nodes possess non-uniform energy budget in recharge- able Wireless Sensor Networks (WSNs). An energy-aware workload distribution strategy is therefore nec- essary to achieve good data accuracy subject to energy-neutral operation. Recently proposed signal approx- imation strategies assume uniform sampling and fail to ensure energy neutral operation in rechargeable wireless sensor networks. We propose EAST (Energy Aware Sparse approximation Technique), which ap- proximates a signal, by adapting sensor node sampling workload according to solar energy availability. To the best of our knowledge, we are the first to propose sparse approximation to model energy-aware workload distribution in rechargeable WSNs. Experimental results, using data from an outdoor WSN deployment suggest that EAST significantly improves the approximation accuracy offering approximately 50% higher sensor on-time. EAST requires the approximation error to be known beforehand to determine the number of measure- ments. However, it is not always possible to decide the accuracy a-priori. We improve EAST and propose EAST+, which, given only the energy budget of the nodes, computes the optimal number of measurements subject to the energy neutral operation.
ImageSpirit: Verbal Guided Image Parsing
Venue: arXiv cs.GR 2014
Year: 2014

Humans describe images in terms of nouns and adjectives while algorithms operate on images represented as sets of pixels. Bridging this gap between how humans would like to access images versus their typical representation is the goal of image parsing, which involves assigning object and attribute labels to pixel. In this paper we propose treating nouns as object labels and adjectives as visual attribute labels. This allows us to formulate the image parsing problem as one of jointly estimating per-pixel object and attribute labels from a set of training images. We propose an efficient (interactive time) solution. Using the extracted labels as handles, our system empowers a user to verbally refine the results. This enables hands-free parsing of an image into pixel-wise object/attribute labels that correspond to human semantics. Verbally selecting objects of interests enables a novel and natural interaction modality that can possibly be used to interact with new generation devices (e.g. smart phones, Google Glass, living room devices). We demonstrate our system on a large number of real-world images with varying complexity. To help understand the tradeoffs compared to traditional mouse based interactions, results are reported for both a large scale quantitative evaluation and a user study.
Submodular Stochastic Probing on Matroids
Venue: arXiv cs.DS 2014
Year: 2014

In a stochastic probing problem we are given a universe $E$, where each element $e \in E$ is active independently with probability $p_e$, and only a probe of e can tell us whether it is active or not. On this universe we execute a process that one by one probes elements --- if a probed element is active, then we have to include it in the solution, which we gradually construct. Throughout the process we need to obey inner constraints on the set of elements taken into the solution, and outer constraints on the set of all probed elements. This abstract model was presented by Gupta and Nagarajan (IPCO '13), and provides a unified view of a number of problems. Thus far, all the results falling under this general framework pertain mainly to the case in which we are maximizing a linear objective function of the successfully probed elements. In this paper we generalize the stochastic probing problem by considering a monotone submodular objective function. We give a $(1 - 1/e)/(k_{in} + k_{out}+1)$-approximation algorithm for the case in which we are given $k_{in}$ matroids as inner constraints and $k_{out}$ matroids as outer constraints. Additionally, we obtain an improved $1/(k_{in} + k_{out})$-approximation algorithm for linear objective functions.
Content-Specific Broadcast Cellular Networks based on User Demand Prediction: A Revenue Perspective
Venue: arXiv cs.NI 2014
Year: 2014

The Long Term Evolution (LTE) broadcast is a promising solution to cope with exponentially increasing user traffic by broadcasting common user requests over the same frequency channels. In this paper, we propose a novel network framework provisioning broadcast and unicast services simultaneously. For each serving file to users, a cellular base station determines either to broadcast or unicast the file based on user demand prediction examining the file's content specific characteristics such as: file size, delay tolerance, price sensitivity. In a network operator's revenue maximization perspective while not inflicting any user payoff degradation, we jointly optimize resource allocation, pricing, and file scheduling. In accordance with the state of the art LTE specifications, the proposed network demonstrates up to 32% increase in revenue for a single cell and more than a 7-fold increase for a 7 cell coordinated LTE broadcast network, compared to the conventional unicast cellular networks.
Effective Quotation: relating approaches to language-integrated query
Venue: arXiv cs.PL 2014
Year: 2014

Language-integrated query techniques have been explored in a number of different language designs. We consider two different, type-safe approaches employed by Links and F#. Both approaches provide rich dynamic query generation capabilities, and thus amount to a form of heterogeneous staged computation, but to date there has been no formal investigation of their relative expressiveness. We present two core calculi Eff and Quot, respectively capturing the essential aspects of language-integrated querying using effects in Links and quotation in LINQ. We show via translations from Eff to Quot and back that the two approaches are equivalent in expressiveness. Based on the translation from Eff to Quot, we extend a simple Links compiler to handle queries.
Principal motion components for gesture recognition using a single-example
Venue: arXiv cs.CV 2014
Year: 2014

This paper introduces principal motion components (PMC), a new method for one-shot gesture recognition. In the considered scenario a single training-video is available for each gesture to be recognized, which limits the application of traditional techniques (e.g., HMMs). In PMC, a 2D map of motion energy is obtained per each pair of consecutive frames in a video. Motion maps associated to a video are processed to obtain a PCA model, which is used for recognition under a reconstruction-error approach. The main benefits of the proposed approach are its simplicity, easiness of implementation, competitive performance and efficiency. We report experimental results in one-shot gesture recognition using the ChaLearn Gesture Dataset; a benchmark comprising more than 50,000 gestures, recorded as both RGB and depth video with a Kinect camera. Results obtained with PMC are competitive with alternative methods proposed for the same data set.
The (Nested) Word Problem
Venue: arXiv cs.FL 2014
Year: 2014

In this article we provide a new perspective on the word problem of a group by using languages of nested words. These were introduced by Alur and Madhusudan as a way to model programming languages such as HTML. We demonstrate how a class of nested word languages called visibly pushdown can be used to study the word problem of virtually free groups in a natural way.
How To Place a Point to Maximize Angles
Venue: arXiv cs.CG 2014
Year: 2014

We describe a randomized algorithm that, given a set $P$ of points in the plane, computes the best location to insert a new point $p$, such that the Delaunay triangulation of $P\cup\{p\}$ has the largest possible minimum angle. The expected running time of our algorithm is at most cubic, improving the roughly quartic time of the best previously known algorithm. It slows down to slightly super-cubic if we also specify a set of non-crossing segments with endpoints in $P$ and insist that the triangulation respect these segments, i.e., is the constrained Delaunay triangulation of the points and segments.
Secret Key Cryptosystem based on Non-Systematic Polar Codes
Venue: arXiv cs.CR 2014
Year: 2014

Polar codes are a new class of error correcting linear block codes, whose generator matrix is specified by the knowledge of transmission channel parameters, code length and code dimension. Moreover, regarding computational security, it is assumed that an attacker with a restricted processing power has unlimited access to the transmission media. Therefore, the attacker can construct the generator matrix of polar codes, especially in the case of Binary Erasure Channels, on which this matrix can be easily constructed. In this paper, we introduce a novel method to keep the generator matrix of polar codes in secret in a way that the attacker cannot access the required information to decode the intended polar code. With the help of this method, a secret key cryptosystem is proposed based on non-systematic polar codes. In fact, the main objective of this study is to achieve an acceptable level of security and reliability through taking advantage of the special properties of polar codes. The analyses revealed that our scheme resists the typical attacks on the secret key cryptosystems based on linear block codes. In addition, by employing some efficient methods, the key length of the proposed scheme is decreased compared to that of the previous cryptosystems. Moreover, this scheme enjoys other advantages including high code rate, and proper error performance as well.
Some hard families of parameterised counting problems
Venue: arXiv cs.CC 2014
Year: 2014

We consider parameterised subgraph-counting problems of the following form: given a graph G, how many k-tuples of its vertices have a given property? A number of such problems are known to be #W[1]-complete; here we substantially generalise some of these existing results by proving hardness for two large families of such problems. We demonstrate that it is #W[1]-hard to count the number of k-vertex subgraphs having any property where the number of distinct edge-densities of labelled subgraphs that satisfy the property is o(k^2). In the special case that the property in question depends only on the number of edges in the subgraph, we give a strengthening of this result which leads to our second family of hard problems.
Dealing with Interference in Distributed Large-scale MIMO Systems: A Statistical Approach
Venue: arXiv cs.IT 2014
Year: 2014

This paper considers the problem of interference control through the use of second-order statistics in massive MIMO multi-cell networks. We consider both the cases of co-located massive arrays and large-scale distributed antenna settings. We are interested in characterizing the low-rankness of users' channel covariance matrices, as such a property can be exploited towards improved channel estimation (so-called pilot decontamination) as well as interference rejection via spatial filtering. In previous work, it was shown that massive MIMO channel covariance matrices exhibit a useful finite rank property that can be modeled via the angular spread of multipath at a MIMO uniform linear array. This paper extends this result to more general settings including certain non-uniform arrays, and more surprisingly, to two dimensional distributed large scale arrays. In particular our model exhibits the dependence of the signal subspace's richness on the scattering radius around the user terminal, through a closed form expression. The applications of the low-rankness covariance property to channel estimation's denoising and low-complexity interference filtering are highlighted.
Mining Maximal Cliques from an Uncertain Graph
Venue: arXiv cs.DS 2014
Year: 2014

We consider mining dense substructures (maximal cliques) from an uncertain graph, which is a probability distribution on a set of deterministic graphs. For parameter 0 < α < 1, we present a precise definition of an α-maximal clique in an uncertain graph. We present matching upper and lower bounds on the number of α-maximal cliques possible within an uncertain graph. We present an algorithm to enumerate α-maximal cliques in an uncertain graph whose worst-case runtime is near-optimal, and an experimental evaluation showing the practical utility of the algorithm.
Electric Vehicle Charging Station Placement: Formulation, Complexity, and Solutions
Venue: arXiv cs.SY 2014
Year: 2014

To enhance environmental sustainability, many countries will electrify their transportation systems in their future smart city plans. So the number of electric vehicles (EVs) running in a city will grow significantly. There are many ways to re-charge EVs' batteries and charging stations will be considered as the main source of energy. The locations of charging stations are critical; they should not only be pervasive enough such that an EV anywhere can easily access a charging station within its driving range, but also widely spread so that EVs can cruise around the whole city upon being re-charged. Based on these new perspectives, we formulate the Electric Vehicle Charging Station Placement Problem (EVCSPP) in this paper. We prove that the problem is non-deterministic polynomial-time hard. We also propose four solution methods to tackle EVCSPP and evaluate their performance on various artificial and practical cases. As verified by the simulation results, the methods have their own characteristics and they are suitable for different situations depending on the requirements for solution quality, algorithmic efficiency, problem size, nature of the algorithm, and existence of system prerequisite.
A New Push-Relabel Algorithm for Sparse Networks
Venue: arXiv cs.DS 2014
Year: 2014

In this paper, we present a new push-relabel algorithm for the maximum flow problem on flow networks with $n$ vertices and $m$ arcs. Our algorithm computes a maximum flow in $O(mn)$ time on sparse networks where $m = O(n)$. To our knowledge, this is the first $O(mn)$ time push-relabel algorithm for the $m = O(n)$ edge case; previously, it was known that push-relabel implementations could find a max-flow in $O(mn)$ time when $m = Ω(n^{1+ε})$ (King, et. al., SODA `92). This also matches a recent flow decomposition-based algorithm due to Orlin (STOC `13), which finds a max-flow in $O(mn)$ time on sparse networks. Our main result is improving on the Excess-Scaling algorithm (Ahuja & Orlin, 1989) by reducing the number of nonsaturating pushes to $O(mn)$ across all scaling phases. This is reached by combining Ahuja and Orlin's algorithm with Orlin's compact flow networks. A contribution of this paper is demonstrating that the compact networks technique can be extended to the push-relabel family of algorithms. We also provide evidence that this approach could be a promising avenue towards an $O(mn)$-time algorithm for all edge densities.
Deep AutoRegressive Networks
Venue: arXiv cs.LG 2014
Year: 2014

We introduce a deep, generative autoencoder capable of learning hierarchies of distributed representations from data. Successive deep stochastic hidden layers are equipped with autoregressive connections, which enable the model to be sampled from quickly and exactly via ancestral sampling. We derive an efficient approximate parameter estimation method based on the minimum description length (MDL) principle, which can be seen as maximising a variational lower bound on the log-likelihood, with a feedforward neural network implementing approximate inference. We demonstrate state-of-the-art generative performance on a number of classic data sets: several UCI data sets, MNIST and Atari 2600 games.
$L_{1/2}$ Regularization: Convergence of Iterative Half Thresholding Algorithm
Venue: arXiv cs.NA 2014
Year: 2014

In recent studies on sparse modeling, the nonconvex regularization approaches (particularly, $L_{q}$ regularization with $q\in(0,1)$) have been demonstrated to possess capability of gaining much benefit in sparsity-inducing and efficiency. As compared with the convex regularization approaches (say, $L_{1}$ regularization), however, the convergence issue of the corresponding algorithms are more difficult to tackle. In this paper, we deal with this difficult issue for a specific but typical nonconvex regularization scheme, the $L_{1/2}$ regularization, which has been successfully used to many applications. More specifically, we study the convergence of the iterative \textit{half} thresholding algorithm (the \textit{half} algorithm for short), one of the most efficient and important algorithms for solution to the $L_{1/2}$ regularization. As the main result, we show that under certain conditions, the \textit{half} algorithm converges to a local minimizer of the $L_{1/2}$ regularization, with an eventually linear convergence rate. The established result provides a theoretical guarantee for a wide range of applications of the \textit{half} algorithm. We provide also a set of simulations to support the correctness of theoretical assertions and compare the time efficiency of the \textit{half} algorithm with other known typical algorithms for $L_{1/2}$ regularization like the iteratively reweighted least squares (IRLS) algorithm and the iteratively reweighted $l_{1}$ minimization (IRL1) algorithm.
Capturing Variation and Uncertainty in Human Judgment
Venue: arXiv cs.IR 2014
Year: 2014

The well-studied problem of statistical rank aggregation has been applied to comparing sports teams, information retrieval, and most recently to data generated by human judgment. Such human-generated rankings may be substantially different from traditional statistical ranking data. In this work, we show that a recently proposed generalized random utility model reveals distinctive patterns in human judgment across three different domains, and provides a succinct representation of variance in both population preferences and imperfect perception. In contrast, we also show that classical statistical ranking models fail to capture important features from human-generated input. Our work motivates the use of more flexible ranking models for representing and describing the collective preferences or decision-making of human participants.
Modeling Vanilla Option prices: A simulation study by an implicit method
Venue: arXiv cs.CE 2014
Year: 2014

Option contracts can be valued by using the Black-Scholes equation, a partial differential equation with initial conditions. An exact solution for European style options is known. The computation time and the error need to be minimized simultaneously. In this paper, the authors have solved the Black-Scholes equation by employing a reasonably accurate implicit method. Options with known analytic solutions have been evaluated. Furthermore, an overall second order accurate space and time discretization is proposed in this paper Keywords: Computational finance, implicit methods, finite differences, call/put options.
Abstract Acceleration of General Linear Loops
Venue: arXiv cs.PL 2014
Year: 2014

We present abstract acceleration techniques for computing loop invariants for numerical programs with linear assignments and conditionals. Whereas abstract interpretation techniques typically over-approximate the set of reachable states iteratively, abstract acceleration captures the effect of the loop with a single, non-iterative transfer function applied to the initial states at the loop head. In contrast to previous acceleration techniques, our approach applies to any linear loop without restrictions. Its novelty lies in the use of the Jordan normal form decomposition of the loop body to derive symbolic expressions for the entries of the matrix modeling the effect of n>=0 iterations of the loop. The entries of such a matrix depend on $n$ through complex polynomial, exponential and trigonometric functions. Therefore, we introduces an abstract domain for matrices that captures the linear inequality relations between these complex expressions. This results in an abstract matrix for describing the fixpoint semantics of the loop. Our approach integrates smoothly into standard abstract interpreters and can handle programs with nested loops and loops containing conditional branches. We evaluate it over small but complex loops that are commonly found in control software, comparing it with other tools for computing linear loop invariants. The loops in our benchmarks typically exhibit polynomial, exponential and oscillatory behaviors that present challenges to existing approaches. Our approach finds non-trivial invariants to prove useful bounds on the values of variables for such loops, clearly outperforming the existing approaches in terms of precision while exhibiting good performance.
Unary languages recognized by two-way one-counter automata
Venue: arXiv cs.FL 2014
Year: 2014

A two-way deterministic finite state automaton with one counter (2D1CA) is a fundamental computational model that has been examined in many different aspects since sixties, but we know little about its power in the case of unary languages. Up to our knowledge, the only known unary nonregular languages recognized by 2D1CAs are those formed by strings having exponential length, where the exponents form some trivial unary regular language. In this paper, we present some non-trivial subsets of these languages. By using the input head as a second counter, we present simulations of two-way deterministic finite automata with linearly bounded counters and linear--space Turing machines. We also show how a fixed-size quantum register can help to simplify some of these languages. Finally, we compare unary 2D1CAs with two--counter machines and provide some insights about the limits of their computational power.
A general construction for monoid-based knapsack protocols
Venue: arXiv cs.CR 2014
Year: 2014

We present a generalized version of the knapsack protocol proposed by D. Naccache and J. Stern at the Proceedings of Eurocrypt (1997). Our new framework will allow the construction of other knapsack protocols having similar security features. We will outline a very concrete example of a new protocol using extension fields of a finite field of small characteristic instead of the prime field Z/pZ, but more efficient in terms of computational costs for asymptotically equal information rate and similar key size.