OpenRaiser/Intern-Atlas huggingface dataset:
The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version
Venue: arXiv cs.PL 2012
Year: 2012

The classical technique for proving termination of a generic sequential computer program involves the synthesis of a ranking function for each loop of the program. Linear ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers.
The Multi-way Relay Channel
Venue: arXiv cs.IT 2012
Year: 2012

The multiuser communication channel, in which multiple users exchange information with the help of a relay terminal, termed the multi-way relay channel (mRC), is introduced. In this model, multiple interfering clusters of users communicate simultaneously, where the users within the same cluster wish to exchange messages among themselves. It is assumed that the users cannot receive each other's signals directly, and hence the relay terminal in this model is the enabler of communication. In particular, restricted encoders, which ignore the received channel output and use only the corresponding messages for generating the channel input, are considered. Achievable rate regions and an outer bound are characterized for the Gaussian mRC, and their comparison is presented in terms of exchange rates in a symmetric Gaussian network scenario. It is shown that the compress-and-forward (CF) protocol achieves exchange rates within a constant bit offset of the exchange capacity independent of the power constraints of the terminals in the network. A finite bit gap between the exchange rates achieved by the CF and the amplify-and-forward (AF) protocols is also shown. The two special cases of the mRC, the full data exchange model, in which every user wants to receive messages of all other users, and the pairwise data exchange model which consists of multiple two-way relay channels, are investigated in detail. In particular for the pairwise data exchange model, in addition to the proposed random coding based achievable schemes, a nested lattice coding based scheme is also presented and is shown to achieve exchange rates within a constant bit gap of the exchange capacity.
Capacity-Achieving Polar Codes for Arbitrarily-Permuted Parallel Channels
Venue: arXiv cs.IT 2012
Year: 2012

Channel coding over arbitrarily-permuted parallel channels was first studied by Willems et al. (2008). This paper introduces capacity-achieving polar coding schemes for arbitrarily-permuted parallel channels where the component channels are memoryless, binary-input and output-symmetric.
Variants of Mersenne Twister Suitable for Graphic Processors
Venue: arXiv cs.MS 2012
Year: 2012

This paper proposes a type of pseudorandom number generator, Mersenne Twister for Graphic Processor (MTGP), for efficient generation on graphic processessing units (GPUs). MTGP supports large state sizes such as 11213 bits, and uses the high parallelism of GPUs in computing many steps of the recursion in parallel. The second proposal is a parameter-set generator for MTGP, named MTGP Dynamic Creator (MTGPDC). MT- GPDC creates up to 2^32 distinct parameter sets which generate sequences with high-dimensional uniformity. This facility is suitable for a large grid of GPUs where each GPU requires separate random number streams. MTGP is based on linear recursion over the two-element field, and has better high-dimensional equidistribution than the Mersenne Twister pseudorandom number generator.
Discrete Variational Calculus for B-spline Approximated Curves
Venue: arXiv cs.NA 2012
Year: 2012

We study variational problems for curves approximated by B-spline curves. We show that, one can obtain discrete Euler-Lagrange equations, for the data describing the approximated curves. Our main application is to the curve completion problem in 2D and 3D. In this case, the aim is to find various aesthetically pleasing solutions as opposed to a solution of a physical problem. The Lagrangians of interest are invariant under the special Euclidean group action for which B-spline approximated curves are well suited. Smooth Lagrangians with special Euclidean symmetries involve curvature, torsion, and arc length. Expressions in these, in the original coordinates, are highly complex. We show that, by contrast, relatively simple discrete Lagrangians offer excellent results for the curve completion problem. The methods we develop for the discrete curve completion problem are general and can be used to solve other discrete variational problems for B-spline curves.
Approximating the Tutte polynomial of a binary matroid and other related combinatorial polynomials
Venue: arXiv cs.CC 2012
Year: 2012

We consider the problem of approximating certain combinatorial polynomials. First, we consider the problem of approximating the Tutte polynomial of a binary matroid with parameters q>= 2 and gamma. (Relative to the classical (x,y) parameterisation, q=(x-1)(y-1) and gamma=y-1.) A graph is a special case of a binary matroid, so earlier work by the authors shows inapproximability (subject to certain complexity assumptions) for q>2, apart from the trivial case gamma=0. The situation for q=2 is different. Previous results for graphs imply inapproximability in the region -2<=gamma<0, apart from at two "special points" where the polynomial can be computed exactly in polynomial time. For binary matroids, we extend this result by showing (i) there is no FPRAS in the region gamma<-2 unless NP=RP, and (ii) in the region gamma>0, the approximation problem is hard for the complexity class #RHPi_1 under approximation-preserving (AP) reducibility. The latter result indicates a gap in approximation complexity at q=2: whereas an FPRAS is known in the graphical case, there can be none in the binary matroid case, unless there is an FPRAS for all of #RHPi_1. The result also implies that it is computationally difficult to approximate the weight enumerator of a binary linear code, apart from at the special weights at which the problem is exactly solvable in polynomial time. As a consequence, we show that approximating the cycle index polynomial of a permutation group is hard for #RHPi_1 under AP-reducibility, partially resolving a question that we first posed in 1992.
A general method for deciding about logically constrained issues
Venue: arXiv cs.AI 2012
Year: 2012

A general method is given for revising degrees of belief and arriving at consistent decisions about a system of logically constrained issues. In contrast to other works about belief revision, here the constraints are assumed to be fixed. The method has two variants, dual of each other, whose revised degrees of belief are respectively above and below the original ones. The upper [resp. lower] revised degrees of belief are uniquely characterized as the lowest [resp. highest] ones that are invariant by a certain max-min [resp. min-max] operation determined by the logical constraints. In both variants, making balance between the revised degree of belief of a proposition and that of its negation leads to decisions that are ensured to be consistent with the logical constraints. These decisions are ensured to agree with the majority criterion as applied to the original degrees of belief whenever this gives a consistent result. They are also also ensured to satisfy a property of respect for unanimity about any particular issue, as well as a property of monotonicity with respect to the original degrees of belief. The application of the method to certain special domains comes down to well established or increasingly accepted methods, such as the single-link method of cluster analysis and the method of paths in preferential voting.
Fast L1-Minimization Algorithms For Robust Face Recognition
Venue: arXiv cs.CV 2012
Year: 2012

L1-minimization refers to finding the minimum L1-norm solution to an underdetermined linear system b=Ax. Under certain conditions as described in compressive sensing theory, the minimum L1-norm solution is also the sparsest solution. In this paper, our study addresses the speed and scalability of its algorithms. In particular, we focus on the numerical implementation of a sparsity-based classification framework in robust face recognition, where sparse representation is sought to recover human identities from very high-dimensional facial images that may be corrupted by illumination, facial disguise, and pose variation. Although the underlying numerical problem is a linear program, traditional algorithms are known to suffer poor scalability for large-scale applications. We investigate a new solution based on a classical convex optimization framework, known as Augmented Lagrangian Methods (ALM). The new convex solvers provide a viable solution to real-world, time-critical applications such as face recognition. We conduct extensive experiments to validate and compare the performance of the ALM algorithms against several popular L1-minimization solvers, including interior-point method, Homotopy, FISTA, SESOP-PCD, approximate message passing (AMP) and TFOCS. To aid peer evaluation, the code for all the algorithms has been made publicly available.
Submodular Functions: Learnability, Structure, and Optimization
Venue: arXiv cs.DS 2012
Year: 2012

Submodular functions are discrete functions that model laws of diminishing returns and enjoy numerous algorithmic applications. They have been used in many areas, including combinatorial optimization, machine learning, and economics. In this work we study submodular functions from a learning theoretic angle. We provide algorithms for learning submodular functions, as well as lower bounds on their learnability. In doing so, we uncover several novel structural results revealing ways in which submodular functions can be both surprisingly structured and surprisingly unstructured. We provide several concrete implications of our work in other domains including algorithmic game theory and combinatorial optimization. At a technical level, this research combines ideas from many areas, including learning theory (distributional learning and PAC-style analyses), combinatorics and optimization (matroids and submodular functions), and pseudorandomness (lossless expander graphs).
Bottleneck of using single memristor as a synapse and its solution
Venue: arXiv cs.NE 2012
Year: 2012

It is now widely accepted that memristive devices are perfect candidates for the emulation of biological synapses in neuromorphic systems. This is mainly because of the fact that like the strength of synapse, memristance of the memristive device can be tuned actively (e.g., by the application of volt- age or current). In addition, it is also possible to fabricate very high density of memristive devices (comparable to the number of synapses in real biological system) through the nano-crossbar structures. However, in this paper we will show that there are some problems associated with memristive synapses (memristive devices which are playing the role of biological synapses). For example, we show that the variation rate of the memristance of memristive device depends completely on the current memristance of the device and therefore it can change significantly with time during the learning phase. This phenomenon can degrade the performance of learning methods like Spike Timing-Dependent Plasticity (STDP) and cause the corresponding neuromorphic systems to become unstable. Finally, at the end of this paper, we illustrate that using two serially connected memristive devices with different polarities as a synapse can somewhat fix the aforementioned problem.
Intra- and Inter-Session Network Coding in Wireless Networks
Venue: arXiv cs.NI 2012
Year: 2012

In this paper, we are interested in improving the performance of constructive network coding schemes in lossy wireless environments.We propose I2NC - a cross-layer approach that combines inter-session and intra-session network coding and has two strengths. First, the error-correcting capabilities of intra-session network coding make our scheme resilient to loss. Second, redundancy allows intermediate nodes to operate without knowledge of the decoding buffers of their neighbors. Based only on the knowledge of the loss rates on the direct and overhearing links, intermediate nodes can make decisions for both intra-session (i.e., how much redundancy to add in each flow) and inter-session (i.e., what percentage of flows to code together) coding. Our approach is grounded on a network utility maximization (NUM) formulation of the problem. We propose two practical schemes, I2NC-state and I2NC-stateless, which mimic the structure of the NUM optimal solution. We also address the interaction of our approach with the transport layer. We demonstrate the benefits of our schemes through simulations.
Empirical processes, typical sequences and coordinated actions in standard Borel spaces
Venue: arXiv cs.IT 2012
Year: 2012

This paper proposes a new notion of typical sequences on a wide class of abstract alphabets (so-called standard Borel spaces), which is based on approximations of memoryless sources by empirical distributions uniformly over a class of measurable "test functions." In the finite-alphabet case, we can take all uniformly bounded functions and recover the usual notion of strong typicality (or typicality under the total variation distance). For a general alphabet, however, this function class turns out to be too large, and must be restricted. With this in mind, we define typicality with respect to any Glivenko-Cantelli function class (i.e., a function class that admits a Uniform Law of Large Numbers) and demonstrate its power by giving simple derivations of the fundamental limits on the achievable rates in several source coding scenarios, in which the relevant operational criteria pertain to reproducing empirical averages of a general-alphabet stationary memoryless source with respect to a suitable function class.
Opinion fluctuations and disagreement in social networks
Venue: arXiv cs.SI 2012
Year: 2012

We study a tractable opinion dynamics model that generates long-run disagreements and persistent opinion fluctuations. Our model involves an inhomogeneous stochastic gossip process of continuous opinion dynamics in a society consisting of two types of agents: regular agents, who update their beliefs according to information that they receive from their social neighbors; and stubborn agents, who never update their opinions. When the society contains stubborn agents with different opinions, the belief dynamics never lead to a consensus (among the regular agents). Instead, beliefs in the society fail to converge almost surely, the belief profile keeps on fluctuating in an ergodic fashion, and it converges in law to a non-degenerate random vector. The structure of the network and the location of the stubborn agents within it shape the opinion dynamics. The expected belief vector evolves according to an ordinary differential equation coinciding with the Kolmogorov backward equation of a continuous-time Markov chain with absorbing states corresponding to the stubborn agents and converges to a harmonic vector, with every regular agent's value being the weighted average of its neighbors' values, and boundary conditions corresponding to the stubborn agents'. Expected cross-products of the agents' beliefs allow for a similar characterization in terms of coupled Markov chains on the network. We prove that, in large-scale societies which are highly fluid, meaning that the product of the mixing time of the Markov chain on the graph describing the social network and the relative size of the linkages to stubborn agents vanishes as the population size grows large, a condition of \emph{homogeneous influence} emerges, whereby the stationary beliefs' marginal distributions of most of the regular agents have approximately equal first and second moments.
Improving the Space-Bounded Version of Muchnik's Conditional Complexity Theorem via "Naive" Derandomization
Venue: arXiv cs.CC 2012
Year: 2012

Many theorems about Kolmogorov complexity rely on existence of combinatorial objects with specific properties. Usually the probabilistic method gives such objects with better parameters than explicit constructions do. But the probabilistic method does not give "effective" variants of such theorems, i.e. variants for resource-bounded Kolmogorov complexity. We show that a "naive derandomization" approach of replacing these objects by the output of Nisan-Wigderson pseudo-random generator may give polynomial-space variants of such theorems. Specifically, we improve the preceding polynomial-space analogue of Muchnik's conditional complexity theorem. I.e., for all $a$ and $b$ there exists a program $p$ of least possible length that transforms $a$ to $b$ and is simple conditional on $b$. Here all programs work in polynomial space and all complexities are measured with logarithmic accuracy instead of polylogarithmic one in the previous work.
Cooperative Precoding with Limited Feedback for MIMO Interference Channels
Venue: arXiv cs.IT 2012
Year: 2012

Multi-antenna precoding effectively mitigates the interference in wireless networks. However, the resultant performance gains can be significantly compromised in practice if the precoder design fails to account for the inaccuracy in the channel state information (CSI) feedback. This paper addresses this issue by considering finite-rate CSI feedback from receivers to their interfering transmitters in the two-user multiple-input-multiple-output (MIMO) interference channel, called cooperative feedback, and proposing a systematic method for designing transceivers comprising linear precoders and equalizers. Specifically, each precoder/equalizer is decomposed into inner and outer components for nulling the cross-link interference and achieving array gain, respectively. The inner precoders/equalizers are further optimized to suppress the residual interference resulting from finite-rate cooperative feedback. Further- more, the residual interference is regulated by additional scalar cooperative feedback signals that are designed to control transmission power using different criteria including fixed interference margin and maximum sum throughput. Finally, the required number of cooperative precoder feedback bits is derived for limiting the throughput loss due to precoder quantization.
Exploiting Statistical Dependencies in Sparse Representations for Signal Recovery
Venue: arXiv cs.IT 2012
Year: 2012

Signal modeling lies at the core of numerous signal and image processing applications. A recent approach that has drawn considerable attention is sparse representation modeling, in which the signal is assumed to be generated as a combination of a few atoms from a given dictionary. In this work we consider a Bayesian setting and go beyond the classic assumption of independence between the atoms. The main goal of this paper is to introduce a statistical model that takes such dependencies into account and show how this model can be used for sparse signal recovery. We follow the suggestion of two recent works and assume that the sparsity pattern is modeled by a Boltzmann machine, a commonly used graphical model. For general dependency models, exact MAP and MMSE estimation of the sparse representation becomes computationally complex. To simplify the computations, we propose greedy approximations of the MAP and MMSE estimators. We then consider a special case in which exact MAP is feasible, by assuming that the dictionary is unitary and the dependency model corresponds to a certain sparse graph. Exploiting this structure, we develop an efficient message passing algorithm that recovers the underlying signal. When the model parameters defining the underlying graph are unknown, we suggest an algorithm that learns these parameters directly from the data, leading to an iterative scheme for adaptive sparse signal recovery. The effectiveness of our approach is demonstrated on real-life signals - patches of natural images - where we compare the denoising performance to that of previous recovery methods that do not exploit the statistical dependencies.
On the size of identifying codes in triangle-free graphs
Venue: arXiv cs.DM 2012
Year: 2012

In an undirected graph $G$, a subset $C\subseteq V(G)$ such that $C$ is a dominating set of $G$, and each vertex in $V(G)$ is dominated by a distinct subset of vertices from $C$, is called an identifying code of $G$. The concept of identifying codes was introduced by Karpovsky, Chakrabarty and Levitin in 1998. For a given identifiable graph $G$, let $\M(G)$ be the minimum cardinality of an identifying code in $G$. In this paper, we show that for any connected identifiable triangle-free graph $G$ on $n$ vertices having maximum degree $Δ\geq 3$, $\M(G)\le n-\tfrac{n}{Δ+o(Δ)}$. This bound is asymptotically tight up to constants due to various classes of graphs including $(Δ-1)$-ary trees, which are known to have their minimum identifying code of size $n-\tfrac{n}{Δ-1+o(1)}$. We also provide improved bounds for restricted subfamilies of triangle-free graphs, and conjecture that there exists some constant $c$ such that the bound $\M(G)\le n-\tfrac{n}Δ+c$ holds for any nontrivial connected identifiable graph $G$.
Linearity in the non-deterministic call-by-value setting
Venue: arXiv cs.LO 2012
Year: 2012

We consider the non-deterministic extension of the call-by-value lambda calculus, which corresponds to the additive fragment of the linear-algebraic lambda-calculus. We define a fine-grained type system, capturing the right linearity present in such formalisms. After proving the subject reduction and the strong normalisation properties, we propose a translation of this calculus into the System F with pairs, which corresponds to a non linear fragment of linear logic. The translation provides a deeper understanding of the linearity in our setting.
Continuation-Passing C: compiling threads to events through continuations
Venue: arXiv cs.PL 2012
Year: 2012

In this paper, we introduce Continuation Passing C (CPC), a programming language for concurrent systems in which native and cooperative threads are unified and presented to the programmer as a single abstraction. The CPC compiler uses a compilation technique, based on the CPS transform, that yields efficient code and an extremely lightweight representation for contexts. We provide a proof of the correctness of our compilation scheme. We show in particular that lambda-lifting, a common compilation technique for functional languages, is also correct in an imperative language like C, under some conditions enforced by the CPC compiler. The current CPC compiler is mature enough to write substantial programs such as Hekate, a highly concurrent BitTorrent seeder. Our benchmark results show that CPC is as efficient, while using significantly less space, as the most efficient thread libraries available.