OpenRaiser/Intern-Atlas huggingface dataset:
Mackey-complete spaces and power series -- A topological model of Differential Linear Logic
Venue: arXiv cs.LO 2015
Year: 2015

In this paper, we have described a denotational model of Intuitionist Linear Logic which is also a differential category. Formulas are interpreted as Mackey-complete topological vector space and linear proofs are interpreted by bounded linear functions. So as to interpret non-linear proofs of Linear Logic, we have used a notion of power series between Mackey-complete spaces, generalizing the notion of entire functions in C. Finally, we have obtained a quantitative model of Intuitionist Differential Linear Logic, where the syntactic differentiation correspond to the usual one and where the interpretations of proofs satisfy a Taylor expansion decomposition.
Using RDMA for Lock Management
Venue: arXiv cs.DC 2015
Year: 2015

In this work, we aim to evaluate different Distributed Lock Management service designs with Remote Direct Memory Access (RDMA). In specific, we implement and evaluate the centralized and the RDMA-enabled lock manager designs for fast network settings. Experimental results confirms a couple of hypotheses. First, in the traditional centralized lock manager design, CPU is the bottleneck and bypassing CPU on client-to-server communication using RDMA results in better lock service perofrmance. Second, different lock manager designs with RDMA in consideration result in even better performance; we need to re-design lock management system for RDMA and fast networks.
A Batteryless Sensor ASIC for Implantable Bio-impedance Applications
Venue: arXiv cs.ET 2015
Year: 2015

The measurement of the biological tissue's electrical impedance is an active research field that has attracted a lot of attention during the last decades. Bio-impedances are closely related to a large variety of physiological conditions; therefore, they are useful for diagnosis and monitoring in many medical applications. Measuring living tissues, however, is a challenging task that poses countless technical and practical problems, in particular if the tissues need to be measured under the skin. This paper presents a bio-impedance sensor ASIC targeting a battery-free, miniature size, implantable device, which performs accurate 4-point complex impedance extraction in the frequency range from 2 kHz to 2 MHz. The ASIC is fabricated in 150 nm CMOS, has a size of 1.22 mm x 1.22 mm and consumes 165 uA from a 1.8 V power supply. The ASIC is embedded in a prototype which communicates with, and is powered by an external reader device through inductive coupling. The prototype is validated by measuring the impedances of different combinations of discrete components, measuring the electrochemical impedance of physiological solution, and performing ex vivo measurements on animal organs. The proposed ASIC is able to extract complex impedances with around 1 Ohm resolution; therefore enabling accurate wireless tissue measurements.
Using HTML5 to Prevent Detection of Drive-by-Download Web Malware
Venue: arXiv cs.CR 2015
Year: 2015

The web is experiencing an explosive growth in the last years. New technologies are introduced at a very fast-pace with the aim of narrowing the gap between web-based applications and traditional desktop applications. The results are web applications that look and feel almost like desktop applications while retaining the advantages of being originated from the web. However, these advancements come at a price. The same technologies used to build responsive, pleasant and fully-featured web applications, can also be used to write web malware able to escape detection systems. In this article we present new obfuscation techniques, based on some of the features of the upcoming HTML5 standard, which can be used to deceive malware detection systems. The proposed techniques have been experimented on a reference set of obfuscated malware. Our results show that the malware rewritten using our obfuscation techniques go undetected while being analyzed by a large number of detection systems. The same detection systems were able to correctly identify the same malware in its original unobfuscated form. We also provide some hints about how the existing malware detection systems can be modified in order to cope with these new techniques.
Middle-Solving Grobner bases algorithm for cryptanalysis over finite fields
Venue: arXiv cs.CR 2015
Year: 2015

Algebraic cryptanalysis usually requires to recover the secret key by solving polynomial equations. Grobner bases algorithm is a well-known method to solve this problem. However, a serious drawback exists in the Grobner bases based algebraic attacks, namely, any information won't be got if we couldn't work out the Grobner bases of the polynomial equations system. In this paper, firstly, a generalized model of Grobner basis algorithms is presented, which provides us a platform to analyze and solve common problems of the algorithms. Secondly, we give and prove the degree bound of the polynomials appeared during the computation of Grobner basis after field polynomials is added. Finally, by detecting the temporary basis during the computation of Grobner bases and then extracting the univariate polynomials contained unique solution in the temporary basis, a heuristic strategy named Middle-Solving is presented to solve these polynomials at each iteration of the algorithm. Farther, two specific application mode of Middle-Solving strategy for the incremental and non-incremental Grobner bases algorithms are presented respectively. By using the Middle-Solving strategy, even though we couldn't work out the final Grobner bases, some information of the variables still leak during the computational process.
Deadline-aware Power Management in Data Centers
Venue: arXiv cs.DS 2015
Year: 2015

We study the dynamic power optimization problem in data centers. We formulate and solve the following offline problem: in which slot which server has to be assigned to which job; and in which slot which server has to be switched ON or OFF so that the total power is optimal for some time horizon. We show that the offline problem is a new version of generalized assignment problem including new constraints issuing from deadline characteristics of jobs and difference of activation energy of servers. We propose an online algorithm that solves the problem heuristically and compare it to randomized routing.
S-index: Towards Better Metrics for Quantifying Research Impact
Venue: arXiv cs.DL 2015
Year: 2015

The ongoing growth in the volume of scientific literature available today precludes researchers from efficiently discerning the relevant from irrelevant content. Researchers are constantly interested in impactful papers, authors and venues in their respective fields. Moreover, they are interested in the so-called recent "rising stars" of these contexts which may lead to attractive directions for future work, collaborations or impactful publication venues. In this work, we address the problem of quantifying research impact in each of these contexts, in order to better direct attention of researchers and streamline the processes of comparison, ranking and evaluation of contribution. Specifically, we begin by outlining intuitive underlying assumptions that impact quantification methods should obey and evaluate when current state-of-the-art methods fail to satisfy these properties. To this end, we introduce the s-index metric which quantifies research impact through influence propagation over a heterogeneous citation network. s-index is tailored from these intuitive assumptions and offers a number of desirable qualities including robustness, natural temporality and straightforward extensibility from the paper impact to broader author and venue impact contexts. We evaluate its effectiveness on the publicly available Microsoft Academic Search citation graph with over 119 million papers and 1 billion citation edges with 103 million and 21 thousand associated authors and venues respectively.
Teaching Leśniewski's Prothetic with a Natural Deduction System
Venue: arXiv cs.CY 2015
Year: 2015

Protothetic is one of the most stimulating systems for propositional logic. Including quantifiers and an inference rule for definitions, it is a very interesting mean for the study of many questions of metalogic. Unfortunately, it only exists in an axiomatic version, far too complicated and unusual to be easily understood by nowadays students in logic. In this paper, we present a system which is a natural deduction (in Fitch-Jaśkowski's style) version of protothetic. According to us, this system is adequate for teaching Leśniewski's logic to students accustomed to natural deduction.
Algorithm for Solving Massively Underdefined Systems of Multivariate Quadratic Equations over Finite Fields
Venue: arXiv cs.CR 2015
Year: 2015

Solving systems of m multivariate quadratic equations in n variables (MQ-problem) over finite fields is NP-hard. The security of many cryptographic systems is based on this problem. Up to now, the best algorithm for solving the underdefined MQ-problem is Hiroyuki Miura et al.'s algorithm, which is a polynomial-time algorithm when \[n \ge m(m + 3)/2\] and the characteristic of the field is even. In order to get a wider applicable range, we reduce the underdefined MQ-problem to the problem of finding square roots over finite field, and then combine with the guess and determine method. In this way, the applicable range is extended to \[n \ge m(m + 1)/2\], which is the widest range until now. Theory analysis indicates that the complexity of our algorithm is \[O(q{n^ω}m{(\log {\kern 1pt} {\kern 1pt} q)^2}){\kern 1pt} \] when characteristic of the field is even and \[O(q{2^m}{n^ω}m{(\log {\kern 1pt} {\kern 1pt} q)^2})\] when characteristic of the field is odd, where \[2 \le ω\le 3\] is the complexity of Gaussian elimination.
A lower bound on the data rate of dirty paper coding in general noise and interference
Venue: arXiv cs.IT 2015
Year: 2015

Dirty paper coding (DPC) allows a transmitter to send information to a receiver in the presence of interference that is known (non-causally) to the transmitter. The original version of DPC was derived for the case where the noise and the interference are statistically independent Gaussian random sequences. More recent works extended this approach to the case where the noise and the interference are mutually independent and at least one of them is Gaussian. In this letter we further extend the DPC scheme by relaxing the Gaussian and statistical independence assumptions. We provide lower bounds on the achievable data rates in a DPC setting for the case of possibly dependent noise, interference and input signals. Also, the interference and noise terms are allowed to have arbitrary probability distributions. The bounds are relatively simple, are phrased in terms of second-order statistics, and are tight when the actual noise distribution is close to Gaussian.
Ensemble of Hankel Matrices for Face Emotion Recognition
Venue: arXiv cs.CV 2015
Year: 2015

In this paper, a face emotion is considered as the result of the composition of multiple concurrent signals, each corresponding to the movements of a specific facial muscle. These concurrent signals are represented by means of a set of multi-scale appearance features that might be correlated with one or more concurrent signals. The extraction of these appearance features from a sequence of face images yields to a set of time series. This paper proposes to use the dynamics regulating each appearance feature time series to recognize among different face emotions. To this purpose, an ensemble of Hankel matrices corresponding to the extracted time series is used for emotion classification within a framework that combines nearest neighbor and a majority vote schema. Experimental results on a public available dataset shows that the adopted representation is promising and yields state-of-the-art accuracy in emotion classification.
Modelling Structured Societies: a Multi-relational Approach to Context Permeability
Venue: arXiv cs.MA 2015
Year: 2015

The structure of social relations is fundamental for the construction of plausible simulation scenarios. It shapes the way actors interact and create their identity within overlapping social contexts. Each actor interacts in multiple contexts within different types of social relations that constitute their social space. In this article, we present an approach to model structured agent societies with multiple coexisting social networks. We study the notion of context permeability, using a game in which agents try to achieve global consensus. We design and analyse two different models of permeability. In the first model, agents interact concurrently in multiple social networks. In the second, we introduce a context switching mechanism which adds a dynamic temporal component to agent interaction in the model. Agents switch between the different networks spending more or less time in each one. We compare these models and analyse the influence of different social networks regarding the speed of convergence to consensus. We conduct a series of experiments that show the impact of different configurations for coexisting social networks. This approach unveils both the limitations of the current modelling approaches and possible research directions for complex social space simulations.
Pseudo-Query Reformulation
Venue: arXiv cs.IR 2015
Year: 2015

Automatic query reformulation refers to rewriting a user's original query in order to improve the ranking of retrieval results compared to the original query. We present a general framework for automatic query reformulation based on discrete optimization. Our approach, referred to as pseudo-query reformulation, treats automatic query reformulation as a search problem over the graph of unweighted queries linked by minimal transformations (e.g. term additions, deletions). This framework allows us to test existing performance prediction methods as heuristics for the graph search process. We demonstrate the effectiveness of the approach on several publicly available datasets.
NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
Venue: arXiv cs.CY 2015
Year: 2015

We present a new software tool for teaching logic based on natural deduction. Its proof system is formalized in the proof assistant Isabelle such that its definition is very precise. Soundness of the formalization has been proved in Isabelle. The tool is open source software developed in TypeScript / JavaScript and can thus be used directly in a browser without any further installation. Although developed for undergraduate computer science students who are used to study and program concrete computer code in a programming language we consider the approach relevant for a broader audience and for other proof systems as well.
Graph Coloring Based Pilot Allocation to Mitigate Pilot Contamination for Multi-Cell Massive MIMO Systems
Venue: arXiv cs.IT 2015
Year: 2015

A massive multiple-input multiple-output (MIMO) system, which utilizes a large number of base station (BS) antennas to serve a set of users, suffers from pilot contamination due to the inter-cell interference (ICI). In this letter, a graph coloring based pilot allocation (GC-PA) scheme is proposed to mitigate pilot contamination for multi-cell massive MIMO systems. Specifically, by exploiting the large-scale characteristics of fading channels, an interference graph is firstly constructed to describe the potential ICI relationship of all users. Then, with the limited pilot resource, the proposed GC-PA scheme aims to mitigate the potential ICI by efficiently allocating pilots among users in the interference graph. The performance gain of the proposed scheme is verified by simulations.
The projection method for continuous-time consensus seeking
Venue: arXiv cs.SY 2015
Year: 2015

For the case where the dependency digraph has no spanning in-tree, we characterize the region of convergence of the basic continuous-time distributed consensus algorithm and show that consensus can be achieved by employing the method of orthogonal projection, which has been proposed for the discrete-time coordination problem.
Wikidata through the Eyes of DBpedia
Venue: arXiv cs.DB 2015
Year: 2015

DBpedia is one of the first and most prominent nodes of the Linked Open Data cloud. It provides structured data for more than 100 Wikipedia language editions as well as Wikimedia Commons, has a mature ontology and a stable and thorough Linked Data publishing lifecycle. Wikidata, on the other hand, has recently emerged as a user curated source for structured information which is included in Wikipedia. In this paper, we present how Wikidata is incorporated in the DBpedia ecosystem. Enriching DBpedia with structured information from Wikidata provides added value for a number of usage scenarios. We outline those scenarios and describe the structure and conversion process of the DBpediaWikidata dataset.
Formulas for Continued Fractions. An Automated Guess and Prove Approach
Venue: arXiv cs.SC 2015
Year: 2015

We describe a simple method that produces automatically closed forms for the coefficients of continued fractions expansions of a large number of special functions. The function is specified by a non-linear differential equation and initial conditions. This is used to generate the first few coefficients and from there a conjectured formula. This formula is then proved automatically thanks to a linear recurrence satisfied by some remainder terms. Extensive experiments show that this simple approach and its straightforward generalization to difference and $q$-difference equations capture a large part of the formulas in the literature on continued fractions.
Strong games played on random graphs
Venue: arXiv cs.DM 2015
Year: 2015

In a strong game played on the edge set of a graph G there are two players, Red and Blue, alternating turns in claiming previously unclaimed edges of G (with Red playing first). The winner is the first one to claim all the edges of some target structure (such as a clique, a perfect matching, a Hamilton cycle, etc.). It is well known that Red can always ensure at least a draw in any strong game, but finding explicit winning strategies is a difficult and a quite rare task. We consider strong games played on the edge set of a random graph G ~ G(n,p) on n vertices. We prove, for sufficiently large $n$ and a fixed constant 0 < p < 1, that Red can w.h.p win the perfect matching game on a random graph G ~ G(n,p).
Effective Rate Analysis of MISO Systems over $α$-$μ$ Fading Channels
Venue: arXiv cs.IT 2015
Year: 2015

The effective rate is an important performance metric of real-time applications in next generation wireless networks. In this paper, we present an analysis of the effective rate of multiple-input single-output (MISO) systems over $α$-$μ$ fading channels under a maximum delay constraint. More specifically, novel and highly accurate closed-form approximate expressions of the effective rate are derived for such systems assuming the generalized $α$-$μ$ channel model. In order to examine the impact of system and channel parameters on the effective rate, we also derive closed-form expressions of the effective rate in asymptotically high and low signal-to-noise ratio (SNR) regimes. Furthermore, connections between our derived results and existing results from the literature are revealed for the sake of completeness. Our results demonstrate that the effective rate is a monotonically increasing function of channel fading parameters $α$ and $μ$, as well as the number of transmit antennas, while it decreases to zero when the delay constraint becomes stringent.
Hybrid access control with modified SINR association for future heterogeneous networks
Venue: arXiv cs.IT 2015
Year: 2015

The heterogeneity in cellular networks that comprise multiple base stations types imposes new challenges in network planning and deployment of future generation of cellular networks. The Radio Resource Management (RRM) techniques, such as dynamic sharing of the available resources and advanced user association strategies, determine the overall network capacity and efficiency. This paper evaluates the downlink performance of a two tier heterogeneous network (consisting of macro and femto tiers) in terms of rate distribution, i.e. the percentage of users that achieve certain rate in the system. The paper specifically addresses the femto tier RRM by randomization of the allocated resources and the user association process by introducing a modified SINR association strategy with bias factor for load balancing. Also, the paper introduces hybrid access control mechanism at the femto tier that allows the authorized users of the femtocell, which are part of the Closed Subscriber Group (CSG) on the femtocell, to achieve higher data rates up to 10 times compared to the other regular users associated in the access.
Uniform-Price Mechanism Design for a Large Population of Dynamic Agents
Venue: arXiv cs.SY 2015
Year: 2015

This paper focuses on the coordination of a large population of dynamic agents with private information over multiple periods. Each agent maximizes the individual utility, while the coordinator determines the market rule to achieve group objectives. The coordination problem is formulated as a dynamic mechanism design problem. A mechanism is proposed based on the competitive equilibrium of the large population game. We derive the conditions for the general nonlinear dynamic systems under which the proposed mechanism is incentive compatible and can implement the social choice function in $ε$-Nash equilibrium. In addition, we show that for linear quadratic problems with bounded parameters, the proposed mechanism can maximize the social welfare subject to a total resource constraint in $ε$-dominant strategy equilibrium.
Scaling Monte Carlo Tree Search on Intel Xeon Phi
Venue: arXiv cs.DC 2015
Year: 2015

Many algorithms have been parallelized successfully on the Intel Xeon Phi coprocessor, especially those with regular, balanced, and predictable data access patterns and instruction flows. Irregular and unbalanced algorithms are harder to parallelize efficiently. They are, for instance, present in artificial intelligence search algorithms such as Monte Carlo Tree Search (MCTS). In this paper we study the scaling behavior of MCTS, on a highly optimized real-world application, on real hardware. The Intel Xeon Phi allows shared memory scaling studies up to 61 cores and 244 hardware threads. We compare work-stealing (Cilk Plus and TBB) and work-sharing (FIFO scheduling) approaches. Interestingly, we find that a straightforward thread pool with a work-sharing FIFO queue shows the best performance. A crucial element for this high performance is the controlling of the grain size, an approach that we call Grain Size Controlled Parallel MCTS. Our subsequent comparing with the Xeon CPUs shows an even more comprehensible distinction in performance between different threading libraries. We achieve, to the best of our knowledge, the fastest implementation of a parallel MCTS on the 61 core Intel Xeon Phi using a real application (47 relative to a sequential run).