OpenRaiser/Intern-Atlas huggingface dataset:
Some Ideas for Program Verifier Tactics
Venue: arXiv cs.SE 2014
Year: 2014

A program verifier is a tool that can be used to verify that a "contract" for a program holds - i.e. given a precondition the program guarantees that a given postcondition holds - by only working at the level of the annotated program. An alternative approach is to use an interactive theorem prover, which enables users to encode common proof patterns as special programs called "tactics". This offers more flexibility than program verifiers, but at the expense of skills required by the user. Here, we add such flexibility to program verifiers by developing "tactics" as a form of program refactoring called DTacs. A formal characterisation and set of examples are given, illustrated with a case study from NASA.
The Linear Information Coupling Problems
Venue: arXiv cs.IT 2014
Year: 2014

Many network information theory problems face the similar difficulty of single-letterization. We argue that this is due to the lack of a geometric structure on the space of probability distribution. In this paper, we develop such a structure by assuming that the distributions of interest are close to each other. Under this assumption, the K-L divergence is reduced to the squared Euclidean metric in an Euclidean space. In addition, we construct the notion of coordinate and inner product, which will facilitate solving communication problems. We will present the application of this approach to the point-to-point channel, general broadcast channel, and the multiple access channel (MAC) with the common source. It can be shown that with this approach, information theory problems, such as the single-letterization, can be reduced to some linear algebra problems. Moreover, we show that for the general broadcast channel, transmitting the common message to receivers can be formulated as the trade-off between linear systems. We also provide an example to visualize this trade-off in a geometric way. Finally, for the MAC with the common source, we observe a coherent combining gain due to the cooperation between transmitters, and this gain can be quantified by applying our technique.
POS Tagging and its Applications for Mathematics
Venue: arXiv cs.DL 2014
Year: 2014

Content analysis of scientific publications is a nontrivial task, but a useful and important one for scientific information services. In the Gutenberg era it was a domain of human experts; in the digital age many machine-based methods, e.g., graph analysis tools and machine-learning techniques, have been developed for it. Natural Language Processing (NLP) is a powerful machine-learning approach to semiautomatic speech and language processing, which is also applicable to mathematics. The well established methods of NLP have to be adjusted for the special needs of mathematics, in particular for handling mathematical formulae. We demonstrate a mathematics-aware part of speech tagger and give a short overview about our adaptation of NLP methods for mathematical publications. We show the use of the tools developed for key phrase extraction and classification in the database zbMATH.
Acoustic Gait-based Person Identification using Hidden Markov Models
Venue: arXiv cs.HC 2014
Year: 2014

We present a system for identifying humans by their walking sounds. This problem is also known as acoustic gait recognition. The goal of the system is to analyse sounds emitted by walking persons (mostly the step sounds) and identify those persons. These sounds are characterised by the gait pattern and are influenced by the movements of the arms and legs, but also depend on the type of shoe. We extract cepstral features from the recorded audio signals and use hidden Markov models for dynamic classification. A cyclic model topology is employed to represent individual gait cycles. This topology allows to model and detect individual steps, leading to very promising identification rates. For experimental validation, we use the publicly available TUM GAID database, which is a large gait recognition database containing 3050 recordings of 305 subjects in three variations. In the best setup, an identification rate of 65.5 % is achieved out of 155 subjects. This is a relative improvement of almost 30 % compared to our previous work, which used various audio features and support vector machines.
Bird Species Categorization Using Pose Normalized Deep Convolutional Nets
Venue: arXiv cs.CV 2014
Year: 2014

We propose an architecture for fine-grained visual categorization that approaches expert human performance in the classification of bird species. Our architecture first computes an estimate of the object's pose; this is used to compute local image features which are, in turn, used for classification. The features are computed by applying deep convolutional nets to image patches that are located and normalized by the pose. We perform an empirical study of a number of pose normalization schemes, including an investigation of higher order geometric warping functions. We propose a novel graph-based clustering algorithm for learning a compact pose normalization space. We perform a detailed investigation of state-of-the-art deep convolutional feature implementations and fine-tuning feature learning for fine-grained classification. We observe that a model that integrates lower-level feature layers with pose-normalized extraction routines and higher-level feature layers with unaligned image features works best. Our experiments advance state-of-the-art performance on bird species recognition, with a large improvement of correct classification rates over previous methods (75% vs. 55-65%).
A note on the largest number of red nodes in red-black trees
Venue: arXiv cs.DS 2014
Year: 2014

In this paper, we are interested in the number of red nodes in red-black trees. We first present an $O(n^2\log n)$ time dynamic programming solution for computing $r(n)$, the largest number of red internal nodes in a red-black tree on $n$ keys. Then the algorithm is improved to some $O(\log n)$ time recursive and nonrecursive algorithms. Based on these improved algorithms we finally find a closed-form solution of $r(n)$.
Labelings for Decreasing Diagrams
Venue: arXiv cs.LO 2014
Year: 2014

This article is concerned with automating the decreasing diagrams technique of van Oostrom for establishing confluence of term rewrite systems. We study abstract criteria that allow to lexicographically combine labelings to show local diagrams decreasing. This approach has two immediate benefits. First, it allows to use labelings for linear rewrite systems also for left-linear ones, provided some mild conditions are satisfied. Second, it admits an incremental method for proving confluence which subsumes recent developments in automating decreasing diagrams. The techniques proposed in the article have been implemented and experimental results demonstrate how, e.g., the rule labeling benefits from our contributions.
Kalman Temporal Differences
Venue: arXiv cs.LG 2014
Year: 2014

Because reinforcement learning suffers from a lack of scalability, online value (and Q-) function approximation has received increasing interest this last decade. This contribution introduces a novel approximation scheme, namely the Kalman Temporal Differences (KTD) framework, that exhibits the following features: sample-efficiency, non-linear approximation, non-stationarity handling and uncertainty management. A first KTD-based algorithm is provided for deterministic Markov Decision Processes (MDP) which produces biased estimates in the case of stochastic transitions. Than the eXtended KTD framework (XKTD), solving stochastic MDP, is described. Convergence is analyzed for special cases for both deterministic and stochastic transitions. Related algorithms are experimented on classical benchmarks. They compare favorably to the state of the art while exhibiting the announced features.
On the Complexity of List Ranking in the Parallel External Memory Model
Venue: arXiv cs.DS 2014
Year: 2014

We study the problem of list ranking in the parallel external memory (PEM) model. We observe an interesting dual nature for the hardness of the problem due to limited information exchange among the processors about the structure of the list, on the one hand, and its close relationship to the problem of permuting data, which is known to be hard for the external memory models, on the other hand. By carefully defining the power of the computational model, we prove a permuting lower bound in the PEM model. Furthermore, we present a stronger Ω(log^2 N) lower bound for a special variant of the problem and for a specific range of the model parameters, which takes us a step closer toward proving a non-trivial lower bound for the list ranking problem in the bulk-synchronous parallel (BSP) and MapReduce models. Finally, we also present an algorithm that is tight for a larger range of parameters of the model than in prior work.
Robotic positioning device for three-dimensional printing
Venue: arXiv cs.RO 2014
Year: 2014

Additive manufacturing brings a variety of new possibilities to the construction industry, extending the capabilities of existing fabrication methods whilst also creating new possibilities. Currently three-dimensional printing is used to produce small-scale objects; large-scale three-dimensional printing is difficult due to the size of positioning devices and machine elements. Presently fixed Computer Numerically Controlled (CNC) routers and robotic arms are used to position print-heads. Fixed machines have work envelope limitations and can't produce objects outside of these limits. Large-scale three-dimensional printing requires large machines that are costly to build and hard to transport. This paper presents a compact print-head positioning device for Fused Deposition Modeling (FDM) a method of three-dimensional printing independent from the size of the object it prints.
Pilot Signal Design for Massive MIMO Systems: A Received Signal-To-Noise-Ratio-Based Approach
Venue: arXiv cs.IT 2014
Year: 2014

In this paper, the pilot signal design for massive MIMO systems to maximize the training-based received signal-to-noise ratio (SNR) is considered under two channel models: block Gauss-Markov and block independent and identically distributed (i.i.d.) channel models. First, it is shown that under the block Gauss-Markov channel model, the optimal pilot design problem reduces to a semi-definite programming (SDP) problem, which can be solved numerically by a standard convex optimization tool. Second, under the block i.i.d. channel model, an optimal solution is obtained in closed form. Numerical results show that the proposed method yields noticeably better performance than other existing pilot design methods in terms of received SNR.
Clifford Type Algebra Characteristics Investigation
Venue: arXiv cs.NA 2014
Year: 2014

The main properties of hypercomplex generalization of quaternion system as antiquaternion are presented in this article. Definitions and studied of antiquaternions conjugation are introduced, their norm and zero divisor, and how to perform operations on them.
Multiparty Session Actors
Venue: arXiv cs.DC 2014
Year: 2014

Actor coordination armoured with a suitable protocol description language has been a pressing problem in the actors community. We study the applicability of multiparty session type (MPST) protocols for verification of actor programs. We incorporate sessions to actors by introducing minimum additions to the model such as the notion of actor roles and protocol mailbox. The framework uses Scribble, which is a protocol description language based on multiparty session types. Our programming model supports actor-like syntax and runtime verification mechanism guaranteeing type-safety and progress of the communicating entities. An actor can implement multiple roles in a similar way as an object can implement multiple interfaces. Multiple roles allow for inter-concurrency in a single actor still preserving its progress property. We demonstrate our framework by designing and implementing a session actor library in Python and its runtime verification mechanism.
Towards Composable Concurrency Abstractions
Venue: arXiv cs.PL 2014
Year: 2014

In the past decades, many different programming models for managing concurrency in applications have been proposed, such as the actor model, Communicating Sequential Processes, and Software Transactional Memory. The ubiquity of multi-core processors has made harnessing concurrency even more important. We observe that modern languages, such as Scala, Clojure, or F#, provide not one, but multiple concurrency models that help developers manage concurrency. Large end-user applications are rarely built using just a single concurrency model. Programmers need to manage a responsive UI, deal with file or network I/O, asynchronous workflows, and shared resources. Different concurrency models facilitate different requirements. This raises the issue of how these concurrency models interact, and whether they are composable. After all, combining different concurrency models may lead to subtle bugs or inconsistencies. In this paper, we perform an in-depth study of the concurrency abstractions provided by the Clojure language. We study all pairwise combinations of the abstractions, noting which ones compose without issues, and which do not. We make an attempt to abstract from the specifics of Clojure, identifying the general properties of concurrency models that facilitate or hinder composition.
Session Type Isomorphisms
Venue: arXiv cs.LO 2014
Year: 2014

There has been a considerable amount of work on retrieving functions in function libraries using their type as search key. The availability of rich component specifications, in the form of behavioral types, enables similar queries where one can search a component library using the behavioral type of a component as the search key. Just like for function libraries, however, component libraries will contain components whose type differs from the searched one in the order of messages or in the position of the branching points. Thus, it makes sense to also look for those components whose type is different from, but isomorphic to, the searched one. In this article we give semantic and axiomatic characterizations of isomorphic session types. The theory of session type isomorphisms turns out to be subtle. In part this is due to the fact that it relies on a non-standard notion of equivalence between processes. In addition, we do not know whether the axiomatization is complete. It is known that the isomorphisms for arrow, product and sum types are not finitely axiomatisable, but it is not clear yet whether this negative results holds also for the family of types we consider in this work.
Multi-objective Reinforcement Learning with Continuous Pareto Frontier Approximation Supplementary Material
Venue: arXiv cs.AI 2014
Year: 2014

This document contains supplementary material for the paper "Multi-objective Reinforcement Learning with Continuous Pareto Frontier Approximation", published at the Twenty-Ninth AAAI Conference on Artificial Intelligence (AAAI-15). The paper is about learning a continuous approximation of the Pareto frontier in Multi-Objective Markov Decision Problems (MOMDPs). We propose a policy-based approach that exploits gradient information to generate solutions close to the Pareto ones. Differently from previous policy-gradient multi-objective algorithms, where n optimization routines are use to have n solutions, our approach performs a single gradient-ascent run that at each step generates an improved continuous approximation of the Pareto frontier. The idea is to exploit a gradient-based approach to optimize the parameters of a function that defines a manifold in the policy parameter space so that the corresponding image in the objective space gets as close as possible to the Pareto frontier. Besides deriving how to compute and estimate such gradient, we will also discuss the non-trivial issue of defining a metric to assess the quality of the candidate Pareto frontiers. Finally, the properties of the proposed approach are empirically evaluated on two interesting MOMDPs.
Energy efficient neighbor selection for flat wireless sensor networks
Venue: arXiv cs.NI 2014
Year: 2014

In this paper we have analyzed energy efficient neighbour selection algorithms for routing in wireless sensor networks. Since energy saving or consumption is an important aspect of wireless sensor networks, its precise usage is highly desirable both for the faithful performance of network and to increase the network life time. For this work, we have considered a flat network topology where every node has the same responsibility and capability. We have compared two energy efficient algorithms and analyzed their performances with increase in number of nodes, time rounds and node failures.
On the MIMO Capacity with Residual Transceiver Hardware Impairments
Venue: arXiv cs.IT 2014
Year: 2014

Radio-frequency (RF) impairments in the transceiver hardware of communication systems (e.g., phase noise (PN), high power amplifier (HPA) nonlinearities, or in-phase/quadrature-phase (I/Q) imbalance) can severely degrade the performance of traditional multiple-input multiple-output (MIMO) systems. Although calibration algorithms can partially compensate these impairments, the remaining distortion still has substantial impact. Despite this, most prior works have not analyzed this type of distortion. In this paper, we investigate the impact of residual transceiver hardware impairments on the MIMO system performance. In particular, we consider a transceiver impairment model, which has been experimentally validated, and derive analytical ergodic capacity expressions for both exact and high signal-to-noise ratios (SNRs). We demonstrate that the capacity saturates in the high-SNR regime, thereby creating a finite capacity ceiling. We also present a linear approximation for the ergodic capacity in the low-SNR regime, and show that impairments have only a second-order impact on the capacity. Furthermore, we analyze the effect of transceiver impairments on large-scale MIMO systems; interestingly, we prove that if one increases the number of antennas at one side only, the capacity behaves similar to the finite-dimensional case. On the contrary, if the number of antennas on both sides increases with a fixed ratio, the capacity ceiling vanishes; thus, impairments cause only a bounded offset in the capacity compared to the ideal transceiver hardware case.
Channel Modeling of Human Somatosensory Nanonetwork: Body Discriminative Touch and Proprioception Perspective
Venue: arXiv cs.ET 2014
Year: 2014

Nanonetwork design and analysis has become a very interesting topic in recent years. Though this area of research is in its formative stage, it definitely posses a strong integrity in finding out numerous applications in medical and allied sciences. Nanonetworking is indeed a nature built foundation which comprises human intra body communications. Somatosensory system is the one of the critical and must have systems of human body. This literature concentrates on the body discriminative touch and proprioception mechanism of somatosensory system. This particular system is well architecture by medial lemniscal pathway, in human body for transduction of touch and proprioceptive information. This paper seeks out the novel communication channel model of somatosensory system. The working principle of the channel model is established by an equivalent Moore machine. A novel algorithm MLP is proposed after its name, medial lemniscal pathway. A novel naomachine and appropriate processing unit are also devised, based on the automaton.
Mining of product reviews at aspect level
Venue: arXiv cs.CL 2014
Year: 2014

Todays world is a world of Internet, almost all work can be done with the help of it, from simple mobile phone recharge to biggest business deals can be done with the help of this technology. People spent their most of the times on surfing on the Web it becomes a new source of entertainment, education, communication, shopping etc. Users not only use these websites but also give their feedback and suggestions that will be useful for other users. In this way a large amount of reviews of users are collected on the Web that needs to be explored, analyse and organized for better decision making. Opinion Mining or Sentiment Analysis is a Natural Language Processing and Information Extraction task that identifies the users views or opinions explained in the form of positive, negative or neutral comments and quotes underlying the text. Aspect based opinion mining is one of the level of Opinion mining that determines the aspect of the given reviews and classify the review for each feature. In this paper an aspect based opinion mining system is proposed to classify the reviews as positive, negative and neutral for each feature. Negation is also handled in the proposed system. Experimental results using reviews of products show the effectiveness of the system.
BER Analysis of Multi-Cellular MIMO Systems with Increasing Number of BS Antennas
Venue: arXiv cs.NI 2014
Year: 2014

In this work, salient characteristics of a wireless communication system deploying a great number of antennas in the base station (BS), namely Massive MIMO system, are investigated. In particular, we found a simple and meaningful relationship that corroborates a fundamental assumption in recent related works: according the number of BS antennas $N$ grows, the product of the small-scale fading channel matrix with its conjugate transpose tends to a scaled identity, with a variability measure inversely proportional to $N$. Furthermore, analysis of the Massive MIMO system downlink is carried out from a bit-error-rate (BER) performance viewpoint, including some realistic adverse effects, such as interference from neighboring cells, channel estimation errors due to background thermal noise, and pilot contamination, which was recently shown to be the only impairment that remains in the MIMO multicell system with infinite number of BS antennas. Our numerical result findings show that, in the same way as with the sum capacity, the pilot contamination also limits the BER performance of a noncooperative multi-cell MIMO system with infinite number of BS antennas.
Hadwiger number of graphs with small chordality
Venue: arXiv cs.DS 2014
Year: 2014

The Hadwiger number of a graph G is the largest integer h such that G has the complete graph K_h as a minor. We show that the problem of determining the Hadwiger number of a graph is NP-hard on co-bipartite graphs, but can be solved in polynomial time on cographs and on bipartite permutation graphs. We also consider a natural generalization of this problem that asks for the largest integer h such that G has a minor with h vertices and diameter at most $s$. We show that this problem can be solved in polynomial time on AT-free graphs when s>=2, but is NP-hard on chordal graphs for every fixed s>=2.
A fast 25/6-approximation for the minimum unit disk cover problem
Venue: arXiv cs.CG 2014
Year: 2014

Given a point set P in 2D, the problem of finding the smallest set of unit disks that cover all of P is NP-hard. We present a simple algorithm for this problem with an approximation factor of 25/6 in the Euclidean norm and 2 in the max norm, by restricting the disk centers to lie on parallel lines. The run time and space of this algorithm is O(n log n) and O(n) respectively. This algorithm extends to any Lp norm and is asymptotically faster than known alternative approximation algorithms for the same approximation factor.