OpenRaiser/Intern-Atlas huggingface dataset:
Lost in Self-stabilization
Venue: arXiv cs.DM 2014
Year: 2014

One of the questions addressed here is How can a twisted thread correct itself?. We consider a theoretical model where the studied mathematical object represents a 2D twisted discrete thread linking two points. This thread is made of a chain of agents which are lost, i.e. they have no knowledge of the global setting and no sense of direction. Thus, the modifications made by the agents are local and all the decisions use only minimal information about the local neighborhood. We introduce a random process such that the thread reorganizes itself efficiently to become a discrete line between these two points. The second question addressed here is to reorder a word by local flips in order to scatter the letters to avoid long successions of the same letter. These two questions are equivalent. The work presented here is at the crossroad of many different domains such as modeling cooling process in crystallography [2, 3, 8], stochastic cellular automata [6, 7], organizing a line of robots in distributed algorithms (the robot chain problem [5, 11]), and Christoffel words in language theory [1].
Immersive and Collaborative Data Visualization Using Virtual Reality Platforms
Venue: arXiv cs.HC 2014
Year: 2014

Effective data visualization is a key part of the discovery process in the era of big data. It is the bridge between the quantitative content of the data and human intuition, and thus an essential component of the scientific path from data into knowledge and understanding. Visualization is also essential in the data mining process, directing the choice of the applicable algorithms, and in helping to identify and remove bad data from the analysis. However, a high complexity or a high dimensionality of modern data sets represents a critical obstacle. How do we visualize interesting structures and patterns that may exist in hyper-dimensional data spaces? A better understanding of how we can perceive and interact with multi dimensional information poses some deep questions in the field of cognition technology and human computer interaction. To this effect, we are exploring the use of immersive virtual reality platforms for scientific data visualization, both as software and inexpensive commodity hardware. These potentially powerful and innovative tools for multi dimensional data visualization can also provide an easy and natural path to a collaborative data visualization and exploration, where scientists can interact with their data and their colleagues in the same visual space. Immersion provides benefits beyond the traditional desktop visualization tools: it leads to a demonstrably better perception of a datascape geometry, more intuitive data understanding, and a better retention of the perceived relationships in the data.
Super-resolution method using sparse regularization for point-spread function recovery
Venue: arXiv cs.CV 2014
Year: 2014

In large-scale spatial surveys, such as the forthcoming ESA Euclid mission, images may be undersampled due to the optical sensors sizes. Therefore, one may consider using a super-resolution (SR) method to recover aliased frequencies, prior to further analysis. This is particularly relevant for point-source images, which provide direct measurements of the instrument point-spread function (PSF). We introduce SPRITE, SParse Recovery of InsTrumental rEsponse, which is an SR algorithm using a sparse analysis prior. We show that such a prior provides significant improvements over existing methods, especially on low SNR PSFs.
A hierarchical framework for object recognition
Venue: arXiv cs.CV 2014
Year: 2014

Object recognition in the presence of background clutter and distractors is a central problem both in neuroscience and in machine learning. However, the performance level of the models that are inspired by cortical mechanisms, including deep networks such as convolutional neural networks and deep belief networks, is shown to significantly decrease in the presence of noise and background objects [19, 24]. Here we develop a computational framework that is hierarchical, relies heavily on key properties of the visual cortex including mid-level feature selectivity in visual area V4 and Inferotemporal cortex (IT) [4, 9, 12, 18], high degrees of selectivity and invariance in IT [13, 17, 18] and the prior knowledge that is built into cortical circuits (such as the emergence of edge detector neurons in primary visual cortex before the onset of the visual experience) [1, 21], and addresses the problem of object recognition in the presence of background noise and distractors. Our approach is specifically designed to address large deformations, allows flexible communication between different layers of representation and learns highly selective filters from a small number of training examples.
A mutli-thread tabu search algorithm
Venue: arXiv cs.AI 2014
Year: 2014

This paper describes a novel refinement to a Tabu search algorithm that has been implemented in an attempt to improve the robustness of the search when applied to particularly complex problems. In this approach, two Tabu searches are carried out in parallel. Each search thread is characterised by it's own short term memory which forces that point out of local optima. However, the two search threads share an intermediate term memory so allowing a degree of information to be passed between them. Results are presented for both unconstrained and constrained numerical functions as well as a problem in the field of hydraulic circuit optimization. Simulation of hydraulic circuit performance is achieved by linking the optimization algorithm to the commercial simulation package Bathfp.
Implementation and Experimental Evaluation of a Collision-Free MAC Protocol for WLANs
Venue: arXiv cs.NI 2014
Year: 2014

Collisions are a main cause of throughput degradation in Wireless LANs. The current contention mechanism for these networks is based on a random backoff strategy to avoid collisions with other transmitters. Even though it can reduce the probability of collisions, the random backoff prevents users from achieving Collision-Free schedules, where the channel would be used more efficiently. Modifying the contention mechanism by waiting for a deterministic timer after successful transmissions, users would be able to construct a Collision-Free schedule among successful contenders. This work shows the experimental results of a Collision-Free MAC (CF-MAC) protocol for WLANs using commercial hardware and open firmware for wireless network cards which is able to support many users. Testbed results show that the proposed CF-MAC protocol leads to a better distribution of the available bandwidth among users, higher throughput and lower losses than the unmodified WLANs clients using a legacy firmware.
A Description of the Subgraph Induced at a Labeling of a Graph by the Subset of Vertices with an Interval Spectrum
Venue: arXiv cs.DM 2014
Year: 2014

The sets of vertices and edges of an undirected, simple, finite, connected graph $G$ are denoted by $V(G)$ and $E(G)$, respectively. An arbitrary nonempty finite subset of consecutive integers is called an interval. An injective mapping $φ:E(G)\rightarrow \{1,2,...,|E(G)|\}$ is called a labeling of the graph $G$. If $G$ is a graph, $x$ is its arbitrary vertex, and $φ$ is its arbitrary labeling, then the set $S_G(x,φ)\equiv\{φ(e)/ e\in E(G), e \textrm{is incident with} x$\} is called a spectrum of the vertex $x$ of the graph $G$ at its labeling $φ$. For any graph $G$ and its arbitrary labeling $φ$, a structure of the subgraph of $G$, induced by the subset of vertices of $G$ with an interval spectrum, is described.
Technical Report: Compressive Temporal Higher Order Cyclostationary Statistics
Venue: arXiv cs.IT 2014
Year: 2014

The application of nonlinear transformations to a cyclostationary signal for the purpose of revealing hidden periodicities has proven to be useful for applications requiring signal selectivity and noise tolerance. The fact that the hidden periodicities, referred to as cyclic moments, are often compressible in the Fourier domain motivates the use of compressive sensing (CS) as an efficient acquisition protocol for capturing such signals. In this work, we consider the class of Temporal Higher Order Cyclostationary Statistics (THOCS) estimators when CS is used to acquire the cyclostationary signal assuming compressible cyclic moments in the Fourier domain. We develop a theoretical framework for estimating THOCS using the low-rate nonuniform sampling protocol from CS and illustrate the performance of this framework using simulated data.
Understanding the Mechanics of Some Localized Protocols by Theory of Complex Networks
Venue: arXiv cs.NI 2014
Year: 2014

In the study of ad hoc sensor networks, clustering plays an important role in energy conservation therefore analyzing the mechanics of such topology can be helpful to make logistic decisions .Using the theory of complex network the topological model is extended, where we account for the probability of preferential attachment and anti preferential attachment policy of sensor nodes to analyze the formation of clusters and calculate the probability of clustering. The theoretical analysis is conducted to determine nature of topology and quantify some of the observed facts during the execution of topology control protocols. The quantification of the observed facts leads to the alternative understanding of the energy efficiency of the routing protocols.
Performance Analysis of Mean Value-Based Power Allocation with Primary User Interference in Spectrum Sharing Systems
Venue: arXiv cs.IT 2014
Year: 2014

In this paper, we provide an exact expression for the ergodic capacity of the secondary user, and a unified closed-form expression for its bounds with taking the consideration of the primary interference at the secondary receiver. In addition, a simple but accurate approximation of the the ergodic capacity of the primary user is presented. Moreover, a primary user capacity loss based power allocation scheme for the secondary user is also proposed. Finally, we compare the performance of the two power allocation schemes in terms of the sum capacity. The results are validated through using numerical results and simulations.
Black-box Modeling and Compensation of Bursty Communication Signals in RF Power Amplifiers with Power-Dependent Parameters
Venue: arXiv cs.SY 2014
Year: 2014

This paper presents a new black-box technique for modeling long term memory effects in radio frequency power amplifiers. The proposed technique extends commonly used behavioral models by utilizing parameters that dynamically change depending on a long term memory effect while keeping the original model structure intact. This enables us to accurately track and model transient changes in power amplifier characteristics that vary slowly and are induced by the input signal. Identification of long term memory effects is discussed and an iterative identification algorithm for the model parameters is proposed. The model is experimentally tested on a 100 Watt Doherty power amplifier with a 4 MHz Gaussian noise signal that has a step--like change in the amplitude, representative of a realistic communication signal with bursty behavior and a 20 MHz 3GPP LTE test data. Results of behavioral modeling show a 2-2.5 dB and 5-6 dB improvement in average and peak NMSE modeling performance respectively, which shows the suitability of the technique to model bursty signals.
Drawing Partially Embedded and Simultaneously Planar Graphs
Venue: arXiv cs.CG 2014
Year: 2014

We investigate the problem of constructing planar drawings with few bends for two related problems, the partially embedded graph problem---to extend a straight-line planar drawing of a subgraph to a planar drawing of the whole graph---and the simultaneous planarity problem---to find planar drawings of two graphs that coincide on shared vertices and edges. In both cases we show that if the required planar drawings exist, then there are planar drawings with a linear number of bends per edge and, in the case of simultaneous planarity, a constant number of crossings between every pair of edges. Our proofs provide efficient algorithms if the combinatorial embedding of the drawing is given. Our result on partially embedded graph drawing generalizes a classic result by Pach and Wenger which shows that any planar graph can be drawn with a linear number of bends per edge if the location of each vertex is fixed.
How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers
Venue: arXiv cs.LO 2014
Year: 2014

In recent years the effectiveness of interactive theorem provers has increased to an extent that the bottleneck in the interactive process shifted to efficiency: while in principle large and complex theorems are provable (effectiveness), it takes a lot of effort for the user interacting with the system (lack of efficiency). We conducted focus groups to evaluate the usability of Isabelle/HOL and the KeY system with two goals: (a) detect usability issues in the interaction between interactive theorem provers and their user, and (b) analyze how evaluation and survey methods commonly used in the area of human-computer interaction, such as focus groups and co-operative evaluation, are applicable to the specific field of interactive theorem proving (ITP). In this paper, we report on our experience using the evaluation method focus groups and how we adapted this method to ITP. We describe our results and conclusions mainly on the "meta-level," i.e., we focus on the impact that specific characteristics of ITPs have on the setup and the results of focus groups. On the concrete level, we briefly summarise insights into the usability of the ITPs used in our case study.
Tinker, tailor, solver, proof
Venue: arXiv cs.LO 2014
Year: 2014

We introduce Tinker, a tool for designing and evaluating proof strategies based on proof-strategy graphs, a formalism previously introduced by the authors. We represent proof strategies as open-graphs, which are directed graphs with additional input/output edges. Tactics appear as nodes in a graph, and can be `piped' together by adding edges between them. Goals are added to the input edges of such a graph, and flow through the graph as the strategy is evaluated. Properties of the edges ensure that only the right `type' of goals are accepted. In this paper, we detail the Tinker tool and show how it can be integrated with two different theorem provers: Isabelle and ProofPower.
Advanced Proof Viewing in ProofTool
Venue: arXiv cs.LO 2014
Year: 2014

Sequent calculus is widely used for formalizing proofs. However, due to the proliferation of data, understanding the proofs of even simple mathematical arguments soon becomes impossible. Graphical user interfaces help in this matter, but since they normally utilize Gentzen's original notation, some of the problems persist. In this paper, we introduce a number of criteria for proof visualization which we have found out to be crucial for analyzing proofs. We then evaluate recent developments in tree visualization with regard to these criteria and propose the Sunburst Tree layout as a complement to the traditional tree structure. This layout constructs inferences as concentric circle arcs around the root inference, allowing the user to focus on the proof's structural content. Finally, we describe its integration into ProofTool and explain how it interacts with the Gentzen layout.
A Logic-Independent IDE
Venue: arXiv cs.LO 2014
Year: 2014

The author's MMT system provides a framework for defining and implementing logical systems. By combining MMT with the jEdit text editor, we obtain a logic-independent IDE. The IDE functionality includes advanced features such as context-sensitive auto-completion, search, and change management.
Graph Guessing Games and non-Shannon Information Inequalities
Venue: arXiv cs.IT 2014
Year: 2014

Guessing games for directed graphs were introduced by Riis for studying multiple unicast network coding problems. In a guessing game, the players toss generalised dice and can see some of the other outcomes depending on the structure of an underlying digraph. They later guess simultaneously the outcome of their own die. Their objective is to find a strategy which maximises the probability that they all guess correctly. The performance of the optimal strategy for a graph is measured by the guessing number of the digraph. Christofides and Markström studied guessing numbers of undirected graphs and defined a strategy which they conjectured to be optimal. One of the main results of this paper is a disproof of this conjecture. The main tool so far for computing guessing numbers of graphs is information theoretic inequalities. In the paper we show that Shannon's information inequalities, which work particularly well for a wide range of graph classes, are not sufficient for computing the guessing number. Finally we pose a few more interesting questions some of which we can answer and some which we leave as open problems.
Training for Fast Sequential Prediction Using Dynamic Feature Selection
Venue: arXiv cs.CL 2014
Year: 2014

We present paired learning and inference algorithms for significantly reducing computation and increasing speed of the vector dot products in the classifiers that are at the heart of many NLP components. This is accomplished by partitioning the features into a sequence of templates which are ordered such that high confidence can often be reached using only a small fraction of all features. Parameter estimation is arranged to maximize accuracy and early confidence in this sequence. We present experiments in left-to-right part-of-speech tagging on WSJ, demonstrating that we can preserve accuracy above 97% with over a five-fold reduction in run-time.
Addressing the non-functional requirements of computer vision systems: A case study
Venue: arXiv cs.CV 2014
Year: 2014

Computer vision plays a major role in the robotics industry, where vision data is frequently used for navigation and high-level decision making. Although there is significant research in algorithms and functional requirements, there is a comparative lack of emphasis on how best to map these abstract concepts onto an appropriate software architecture. In this study, we distinguish between the functional and non-functional requirements of a computer vision system. Using a RoboCup humanoid robot system as a case study, we propose and develop a software architecture that fulfills the latter criteria. The modifiability of the proposed architecture is demonstrated by detailing a number of feature detection algorithms and emphasizing which aspects of the underlying framework were modified to support their integration. To demonstrate portability, we port our vision system (designed for an application-specific DARwIn-OP humanoid robot) to a general-purpose, Raspberry Pi computer. We evaluate performance on both platforms and compare them to a vision system optimised for functional requirements only. The architecture and implementation presented in this study provide a highly generalisable framework for computer vision system design that is of particular benefit in research and development, competition and other environments in which rapid system evolution is necessary.
Wireless Charger Networking for Mobile Devices: Fundamentals, Standards, and Applications
Venue: arXiv cs.NI 2014
Year: 2014

Wireless charging is a technique of transmitting power through an air gap to an electrical device for the purpose of energy replenishment. Recently, the wireless charging technology has been significantly advanced in terms of efficiency and functionality. This article first presents an overview and fundamentals of wireless charging. We then provide the review of standards, i.e., Qi and Alliance for Wireless Power (A4WP), and highlight on their communication protocols. Next, we propose a novel concept of wireless charger networking which allows chargers to be connected to facilitate information collection and control. We demonstrate the application of the wireless charger network in user-charger assignment, which clearly shows the benefit in terms of reduced cost for users to identify the best chargers to replenish energy for their mobile devices.
A Novel Predictive and Non-Predictive Cooperative Model for Routing in Ad Hoc Networks
Venue: arXiv cs.NI 2014
Year: 2014

Adhoc networks are formed by intermediate nodes which agree to relay traffic.The link between nodes is broken when a node rejects to relay traffic. Various parameters like depreciation in the energy of a node, distance between nodes and mobility of the nodes play a vital role in determining the nodes rejection to relay traffic.The objective of this paper is to propose a novel model that identifies the cooperative nodes forming stable routes at the route discovery phase.The weight factor of the different parameters decides the varied type of networks where the proposed model can be applied. Hence, an Artificial Neural Network based nondeterministic generic predictive model is proposed to identify the varied types of networks based on the weight factor.This study has been substantiated by simulation using OMNET++ simulator. We are sure that this paper will give a better solution to identify cooperative nodes thereby improving the performance of the network.
Experiments to Improve Named Entity Recognition on Turkish Tweets
Venue: arXiv cs.CL 2014
Year: 2014

Social media texts are significant information sources for several application areas including trend analysis, event monitoring, and opinion mining. Unfortunately, existing solutions for tasks such as named entity recognition that perform well on formal texts usually perform poorly when applied to social media texts. In this paper, we report on experiments that have the purpose of improving named entity recognition on Turkish tweets, using two different annotated data sets. In these experiments, starting with a baseline named entity recognition system, we adapt its recognition rules and resources to better fit Twitter language by relaxing its capitalization constraint and by diacritics-based expansion of its lexical resources, and we employ a simplistic normalization scheme on tweets to observe the effects of these on the overall named entity recognition performance on Turkish tweets. The evaluation results of the system with these different settings are provided with discussions of these results.
Labeled embedding of (n,n-2)-graphs in their complements
Venue: arXiv cs.DM 2014
Year: 2014

Graph packing generally deals with unlabeled graphs. In \cite{EHRT11}, the authors have introduced a new variant of the graph packing problem, called the \textit{labeled packing of a graph}. This problem has recently been studied on trees \cite{TDK13} and cycles \cite{EHRT11}. In this note, we present a lower bound on the labeled packing number of any $(n,n-2)$-graph into $K_n$. This result improves the bound given by Woźniak in \cite{W94}.
Localization in Wireless Sensor Networks: A Survey
Venue: arXiv cs.NI 2014
Year: 2014

Localization is widely used in Wireless Sensor Networks (WSNs) to identify the current location of the sensor odes. A WSN consist of thousands of nodes that make the installation of GPS on each sensor node expensive and moreover GPS may not provide exact localization results in an indoor environment. Manually configuring location reference on each sensor node is also not possible for dense network. This gives rise to a problem where the sensor nodes must identify its current location without using any special hardware like GPS and without the help of manual configuration. In this paper we review the localization techniques used by wireless sensor nodes to identify their current location.
Achieving Shannon Capacity Region as Secrecy Rate Region in a Multiple Access Wiretap Channel
Venue: arXiv cs.IT 2014
Year: 2014

We consider a two user multiple-access channel with an eavesdropper at the receiving end. We use previously transmitted messages as a key in the next slot till we achieve the capacity region of the usual Multiple Access Channel (MAC).