OpenRaiser/Intern-Atlas huggingface dataset:
Finite Countermodel Based Verification for Program Transformation (A Case Study)
Venue: arXiv cs.SE 2015
Year: 2015

Both automatic program verification and program transformation are based on program analysis. In the past decade a number of approaches using various automatic general-purpose program transformation techniques (partial deduction, specialization, supercompilation) for verification of unreachability properties of computing systems were introduced and demonstrated. On the other hand, the semantics based unfold-fold program transformation methods pose themselves diverse kinds of reachability tasks and try to solve them, aiming at improving the semantics tree of the program being transformed. That means some general-purpose verification methods may be used for strengthening program transformation techniques. This paper considers the question how finite countermodels for safety verification method might be used in Turchin's supercompilation method. We extract a number of supercompilation sub-algorithms trying to solve reachability problems and demonstrate use of an external countermodel finder for solving some of the problems.
Active Sampler: Light-weight Accelerator for Complex Data Analytics at Scale
Venue: arXiv cs.DB 2015
Year: 2015

Recent years have witnessed amazing outcomes from "Big Models" trained by "Big Data". Most popular algorithms for model training are iterative. Due to the surging volumes of data, we can usually afford to process only a fraction of the training data in each iteration. Typically, the data are either uniformly sampled or sequentially accessed. In this paper, we study how the data access pattern can affect model training. We propose an Active Sampler algorithm, where training data with more "learning value" to the model are sampled more frequently. The goal is to focus training effort on valuable instances near the classification boundaries, rather than evident cases, noisy data or outliers. We show the correctness and optimality of Active Sampler in theory, and then develop a light-weight vectorized implementation. Active Sampler is orthogonal to most approaches optimizing the efficiency of large-scale data analytics, and can be applied to most analytics models trained by stochastic gradient descent (SGD) algorithm. Extensive experimental evaluations demonstrate that Active Sampler can speed up the training procedure of SVM, feature selection and deep learning, for comparable training quality by 1.6-2.2x.
Query Answering over Contextualized RDF/OWL Knowledge with Forall-Existential Bridge Rules: Decidable Finite Extension Classes (Post Print)
Venue: arXiv cs.DB 2015
Year: 2015

The proliferation of contextualized knowledge in the Semantic Web (SW) has led to the popularity of knowledge formats such as \emph{quads} in the SW community. A quad is an extension of an RDF triple with contextual information of the triple. In this paper, we study the problem of query answering over quads augmented with forall-existential bridge rules that enable interoperability of reasoning between triples in various contexts. We call a set of quads together with such expressive bridge rules, a quad-system. Query answering over quad-systems is undecidable, in general. We derive decidable classes of quad-systems, for which query answering can be done using forward chaining. Sound, complete and terminating procedures, which are adaptations of the well known chase algorithm, are provided for these classes for deciding query entailment. Safe, msafe, and csafe class of quad-systems restrict the structure of blank nodes generated during the chase computation process to be directed acyclic graphs (DAGs) of bounded depth. RR and restricted RR classes do not allow the generation of blank nodes during the chase computation process. Both data and combined complexity of query entailment has been established for the classes derived. We further show that quad-systems are equivalent to forall-existential rules whose predicates are restricted to ternary arity, modulo polynomial time translations. We subsequently show that the technique of safety, strictly subsumes in expressivity, some of the well known and expressive techniques, such as joint acyclicity and model faithful acyclicity, used for decidability guarantees in the realm of forall-existential rules.
BYOD and the Mobile Enterprise - Organisational challenges and solutions to adopt BYOD
Venue: arXiv cs.CY 2015
Year: 2015

Bring Your Own Device, also known under the term BOYD refers to the trend in employees bringing their personal mobile devices into organisations to use as a primary device for their daily work activities. With the rapid development in computing technology in smartphones and tablet computers and innovations in mobile software and applications, mobile devices are becoming ever more powerful tools for consumers to access information. Consumers are becoming more inseparable from their personal mobile devices and development in mobile technologies within the consumer space has led to the significance of Consumerization. Enterprises everywhere want to introduce BYOD strategies to improve mobility and productivity of their employees. However making the necessary organizational changes to adopt BYOD may require a shift away from centralized systems towards more open enterprise systems and this change can present challenges to enterprises in particular over security, control, technology and policy to the traditional IT model within organisations. This paper explores some of the present challenges and solutions in relation to mobile security, technology and policy that enterprise systems within organisations can encounter. This paper also reviews real-life studies where such changes were made in organisations aiming to implement BYOD. This paper proposes a mobile enterprise model that aims to address security concerns and the challenges of technology and policy change. This paper ends with looking ahead to the future of mobile enterprise systems.
A Novel Methodologyof Router-To-ASMapping inspired by Community Discovery
Venue: arXiv cs.NI 2015
Year: 2015

In the last decade many works has been done on the Internet topology at router or autonomous system (AS) level. As routers is the essential composition of ASes while ASes dominate the behavior of their routers. It is no doubt that identifying the affiliation between routers and ASes can let us gain a deeper understanding on the topology. However, the existing methods that assign a router to an AS just based on the origin ASes of its IP addresses, which does not make full use of information in our hand. In this paper, we propose a methodology to assign routers to their owner ASes based on community discovery tech. First, we use the origin ASes information along with router-pairs similarities to construct a weighted router level topology, secondly, for enormous topology data (more than 2M nodes and 19M edges) from CAIDA ITDK project, we propose a fast hierarchy clustering which time and space complex are both linear to do ASes community discovery, last we do router-to-AS mapping based on these ASes communities. Experiments show that combining with ASes communities our methodology discovers, the best accuracy rate of router-to-AS mapping can reach to 82.62%, which is drastically high comparing to prior works that stagnate on 65.44%.
The price of anarchy and stability in general noisy best-response dynamics
Venue: arXiv cs.GT 2015
Year: 2015

Logit-response dynamics (Alos-Ferrer and Netzer, Games and Economic Behavior 2010) are a rich and natural class of noisy best-response dynamics. In this work we revise the price of anarchy and the price of stability by considering the quality of long-run equilibria in these dynamics. Our results show that prior studies on simpler dynamics of this type can strongly depend on a synchronous schedule of the players' moves. In particular, a small noise by itself is not enough to improve the quality of equilibria as soon as other very natural schedules are used.
The Rationale behind the Concept of Goal
Venue: arXiv cs.LO 2015
Year: 2015

The paper proposes a fresh look at the concept of goal and advances that motivational attitudes like desire, goal and intention are just facets of the broader notion of (acceptable) outcome. We propose to encode the preferences of an agent as sequences of "alternative acceptable outcomes". We then study how the agent's beliefs and norms can be used to filter the mental attitudes out of the sequences of alternative acceptable outcomes. Finally, we formalise such intuitions in a novel Modal Defeasible Logic and we prove that the resulting formalisation is computationally feasible.
Discrete-Time Ping-pong Optimized Pulse Shaping-OFDM (POPS-OFDM) Operating on Time and Frequency Dispersive Channels for 5G Systems
Venue: arXiv cs.IT 2015
Year: 2015

The Fourth Generation (4G) of mobile communication systems was optimized to offer high data rates with high terminal mobility by ensuring strict synchronism and perfect orthogonality. However, the trend for novel applications, that had not been feasible a few years back, reveals major limits of this strict synchronism and imposes new challenges and severe requirements. But, coarse synchronization can dramatically damage the waveforms orthogonality in the Orthogonal Frequency Division Multiplexing (OFDM) signals, which results in oppressive Inter-Carrier Interference (ICI) and Inter-Symbol Interference (ISI). As a consequence, the use of non-orthogonal waveforms becomes further essential in order to meet the upcoming requirements. In this context, we propose here a novel waveform construction, referred to Ping-pong Optimized Pulse Shaping-OFDM (POPS-OFDM), which is believed to be an attractive candidate for the optimization of the radio interface of next 5G mobile communication systems. Through a maximization of the Signal to Interference plus Noise Ratio (SINR), this approach allows optimal and straightforward waveform design for multicarrier systems at the Transmitter (Tx) and Receiver (Rx) sides. In this paper, we analyze several characteristics of the proposed waveforms and shed light on relevant features, which make it a powerful candidate for the design of 5G system radio interface waveforms.
A Survey on Security in Named Data Networking
Venue: arXiv cs.NI 2015
Year: 2015

Over the past three decades, since its invention, the Internet has evolved in both its sheer volume and usage. The Internet's core protocol, Internet Protocol (IP), has proven its usability and effectiveness to support a communication network. However, current Internet usage requires more than a communication network due to a shift in the nature of Internet applications from simple email application to large content producers such as NetFlix, Google, Amazon, etc. Named Data Networking (NDN) is one of the few initiatives/projects addressing the shortcomings of the current Internet architecture and intends to move the Internet toward a content distribution architecture. In this paper, we conduct a brief survey of security topics/problems inherent to the NDN architecture. Specifically, we describe current known problems and propose solutions to major security problems.
Evaluation of Pose Tracking Accuracy in the First and Second Generations of Microsoft Kinect
Venue: arXiv cs.CV 2015
Year: 2015

Microsoft Kinect camera and its skeletal tracking capabilities have been embraced by many researchers and commercial developers in various applications of real-time human movement analysis. In this paper, we evaluate the accuracy of the human kinematic motion data in the first and second generation of the Kinect system, and compare the results with an optical motion capture system. We collected motion data in 12 exercises for 10 different subjects and from three different viewpoints. We report on the accuracy of the joint localization and bone length estimation of Kinect skeletons in comparison to the motion capture. We also analyze the distribution of the joint localization offsets by fitting a mixture of Gaussian and uniform distribution models to determine the outliers in the Kinect motion data. Our analysis shows that overall Kinect 2 has more robust and more accurate tracking of human pose as compared to Kinect 1.
Inside-Outside Net: Detecting Objects in Context with Skip Pooling and Recurrent Neural Networks
Venue: arXiv cs.CV 2015
Year: 2015

It is well known that contextual and multi-scale representations are important for accurate visual recognition. In this paper we present the Inside-Outside Net (ION), an object detector that exploits information both inside and outside the region of interest. Contextual information outside the region of interest is integrated using spatial recurrent neural networks. Inside, we use skip pooling to extract information at multiple scales and levels of abstraction. Through extensive experiments we evaluate the design space and provide readers with an overview of what tricks of the trade are important. ION improves state-of-the-art on PASCAL VOC 2012 object detection from 73.9% to 76.4% mAP. On the new and more challenging MS COCO dataset, we improve state-of-art-the from 19.7% to 33.1% mAP. In the 2015 MS COCO Detection Challenge, our ION model won the Best Student Entry and finished 3rd place overall. As intuition suggests, our detection results provide strong evidence that context and multi-scale representations improve small object detection.
Recursion-based Analysis for Information Propagation in Vehicular Ad Hoc Networks
Venue: arXiv cs.NI 2015
Year: 2015

Effective inter-vehicle communication is fundamental to a decentralized traffic information system based on Vehicular Ad Hoc Networks (VANETs). To reflect the uncertainty of the information propagation, most of the existing work was conducted by assuming the inter-vehicle distance follows some specific probability models, e.g., the lognormal or exponential distribution, while reducing the analysis complexity. Aimed at providing more generic results, a recursive modeling framework is proposed for VANETs in this paper when the vehicle spacing can be captured by a general i.i.d. distribution. With the framework, the analytical expressions for a series of commonly discussed metrics are derived respectively, including the mean, variance, probability distribution of the propagation distance, and expectation for the number of vehicles included in a propagation process, when the transmission failures are mainly caused by MAC contentions. Moreover, a discussion is also made for demonstrating the efficiency of the recursive analysis method when the impact of channel fading is also considered. All the analytical results are verified by extensive simulations. We believe that this work is able to potentially reveal a more insightful understanding of information propagation in VANETs by allowing to evaluate the effect of any vehicle headway distributions.
Trigonometric dictionary based codec for music compression with high quality recovery
Venue: arXiv cs.SD 2015
Year: 2015

A codec for compression of music signals is proposed. The method belongs to the class of transform lossy compression. It is conceived to be applied in the high quality recovery range though. The transformation, endowing the codec with its distinctive feature, relies on the ability to construct high quality sparse approximation of music signals. This is achieved by a redundant trigonometric dictionary and a dedicated pursuit strategy. The potential of the approach is illustrated by comparison with the OGG Vorbis format, on a sample consisting of clips of melodic music. The comparison evidences remarkable improvements in compression performance for the identical quality of the decompressed signal.
An Event Calculus Production Rule System for Reasoning in Dynamic and Uncertain Domains
Venue: arXiv cs.AI 2015
Year: 2015

Action languages have emerged as an important field of Knowledge Representation for reasoning about change and causality in dynamic domains. This article presents Cerbere, a production system designed to perform online causal, temporal and epistemic reasoning based on the Event Calculus. The framework implements the declarative semantics of the underlying logic theories in a forward-chaining rule-based reasoning system, coupling the high expressiveness of its formalisms with the efficiency of rule-based systems. To illustrate its applicability, we present both the modeling of benchmark problems in the field, as well as its utilization in the challenging domain of smart spaces. A hybrid framework that combines logic-based with probabilistic reasoning has been developed, that aims to accommodate activity recognition and monitoring tasks in smart spaces. Under consideration in Theory and Practice of Logic Programming (TPLP)
Memory-based control with recurrent neural networks
Venue: arXiv cs.LG 2015
Year: 2015

Partially observed control problems are a challenging aspect of reinforcement learning. We extend two related, model-free algorithms for continuous control -- deterministic policy gradient and stochastic value gradient -- to solve partially observed domains using recurrent neural networks trained with backpropagation through time. We demonstrate that this approach, coupled with long-short term memory is able to solve a variety of physical control problems exhibiting an assortment of memory requirements. These include the short-term integration of information from noisy sensors and the identification of system parameters, as well as long-term memory problems that require preserving information over many time steps. We also demonstrate success on a combined exploration and memory problem in the form of a simplified version of the well-known Morris water maze task. Finally, we show that our approach can deal with high-dimensional observations by learning directly from pixels. We find that recurrent deterministic and stochastic policies are able to learn similarly good solutions to these tasks, including the water maze where the agent must learn effective search strategies.
Semisupervised Autoencoder for Sentiment Analysis
Venue: arXiv cs.LG 2015
Year: 2015

In this paper, we investigate the usage of autoencoders in modeling textual data. Traditional autoencoders suffer from at least two aspects: scalability with the high dimensionality of vocabulary size and dealing with task-irrelevant words. We address this problem by introducing supervision via the loss function of autoencoders. In particular, we first train a linear classifier on the labeled data, then define a loss for the autoencoder with the weights learned from the linear classifier. To reduce the bias brought by one single classifier, we define a posterior probability distribution on the weights of the classifier, and derive the marginalized loss of the autoencoder with Laplace approximation. We show that our choice of loss function can be rationalized from the perspective of Bregman Divergence, which justifies the soundness of our model. We evaluate the effectiveness of our model on six sentiment analysis datasets, and show that our model significantly outperforms all the competing methods with respect to classification accuracy. We also show that our model is able to take advantage of unlabeled dataset and get improved performance. We further show that our model successfully learns highly discriminative feature maps, which explains its superior performance.
An Example for BeSpaceD and its Use for Decision Support in Industrial Automation
Venue: arXiv cs.SE 2015
Year: 2015

We describe our formal methods-based spatial reasoning framework BeSpaceD and its application in decision support for industrial automation. In particular we are supporting analysis and decisions based on formal models for industrial plant and mining operations. BeSpaceD is a framework for deciding geometric and topological properties of spatio-temporal models. We present an example and report on our ongoing experience with applications in different projects around software and cyber-physical systems engineering. The example features abstracted aspects of a production plant model. Using the example we motivate the use of our framework in the context of an existing software platform supporting monitoring, incident handling and maintenance of industrial automation facilities in remote locations.
Robust Group Sparse Beamforming for Multicast Green Cloud-RAN with Imperfect CSI
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we investigate the network power minimization problem for the multicast cloud radio access network (Cloud-RAN) with imperfect channel state information (CSI). The key observation is that network power minimization can be achieved by adaptively selecting active remote radio heads (RRHs) via controlling the group-sparsity structure of the beamforming vector. However, this yields a non-convex combinatorial optimization problem, for which we propose a three-stage robust group sparse beamforming algorithm. In the first stage, a quadratic variational formulation of the weighted mixed l1/l2-norm is proposed to induce the group-sparsity structure in the aggregated beamforming vector, which indicates those RRHs that can be switched off. A perturbed alternating optimization algorithm is then proposed to solve the resultant non-convex group-sparsity inducing optimization problem by exploiting its convex substructures. In the second stage, we propose a PhaseLift technique based algorithm to solve the feasibility problem with a given active RRH set, which helps determine the active RRHs. Finally, the semidefinite relaxation (SDR) technique is adopted to determine the robust multicast beamformers. Simulation results will demonstrate the convergence of the perturbed alternating optimization algorithm, as well as, the effectiveness of the proposed algorithm to minimize the network power consumption for multicast Cloud-RAN.
Tight Bounds for Distributed Minimum-Weight Spanning Tree Verification
Venue: arXiv cs.DC 2015
Year: 2015

This paper introduces the notion of distributed verification without preprocessing. It focuses on the Minimum-weight Spanning Tree (MST) verification problem and establishes tight upper and lower bounds for the time and message complexities of this problem. Specifically, we provide an MST verification algorithm that achieves simultaneously O(m) messages and O($\sqrt$ n+D) time, where m is the number of edges in the given graph G, n is the number of nodes, and D is G's diameter. On the other hand, we show that any MST verification algorithm must send Ω(m) messages and incur Ω($\sqrt$ n + D) time in worst case. Our upper bound result appears to indicate that the verification of an MST may be easier than its construction, since for MST construction, both lower bounds of Ω(m) messages and Ω($\sqrt$ n+D time hold, but at the moment there is no known distributed algorithm that constructs an MST and achieves simultaneously O(m) messages and O($\sqrt$ n + D) time. Specifically, the best known time-optimal algorithm (using O($\sqrt$ n + D) time) requires O(m + n 3/2) messages, and the best known message-optimal algorithm (using O(m) messages) requires O(n) time. On the other hand, our lower bound results indicate that the verification of an MST is not significantly easier than its construction.
Strategies for Training Large Vocabulary Neural Language Models
Venue: arXiv cs.CL 2015
Year: 2015

Training neural network language models over large vocabularies is still computationally very costly compared to count-based models such as Kneser-Ney. At the same time, neural language models are gaining popularity for many applications such as speech recognition and machine translation whose success depends on scalability. We present a systematic comparison of strategies to represent and train large vocabularies, including softmax, hierarchical softmax, target sampling, noise contrastive estimation and self normalization. We further extend self normalization to be a proper estimator of likelihood and introduce an efficient variant of softmax. We evaluate each method on three popular benchmarks, examining performance on rare words, the speed/accuracy trade-off and complementarity to Kneser-Ney.