OpenRaiser/Intern-Atlas huggingface dataset:
Proving soundness of combinatorial Vickrey auctions and generating verified executable code
Venue: arXiv cs.GT 2013
Year: 2013

Using mechanised reasoning we prove that combinatorial Vickrey auctions are soundly specified in that they associate a unique outcome (allocation and transfers) to any valid input (bids). Having done so, we auto-generate verified executable code from the formally defined auction. This removes a source of error in implementing the auction design. We intend to use formal methods to verify new auction designs. Here, our contribution is to introduce and demonstrate the use of formal methods for auction verification in the familiar setting of a well-known auction.
The Royal Birth of 2013: Analysing and Visualising Public Sentiment in the UK Using Twitter
Venue: arXiv cs.CL 2013
Year: 2013

Analysis of information retrieved from microblogging services such as Twitter can provide valuable insight into public sentiment in a geographic region. This insight can be enriched by visualising information in its geographic context. Two underlying approaches for sentiment analysis are dictionary-based and machine learning. The former is popular for public sentiment analysis, and the latter has found limited use for aggregating public sentiment from Twitter data. The research presented in this paper aims to extend the machine learning approach for aggregating public sentiment. To this end, a framework for analysing and visualising public sentiment from a Twitter corpus is developed. A dictionary-based approach and a machine learning approach are implemented within the framework and compared using one UK case study, namely the royal birth of 2013. The case study validates the feasibility of the framework for analysis and rapid visualisation. One observation is that there is good correlation between the results produced by the popular dictionary-based approach and the machine learning approach when large volumes of tweets are analysed. However, for rapid analysis to be possible faster methods need to be developed using big data techniques and parallel methods.
Link Failure Recovery over Very Large Arbitrary Networks: The Case of Coding
Venue: arXiv cs.NI 2013
Year: 2013

Network coding-based link failure recovery techniques provide near-hitless recovery and offer high capacity efficiency. Diversity coding is the first technique to incorporate coding in this field and is easy to implement over small arbitrary networks. However, its capacity efficiency is restricted by its systematic coding and high design complexity even though its design complexity is lower than the other coding-based recovery techniques. Alternative techniques mitigate some of these limitations, but they are difficult to implement over arbitrary networks. In this paper, we propose a simple column generation-based design algorithm and a novel advanced diversity coding technique to achieve near-hitless recovery over arbitrary networks. The design framework consists of two parts: a main problem and subproblem. Main problem is realized with Linear Programming (LP) and Integer Linear Programming (ILP), whereas the subproblem can be realized with different methods. The simulation results suggest that both the novel coding structure and the novel design algorithm lead to higher capacity efficiency for near-hitless recovery. The novel design algorithm simplifies the capacity placement problem which enables implementing diversity coding-based techniques on very large arbitrary networks.
RBioCloud: A Light-weight Framework for Bioconductor and R-based Jobs on the Cloud
Venue: arXiv cs.DC 2013
Year: 2013

Large-scale ad hoc analytics of genomic data is popular using the R-programming language supported by 671 software packages provided by Bioconductor. More recently, analytical jobs are benefitting from on-demand computing and storage, their scalability and their low maintenance cost, all of which are offered by the cloud. While Biologists and Bioinformaticists can take an analytical job and execute it on their personal workstations, it remains challenging to seamlessly execute the job on the cloud infrastructure without extensive knowledge of the cloud dashboard. How analytical jobs can not only with minimum effort be executed on the cloud, but also how both the resources and data required by the job can be managed is explored in this paper. An open-source light-weight framework for executing R-scripts using Bioconductor packages, referred to as `RBioCloud', is designed and developed. RBioCloud offers a set of simple command-line tools for managing the cloud resources, the data and the execution of the job. Three biological test cases validate the feasibility of RBioCloud. The framework is publicly available from http://www.rbiocloud.com.
Axioms for Centrality
Venue: arXiv cs.SI 2013
Year: 2013

Given a social network, which of its nodes are more central? This question has been asked many times in sociology, psychology and computer science, and a whole plethora of centrality measures (a.k.a. centrality indices, or rankings) were proposed to account for the importance of the nodes of a network. In this paper, we try to provide a mathematically sound survey of the most important classic centrality measures known from the literature and propose an axiomatic approach to establish whether they are actually doing what they have been designed for. Our axioms suggest some simple, basic properties that a centrality measure should exhibit. Surprisingly, only a new simple measure based on distances, harmonic centrality, turns out to satisfy all axioms; essentially, harmonic centrality is a correction to Bavelas's classic closeness centrality designed to take unreachable nodes into account in a natural way. As a sanity check, we examine in turn each measure under the lens of information retrieval, leveraging state-of-the-art knowledge in the discipline to measure the effectiveness of the various indices in locating web pages that are relevant to a query. While there are some examples of this comparisons in the literature, here for the first time we take into consideration centrality measures based on distances, such as closeness, in an information-retrieval setting. The results match closely the data we gathered using our axiomatic approach. Our results suggest that centrality measures based on distances, which have been neglected in information retrieval in favour of spectral centrality measures in the last years, are actually of very high quality; moreover, harmonic centrality pops up as an excellent general-purpose centrality index for arbitrary directed graphs.
Fast image segmentation and restoration using parametric curve evolution with junctions and topology changes
Venue: arXiv cs.CV 2013
Year: 2013

Curve evolution schemes for image segmentation based on a region based contour model allowing for junctions, vector-valued images and topology changes are introduced. Together with an a posteriori denoising in the segmented homogeneous regions this leads to a fast and efficient method for image segmentation and restoration. An uneven spread of mesh points is avoided by using the tangential degrees of freedom. Several numerical simulations on artificial test problems and on real images illustrate the performance of the method.
On the Detection of Passive Eavesdroppers in the MIMO Wiretap Channel
Venue: arXiv cs.IT 2013
Year: 2013

The classic MIMO wiretap channel comprises a passive eavesdropper that attempts to intercept communications between an authorized transmitter-receiver pair, each node being equipped with multiple antennas. In a dynamic network, it is imperative that the presence of an eavesdropper be determined before the transmitter can deploy robust secrecyencoding schemes as a countermeasure. This is a difficult task in general, since by definition the eavesdropper is passive and never transmits. In this work we adopt a method that allows the legitimate nodes to detect the passive eavesdropper from the local oscillator power that is inadvertently leaked from its RF front end. We examine the performance of non-coherent energy detection and optimal coherent detection, followed by composite GLRT detection methods that account for unknown parameters. Numerical experiments demonstrate that the proposed detectors allow the legitimate nodes to increase the secrecy rate of the MIMO wiretap channel.
Adaptive Technique for Computationally Efficient Time Delay and Magnitude Estimation of Sinusoidal Signals
Venue: arXiv cs.SY 2013
Year: 2013

An online, adaptive method of time delay and magnitude estimation for sinusoidal signals is presented. The method is based on an adaptive gradient descent algorithm that directly determines the time delay and magnitudes of two noisy sinusoidal signals. The new estimator uses a novel quadrature carrier generator to produce the carriers for an adaptive quadrature phase detector, which in turn uses an arc tan function to compute the time delay. The proposed method is quite robust and can adapt to significant variation in input signal characteristics like magnitude and frequency imposing no requirement on the magnitudes of the two signals. It even works effectively when the signals have time-varying magnitudes. The convergence analysis of the proposed technique shows that estimate converges exponentially fast to their nominal values. In addition, if the technique is implemented in the continuous time domain, the delay estimation accuracy will not be constrained by the sampling frequency as observed in some of the classical techniques. Extensive simulations show that the proposed method provides very accurate estimates of the time delay comparable to that of the popular methods like Sinc-based estimator, Lagrange estimator, and the Quadrature estimator, as well the magnitude estimate of the input signals at lower signal to noise ratio at appreciably reduced computational cost.
Collective Mind: cleaning up the research and experimentation mess in computer engineering using crowdsourcing, big data and machine learning
Venue: arXiv cs.SE 2013
Year: 2013

Software and hardware co-design and optimization of HPC systems has become intolerably complex, ad-hoc, time consuming and error prone due to enormous number of available design and optimization choices, complex interactions between all software and hardware components, and multiple strict requirements placed on performance, power consumption, size, reliability and cost. We present our novel long-term holistic and practical solution to this problem based on customizable, plugin-based, schema-free, heterogeneous, open-source Collective Mind repository and infrastructure with unified web interfaces and on-line advise system. This collaborative framework distributes analysis and multi-objective off-line and on-line auto-tuning of computer systems among many participants while utilizing any available smart phone, tablet, laptop, cluster or data center, and continuously observing, classifying and modeling their realistic behavior. Any unexpected behavior is analyzed using shared data mining and predictive modeling plugins or exposed to the community at cTuning.org for collaborative explanation, top-down complexity reduction, incremental problem decomposition and detection of correlating program, architecture or run-time properties (features). Gradually increasing optimization knowledge helps to continuously improve optimization heuristics of any compiler, predict optimizations for new programs or suggest efficient run-time (online) tuning and adaptation strategies depending on end-user requirements. We decided to share all our past research artifacts including hundreds of codelets, numerical applications, data sets, models, universal experimental analysis and auto-tuning pipelines, self-tuning machine learning based meta compiler, and unified statistical analysis and machine learning plugins in a public repository to initiate systematic, reproducible and collaborative research, development and experimentation with a new publication model where experiments and techniques are validated, ranked and improved by the community.
Understanding the Benefits of Open Access in Femtocell Networks: Stochastic Geometric Analysis in the Uplink
Venue: arXiv cs.NI 2013
Year: 2013

We introduce a comprehensive analytical framework to compare between open access and closed access in two-tier femtocell networks, with regard to uplink interference and outage. Interference at both the macrocell and femtocell levels is considered. A stochastic geometric approach is employed as the basis for our analysis. We further derive sufficient conditions for open access and closed access to outperform each other in terms of the outage probability, leading to closed-form expressions to upper and lower bound the difference in the targeted received power between the two access modes. Simulations are conducted to validate the accuracy of the analytical model and the correctness of the bounds.
A thread-parallel algorithm for anisotropic mesh adaptation
Venue: arXiv cs.DC 2013
Year: 2013

Anisotropic mesh adaptation is a powerful way to directly minimise the computational cost of mesh based simulation. It is particularly important for multi-scale problems where the required number of floating-point operations can be reduced by orders of magnitude relative to more traditional static mesh approaches. Increasingly, finite element and finite volume codes are being optimised for modern multi-core architectures. Typically, decomposition methods implemented through the Message Passing Interface (MPI) are applied for inter-node parallelisation, while a threaded programming model, such as OpenMP, is used for intra-node parallelisation. Inter-node parallelism for mesh adaptivity has been successfully implemented by a number of groups. However, thread-level parallelism is significantly more challenging because the underlying data structures are extensively modified during mesh adaptation and a greater degree of parallelism must be realised. In this paper we describe a new thread-parallel algorithm for anisotropic mesh adaptation algorithms. For each of the mesh optimisation phases (refinement, coarsening, swapping and smoothing) we describe how independent sets of tasks are defined. We show how a deferred updates strategy can be used to update the mesh data structures in parallel and without data contention. We show that despite the complex nature of mesh adaptation and inherent load imbalances in the mesh adaptivity, a parallel efficiency of 60% is achieved on an 8 core Intel Xeon Sandybridge, and a 40% parallel efficiency is achieved using 16 cores in a 2 socket Intel Xeon Sandybridge ccNUMA system.
Induction in Algebra: a First Case Study
Venue: arXiv cs.LO 2013
Year: 2013

Many a concrete theorem of abstract algebra admits a short and elegant proof by contradiction but with Zorn's Lemma (ZL). A few of these theorems have recently turned out to follow in a direct and elementary way from the Principle of Open Induction distinguished by Raoult. The ideal objects characteristic of any invocation of ZL are eliminated, and it is made possible to pass from classical to intuitionistic logic. If the theorem has finite input data, then a finite partial order carries the required instance of induction, which thus is constructively provable. A typical example is the well-known theorem "every nonconstant coefficient of an invertible polynomial is nilpotent".
Stochastic Models Predict User Behavior in Social Media
Venue: arXiv cs.CY 2013
Year: 2013

User response to contributed content in online social media depends on many factors. These include how the site lays out new content, how frequently the user visits the site, how many friends the user follows, how active these friends are, as well as how interesting or useful the content is to the user. We present a stochastic modeling framework that relates a user's behavior to details of the site's user interface and user activity and describe a procedure for estimating model parameters from available data. We apply the model to study discussions of controversial topics on Twitter, specifically, to predict how followers of an advocate for a topic respond to the advocate's posts. We show that a model of user behavior that explicitly accounts for a user transitioning through a series of states before responding to an advocate's post better predicts response than models that fail to take these states into account. We demonstrate other benefits of stochastic models, such as their ability to identify users who are highly interested in advocate's posts.
H-infinity Optimal Approximation for Causal Spline Interpolation
Venue: arXiv cs.IT 2013
Year: 2013

In this paper, we give a causal solution to the problem of spline interpolation using H-infinity optimal approximation. Generally speaking, spline interpolation requires filtering the whole sampled data, the past and the future, to reconstruct the inter-sample values. This leads to non-causality of the filter, and this becomes a critical issue for real-time applications. Our objective here is to derive a causal system which approximates spline interpolation by H-infinity optimization for the filter. The advantage of H-infinity optimization is that it can address uncertainty in the input signals to be interpolated in design, and hence the optimized system has robustness property against signal uncertainty. We give a closed-form solution to the H-infinity optimization in the case of the cubic splines. For higher-order splines, the optimal filter can be effectively solved by a numerical computation. We also show that the optimal FIR (Finite Impulse Response) filter can be designed by an LMI (Linear Matrix Inequality), which can also be effectively solved numerically. A design example is presented to illustrate the result.
IDS in Telecommunication Network Using PCA
Venue: arXiv cs.NI 2013
Year: 2013

Data Security has become a very serious part of any organizational information system. Internet threats have become more intelligent so it can deceive the basic security solutions such as firewalls and antivirus scanners. To enhance the overall security of the network an additional security layer such as intrusion detection system (IDS) has to be added. The anomaly detection IDS is a type of IDS that can differentiate between normal and abnormal in the data monitored. This paper proposes two types of IDS, one of them can be used as a network intrusion detection system (NIDS) with overall success (0.9161) and high detection rate (0.9288) and the other type can also be used as a host intrusion detection system (HIDS) with overall success (0.8493) and very high detection rate (0.9628) using NSL-KDD data set.
Wireless Information and Energy Transfer in Multi-Antenna Interference Channel
Venue: arXiv cs.IT 2013
Year: 2013

This paper considers the transmitter design for wireless information and energy transfer (WIET) in a multiple-input single-output (MISO) interference channel (IFC). The design problem is to maximize the system throughput (i.e., the weighted sum rate) subject to individual energy harvesting constraints and power constraints. Different from the conventional IFCs without energy harvesting, the cross-link signals in the considered scenario play two opposite roles in information detection (ID) and energy harvesting (EH). It is observed that the ideal scheme, where the receivers can simultaneously perform ID and EH from the received signal, may not always achieve the best tradeoff between information transfer and energy harvesting, but simple practical schemes based on time splitting may perform better. We therefore propose two practical time splitting schemes, namely time division mode switching (TDMS) and time division multiple access (TDMA), in addition to a power splitting (PS) scheme which separates the received signal into two parts for ID and EH, respectively. In the two-user scenario, we show that beamforming is optimal to all the schemes. Moreover, the design problems associated with the TDMS and TDMA schemes admit semi-analytical solutions. In the general K-user scenario, a successive convex approximation method is proposed to handle the WIET problems associated with the ideal scheme and the PS scheme, which are known to be NP-hard in general. The K-user TDMS and TDMA schemes are shown efficiently solvable as convex problems. Simulation results show that stronger cross-link channel powers actually improve the information sum rate under energy harvesting constraints. Moreover, none of the schemes under consideration can dominate another in terms of the sum rate performance.
Service Discovery -- A Survey and Comparison
Venue: arXiv cs.NI 2013
Year: 2013

With the increasing number of services in the internet, companies intranets, and home networks: service discovery becomes an integral part of modern networked system. This paper provides a comprehensive survey of major solutions for service discovery. We cover techniques and features used in existing systems. Although a few survey articles have been published on this object, our contribution focuses on comparing and analyzing surveyed solutions according eight prime criteria, which we have defined before. This comparison will be helpful to determine limits of existing discovery protocols and identify future research opportunities in service discovery.
Mobile operators as banks or vice-versa? and: regulators interest in the best efficiency for payments
Venue: arXiv cs.CY 2013
Year: 2013

This paper addresses the strategic challenges of deposit banks, and payment clearinghouses, posed by the growing role of mobile operators as collectors and payment agents for flows of cash for themselves and third parties. Through analysis and data analysis from selected operators, it is shown that mobile operators achieve as money flow handlers levels of efficiency, profitability,and risk control comparable with deposit banks. Furthermore, the payment infrastructures deployed by both are found to be quite similar, and are analyzed in relation to financial profitability, strategic challenges and opportunities. This paves the way to either mobile operators taking a bigger role,or for banks to tie up such operators to them even more tightly,or for alliances/mergers to take place,all these options being subject to regulatory evolution which is analyzed as well . The consequences are mapped out in operational and regulatory terms
Subadditivity of Matrix phi-Entropy and Concentration of Random Matrices
Venue: arXiv cs.IT 2013
Year: 2013

Matrix concentration inequalities provide a direct way to bound the typical spectral norm of a random matrix. The methods for establishing these results often parallel classical arguments, such as the Laplace transform method. This work develops a matrix extension of the entropy method, and it applies these ideas to obtain some matrix concentration inequalities.
Information filtering in sparse online systems: recommendation via semi-local diffusion
Venue: arXiv cs.IR 2013
Year: 2013

With the rapid growth of the Internet and overwhelming amount of information and choices that people are confronted with, recommender systems have been developed to effectively support users' decision-making process in the online systems. However, many recommendation algorithms suffer from the data sparsity problem, i.e. the user-object bipartite networks are so sparse that algorithms cannot accurately recommend objects for users. This data sparsity problem makes many well-known recommendation algorithms perform poorly. To solve the problem, we propose a recommendation algorithm based on the semi-local diffusion process on a user-object bipartite network. The numerical simulation on two sparse datasets, Amazon and Bookcross, show that our method significantly outperforms the state-of-the-art methods especially for those small-degree users. Two personalized semi-local diffusion methods are proposed which further improve the recommendation accuracy. Finally, our work indicates that sparse online systems are essentially different from the dense online systems, all the algorithms and conclusions based on dense data should be rechecked again in sparse data.