OpenRaiser/Intern-Atlas huggingface dataset:
Query Answering in Resource-Based Answer Set Semantics
Venue: arXiv cs.AI 2016
Year: 2016

In recent work we defined resource-based answer set semantics, which is an extension to answer set semantics stemming from the study of its relationship with linear logic. In fact, the name of the new semantics comes from the fact that in the linear-logic formulation every literal (including negative ones) were considered as a resource. In this paper, we propose a query-answering procedure reminiscent of Prolog for answer set programs under this extended semantics as an extension of XSB-resolution for logic programs with negation. We prove formal properties of the proposed procedure. Under consideration for acceptance in TPLP.
Rumours spread slowly in a small world spatial network
Venue: arXiv cs.SI 2016
Year: 2016

Rumour spreading is a protocol for modelling the spread of information through a network via user-to-user interaction. The Spatial Preferred Attachment (SPA) model is a random graph model for complex networks: vertices are placed in a metric space, and the link probability depends on the metric distance between vertices, and on their degree. We show that the SPA model typically produces graphs that have small effective diameter, i.e. $O(\log^2 n)$, while rumour spreading is relatively slow, namely polynomial in $n$.
Lévy NMF for robust nonnegative source separation
Venue: arXiv cs.SD 2016
Year: 2016

Source separation, which consists in decomposing data into meaningful structured components, is an active research topic in many areas, such as music and image signal processing, applied physics and text mining. In this paper, we introduce the Positive $α$-stable (P$α$S) distributions to model the latent sources, which are a subclass of the stable distributions family. They notably permit us to model random variables that are both nonnegative and impulsive. Considering the Lévy distribution, the only P$α$S distribution whose density is tractable, we propose a mixture model called Lévy Nonnegative Matrix Factorization (Lévy NMF). This model accounts for low-rank structures in nonnegative data that possibly has high variability or is corrupted by very adverse noise. The model parameters are estimated in a maximum-likelihood sense. We also derive an estimator of the sources given the parameters, which extends the validity of the generalized Wiener filtering to the P$α$S case. Experiments on synthetic data show that Lévy NMF compares favorably with state-of-the art techniques in terms of robustness to impulsive noise. The analysis of two types of realistic signals is also considered: musical spectrograms and fluorescence spectra of chemical species. The results highlight the potential of the Lévy NMF model for decomposing nonnegative data.
The Power of Non-Ground Rules in Answer Set Programming
Venue: arXiv cs.AI 2016
Year: 2016

Answer set programming (ASP) is a well-established logic programming language that offers an intuitive, declarative syntax for problem solving. In its traditional application, a fixed ASP program for a given problem is designed and the actual instance of the problem is fed into the program as a set of facts. This approach typically results in programs with comparably short and simple rules. However, as is known from complexity analysis, such an approach limits the expressive power of ASP; in fact, an entire NP-check can be encoded into a single large rule body of bounded arity that performs both a guess and a check within the same rule. Here, we propose a novel paradigm for encoding hard problems in ASP by making explicit use of large rules which depend on the actual instance of the problem. We illustrate how this new encoding paradigm can be used, providing examples of problems from the first, second, and even third level of the polynomial hierarchy. As state-of-the-art solvers are tuned towards short rules, rule decomposition is a key technique in the practical realization of our approach. We also provide some preliminary benchmarks which indicate that giving up the convenient way of specifying a fixed program can lead to a significant speed-up. This paper is under consideration for acceptance into TPLP.
Winograd Schemas and Machine Translation
Venue: arXiv cs.AI 2016
Year: 2016

A Winograd schema is a pair of sentences that differ in a single word and that contain an ambiguous pronoun whose referent is different in the two sentences and requires the use of commonsense knowledge or world knowledge to disambiguate. This paper discusses how Winograd schemas and other sentence pairs could be used as challenges for machine translation using distinctions between pronouns, such as gender, that appear in the target language but not in the source.
Nondeterminism and an abstract formulation of Nečiporuk's lower bound method
Venue: arXiv cs.CC 2016
Year: 2016

A formulation of "Nečiporuk's lower bound method" slightly more inclusive than the usual complexity-measure-specific formulation is presented. Using this general formulation, limitations to lower bounds achievable by the method are obtained for several computation models, such as branching programs and Boolean formulas having access to a sublinear number of nondeterministic bits. In particular, it is shown that any lower bound achievable by the method of Nečiporuk for the size of nondeterministic and parity branching programs is at most $O(n^{3/2}/\log n)$.
Geoplotlib: a Python Toolbox for Visualizing Geographical Data
Venue: arXiv cs.GR 2016
Year: 2016

We introduce geoplotlib, an open-source python toolbox for visualizing geographical data. geoplotlib supports the development of hardware-accelerated interactive visualizations in pure python, and provides implementations of dot maps, kernel density estimation, spatial graphs, Voronoi tesselation, shapefiles and many more common spatial visualizations. We describe geoplotlib design, functionalities and use cases.
Compressive Change Retrieval for Moving Object Detection
Venue: arXiv cs.CV 2016
Year: 2016

Change detection, or anomaly detection, from street-view images acquired by an autonomous robot at multiple different times, is a major problem in robotic mapping and autonomous driving. Formulation as an image comparison task, which operates on a given pair of query and reference images is common to many existing approaches to this problem. Unfortunately, providing relevant reference images is not straightforward. In this paper, we propose a novel formulation for change detection, termed compressive change retrieval, which can operate on a query image and similar reference images retrieved from the web. Compared to previous formulations, there are two sources of difficulty. First, the retrieved reference images may frequently contain non-relevant reference images, because even state-of-the-art place-recognition techniques suffer from retrieval noise. Second, image comparison needs to be conducted in a compressed domain to minimize the storage cost of large collections of street-view images. To address the above issues, we also present a practical change detection algorithm that uses compressed bag-of-words (BoW) image representation as a scalable solution. The results of experiments conducted on a practical change detection task, "moving object detection (MOD)," using the publicly available Malaga dataset validate the effectiveness of the proposed approach.
How Much Did it Rain? Predicting Real Rainfall Totals Based on Radar Data
Venue: arXiv cs.LG 2016
Year: 2016

We applied a variety of parametric and non-parametric machine learning models to predict the probability distribution of rainfall based on 1M training examples over a single year across several U.S. states. Our top performing model based on a squared loss objective was a cross-validated parametric k-nearest-neighbor predictor that took about six days to compute, and was competitive in a world-wide competition.
LCD Cyclic Codes over Finite Fields
Venue: arXiv cs.IT 2016
Year: 2016

In addition to their applications in data storage, communications systems, and consumer electronics, LCD codes -- a class of linear codes -- have been employed in cryptography recently. LCD cyclic codes were referred to as reversible cyclic codes in the literature. The objective of this paper is to construct several families of reversible cyclic codes over finite fields and analyse their parameters. The LCD cyclic codes presented in this paper have very good parameters in general, and contain many optimal codes. A well rounded treatment of reversible cyclic codes is also given in this paper.
Residual CNDS
Venue: arXiv cs.CV 2016
Year: 2016

Convolutional Neural networks nowadays are of tremendous importance for any image classification system. One of the most investigated methods to increase the accuracy of CNN is by increasing the depth of CNN. Increasing the depth by stacking more layers also increases the difficulty of training besides making it computationally expensive. Some research found that adding auxiliary forks after intermediate layers increases the accuracy. Specifying which intermediate layer shoud have the fork just addressed recently. Where a simple rule were used to detect the position of intermediate layers that needs the auxiliary supervision fork. This technique known as convolutional neural networks with deep supervision (CNDS). This technique enhanced the accuracy of classification over the straight forward CNN used on the MIT places dataset and ImageNet. In the other side, Residual Learning is another technique emerged recently to ease the training of very deep CNN. Residual Learning framwork changed the learning of layers from unreferenced functions to learning residual function with regard to the layer's input. Residual Learning achieved state of arts results on ImageNet 2015 and COCO competitions. In this paper, we study the effect of adding residual connections to CNDS network. Our experiments results show increasing of accuracy over using CNDS only.
Enforcing Biconnectivity in Multi-robot Systems
Venue: arXiv cs.RO 2016
Year: 2016

Connectivity maintenance is an essential task in multi-robot systems and it has received a considerable attention during the last years. A connected system can be broken into two or more subsets simply if a single robot fails. A more robust communication can be achieved if the network connectivity is guaranteed in the case of one-robot failures. The resulting network is called biconnected. In \cite{Zareh2016biconnectivitycheck}, we presented a criterion for biconnectivity check, which basically determines a lower bound on the third-smallest eigenvalue of the Laplacian matrix. In this paper, we introduce a decentralized gradient-based protocol to increase the value of the third-smallest eigenvalue of the Laplacian matrix, when the biconnectivity check fails. We also introduce a decentralized algorithm to estimate the eigenvectors of the Laplacian matrix, which are used for defining the gradient. Simulations show the effectiveness of the theoretical findings.
Deciding structural liveness of Petri nets
Venue: arXiv cs.LO 2016
Year: 2016

Place/transition Petri nets are a standard model for a class of distributed systems whose reachability spaces might be infinite. One of well-studied topics is the verification of safety and liveness properties in this model; despite the extensive research effort, some basic problems remain open, which is exemplified by the open complexity status of the reachability problem. The liveness problems are known to be closely related to the reachability problem, and many structural properties of nets that are related to liveness have been studied. Somewhat surprisingly, the decidability status of the problem if a net is structurally live, i.e. if there is an initial marking for which it is live, has remained open, as also a recent paper (Best and Esparza, 2016) emphasizes. Here we show that the structural liveness problem for Petri nets is decidable. A crucial ingredient of the proof is the result by Leroux (LiCS 2013) showing that we can compute a finite (Presburger) description of the reachability set for a marked Petri net if this set is semilinear.
Complexity Results for Manipulation, Bribery and Control of the Kemeny Procedure in Judgment Aggregation
Venue: arXiv cs.AI 2016
Year: 2016

We study the computational complexity of several scenarios of strategic behavior for the Kemeny procedure in the setting of judgment aggregation. In particular, we investigate (1) manipulation, where an individual aims to achieve a better group outcome by reporting an insincere individual opinion, (2) bribery, where an external agent aims to achieve an outcome with certain properties by bribing a number of individuals, and (3) control (by adding or deleting issues), where an external agent aims to achieve an outcome with certain properties by influencing the set of issues in the judgment aggregation situation. We show that determining whether these types of strategic behavior are possible (and if so, computing a policy for successful strategic behavior) is complete for the second level of the Polynomial Hierarchy. That is, we show that these problems are $Σ^p_2$-complete.
ActiveCrowd: A Framework for Optimized Multi-Task Allocation in Mobile Crowdsensing Systems
Venue: arXiv cs.HC 2016
Year: 2016

Worker selection is a key issue in Mobile Crowd Sensing (MCS). While previous worker selection approaches mainly focus on selecting a proper subset of workers for a single MCS task, multi-task-oriented worker selection is essential and useful for the efficiency of large-scale MCS platforms. This paper proposes ActiveCrowd, a worker selection framework for multi-task MCS environments.
Further Algebraic Algorithms in the Congested Clique Model and Applications to Graph-Theoretic Problems
Venue: arXiv cs.DC 2016
Year: 2016

Censor-Hillel et al. [PODC'15] recently showed how to efficiently implement centralized algebraic algorithms for matrix multiplication in the congested clique model, a model of distributed computing that has received increasing attention in the past few years. This paper develops further algebraic techniques for designing algorithms in this model. We present deterministic and randomized algorithms, in the congested clique model, for efficiently computing multiple independent instances of matrix products, computing the determinant, the rank and the inverse of a matrix, and solving systems of linear equations. As applications of these techniques, we obtain more efficient algorithms for the computation, again in the congested clique model, of the all-pairs shortest paths and the diameter in directed and undirected graphs with small weights, improving over Censor-Hillel et al.'s work. We also obtain algorithms for several other graph-theoretic problems such as computing the number of edges in a maximum matching and the Gallai-Edmonds decomposition of a simple graph, and computing a minimum vertex cover of a bipartite graph.
OnionNet: Sharing Features in Cascaded Deep Classifiers
Venue: arXiv cs.CV 2016
Year: 2016

The focus of our work is speeding up evaluation of deep neural networks in retrieval scenarios, where conventional architectures may spend too much time on negative examples. We propose to replace a monolithic network with our novel cascade of feature-sharing deep classifiers, called OnionNet, where subsequent stages may add both new layers as well as new feature channels to the previous ones. Importantly, intermediate feature maps are shared among classifiers, preventing them from the necessity of being recomputed. To accomplish this, the model is trained end-to-end in a principled way under a joint loss. We validate our approach in theory and on a synthetic benchmark. As a result demonstrated in three applications (patch matching, object detection, and image retrieval), our cascade can operate significantly faster than both monolithic networks and traditional cascades without sharing at the cost of marginal decrease in precision.
A General Framework for Static Profiling of Parametric Resource Usage
Venue: arXiv cs.PL 2016
Year: 2016

Traditional static resource analyses estimate the total resource usage of a program, without executing it. In this paper we present a novel resource analysis whose aim is instead the static profiling of accumulated cost, i.e., to discover, for selected parts of the program, an estimate or bound of the resource usage accumulated in each of those parts. Traditional resource analyses are parametric in the sense that the results can be functions on input data sizes. Our static profiling is also parametric, i.e., our accumulated cost estimates are also parameterized by input data sizes. Our proposal is based on the concept of cost centers and a program transformation that allows the static inference of functions that return bounds on these accumulated costs depending on input data sizes, for each cost center of interest. Such information is much more useful to the software developer than the traditional resource usage functions, as it allows identifying the parts of a program that should be optimized, because of their greater impact on the total cost of program executions. We also report on our implementation of the proposed technique using the CiaoPP program analysis framework, and provide some experimental results. This paper is under consideration for acceptance in TPLP.
Verification of Time-Aware Business Processes using Constrained Horn Clauses
Venue: arXiv cs.LO 2016
Year: 2016

We present a method for verifying properties of time-aware business processes, that is, business process where time constraints on the activities are explicitly taken into account. Business processes are specified using an extension of the Business Process Modeling Notation (BPMN) and durations are defined by constraints over integer numbers. The definition of the operational semantics is given by a set OpSem of constrained Horn clauses (CHCs). Our verification method consists of two steps. (Step 1) We specialize OpSem with respect to a given business process and a given temporal property to be verified, whereby getting a set of CHCs whose satisfiability is equivalent to the validity of the given property. (Step 2) We use state-of-the-art solvers for CHCs to check the satisfiability of such sets of clauses. We have implemented our verification method using the VeriMAP transformation system, and the Eldarica and Z3 solvers for CHCs.
Correlated Interference from Uncorrelated Users in Bounded Ad Hoc Networks with Blockage
Venue: arXiv cs.NI 2016
Year: 2016

In this letter, we study the joint impact of user density, blockage density and deployment area on the temporal correlation of interference for static and highly mobile users. We show that even if the user locations become uncorrelated, the interference level can still be correlated when the deployment area is bounded and/or there is blockage. In addition, we study how the correlation coefficients of interference scale at a high density of blockage.
Albanian Sign Language (AlbSL) Number Recognition from Both Hand's Gestures Acquired by Kinect Sensors
Venue: arXiv cs.HC 2016
Year: 2016

Albanian Sign Language (AlbSL) is relatively new and until now there doesn't exist a system that is able to recognize Albanian signs by using natural user interfaces (NUI). The aim of this paper is to present a real-time gesture recognition system that is able to automatically recognize number signs for Albanian Sign Language, captured from signer's both hands. Kinect device is used to obtain data streams. Every pixel generated from Kinect device contains depth data information which is used to construct a depth map. Hands segmentation process is performed by applying a threshold constant to depth map. In order to differentiate signer's hands a K-means clustering algorithm is applied to partition pixels into two groups corresponding to each signer's hands. Centroid distance function is calculated in each hand after extracting hand's contour pixels. Fourier descriptors, derived form centroid distance is used as a hand shape representation. For each number gesture there are 15 Fourier descriptors coefficients generated which represent uniquely that gesture. Every input data is compared against training data set by calculating Euclidean distance, using Fourier coefficients. Sign with the lowest Euclidean distance is considered as a match. The system is able to recognize number signs captured from one hand or both hands. When both signer's hands are used, some of the methodology processes are executed in parallel in order to improve the overall performance. The proposed system achieves an accuracy of 91% and is able to process 55 frames per second.
Towards Visual Type Theory as a Mathematical Tool and Mathematical User Interface
Venue: arXiv cs.AI 2016
Year: 2016

A visual type theory is a cognitive tool that has much in common with language, and may be regarded as an exceptional form of spatial text adjunct. A mathematical visual type theory, called NPM, has been under development that can be viewed as an early-stage project in mathematical knowledge management and mathematical user interface development. We discuss in greater detail the notion of a visual type theory, report on progress towards a usable mathematical visual type theory, and discuss the outlook for future work on this project.
Dimensions of three types of BCH codes over GF(q)
Venue: arXiv cs.IT 2016
Year: 2016

BCH codes have been studied for over fifty years and widely employed in consumer devices, communication systems, and data storage systems. However, the dimension of BCH codes is settled only for a very small number of cases. In this paper, we study the dimensions of BCH codes over finite fields with three types of lengths $n$, namely $n=q^m-1$, $n=(q^m-1)/(q-1)$ and $n=q^m+1$. For narrow-sense primitive BCH codes with designed distance $δ$, we investigate their dimensions for $δ$ in the range $1\le δ\le q^{\lceil\frac{m}{2}\rceil+1}$. For non-narrow sense primitive BCH codes, we provide two general formulas on their dimensions and give the dimensions explicitly in some cases. Furthermore, we settle the minimum distances of some primitive BCH codes. We also explore the dimensions of the BCH codes of lengths $n=(q^m-1)/(q-1)$ and $n=q^m+1$ over finite fields.