OpenRaiser/Intern-Atlas huggingface dataset:
Cause Clue Clauses: Error Localization using Maximum Satisfiability
Venue: arXiv cs.PL 2011
Year: 2011

Much effort is spent everyday by programmers in trying to reduce long, failing execution traces to the cause of the error. We present a new algorithm for error cause localization based on a reduction to the maximal satisfiability problem (MAX-SAT), which asks what is the maximum number of clauses of a Boolean formula that can be simultaneously satisfied by an assignment. At an intuitive level, our algorithm takes as input a program and a failing test, and comprises the following three steps. First, using symbolic execution, we encode a trace of a program as a Boolean trace formula which is satisfiable iff the trace is feasible. Second, for a failing program execution (e.g., one that violates an assertion or a post-condition), we construct an unsatisfiable formula by taking the trace formula and additionally asserting that the input is the failing test and that the assertion condition does hold at the end. Third, using MAX-SAT, we find a maximal set of clauses in this formula that can be satisfied together, and output the complement set as a potential cause of the error. We have implemented our algorithm in a tool called bug-assist for C programs. We demonstrate the surprising effectiveness of the tool on a set of benchmark examples with injected faults, and show that in most cases, bug-assist can quickly and precisely isolate the exact few lines of code whose change eliminates the error. We also demonstrate how our algorithm can be modified to automatically suggest fixes for common classes of errors such as off-by-one.
Analytical Solution of Covariance Evolution for Irregular LDPC Codes
Venue: arXiv cs.IT 2011
Year: 2011

A scaling law developed by Amraoui et al. is a powerful technique to estimate the block error probability of finite length low-density parity-check (LDPC) codes. Solving a system of differential equations called covariance evolution is a method to obtain the scaling parameter. However, the covariance evolution has not been analytically solved. In this paper, we present the analytical solution of the covariance evolution for irregular LDPC code ensembles.
Least Squares Ranking on Graphs
Venue: arXiv cs.NA 2011
Year: 2011

Given a set of alternatives to be ranked, and some pairwise comparison data, ranking is a least squares computation on a graph. The vertices are the alternatives, and the edge values comprise the comparison data. The basic idea is very simple and old: come up with values on vertices such that their differences match the given edge data. Since an exact match will usually be impossible, one settles for matching in a least squares sense. This formulation was first described by Leake in 1976 for rankingfootball teams and appears as an example in Professor Gilbert Strang's classic linear algebra textbook. If one is willing to look into the residual a little further, then the problem really comes alive, as shown effectively by the remarkable recent paper of Jiang et al. With or without this twist, the humble least squares problem on graphs has far-reaching connections with many current areas ofresearch. These connections are to theoretical computer science (spectral graph theory, and multilevel methods for graph Laplacian systems); numerical analysis (algebraic multigrid, and finite element exterior calculus); other mathematics (Hodge decomposition, and random clique complexes); and applications (arbitrage, and ranking of sports teams). Not all of these connections are explored in this paper, but many are. The underlying ideas are easy to explain, requiring only the four fundamental subspaces from elementary linear algebra. One of our aims is to explain these basic ideas and connections, to get researchers in many fields interested in this topic. Another aim is to use our numerical experiments for guidance on selecting methods and exposing the need for further development.
The Local Emergence and Global Diffusion of Research Technologies: An Exploration of Patterns of Network Formation
Venue: arXiv cs.DL 2011
Year: 2011

Grasping the fruits of "emerging technologies" is an objective of many government priority programs in a knowledge-based and globalizing economy. We use the publication records (in the Science Citation Index) of two emerging technologies to study the mechanisms of diffusion in the case of two innovation trajectories: small interference RNA (siRNA) and nano-crystalline solar cells (NCSC). Methods for analyzing and visualizing geographical and cognitive diffusion are specified as indicators of different dynamics. Geographical diffusion is illustrated with overlays to Google Maps; cognitive diffusion is mapped using an overlay to a map based on the ISI Subject Categories. The evolving geographical networks show both preferential attachment and small-world characteristics. The strength of preferential attachment decreases over time, while the network evolves into an oligopolistic control structure with small-world characteristics. The transition from disciplinary-oriented ("mode-1") to transfer-oriented ("mode-2") research is suggested as the crucial difference in explaining the different rates of diffusion between siRNA and NCSC.
Generic Modal Cut Elimination Applied to Conditional Logics
Venue: arXiv cs.LO 2011
Year: 2011

We develop a general criterion for cut elimination in sequent calculi for propositional modal logics, which rests on absorption of cut, contraction, weakening and inversion by the purely modal part of the rule system. Our criterion applies also to a wide variety of logics outside the realm of normal modal logic. We give extensive example instantiations of our framework to various conditional logics. For these, we obtain fully internalised calculi which are substantially simpler than those known in the literature, along with leaner proofs of cut elimination and complexity. In one case, conditional logic with modus ponens and conditional excluded middle, cut elimination and complexity were explicitly stated as open in the literature.
Biologically Inspired Design Principles for Scalable, Robust, Adaptive, Decentralized Search and Automated Response (RADAR)
Venue: arXiv cs.NE 2011
Year: 2011

Distributed search problems are ubiquitous in Artificial Life (ALife). Many distributed search problems require identifying a rare and previously unseen event and producing a rapid response. This challenge amounts to finding and removing an unknown needle in a very large haystack. Traditional computational search models are unlikely to find, nonetheless, appropriately respond to, novel events, particularly given data distributed across multiple platforms in a variety of formats and sources with variable and unknown reliability. Biological systems have evolved solutions to distributed search and response under uncertainty. Immune systems and ant colonies efficiently scale up massively parallel search with automated response in highly dynamic environments, and both do so using distributed coordination without centralized control. These properties are relevant to ALife, where distributed, autonomous, robust and adaptive control is needed to design robot swarms, mobile computing networks, computer security systems and other distributed intelligent systems. They are also relevant for searching, tracking the spread of ideas, and understanding the impact of innovations in online social networks. We review design principles for Scalable Robust, Adaptive, Decentralized search with Automated Response (Scalable RADAR) in biology. We discuss how biological RADAR scales up efficiently, and then discuss in detail how modular search in the immune system can be mimicked or built upon in ALife. Such search mechanisms are particularly useful when components have limited capacity to communicate and social or physical distance makes long distance communication more costly.
Complexity of Existential Positive First-Order Logic
Venue: arXiv cs.CC 2011
Year: 2011

Let gamma be a (not necessarily finite) structure with a finite relational signature. We prove that deciding whether a given existential positive sentence holds in gamma is in Logspace or complete for the class CSP(gamma)_NP under deterministic polynomial-time many-one reductions. Here, CSP(gamma)_NP is the class of problems that can be reduced to the Constraint Satisfaction Problem of gamma under non-deterministic polynomial-time many-one reductions.
La réduction de termes complexes dans les langues de spécialité
Venue: arXiv cs.CL 2011
Year: 2011

Our study applies statistical methods to French and Italian corpora to examine the phenomenon of multi-word term reduction in specialty languages. There are two kinds of reduction: anaphoric and lexical. We show that anaphoric reduction depends on the discourse type (vulgarization, pedagogical, specialized) but is independent of both domain and language; that lexical reduction depends on domain and is more frequent in technical, rapidly evolving domains; and that anaphoric reductions tend to follow full terms rather than precede them. We define the notion of the anaphoric tree of the term and study its properties. Concerning lexical reduction, we attempt to prove statistically that there is a notion of term lifecycle, where the full form is progressively replaced by a lexical reduction. ----- Nous étudions par des méthodes statistiques sur des corpus français et italiens, le phénomène de réduction des termes complexes dans les langues de spécialité. Il existe deux types de réductions : anaphorique et lexicale. Nous montrons que la réduction anaphorique dépend du type de discours (de vulgarisation, pédagogique, spécialisé) mais ne dépend ni du domaine, ni de la langue, alors que la réduction lexicale dépend du domaine et est plus fréquente dans les domaines techniques à évolution rapide. D'autre part, nous montrons que la réduction anaphorique a tendance à suivre la forme pleine du terme, nous définissons une notion d'arbre anaphorique de terme et nous étudions ses propriétés. Concernant la réduction lexicale, nous tentons de démontrer statistiquement qu'il existe une notion de cycle de vie de terme, où la forme pleine est progressivement remplacée par une réduction lexicale.
Equilibria of Dynamic Games with Many Players: Existence, Approximation, and Market Structure
Venue: arXiv cs.GT 2011
Year: 2011

In this paper we study stochastic dynamic games with many players; these are a fundamental model for a wide range of economic applications. The standard solution concept for such games is Markov perfect equilibrium (MPE), but it is well known that MPE computation becomes intractable as the number of players increases. We instead consider the notion of stationary equilibrium (SE), where players optimize assuming the empirical distribution of others' states remains constant at its long run average. We make two main contributions. First, we provide a rigorous justification for using SE. In particular, we provide a parsimonious collection of exogenous conditions over model primitives that guarantee existence of SE, and ensure that an appropriate approximation property to MPE holds, in a general model with possibly unbounded state spaces. Second, we draw a significant connection between the validity of SE, and market structure: under the same conditions that imply SE exist and approximates MPE well, the market becomes fragmented in the limit of many firms. To illustrate this connection, we study in detail a series of dynamic oligopoly examples. These examples show that our conditions enforce a form of "decreasing returns to larger states"; this yields fragmented industries in the limit. By contrast, violation of these conditions suggests "increasing returns to larger states" and potential market concentration. In that sense, our work uses a fully dynamic framework to also contribute to a longstanding issue in industrial organization: understanding the determinants of market structure in different industries.
An introduction to finite automata and their connection to logic
Venue: arXiv cs.FL 2011
Year: 2011

This is a tutorial on finite automata. We present the standard material on determinization and minimization, as well as an account of the equivalence of finite automata and monadic second-order logic. We conclude with an introduction to the syntactic monoid, and as an application give a proof of the equivalence of first-order definability and aperiodicity.
A proposed Optimized Spline Interpolation
Venue: arXiv cs.MM 2011
Year: 2011

The goal of this paper is to design compact support basis spline functions that best approximate a given filter (e.g., an ideal Lowpass filter). The optimum function is found by minimizing the least square problem ($\ell$2 norm of the difference between the desired and the approximated filters) by means of the calculus of variation; more precisely, the introduced splines give optimal filtering properties with respect to their time support interval. Both mathematical analysis and simulation results confirm the superiority of these splines.
LDPC Codes for Compressed Sensing
Venue: arXiv cs.IT 2011
Year: 2011

We present a mathematical connection between channel coding and compressed sensing. In particular, we link, on the one hand, \emph{channel coding linear programming decoding (CC-LPD)}, which is a well-known relaxation o maximum-likelihood channel decoding for binary linear codes, and, on the other hand, \emph{compressed sensing linear programming decoding (CS-LPD)}, also known as basis pursuit, which is a widely used linear programming relaxation for the problem of finding the sparsest solution of an under-determined system of linear equations. More specifically, we establis a tight connection between CS-LPD based on a zero-one measurement matrix over the reals and CC-LPD of the binary linear channel code that is obtained by viewing this measurement matrix as a binary parity-check matrix. This connection allows the translation of performance guarantees from one setup to the other. The main message of this paper is that parity-check matrices of "good" channel codes can be used as provably "good" measurement matrices under basis pursuit. In particular, we provide the first deterministic construction of compressed sensing measurement matrices with an order-optimal number of rows using high-girth low-density parity-check (LDPC) codes constructed by Gallager.
Terminating Tableaux for Graded Hybrid Logic with Global Modalities and Role Hierarchies
Venue: arXiv cs.LO 2011
Year: 2011

We present a terminating tableau calculus for graded hybrid logic with global modalities, reflexivity, transitivity and role hierarchies. Termination of the system is achieved through pattern-based blocking. Previous approaches to related logics all rely on chain-based blocking. Besides being conceptually simple and suitable for efficient implementation, the pattern-based approach gives us a NExpTime complexity bound for the decision procedure.
A tight bound on the worst-case number of comparisons for Floyd's heap construction algorithm
Venue: arXiv cs.DS 2011
Year: 2011

In this paper a tight bound on the worst-case number of comparisons for Floyd's well known heap construction algorithm, is derived. It is shown that at most 2n-2μ(n)-σ(n) comparisons are executed in the worst case, where μ(n) is the number of ones and σ(n) is the number of zeros after the last one in the binary representation of the number of keys n.
Negative frequency communication
Venue: arXiv cs.IT 2011
Year: 2011

Spectrum is the most valuable resource in communication system, but unfortunately, so far, a half of the spectrum has been wasted. In this paper, we will see that the negative frequency not only has a physical meaning but also can be used in communication. In fact, the complete description of a frequency signal is a rotating complex-frequency signal, in a complete description, positive and negative frequency signals are two distinguishable and independent frequency signals, they can carry different information. But the current carrier modulation and demodulation do not distinguish positive and negative frequencies, so half of the spectrum resources and signal energy are wasted. The complex-carrier modulation and demodulation, proposed by this paper, use the complex-frequency signal as a carrier signal, the negative and positive frequency can carry different information, so the spectrum resources are fully used, the signal energy carried by complex-carrier modulation is focused on a certain band, so the signal energy will not be lost by the complex-carrier demodulation.
Compactly generating all satisfying truth assignments of a Horn formula
Venue: arXiv cs.LO 2011
Year: 2011

As instance of an overarching principle of exclusion an algorithm is presented that compactly (thus not one by one) generates all models of a Horn formula. The principle of exclusion can be adapted to generate only the models of weight $k$. We compare and contrast it with constraint programming, $0,1$ integer programming, and binary decision diagrams.
Improving PPM Algorithm Using Dictionaries
Venue: arXiv cs.IT 2011
Year: 2011

We propose a method to improve traditional character-based PPM text compression algorithms. Consider a text file as a sequence of alternating words and non-words, the basic idea of our algorithm is to encode non-words and prefixes of words using character-based context models and encode suffixes of words using dictionary models. By using dictionary models, the algorithm can encode multiple characters as a whole, and thus enhance the compression efficiency. The advantages of the proposed algorithm are: 1) it does not require any text preprocessing; 2) it does not need any explicit codeword to identify switch between context and dictionary models; 3) it can be applied to any character-based PPM algorithms without incurring much additional computational cost. Test results show that significant improvements can be obtained over character-based PPM, especially in low order cases.
Calibration Using Matrix Completion with Application to Ultrasound Tomography
Venue: arXiv cs.LG 2011
Year: 2011

We study the calibration process in circular ultrasound tomography devices where the sensor positions deviate from the circumference of a perfect circle. This problem arises in a variety of applications in signal processing ranging from breast imaging to sensor network localization. We introduce a novel method of calibration/localization based on the time-of-flight (ToF) measurements between sensors when the enclosed medium is homogeneous. In the presence of all the pairwise ToFs, one can easily estimate the sensor positions using multi-dimensional scaling (MDS) method. In practice however, due to the transitional behaviour of the sensors and the beam form of the transducers, the ToF measurements for close-by sensors are unavailable. Further, random malfunctioning of the sensors leads to random missing ToF measurements. On top of the missing entries, in practice an unknown time delay is also added to the measurements. In this work, we incorporate the fact that a matrix defined from all the ToF measurements is of rank at most four. In order to estimate the missing ToFs, we apply a state-of-the-art low-rank matrix completion algorithm, OPTSPACE . To find the correct positions of the sensors (our ultimate goal) we then apply MDS. We show analytic bounds on the overall error of the whole process in the presence of noise and hence deduce its robustness. Finally, we confirm the functionality of our method in practice by simulations mimicking the measurements of a circular ultrasound tomography device.
Robust and MaxMin Optimization under Matroid and Knapsack Uncertainty Sets
Venue: arXiv cs.DS 2011
Year: 2011

Consider the following problem: given a set system (U,I) and an edge-weighted graph G = (U, E) on the same universe U, find the set A in I such that the Steiner tree cost with terminals A is as large as possible: "which set in I is the most difficult to connect up?" This is an example of a max-min problem: find the set A in I such that the value of some minimization (covering) problem is as large as possible. In this paper, we show that for certain covering problems which admit good deterministic online algorithms, we can give good algorithms for max-min optimization when the set system I is given by a p-system or q-knapsacks or both. This result is similar to results for constrained maximization of submodular functions. Although many natural covering problems are not even approximately submodular, we show that one can use properties of the online algorithm as a surrogate for submodularity. Moreover, we give stronger connections between max-min optimization and two-stage robust optimization, and hence give improved algorithms for robust versions of various covering problems, for cases where the uncertainty sets are given by p-systems and q-knapsacks.
Computationally Efficient Modulation Level Classification Based on Probability Distribution Distance Functions
Venue: arXiv cs.IT 2011
Year: 2011

We present a novel modulation level classification (MLC) method based on probability distribution distance functions. The proposed method uses modified Kuiper and Kolmogorov-Smirnov distances to achieve low computational complexity and outperforms the state of the art methods based on cumulants and goodness-of-fit tests. We derive the theoretical performance of the proposed MLC method and verify it via simulations. The best classification accuracy, under AWGN with SNR mismatch and phase jitter, is achieved with the proposed MLC method using Kuiper distances.
No-Break Dynamic Defragmentation of Reconfigurable Devices
Venue: arXiv cs.DS 2011
Year: 2011

We propose a new method for defragmenting the module layout of a reconfigurable device, enabled by a novel approach for dealing with communication needs between relocated modules and with inhomogeneities found in commonly used FPGAs. Our method is based on dynamic relocation of module positions during runtime, with only very little reconfiguration overhead; the objective is to maximize the length of contiguous free space that is available for new modules. We describe a number of algorithmic aspects of good defragmentation, and present an optimization method based on tabu search. Experimental results indicate that we can improve the quality of module layout by roughly 50 % over static layout. Among other benefits, this improvement avoids unnecessary rejections of modules
Towards a Better Understanding of Large Scale Network Models
Venue: arXiv cs.NI 2011
Year: 2011

Connectivity and capacity are two fundamental properties of wireless multi-hop networks. The scalability of these properties has been a primary concern for which asymptotic analysis is a useful tool. Three related but logically distinct network models are often considered in asymptotic analyses, viz. the dense network model, the extended network model and the infinite network model, which consider respectively a network deployed in a fixed finite area with a sufficiently large node density, a network deployed in a sufficiently large area with a fixed node density, and a network deployed in $\Re^{2}$ with a sufficiently large node density. The infinite network model originated from continuum percolation theory and asymptotic results obtained from the infinite network model have often been applied to the dense and extended networks. In this paper, through two case studies related to network connectivity on the expected number of isolated nodes and on the vanishing of components of finite order k>1 respectively, we demonstrate some subtle but important differences between the infinite network model and the dense and extended network models. Therefore extra scrutiny has to be used in order for the results obtained from the infinite network model to be applicable to the dense and extended network models. Asymptotic results are also obtained on the expected number of isolated nodes, the vanishingly small impact of the boundary effect on the number of isolated nodes and the vanishing of components of finite order k>1 in the dense and extended network models using a generic random connection model.