OpenRaiser/Intern-Atlas huggingface dataset:
A Generic Analysis Server System for Functional Logic Programs
Venue: arXiv cs.PL 2013
Year: 2013

We present a system, called CASS, for the analysis of functional logic programs. The system is generic so that various kinds of analyses (e.g., groundness, non-determinism, demanded arguments) can be easily integrated. In order to analyze larger applications consisting of dozens or hundreds of modules, CASS supports a modular and incremental analysis of programs. Moreover, it can be used by different programming tools, like documentation generators, analysis environments, program optimizers, as well as Eclipse-based development environments. For this purpose, CASS can also be invoked as a server system to get a language-independent access to its functionality. CASS is completely implemented in the functional logic language Curry as a master/worker architecture to exploit parallel or distributed execution environments.
Attention and Visibility in an Information Rich World
Venue: arXiv cs.SI 2013
Year: 2013

As the rate of content production grows, we must make a staggering number of daily decisions about what information is worth acting on. For any flourishing online social media system, users can barely keep up with the new content shared by friends. How does the user-interface design help or hinder users' ability to find interesting content? We analyze the choices people make about which information to propagate on the social media sites Twitter and Digg. We observe regularities in behavior which can be attributed directly to cognitive limitations of humans, resulting from the different visibility policies of each site. We quantify how people divide their limited attention among competing sources of information, and we show how the user-interface design can mediate information spread.
Secure k-Nearest Neighbor Query over Encrypted Data in Outsourced Environments
Venue: arXiv cs.CR 2013
Year: 2013

For the past decade, query processing on relational data has been studied extensively, and many theoretical and practical solutions to query processing have been proposed under various scenarios. With the recent popularity of cloud computing, users now have the opportunity to outsource their data as well as the data management tasks to the cloud. However, due to the rise of various privacy issues, sensitive data (e.g., medical records) need to be encrypted before outsourcing to the cloud. In addition, query processing tasks should be handled by the cloud; otherwise, there would be no point to outsource the data at the first place. To process queries over encrypted data without the cloud ever decrypting the data is a very challenging task. In this paper, we focus on solving the k-nearest neighbor (kNN) query problem over encrypted database outsourced to a cloud: a user issues an encrypted query record to the cloud, and the cloud returns the k closest records to the user. We first present a basic scheme and demonstrate that such a naive solution is not secure. To provide better security, we propose a secure kNN protocol that protects the confidentiality of the data, user's input query, and data access patterns. Also, we empirically analyze the efficiency of our protocols through various experiments. These results indicate that our secure protocol is very efficient on the user end, and this lightweight scheme allows a user to use any mobile device to perform the kNN query.
Oriented chromatic number of Halin graphs
Venue: arXiv cs.DM 2013
Year: 2013

Oriented chromatic number of an oriented graph $G$ is the minimum order of an oriented graph $H$ such that $G$ admits a homomorphism to $H$. The oriented chromatic number of an unoriented graph $G$ is the maximal chromatic number over all possible orientations of $G$. In this paper, we prove that every Halin graph has oriented chromatic number at most 8, improving a previous bound by Hosseini Dolama and Sopena, and confirming the conjecture given by Vignal.
Triggered Clause Pushing for IC3
Venue: arXiv cs.LO 2013
Year: 2013

We propose an improvement of the famous IC3 algorithm for model checking safety properties of finite state systems. We collect models computed by the SAT-solver during the clause propagation phase of the algorithm and use them as witnesses for why the respective clauses could not be pushed forward. It only makes sense to recheck a particular clause for pushing when its witnessing model falsifies a newly added clause. Since this trigger test is both computationally cheap and sufficiently precise, we can afford to keep clauses pushed as far as possible at all times. Experiments indicate that this strategy considerably improves IC3's performance.
A Sharp Double Inequality for the Inverse Tangent Function
Venue: arXiv cs.IT 2013
Year: 2013

The inverse tangent function can be bounded by different inequalities, for example by Shafer's inequality. In this publication, we propose a new sharp double inequality, consisting of a lower and an upper bound, for the inverse tangent function. In particular, we sharpen Shafer's inequality and calculate the best corresponding constants. The maximum relative errors of the obtained bounds are approximately smaller than 0.27% and 0.23% for the lower and upper bound, respectively. Furthermore, we determine an upper bound on the relative errors of the proposed bounds in order to describe their tightness analytically. Moreover, some important properties of the obtained bounds are discussed in order to describe their behavior and achieved accuracy.
On The Complexity of Counter Reachability Games
Venue: arXiv cs.GT 2013
Year: 2013

Counter reachability games are played by two players on a graph with labelled edges. Each move consists in picking an edge from the current location and adding its label to a counter vector. The objective is to reach a given counter value in a given location. We distinguish three semantics for counter reachability games, according to what happens when a counter value would become negative: the edge is either disabled, or enabled but the counter value becomes zero, or enabled. We consider the problem of deciding the winner in counter reachability games and show that, in most cases, it has the same complexity under all semantics. Surprisingly, under one semantics, the complexity in dimension one depends on whether the objective value is zero or any other integer.
Avoiding Whitewashing in Unstructured Peer-to-Peer Resource Sharing Network
Venue: arXiv cs.NI 2013
Year: 2013

In peer-to-peer file sharing network, it is hard to distinguish between a legitimate newcomer and a whitewasher. This makes whitewashing a big problem in peer-to-peer networks. Although the problem of whitewashing can be solved using permanent identities, it may take away the right of anonymity for users. In this paper, we a have proposed a novel algorithm to avoid this problem when network uses free temporary identities. In this algorithm, the initial reputation is adjusted according to the level of whitewashing in the network.
On the NP-Hardness of Approximating Ordering Constraint Satisfaction Problems
Venue: arXiv cs.CC 2013
Year: 2013

We show improved NP-hardness of approximating Ordering Constraint Satisfaction Problems (OCSPs). For the two most well-studied OCSPs, Maximum Acyclic Subgraph and Maximum Betweenness, we prove inapproximability of $14/15+ε$ and $1/2+ε$. An OCSP is said to be approximation resistant if it is hard to approximate better than taking a uniformly random ordering. We prove that the Maximum Non-Betweenness Problem is approximation resistant and that there are width-$m$ approximation-resistant OCSPs accepting only a fraction $1 / (m/2)!$ of assignments. These results provide the first examples of approximation-resistant OCSPs subject only to P $\neq$ \NP.
Clustering Algorithm for Gujarati Language
Venue: arXiv cs.CL 2013
Year: 2013

Natural language processing area is still under research. But now a day it is on platform for worldwide researchers. Natural language processing includes analyzing the language based on its structure and then tagging of each word appropriately with its grammar base. Here we have 50,000 tagged words set and we try to cluster those Gujarati words based on proposed algorithm, we have defined our own algorithm for processing. Many clustering techniques are available Ex. Single linkage, complete, linkage,average linkage, Hear no of clusters to be formed are not known, so it is all depends on the type of data set provided . Clustering is preprocess for stemming . Stemming is the process where root is extracted from its word. Ex. cats= cat+S, meaning. Cat: Noun and plural form.
On GROUSE and Incremental SVD
Venue: arXiv cs.NA 2013
Year: 2013

GROUSE (Grassmannian Rank-One Update Subspace Estimation) is an incremental algorithm for identifying a subspace of Rn from a sequence of vectors in this subspace, where only a subset of components of each vector is revealed at each iteration. Recent analysis has shown that GROUSE converges locally at an expected linear rate, under certain assumptions. GROUSE has a similar flavor to the incremental singular value decomposition algorithm, which updates the SVD of a matrix following addition of a single column. In this paper, we modify the incremental SVD approach to handle missing data, and demonstrate that this modified approach is equivalent to GROUSE, for a certain choice of an algorithmic parameter.
Improved Bounds on the Finite Length Scaling of Polar Codes
Venue: arXiv cs.IT 2013
Year: 2013

Improved bounds on the blocklength required to communicate over binary-input channels using polar codes, below some given error probability, are derived. For that purpose, an improved bound on the number of non-polarizing channels is obtained. The main result is that the blocklength required to communicate reliably scales at most as $O((I(W)-R)^{-5.77})$ where $R$ is the code rate and $I(W)$ the symmetric capacity of the channel, $W$. The results are then extended to polar lossy source coding at rate $R$ of a source with symmetric distortion-rate function $D(\cdot)$. The blocklength required scales at most as $O((D_N-D(R))^{-5.77})$ where $D_N$ is the actual distortion.
A New Optimization Approach Based on Rotational Mutation and Crossover Operator
Venue: arXiv cs.NE 2013
Year: 2013

Evaluating a global optimal point in many global optimization problems in large space is required to more calculations. In this paper, there is presented a new approach for the continuous functions optimization with rotational mutation and crossover operator. This proposed method (RMC) starts from the point which has best fitness value by elitism mechanism and after that rotational mutation and crossover operator are used to reach optimal point. RMC method is implemented by GA (Briefly RMCGA) and is compared with other wellknown algorithms such as: DE, PGA, Grefensstette and Eshelman[15,16] and numerical and simulating results show that RMCGA achieve global optimal point with more decision by smaller generations.
Linear-Time Recognition of Probe Interval Graphs
Venue: arXiv cs.DS 2013
Year: 2013

The interval graph for a set of intervals on a line consists of one vertex for each interval, and an edge for each intersecting pair of intervals. A probe interval graph is a variant that is motivated by an application to genomics, where the intervals are partitioned into two sets: probes and non-probes. The graph has an edge between two vertices if they intersect and at least one of them is a probe. We give a linear-time algorithm for determining whether a given graph and partition of vertices into probes and non-probes is a probe interval graph. If it is, we give a layout of intervals that proves this. We can also determine whether the layout of the intervals is uniquely constrained within the same time bound. As part of the algorithm, we solve the consecutive-ones probe matrix problem in linear time, develop algorithms for operating on PQ trees, and give results that relate PQ trees for different submatrices of a consecutive-ones matrix.
Insufficiency of Linear-Feedback Schemes In Gaussian Broadcast Channels with Common Message
Venue: arXiv cs.IT 2013
Year: 2013

We consider the $K\geq 2$-user memoryless Gaussian broadcast channel (BC) with feedback and common message only. We show that linear-feedback schemes with a message point, in the spirit of Schalkwijk & Kailath's scheme for point-to-point channels or Ozarow & Leung's scheme for BCs with private messages, are strictly suboptimal for this setup. Even with perfect feedback, the largest rate achieved by these schemes is strictly smaller than capacity $C$ (which is the same with and without feedback). In the extreme case where the number of receivers $K\to \infty$, the largest rate achieved by linear-feedback schemes with a message point tends to 0. To contrast this negative result, we describe a scheme for \emph{rate-limited} feedback that uses the feedback in an intermittent way, i.e., the receivers send feedback signals only in few channel uses. This scheme achieves all rates $R$ up to capacity $C$ with an $L$-th order exponential decay of the probability of error if the feedback rate $R_{\textnormal{fb}}$ is at least $(L-1)R$ for some positive integer $L$.
Regularized Discrete Optimal Transport
Venue: arXiv cs.CV 2013
Year: 2013

This article introduces a generalization of the discrete optimal transport, with applications to color image manipulations. This new formulation includes a relaxation of the mass conservation constraint and a regularization term. These two features are crucial for image processing tasks, which necessitate to take into account families of multimodal histograms, with large mass variation across modes. The corresponding relaxed and regularized transportation problem is the solution of a convex optimization problem. Depending on the regularization used, this minimization can be solved using standard linear programming methods or first order proximal splitting schemes. The resulting transportation plan can be used as a color transfer map, which is robust to mass variation across images color palettes. Furthermore, the regularization of the transport plan helps to remove colorization artifacts due to noise amplification. We also extend this framework to the computation of barycenters of distributions. The barycenter is the solution of an optimization problem, which is separately convex with respect to the barycenter and the transportation plans, but not jointly convex. A block coordinate descent scheme converges to a stationary point of the energy. We show that the resulting algorithm can be used for color normalization across several images. The relaxed and regularized barycenter defines a common color palette for those images. Applying color transfer toward this average palette performs a color normalization of the input images.
Characterizations and construction methods for linear functional-repair storage codes
Venue: arXiv cs.IT 2013
Year: 2013

We present a precise characterization of linear functional-repair storage codes in terms of {\em admissible states/}, with each state made up from a collection of vector spaces over some fixed finite field. To illustrate the usefulness of our characterization, we provide several applications. We first describe a simple construction of functional-repair storage codes for a family of code parameters meeting the cutset bound outside the MBR and MSR points; these codes are conjectured to have optimal rate with respect to their repair locality. Then, we employ our characterization to develop a construction method to obtain functional repair codes for given parameters using symmetry groups, which can be used both to find new codes and to improve known ones. As an example of the latter use, we describe a beautiful functional-repair storage code that was found by this method, with parameters belonging to the family investigated earlier, which can be specified in terms of only eight different vector spaces.
Proof search for propositional abstract separation logics via labelled sequents
Venue: arXiv cs.LO 2013
Year: 2013

Separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called propositional abstract separation logics, extend the logic of (Boolean) Bunched Implications (BBI) in various ways. We develop a modular proof theory for various propositional abstract separation logics using cut-free labelled sequent calculi. We first extend the cut-fee labelled sequent calculus for BBI of Hou et al to handle Calcagno et al's original logic of separation algebras by adding sound rules for partial-determinism and cancellativity, while preserving cut-elimination. We prove the completeness of our calculus via a sound intermediate calculus that enables us to construct counter-models from the failure to find a proof. We then capture other propositional abstract separation logics by adding sound rules for indivisible unit and disjointness, while maintaining completeness. We present a theorem prover based on our labelled calculus for these propositional abstract separation logics.
Performance comparison of State-of-the-art Missing Value Imputation Algorithms on Some Bench mark Datasets
Venue: arXiv cs.LG 2013
Year: 2013

Decision making from data involves identifying a set of attributes that contribute to effective decision making through computational intelligence. The presence of missing values greatly influences the selection of right set of attributes and this renders degradation in classification accuracies of the classifiers. As missing values are quite common in data collection phase during field experiments or clinical trails appropriate handling would improve the classifier performance. In this paper we present a review of recently developed missing value imputation algorithms and compare their performance on some bench mark datasets.
MIRAGE: An Iterative MapReduce based FrequentSubgraph Mining Algorithm
Venue: arXiv cs.DB 2013
Year: 2013

Frequent subgraph mining (FSM) is an important task for exploratory data analysis on graph data. Over the years, many algorithms have been proposed to solve this task. These algorithms assume that the data structure of the mining task is small enough to fit in the main memory of a computer. However, as the real-world graph data grows, both in size and quantity, such an assumption does not hold any longer. To overcome this, some graph database-centric methods have been proposed in recent years for solving FSM; however, a distributed solution using MapReduce paradigm has not been explored extensively. Since, MapReduce is becoming the de- facto paradigm for computation on massive data, an efficient FSM algorithm on this paradigm is of huge demand. In this work, we propose a frequent subgraph mining algorithm called MIRAGE which uses an iterative MapReduce based framework. MIRAGE is complete as it returns all the frequent subgraphs for a given user-defined support, and it is efficient as it applies all the optimizations that the latest FSM algorithms adopt. Our experiments with real life and large synthetic datasets validate the effectiveness of MIRAGE for mining frequent subgraphs from large graph datasets. The source code of MIRAGE is available from www.cs.iupui.edu/alhasan/software/
Embedding Noise Prediction into List-Viterbi Decoding using Error Detection Codes for Magnetic Tape Systems
Venue: arXiv cs.IT 2013
Year: 2013

A List Viterbi detector produces a rank ordered list of the N globally best candidates in a trellis search. A List Viterbi detector structure is proposed that incorporates the noise prediction with periodic state-metric updates based on outer error detection codes (EDCs). More specifically, a periodic decision making process is utilized for a non-overlapping sliding windows of P bits based on the use of outer EDCs. In a number of magnetic recording applications, Error Correction Coding (ECC) is adversely effected by the presence of long and dominant error events. Unlike the conventional post processing methods that are usually tailored to a specific set of dominant error events or the joint modulation code trellis architectures that are operating on larger state spaces at the expense of increased implementation complexity, the proposed detector does not use any a priori information about the error event distributions and operates at reduced state trellis. We present pre ECC bit error rate performance as well as the post ECC codeword failure rates of the proposed detector using perfect detection scenario as well as practical detection codes as the EDCs are not essential to the overall design. Furthermore, it is observed that proposed algorithm does not introduce new error events. Simulation results show that the proposed algorithm gives improved bit error and post ECC codeword failure rates at the expense of some increase in complexity.
Matching-Constrained Active Contours
Venue: arXiv cs.CV 2013
Year: 2013

In object segmentation by active contours, the initial contour is often required. Conventionally, the initial contour is provided by the user. This paper extends the conventional active contour model by incorporating feature matching in the formulation, which gives rise to a novel matching-constrained active contour. The numerical solution to the new optimization model provides an automated framework of object segmentation without user intervention. The main idea is to incorporate feature point matching as a constraint in active contour models. To this effect, we obtain a mathematical model of interior points to boundary contour such that matching of interior feature points gives contour alignment, and we formulate the matching score as a constraint to active contour model such that the feature matching of maximum score that gives the contour alignment provides the initial feasible solution to the constrained optimization model of segmentation. The constraint also ensures that the optimal contour does not deviate too much from the initial contour. Projected-gradient descent equations are derived to solve the constrained optimization. In the experiments, we show that our method is capable of achieving the automatic object segmentation, and it outperforms the related methods.
Fourier Domain Beamforming: The Path to Compressed Ultrasound Imaging
Venue: arXiv cs.IT 2013
Year: 2013

Sonography techniques use multiple transducer elements for tissue visualization. Signals detected at each element are sampled prior to digital beamforming. The sampling rates required to perform high resolution digital beamforming are significantly higher than the Nyquist rate of the signal and result in considerable amount of data, that needs to be stored and processed. A recently developed technique, compressed beamforming, based on the finite rate of innovation model, compressed sensing (CS) and Xampling ideas, allows to reduce the number of samples needed to reconstruct an image comprised of strong reflectors. A drawback of this method is its inability to treat speckle, which is of significant importance in medical imaging. Here we build on previous work and extend it to a general concept of beamforming in frequency. This allows to exploit the low bandwidth of the ultrasound signal and bypass the oversampling dictated by digital implementation of beamforming in time. Using beamforming in frequency, the same image quality is obtained from far fewer samples. We next present a CS-technique that allows for further rate reduction, using only a portion of the beamformed signal's bandwidth. We demonstrate our methods on in vivo cardiac data and show that reductions up to 1/28 over standard beamforming rates are possible. Finally, we present an implementation on an ultrasound machine using sub-Nyquist sampling and processing. Our results prove that the concept of sub-Nyquist processing is feasible for medical ultrasound, leading to the potential of considerable reduction in future ultrasound machines size, power consumption and cost.