OpenRaiser/Intern-Atlas huggingface dataset:
Distributed Vertex Cover Algorithms For Wireless Sensor Networks
Venue: arXiv cs.DC 2014
Year: 2014

Vertex covering has important applications for wireless sensor networks such as monitoring link failures, facility location, clustering, and data aggregation. In this study, we designed three algorithms for constructing vertex cover in wireless sensor networks. The first algorithm, which is an adaption of the Parnas & Ron's algorithm, is a greedy approach that finds a vertex cover by using the degrees of the nodes. The second algorithm finds a vertex cover from graph matching where Hoepman's weighted matching algorithm is used. The third algorithm firstly forms a breadth-first search tree and then constructs a vertex cover by selecting nodes with predefined levels from breadth-first tree. We show the operation of the designed algorithms, analyze them, and provide the simulation results in the TOSSIM environment. Finally we have implemented, compared and assessed all these approaches. The transmitted message count of the first algorithm is smallest among other algorithms where the third algorithm has turned out to be presenting the best results in vertex cover approximation ratio.
Analyzing Peer Selection Policies for BitTorrent Multimedia On-Demand Streaming Systems in Internet
Venue: arXiv cs.NI 2014
Year: 2014

The adaptation of the BitTorrent protocol to multimedia on-demand streaming systems essentially lies on the modification of its two core algorithms, namely the piece and the peer selection policies, respectively. Much more attention has though been given to the piece selection policy. Within this context, this article proposes three novel peer selection policies for the design of BitTorrent-like protocols targeted at that type of systems: Select Balanced Neighbour Policy (SBNP), Select Regular Neighbour Policy (SRNP), and Select Optimistic Neighbour Policy (SONP). These proposals are validated through a competitive analysis based on simulations which encompass a variety of multimedia scenarios, defined in function of important characterization parameters such as content type, content size, and client interactivity profile. Service time, number of clients served and efficiency retrieving coefficient are the performance metrics assessed in the analysis. The final results mainly show that the novel proposals constitute scalable solutions that may be considered for real project designs. Lastly, future work is included in the conclusion of this paper.
Compressive sensing for dynamic spectrum access networks: Techniques and tradeoffs
Venue: arXiv cs.NI 2014
Year: 2014

We explore the practical costs and benefits of CS for dynamic spectrum access (DSA) networks. Firstly, we review several fast and practical techniques for energy detection without full reconstruction and provide theoretical guarantees. We also define practical metrics to measure the performance of these techniques. Secondly, we perform comprehensive experiments comparing the techniques on real signals captured over the air. Our results show that we can significantly compressively acquire the signal while still accurately determining spectral occupancy.
Proof terms for infinitary rewriting, progress report
Venue: arXiv cs.LO 2014
Year: 2014

We generalize the notion of proof term to the realm of transfinite reduction. Proof terms represent reductions in the first-order term format, thereby facilitating their formal analysis. We show that any transfinite reduction can be faithfully represented as an infinitary proof term, which is unique up to, infinitary, associativity. Our main use of proof terms is in a definition of permutation equivalence for transfinite reductions, on the basis of permutation equations. This definition involves a variant of equational logic, adapted for dealing with infinite objects. A proof of the compression property via proof terms is presented, which establishes permutation equivalence between the original and the compressed reductions.
Computational Limits for Matrix Completion
Venue: arXiv cs.CC 2014
Year: 2014

Matrix Completion is the problem of recovering an unknown real-valued low-rank matrix from a subsample of its entries. Important recent results show that the problem can be solved efficiently under the assumption that the unknown matrix is incoherent and the subsample is drawn uniformly at random. Are these assumptions necessary? It is well known that Matrix Completion in its full generality is NP-hard. However, little is known if make additional assumptions such as incoherence and permit the algorithm to output a matrix of slightly higher rank. In this paper we prove that Matrix Completion remains computationally intractable even if the unknown matrix has rank $4$ but we are allowed to output any constant rank matrix, and even if additionally we assume that the unknown matrix is incoherent and are shown $90%$ of the entries. This result relies on the conjectured hardness of the $4$-Coloring problem. We also consider the positive semidefinite Matrix Completion problem. Here we show a similar hardness result under the standard assumption that $\mathrm{P}\ne \mathrm{NP}.$ Our results greatly narrow the gap between existing feasibility results and computational lower bounds. In particular, we believe that our results give the first complexity-theoretic justification for why distributional assumptions are needed beyond the incoherence assumption in order to obtain positive results. On the technical side, we contribute several new ideas on how to encode hard combinatorial problems in low-rank optimization problems. We hope that these techniques will be helpful in further understanding the computational limits of Matrix Completion and related problems.
Machine Learner for Automated Reasoning 0.4 and 0.5
Venue: arXiv cs.LG 2014
Year: 2014

Machine Learner for Automated Reasoning (MaLARea) is a learning and reasoning system for proving in large formal libraries where thousands of theorems are available when attacking a new conjecture, and a large number of related problems and proofs can be used to learn specific theorem-proving knowledge. The last version of the system has by a large margin won the 2013 CASC LTB competition. This paper describes the motivation behind the methods used in MaLARea, discusses the general approach and the issues arising in evaluation of such system, and describes the Mizar@Turing100 and CASC'24 versions of MaLARea.
Design Patterns as Quality Influencing Factor in Object Oriented Design Approach
Venue: arXiv cs.SE 2014
Year: 2014

Object Oriented Design methodology is an emerging software development approach for complex systems with huge set of requirements. Unlike procedural approach, it captures the requirements as a set of data rather than services, encapsulated as a single entity. The success such a project relies on major factors like design patterns framework, key principles, metric standards and best practices adapted by the industry. The patterns are key structures for recursive problem bits in the problem domain. The combination of design patterns forms a framework which suits the problem statement in hand. The pattern includes static design and dynamic behavior of different types of entities which can be mapped as a functional diagram with cardinalities between them. The degree of cardinality represents the coupling factor which the industry perceives and measures for software design quality. The organization specific design principles and rich repository of on-the-shelf patterns are the major design-quality-influencing-factor contribute to software success. These are the asset of an industry to deliver a quality product to sustain itself in the competitive market.
Supporting Process Maturation with the Enhanced CoBRA Method
Venue: arXiv cs.SE 2014
Year: 2014

Cost estimation is a very crucial field for software developing companies. In the context of learning organizations, estimation applicability and accuracy are not the only acceptance criteria. The contribution of an estimation technique to the understanding and maturing of related organizational processes (such as identification of cost and productivity factors, measurement, data validation, model validation, model maintenance) has recently been gaining increasing importance. Yet, most of the proposed cost modeling approaches provide software engineers with hardly any assistance in supporting related processes. Insufficient support is provided for validating created cost models (including underlying data collection processes) or, if valid models are obtained, for applying them to achieve an organization's objectives such as improved productivity or reduced schedule. This paper presents an enhancement of the CoBRA(R) cost modeling method by systematically including additional quantitative methods into iterative analysis-feedback cycles. Applied at Oki Electric Industry Co., Ltd., Japan, the CoBRA(R) method contributed to the achievement of the following objectives, including: (1) maturation of existing measurement processes, (2) increased expertise of Oki software project decision makers regarding cost-related software processes, and, finally, (3) reduction of initial estimation error from an initial 120% down to 14%.
A Generalized Apagodu-Zeilberger Algorithm
Venue: arXiv cs.SC 2014
Year: 2014

The Apagodu-Zeilberger algorithm can be used for computing annihilating operators for definite sums over hypergeometric terms, or for definite integrals over hyperexponential functions. In this paper, we propose a generalization of this algorithm which is applicable to arbitrary $\partial$-finite functions. In analogy to the hypergeometric case, we introduce the notion of proper $\partial$-finite functions. We show that the algorithm always succeeds for these functions, and we give a tight a priori bound for the order of the output operator.
Incremental QBF Solving
Venue: arXiv cs.LO 2014
Year: 2014

We consider the problem of incrementally solving a sequence of quantified Boolean formulae (QBF). Incremental solving aims at using information learned from one formula in the process of solving the next formulae in the sequence. Based on a general overview of the problem and related challenges, we present an approach to incremental QBF solving which is application-independent and hence applicable to QBF encodings of arbitrary problems. We implemented this approach in our incremental search-based QBF solver DepQBF and report on implementation details. Experimental results illustrate the potential benefits of incremental solving in QBF-based workflows.
Data Compaction - Compression without Decompression
Venue: arXiv cs.DS 2014
Year: 2014

Data compaction is a new approach for lossless and lossy compression of read-only array data. The biggest advantage over existing approaches is the possibility to access compressed data without any decompression. This makes data compaction most suitable for systems that could currently not apply compression techniques due to real-time or memory constraints. This is true for the majority of all computers, i.e. a wide range of embedded systems.
Design and Implementation of Bit Transition Counter
Venue: arXiv cs.AR 2014
Year: 2014

In today VLSI system design, power consumption is gaining more attention as compared to performance and area. This is due to battery life in portable devices and operating frequency of the design. Power consumption mainly consists of static power, dynamic power, leakage power and short circuit power. Dynamic power is dominant among all which depends on many factors viz. power supply, load capacitance and frequency. Switching activity also affects dynamic power consumption of bus which is determined by calculating the number of bit transitions on bus. The purpose of this paper is to design a bit transition counter which can be used to calculate the switching activity of the circuit nodes. The novel feature is that it can be inserted at any node of the circuit, thus helpful for calculating power consumption of bus.
The CQC Algorithm: Cycling in Graphs to Semantically Enrich and Enhance a Bilingual Dictionary
Venue: arXiv cs.CL 2014
Year: 2014

Bilingual machine-readable dictionaries are knowledge resources useful in many automatic tasks. However, compared to monolingual computational lexicons like WordNet, bilingual dictionaries typically provide a lower amount of structured information, such as lexical and semantic relations, and often do not cover the entire range of possible translations for a word of interest. In this paper we present Cycles and Quasi-Cycles (CQC), a novel algorithm for the automated disambiguation of ambiguous translations in the lexical entries of a bilingual machine-readable dictionary. The dictionary is represented as a graph, and cyclic patterns are sought in the graph to assign an appropriate sense tag to each translation in a lexical entry. Further, we use the algorithms output to improve the quality of the dictionary itself, by suggesting accurate solutions to structural problems such as misalignments, partial alignments and missing entries. Finally, we successfully apply CQC to the task of synonym extraction.
A Fast Two Pass Multi-Value Segmentation Algorithm based on Connected Component Analysis
Venue: arXiv cs.CV 2014
Year: 2014

Connected component analysis (CCA) has been heavily used to label binary images and classify segments. However, it has not been well-exploited to segment multi-valued natural images. This work proposes a novel multi-value segmentation algorithm that utilizes CCA to segment color images. A user defined distance measure is incorporated in the proposed modified CCA to identify and segment similar image regions. The raw output of the algorithm consists of distinctly labelled segmented regions. The proposed algorithm has a unique design architecture that provides several benefits: 1) it can be used to segment any multi-channel multi-valued image; 2) the distance measure/segmentation criteria can be application-specific and 3) an absolute linear-time implementation allows easy extension for real-time video segmentation. Experimental demonstrations of the aforesaid benefits are presented along with the comparison results on multiple datasets with current benchmark algorithms. A number of possible application areas are also identified and results on real-time video segmentation has been presented to show the promise of the proposed method.
On circular-arc graphs having a model with no three arcs covering the circle
Venue: arXiv cs.DM 2014
Year: 2014

An interval graph is the intersection graph of a finite set of intervals on a line and a circular-arc graph is the intersection graph of a finite set of arcs on a circle. While a forbidden induced subgraph characterization of interval graphs was found fifty years ago, finding an analogous characterization for circular-arc graphs is a long-standing open problem. In this work, we study the intersection graphs of finite sets of arcs on a circle no three of which cover the circle, known as normal Helly circular-arc graphs. Those circular-arc graphs which are minimal forbidden induced subgraphs for the class of normal Helly circular-arc graphs were identified by Lin, Soulignac, and Szwarcfiter, who also posed the problem of determining the remaining minimal forbidden induced subgraphs. In this work, we solve their problem, obtaining the complete list of minimal forbidden induced subgraphs for the class of normal Helly circular-arc graphs.
Aggregate Characterization of User Behavior in Twitter and Analysis of the Retweet Graph
Venue: arXiv cs.SI 2014
Year: 2014

Most previous analysis of Twitter user behavior is focused on individual information cascades and the social followers graph. We instead study aggregate user behavior and the retweet graph with a focus on quantitative descriptions. We find that the lifetime tweet distribution is a type-II discrete Weibull stemming from a power law hazard function, the tweet rate distribution, although asymptotically power law, exhibits a lognormal cutoff over finite sample intervals, and the inter-tweet interval distribution is power law with exponential cutoff. The retweet graph is small-world and scale-free, like the social graph, but is less disassortative and has much stronger clustering. These differences are consistent with it better capturing the real-world social relationships of and trust between users. Beyond just understanding and modeling human communication patterns and social networks, applications for alternative, decentralized microblogging systems-both predicting real-word performance and detecting spam-are discussed.
Automated Verification, Synthesis and Correction of Concurrent Systems via MSO Logic
Venue: arXiv cs.LO 2014
Year: 2014

In this work we provide algorithmic solutions to five fundamental problems concerning the verification, synthesis and correction of concurrent systems that can be modeled by bounded p/t-nets. We express concurrency via partial orders and assume that behavioral specifications are given via monadic second order logic. A c-partial-order is a partial order whose Hasse diagram can be covered by c paths. For a finite set T of transitions, we let P(c,T,ϕ) denote the set of all T-labelled c-partial-orders satisfying ϕ. If N=(P,T) is a p/t-net we let P(N,c) denote the set of all c-partially-ordered runs of N. A (b, r)-bounded p/t-net is a b-bounded p/t-net in which each place appears repeated at most r times. We solve the following problems: 1. Verification: given an MSO formula ϕand a bounded p/t-net N determine whether P(N,c)\subseteq P(c,T,ϕ), whether P(c,T,ϕ)\subseteq P(N,c), or whether P(N,c)\cap P(c,T,ϕ)=\emptyset. 2. Synthesis from MSO Specifications: given an MSO formula ϕ, synthesize a semantically minimal (b,r)-bounded p/t-net N satisfying P(c,T,ϕ)\subseteq P(N, c). 3. Semantically Safest Subsystem: given an MSO formula ϕdefining a set of safe partial orders, and a b-bounded p/t-net N, possibly containing unsafe behaviors, synthesize the safest (b,r)-bounded p/t-net N' whose behavior lies in between P(N,c)\cap P(c,T,ϕ) and P(N,c). 4. Behavioral Repair: given two MSO formulas ϕand ψ, and a b-bounded p/t-net N, synthesize a semantically minimal (b,r)-bounded p/t net N' whose behavior lies in between P(N,c) \cap P(c,T,ϕ) and P(c,T,ψ). 5. Synthesis from Contracts: given an MSO formula ϕ^yes specifying a set of good behaviors and an MSO formula ϕ^no specifying a set of bad behaviors, synthesize a semantically minimal (b,r)-bounded p/t-net N such that P(c,T,ϕ^yes) \subseteq P(N,c) but P(c,T,ϕ^no ) \cap P(N,c)=\emptyset.
Noise Analysis for Lensless Compressive Imaging
Venue: arXiv cs.CV 2014
Year: 2014

We analyze the signal to noise ratio (SNR) in a recently proposed lensless compressive imaging architecture. The architecture consists of a sensor of a single detector element and an aperture assembly of an array of aperture elements, each of which has a programmable transmittance. This lensless compressive imaging architecture can be used in conjunction with compressive sensing to capture images in a compressed form of compressive measurements. In this paper, we perform noise analysis of this lensless compressive imaging architecture and compare it with pinhole aperture imaging and lens aperture imaging. We will show that the SNR in the lensless compressive imaging is independent of the image resolution, while that in either pinhole aperture imaging or lens aperture imaging decreases as the image resolution increases. Consequently, the SNR in the lensless compressive imaging can be much higher if the image resolution is large enough.
Planning for Decentralized Control of Multiple Robots Under Uncertainty
Venue: arXiv cs.RO 2014
Year: 2014

We describe a probabilistic framework for synthesizing control policies for general multi-robot systems, given environment and sensor models and a cost function. Decentralized, partially observable Markov decision processes (Dec-POMDPs) are a general model of decision processes where a team of agents must cooperate to optimize some objective (specified by a shared reward or cost function) in the presence of uncertainty, but where communication limitations mean that the agents cannot share their state, so execution must proceed in a decentralized fashion. While Dec-POMDPs are typically intractable to solve for real-world problems, recent research on the use of macro-actions in Dec-POMDPs has significantly increased the size of problem that can be practically solved as a Dec-POMDP. We describe this general model, and show how, in contrast to most existing methods that are specialized to a particular problem class, it can synthesize control policies that use whatever opportunities for coordination are present in the problem, while balancing off uncertainty in outcomes, sensor information, and information about other agents. We use three variations on a warehouse task to show that a single planner of this type can generate cooperative behavior using task allocation, direct communication, and signaling, as appropriate.
Efficient Analysis of Pattern and Association Rule Mining Approaches
Venue: arXiv cs.DB 2014
Year: 2014

The process of data mining produces various patterns from a given data source. The most recognized data mining tasks are the process of discovering frequent itemsets, frequent sequential patterns, frequent sequential rules and frequent association rules. Numerous efficient algorithms have been proposed to do the above processes. Frequent pattern mining has been a focused topic in data mining research with a good number of references in literature and for that reason an important progress has been made, varying from performant algorithms for frequent itemset mining in transaction databases to complex algorithms, such as sequential pattern mining, structured pattern mining, correlation mining. Association Rule mining (ARM) is one of the utmost current data mining techniques designed to group objects together from large databases aiming to extract the interesting correlation and relation among huge amount of data. In this article, we provide a brief review and analysis of the current status of frequent pattern mining and discuss some promising research directions. Additionally, this paper includes a comparative study between the performance of the described approaches.
On the maximum relative error when computing x^n in floating-point arithmetic
Venue: arXiv cs.NA 2014
Year: 2014

In this paper, we improve the usual relative error bound for the computation of x^n through iterated multiplications by x in binary floating-point arithmetic. The obtained error bound is only slightly better than the usual one, but it is simpler. We also discuss the more general problem of computing the product of n terms.
A Bayesian Characterization of Relative Entropy
Venue: arXiv cs.IT 2014
Year: 2014

We give a new characterization of relative entropy, also known as the Kullback-Leibler divergence. We use a number of interesting categories related to probability theory. In particular, we consider a category FinStat where an object is a finite set equipped with a probability distribution, while a morphism is a measure-preserving function $f: X \to Y$ together with a stochastic right inverse $s: Y \to X$. The function $f$ can be thought of as a measurement process, while s provides a hypothesis about the state of the measured system given the result of a measurement. Given this data we can define the entropy of the probability distribution on $X$ relative to the "prior" given by pushing the probability distribution on $Y$ forwards along $s$. We say that $s$ is "optimal" if these distributions agree. We show that any convex linear, lower semicontinuous functor from FinStat to the additive monoid $[0,\infty]$ which vanishes when $s$ is optimal must be a scalar multiple of this relative entropy. Our proof is independent of all earlier characterizations, but inspired by the work of Petz.