OpenRaiser/Intern-Atlas huggingface dataset:
Detecting an induced net subdivision
Venue: arXiv cs.DM 2013
Year: 2013

A {\em net} is a graph consisting of a triangle $C$ and three more vertices, each of degree one and with its neighbour in $C$, and all adjacent to different vertices of $C$. We give a polynomial-time algorithm to test whether an input graph has an induced subgraph which is a subdivision of a net. Unlike many similar questions, this does not seem to be solvable by an application of the "three-in-a-tree" subroutine.
Unary negation
Venue: arXiv cs.LO 2013
Year: 2013

We study fragments of first-order logic and of least fixed point logic that allow only unary negation: negation of formulas with at most one free variable. These logics generalize many interesting known formalisms, including modal logic and the $μ$-calculus, as well as conjunctive queries and monadic Datalog. We show that satisfiability and finite satisfiability are decidable for both fragments, and we pinpoint the complexity of satisfiability, finite satisfiability, and model checking. We also show that the unary negation fragment of first-order logic is model-theoretically very well behaved. In particular, it enjoys Craig Interpolation and the Projective Beth Property.
Direct off-line robot programming via a common CAD package
Venue: arXiv cs.RO 2013
Year: 2013

This paper focuses on intuitive and direct off-line robot programming from a CAD drawing running on a common 3-D CAD package. It explores the most suitable way to represent robot motion in a CAD drawing, how to automatically extract such motion data from the drawing, make the mapping of data from the virtual (CAD model) to the real environment and the process of automatic generation of robot paths/programs. In summary, this study aims to present a novel CAD-based robot programming system accessible to anyone with basic knowledge of CAD and robotics. Experiments on different manipulation tasks show the effectiveness and versatility of the proposed approach.
CAD-based robot programming: The role of Fuzzy-PI force control in unstructured environments
Venue: arXiv cs.RO 2013
Year: 2013

More and more, new ways of interaction between humans and robots are desired, something that allow us to program a robot in an intuitive way, quickly and with a high-level of abstraction from the robot language. In this paper is presented a CAD-based system that allows users with basic skills in CAD and without skills in robot programming to generate robot programs from a CAD model of a robotic cell. When the CAD model reproduces exactly the real scenario, the system presents a satisfactory performance. On the contrary, when the CAD model does not reproduce exactly the real scenario or the calibration process is poorly done, we are dealing with uncertain (unstructured environment). In order to minimize or eliminate the previously mentioned problems, it was introduced sensory feedback (force and torque sensing) in the robotic framework. By controlling the end-effector pose and specifying its relationship to the interaction/contact forces, robot programmers can ensure that the robot maneuvers in an unstructured environment, damping possible impacts and also increasing the tolerance to positioning errors from the calibration process. Fuzzy-PI reasoning was used as a force control technique. The effectiveness of the proposed approach was evaluated in a series of experiments.
Distinguishing Topical and Social Groups Based on Common Identity and Bond Theory
Venue: arXiv cs.SI 2013
Year: 2013

Social groups play a crucial role in social media platforms because they form the basis for user participation and engagement. Groups are created explicitly by members of the community, but also form organically as members interact. Due to their importance, they have been studied widely (e.g., community detection, evolution, activity, etc.). One of the key questions for understanding how such groups evolve is whether there are different types of groups and how they differ. In Sociology, theories have been proposed to help explain how such groups form. In particular, the common identity and common bond theory states that people join groups based on identity (i.e., interest in the topics discussed) or bond attachment (i.e., social relationships). The theory has been applied qualitatively to small groups to classify them as either topical or social. We use the identity and bond theory to define a set of features to classify groups into those two categories. Using a dataset from Flickr, we extract user-defined groups and automatically-detected groups, obtained from a community detection algorithm. We discuss the process of manual labeling of groups into social or topical and present results of predicting the group label based on the defined features. We directly validate the predictions of the theory showing that the metrics are able to forecast the group type with high accuracy. In addition, we present a comparison between declared and detected groups along topicality and sociality dimensions.
Design of Two Dimensional Unipolar (Optical) Orthogonal Codes Through One Dimensional Unipolar (Optical) Orthogonal Codes
Venue: arXiv cs.IT 2013
Year: 2013

In this paper, an algorithm for construction of multiple sets of two dimensional (2D) or matrix unipolar (optical) orthogonal codes has been proposed. Representations of these 2D codes in difference of positions representation (DoPR) have also been discussed along-with conventional weighted positions representation (WPR) of the code. This paper also proposes less complex methods for calculation of auto-correlation as well as cross-correlation constraints within set of matrix codes. The multiple sets of matrix codes provide flexibility for selection of optical orthogonal codes set in wavelength-hopping time-spreading (WHTS) optical code division multiple access (CDMA) system.
A Machine-Checked Proof for a Translation of Event-B Machines to JML
Venue: arXiv cs.SE 2013
Year: 2013

We present a machine-checked soundness proof of a translation of Event-B to the Java Modeling Language (JML). The translation is based on an operator EventB2Jml that maps Evnet-B events to JML method specifications, and deterministic and non-deterministic assignments to JML method post-conditions. This translation has previously been implemented as the EventB2Jml tool. We adopted a taking our own medicine approach in the formalisation of our proof so that Event-B as well as JML are formalised in Event-B and the proof is discharged with the Rodin platform. Hence, for any Event-B substitution (whether an event or an assignment) and for the JML method specification obtained by applying EventB2Jml to the substitution, we prove that the semantics of the JML method specification is simulated by the semantics of the substitution. Therefore, the JML specification obtained as translation from the Event-B substitution is a refinement of the substitution. Our proof includes invariants and the standard Event-B initialising event, but it does not include full machines or Event-B contexts. We assume that the semantics of JML and Event-B operate both on the same initial and final states, and we justify our assumption.
Software for Science: Some Personal Reflections
Venue: arXiv cs.CY 2013
Year: 2013

As computer systems become more and more complex, software and tools lag more and more behind. This is especially true for scientific software that often demands high performance, and thus needs to take advantage of parallelisms, memory hierarchies and other software and systems. How do we help bridge this ever-increasing gap? This paper describes some of my experiences and thoughts regarding licensing, code sharing, code maintenance, open access publishing, and educations and training. Details include my recent experiences with getting industrial funding for GPL licensed software, BSD issues, sharing code on GitHub, and how I inspire students to take my 4th year Parallel Computing elective which this semester has over 50 students enrolled. Some thoughts and comments regarding why both optimization and data locality are such a central issue for scientific software is also included.
TRANS outperforms MTF for two special types of request sequences without locality of reference
Venue: arXiv cs.DS 2013
Year: 2013

Various list accessing algorithms have been proposed in the literature and their performances have been analyzed theoretically and experimentally. Move-To-Front (MTF) and Transpose (TRANS) are two well known primitive list accessing algorithms. MTF has been proved to be the best performing online algorithm till date in the literature for real life inputs and practical applications with locality of reference. It has been shown that when storage space is extremely limited and pointers for lists cannot be used, then array implementation of TRANS gives efficient reorganization. Use of MTF is extensive in the literature whereas, the use of TRANS is rare. As mentioned as an open problem in literature, direct bounds on the behavior and performance of various list accessing algorithms are needed to allow realistic comparisons. Since it has been shown that no single optimal permutation algorithm exists, it becomes necessary to characterize the circumstances that indicate the advantage in using a particular list accessing algorithm. Motivated by above challenging research issue, in this paper we have made an analytical study for evaluating the performance of TRANS list accessing algorithm using two special types of request sequences without locality of reference. We have compared the performance of TRANS with MTF and observed that TRANS outperforms MTF for these considered types of request sequences.
Model Checking Contest @ Petri Nets, Report on the 2013 edition
Venue: arXiv cs.SE 2013
Year: 2013

This document presents the results of the Model Checking Contest held at Petri Nets 2013 in Milano. This contest aimed at a fair and experimental evaluation of the performances of model checking techniques applied to Petri nets. This is the third edition after two successful editions in 2011 and 2012. The participating tools were compared on several examinations (state space generation and evaluation of several types of formulæ -- reachability, LTL, CTL for various classes of atomic propositions) run on a set of common models (Place/Transition and Symmetric Petri nets). After a short overview of the contest, this paper provides the raw results from the contest, model per model and examination per examination. An HTML version of this report is also provided (http://mcc.lip6.fr).
A multi-stream hmm approach to offline handwritten arabic word recognition
Venue: arXiv cs.CV 2013
Year: 2013

In This paper we presented new approach for cursive Arabic text recognition system. The objective is to propose methodology analytical offline recognition of handwritten Arabic for rapid implementation. The first part in the writing recognition system is the preprocessing phase is the preprocessing phase to prepare the data was introduces and extracts a set of simple statistical features by two methods : from a window which is sliding long that text line the right to left and the approach VH2D (consists in projecting every character on the abscissa, on the ordinate and the diagonals 45° and 135°) . It then injects the resulting feature vectors to Hidden Markov Model (HMM) and combined the two HMM by multi-stream approach.
Limits of Efficiency in Sequential Auctions
Venue: arXiv cs.GT 2013
Year: 2013

We study the efficiency of sequential first-price item auctions at (subgame perfect) equilibrium. This auction format has recently attracted much attention, with previous work establishing positive results for unit-demand valuations and negative results for submodular valuations. This leaves a large gap in our understanding between these valuation classes. In this work we resolve this gap on the negative side. In particular, we show that even in the very restricted case in which each bidder has either an additive valuation or a unit-demand valuation, there exist instances in which the inefficiency at equilibrium grows linearly with the minimum of the number of items and the number of bidders. Moreover, these inefficient equilibria persist even under iterated elimination of weakly dominated strategies. Our main result implies linear inefficiency for many natural settings, including auctions with gross substitute valuations, capacitated valuations, budget-additive valuations, and additive valuations with hard budget constraints on the payments. Another implication is that the inefficiency in sequential auctions is driven by the maximum number of items contained in any player's optimal set, and this is tight. For capacitated valuations, our results imply a lower bound that equals the maximum capacity of any bidder, which is tight following the upper-bound technique established by Paes Leme et al. \cite{PaesLeme2012}.
Evaluation of the Performance/Energy Overhead in DSP Video Decoding and its Implications
Venue: arXiv cs.AR 2013
Year: 2013

Video decoding is considered as one of the most compute and energy intensive application in energy constrained mobile devices. Some specific processing units, such as DSPs, are added to those devices in order to optimize the performance and the energy consumption. However, in DSP video decoding, the inter-processor communication overhead may have a considerable impact on the performance and the energy consumption. In this paper, we propose to evaluate this overhead and analyse its impact on the performance and the energy consumption as compared to the GPP decoding. Our work revealed that the GPP can be the best choice in many cases due to the a significant overhead in DSP decoding which may represents 30% of the total decoding energy.
Learning Based Uplink Interference Management in 4G LTE Cellular Systems
Venue: arXiv cs.NI 2013
Year: 2013

LTEs uplink (UL) efficiency critically depends on how the interference across different cells is controlled. The unique characteristics of LTEs modulation and UL resource assignment poses considerable challenges in achieving this goal because most LTE deployments have 1:1 frequency re-use, and the uplink interference can vary considerably across successive time slots. In this work, we propose LeAP, a measurement data driven machine learning paradigm for power control to manage up-link interference in LTE. The data driven approach has the inherent advantage that the solution adapts based on network traffic, propagation and network topology, that is increasingly heterogeneous with multiple cell-overlays. LeAP system design consists of the following components: (i) design of user equipment (UE) measurement statistics that are succinct, yet expressive enough to capture the network dynamics, and (ii) design of two learning based algorithms that use the reported measurements to set the power control parameters and optimize the network performance. LeAP is standards compliant and can be implemented in centralized SON (self organized networking) server resource (cloud). We perform extensive evaluations using radio network plans from real LTE network operational in a major metro area in United States. Our results show that, compared to existing approaches, LeAP provides a 4.9x gain in the 20th percentile of user data rate, and 3.25x gain in median data rate.
Resurrecting My Revolution: Using Social Link Neighborhood in Bringing Context to the Disappearing Web
Venue: arXiv cs.IR 2013
Year: 2013

In previous work we reported that resources linked in tweets disappeared at the rate of 11% in the first year followed by 7.3% each year afterwards. We also found that in the first year 6.7%, and 14.6% in each subsequent year, of the resources were archived in public web archives. In this paper we revisit the same dataset of tweets and find that our prior model still holds and the calculated error for estimating percentages missing was about 4%, but we found the rate of archiving produced a higher error of about 11.5%. We also discovered that resources have disappeared from the archives themselves (7.89%) as well as reappeared on the live web after being declared missing (6.54%). We have also tested the availability of the tweets themselves and found that 10.34% have disappeared from the live web. To mitigate the loss of resources on the live web, we propose the use of a "tweet signature". Using the Topsy API, we extract the top five most frequent terms from the union of all tweets about a resource, and use these five terms as a query to Google. We found that using tweet signatures results in discovering replacement resources with 70+% textual similarity to the missing resource 41% of the time.
Approximate Counting CSP Solutions Using Partition Function
Venue: arXiv cs.AI 2013
Year: 2013

We propose a new approximate method for counting the number of the solutions for constraint satisfaction problem (CSP). The method derives from the partition function based on introducing the free energy and capturing the relationship of probabilities of variables and constraints, which requires the marginal probabilities. It firstly obtains the marginal probabilities using the belief propagation, and then computes the number of solutions according to the partition function. This allows us to directly plug the marginal probabilities into the partition function and efficiently count the number of solutions for CSP. The experimental results show that our method can solve both random problems and structural problems efficiently.
Emptiness and Universality Problems in Timed Automata with Positive Frequency
Venue: arXiv cs.FL 2013
Year: 2013

The languages of infinite timed words accepted by timed automata are traditionally defined using Buchi-like conditions. These acceptance conditions focus on the set of locations visited infinitely often along a run, but completely ignore quantitative timing aspects. In this paper we propose a natural quantitative semantics for timed automata based on the so-called frequency, which measures the proportion of time spent in the accepting locations. We study various properties of timed languages accepted with positive frequency, and in particular the emptiness and universality problems.
General Purpose Textual Sentiment Analysis and Emotion Detection Tools
Venue: arXiv cs.CL 2013
Year: 2013

Textual sentiment analysis and emotion detection consists in retrieving the sentiment or emotion carried by a text or document. This task can be useful in many domains: opinion mining, prediction, feedbacks, etc. However, building a general purpose tool for doing sentiment analysis and emotion detection raises a number of issues, theoretical issues like the dependence to the domain or to the language but also pratical issues like the emotion representation for interoperability. In this paper we present our sentiment/emotion analysis tools, the way we propose to circumvent the di culties and the applications they are used for.
A Scalable Heuristic for Viral Marketing Under the Tipping Model
Venue: arXiv cs.SI 2013
Year: 2013

In a "tipping" model, each node in a social network, representing an individual, adopts a property or behavior if a certain number of his incoming neighbors currently exhibit the same. In viral marketing, a key problem is to select an initial "seed" set from the network such that the entire network adopts any behavior given to the seed. Here we introduce a method for quickly finding seed sets that scales to very large networks. Our approach finds a set of nodes that guarantees spreading to the entire network under the tipping model. After experimentally evaluating 31 real-world networks, we found that our approach often finds seed sets that are several orders of magnitude smaller than the population size and outperform nodal centrality measures in most cases. In addition, our approach scales well - on a Friendster social network consisting of 5.6 million nodes and 28 million edges we found a seed set in under 3.6 hours. Our experiments also indicate that our algorithm provides small seed sets even if high-degree nodes are removed. Lastly, we find that highly clustered local neighborhoods, together with dense network-wide community structures, suppress a trend's ability to spread under the tipping model.
Sustainable Software Ecosystems for Open Science
Venue: arXiv cs.SE 2013
Year: 2013

Sustainable software ecosystems are difficult to build, and require concerted effort, community norms and collaborations. In science it is especially important to establish communities in which faculty, staff, students and open-source professionals work together and treat software as a first-class product of scientific investigation-just as mathematics is treated in the physical sciences. Kitware has a rich history of establishing collaborative projects in the science, engineering and medical research fields, and continues to work on improving that model as new technologies and approaches become available. This approach closely follows and is enhanced by the movement towards practicing open, reproducible research in the sciences where data, source code, methodology and approach are all available so that complex experiments can be independently reproduced and verified.
How (Not) to Shoot in Your Foot with SDN Local Fast Failover: A Load-Connectivity Tradeoff
Venue: arXiv cs.NI 2013
Year: 2013

This paper studies the resilient routing and (in-band) fast failover mechanisms supported in Software-Defined Networks (SDN). We analyze the potential benefits and limitations of such failover mechanisms, and focus on two main metrics: (1) correctness (in terms of connectivity and loop-freeness) and (2) load-balancing. We make the following contributions. First, we show that in the worst-case (i.e., under adversarial link failures), the usefulness of local failover is rather limited: already a small number of failures will violate connectivity properties under any fast failover policy, even though the underlying substrate network remains highly connected. We then present randomized and deterministic algorithms to compute resilient forwarding sets; these algorithms achieve an almost optimal tradeoff. Our worst-case analysis is complemented with a simulation study.
Cache Performance Study of Portfolio-Based Parallel CDCL SAT Solvers
Venue: arXiv cs.DC 2013
Year: 2013

Parallel SAT solvers are becoming mainstream. Their performance has made them win the past two SAT competitions consecutively and are in the limelight of research and industry. The problem is that it is not known exactly what is needed to make them perform even better; that is, how to make them solve more problems in less time. Also, it is also not know how well they scale in massive multi-core environments which, predictably, is the scenario of comming new hardware. In this paper we show that cache contention is a main culprit of a slowing down in scalability, and provide empirical results that for some type of searches, physically sharing the clause Database between threads is beneficial.