OpenRaiser/Intern-Atlas huggingface dataset:
Valorising the IoT Databox: Creating Value for Everyone
Venue: arXiv cs.CY 2016
Year: 2016

The Internet of Things (IoT) is expected to generate large amounts of heterogeneous data from diverse sources including physical sensors, user devices, and social media platforms. Over the last few years, significant attention has been focused on personal data, particularly data generated by smart wearable and smart home devices. Making personal data available for access and trade is expected to become a part of the data driven digital economy. In this position paper, we review the research challenges in building personal Databoxes that hold personal data and enable data access by other parties, and potentially thus sharing of data with other parties. These Databoxes are expected to become a core part of future data marketplaces.
SecComp: Towards Practically Defending Against Component Hijacking in Android Applications
Venue: arXiv cs.CR 2016
Year: 2016

Cross-app collaboration via inter-component communication is a fundamental mechanism on Android. Although it brings the benefits such as functionality reuse and data sharing, a threat called component hijacking is also introduced. By hijacking a vulnerable component in victim apps, an attack app can escalate its privilege for originally prohibited operations. Many prior studies have been performed to understand and mitigate this issue, but component hijacking remains a serious open problem in the Android ecosystem due to no effective defense deployed in the wild. In this paper, we present our vision on practically defending against component hijacking in Android apps. First, we argue that to fundamentally prevent component hijacking, we need to switch from the previous mindset (i.e., performing system-level control or repackaging vulnerable apps after they are already released) to a more proactive version that aims to help security-inexperienced developers make secure components in the first place. To this end, we propose to embed into apps a secure component library (SecComp), which performs in-app mandatory access control on behalf of app components. An important factor for SecComp to be effective is that we find it is possible to devise a set of practical in-app policies to stop component hijacking. Furthermore, we allow developers design custom policies, beyond our by-default generic policies, to support more fine-grained access control. We have overcome challenges to implement a preliminary SecComp prototype, which stops component hijacking with very low performance overhead. We hope the future research that fully implements our vision can eventually help real-world apps get rid of component hijacking.
Morphological Constraints for Phrase Pivot Statistical Machine Translation
Venue: arXiv cs.CL 2016
Year: 2016

The lack of parallel data for many language pairs is an important challenge to statistical machine translation (SMT). One common solution is to pivot through a third language for which there exist parallel corpora with the source and target languages. Although pivoting is a robust technique, it introduces some low quality translations especially when a poor morphology language is used as the pivot between rich morphology languages. In this paper, we examine the use of synchronous morphology constraint features to improve the quality of phrase pivot SMT. We compare hand-crafted constraints to those learned from limited parallel data between source and target languages. The learned morphology constraints are based on projected align- ments between the source and target phrases in the pivot phrase table. We show positive results on Hebrew-Arabic SMT (pivoting on English). We get 1.5 BLEU points over a phrase pivot baseline and 0.8 BLEU points over a system combination baseline with a direct model built from parallel data.
Transfer String Kernel for Cross-Context DNA-Protein Binding Prediction
Venue: arXiv cs.LG 2016
Year: 2016

Through sequence-based classification, this paper tries to accurately predict the DNA binding sites of transcription factors (TFs) in an unannotated cellular context. Related methods in the literature fail to perform such predictions accurately, since they do not consider sample distribution shift of sequence segments from an annotated (source) context to an unannotated (target) context. We, therefore, propose a method called "Transfer String Kernel" (TSK) that achieves improved prediction of transcription factor binding site (TFBS) using knowledge transfer via cross-context sample adaptation. TSK maps sequence segments to a high-dimensional feature space using a discriminative mismatch string kernel framework. In this high-dimensional space, labeled examples of the source context are re-weighted so that the revised sample distribution matches the target context more closely. We have experimentally verified TSK for TFBS identifications on fourteen different TFs under a cross-organism setting. We find that TSK consistently outperforms the state-of the-art TFBS tools, especially when working with TFs whose binding sequences are not conserved across contexts. We also demonstrate the generalizability of TSK by showing its cutting-edge performance on a different set of cross-context tasks for the MHC peptide binding predictions.
Compiling Process Networks to Interaction Nets
Venue: arXiv cs.PL 2016
Year: 2016

Kahn process networks are a model of computation based on a collection of sequential, deterministic processes that communicate by sending messages through unbounded channels. They are well suited for modelling stream-based computations, but are in no way restricted to this application. Interaction nets are graph rewriting systems that have many interesting properties for implementation. In this paper we show how to encode process networks using interaction nets, where we model both networks and messages in the same framework.
A Greedy Algorithm to Cluster Specialists
Venue: arXiv cs.LG 2016
Year: 2016

Several recent deep neural networks experiments leverage the generalist-specialist paradigm for classification. However, no formal study compared the performance of different clustering algorithms for class assignment. In this paper we perform such a study, suggest slight modifications to the clustering procedures, and propose a novel algorithm designed to optimize the performance of of the specialist-generalist classification system. Our experiments on the CIFAR-10 and CIFAR-100 datasets allow us to investigate situations for varying number of classes on similar data. We find that our \emph{greedy pairs} clustering algorithm consistently outperforms other alternatives, while the choice of the confusion matrix has little impact on the final performance.
Graph Aggregation
Venue: arXiv cs.AI 2016
Year: 2016

Graph aggregation is the process of computing a single output graph that constitutes a good compromise between several input graphs, each provided by a different source. One needs to perform graph aggregation in a wide variety of situations, e.g., when applying a voting rule (graphs as preference orders), when consolidating conflicting views regarding the relationships between arguments in a debate (graphs as abstract argumentation frameworks), or when computing a consensus between several alternative clusterings of a given dataset (graphs as equivalence relations). In this paper, we introduce a formal framework for graph aggregation grounded in social choice theory. Our focus is on understanding which properties shared by the individual input graphs will transfer to the output graph returned by a given aggregation rule. We consider both common properties of graphs, such as transitivity and reflexivity, and arbitrary properties expressible in certain fragments of modal logic. Our results establish several connections between the types of properties preserved under aggregation and the choice-theoretic axioms satisfied by the rules used. The most important of these results is a powerful impossibility theorem that generalises Arrow's seminal result for the aggregation of preference orders to a large collection of different types of graphs.
Quantitative identification of technological discontinuities using simulation modeling
Venue: arXiv cs.DL 2016
Year: 2016

The aim of this paper is to develop and test metrics to quantitatively identify technological discontinuities in a knowledge network. We developed five metrics based on innovation theories and tested the metrics by a simulation model-based knowledge network and hypothetically designed discontinuity. The designed discontinuity is modeled as a node which combines two different knowledge streams and whose knowledge is dominantly persistent in the knowledge network. The performances of the proposed metrics were evaluated by how well the metrics can distinguish the designed discontinuity from other nodes on the knowledge network. The simulation results show that the persistence times # of converging main paths provides the best performance in identifying the designed discontinuity: the designed discontinuity was identified as one of the top 3 patents with 96~99% probability by Metric 5 and it is, according to the size of a domain, 12~34% better than the performance of the second best metric. Beyond the simulation analysis, we tested the metrics using a patent set representative of the Magnetic information storage domain. The three representative patents associated with a well-known breakthrough technology in the domain, the giant magneto-resistance (GMR) spin valve sensor, were selected based on the qualitative studies, and the metrics were tested by how well the metrics identify the selected patents as top-ranked patents. The empirical results fully support the simulation results and therefore the persistence times # of converging main paths is recommended for identifying technological discontinuities for any technology.
VIPLFaceNet: An Open Source Deep Face Recognition SDK
Venue: arXiv cs.CV 2016
Year: 2016

Robust face representation is imperative to highly accurate face recognition. In this work, we propose an open source face recognition method with deep representation named as VIPLFaceNet, which is a 10-layer deep convolutional neural network with 7 convolutional layers and 3 fully-connected layers. Compared with the well-known AlexNet, our VIPLFaceNet takes only 20% training time and 60% testing time, but achieves 40\% drop in error rate on the real-world face recognition benchmark LFW. Our VIPLFaceNet achieves 98.60% mean accuracy on LFW using one single network. An open-source C++ SDK based on VIPLFaceNet is released under BSD license. The SDK takes about 150ms to process one face image in a single thread on an i7 desktop CPU. VIPLFaceNet provides a state-of-the-art start point for both academic and industrial face recognition applications.
Distributed Algorithms for Peak Ramp Minimization Problem in Smart Grid
Venue: arXiv cs.SY 2016
Year: 2016

The arrival of small-scale distributed energy generation in the future smart grid has led to the emergence of so-called prosumers, who can both consume as well as produce energy. By using local generation from renewable energy resources, the stress on power generation and supply system can be significantly reduced during high demand periods. However, this also creates a significant challenge for conventional power plants that suddenly need to ramp up quickly when the renewable energy drops off. In this paper, we propose an energy consumption scheduling problem for prosumers to minimize the peak ramp of the system. The optimal schedule of prosumers can be obtained by solving the centralized optimization problem. However, due to the privacy concerns and the distributed topology of the power system, the centralized design is difficult to implement in practice. Therefore, we propose the distributed algorithms to efficiently solve the centralized problem using the alternating direction method of multiplier (ADMM), in which each prosumer independently schedules its energy consumption profile. The simulation results demonstrate the convergence performance of the proposed algorithms as well as the capability of our model in reducing the peak ramp of the system.
Single-image RGB Photometric Stereo With Spatially-varying Albedo
Venue: arXiv cs.CV 2016
Year: 2016

We present a single-shot system to recover surface geometry of objects with spatially-varying albedos, from images captured under a calibrated RGB photometric stereo setup---with three light directions multiplexed across different color channels in the observed RGB image. Since the problem is ill-posed point-wise, we assume that the albedo map can be modeled as piece-wise constant with a restricted number of distinct albedo values. We show that under ideal conditions, the shape of a non-degenerate local constant albedo surface patch can theoretically be recovered exactly. Moreover, we present a practical and efficient algorithm that uses this model to robustly recover shape from real images. Our method first reasons about shape locally in a dense set of patches in the observed image, producing shape distributions for every patch. These local distributions are then combined to produce a single consistent surface normal map. We demonstrate the efficacy of the approach through experiments on both synthetic renderings as well as real captured images.
A Delayed Promotion Policy for Parity Games
Venue: arXiv cs.GT 2016
Year: 2016

Parity games are two-player infinite-duration games on graphs that play a crucial role in various fields of theoretical computer science. Finding efficient algorithms to solve these games in practice is widely acknowledged as a core problem in formal verification, as it leads to efficient solutions of the model-checking and satisfiability problems of expressive temporal logics, e.g., the modal muCalculus. Their solution can be reduced to the problem of identifying sets of positions of the game, called dominions, in each of which a player can force a win by remaining in the set forever. Recently, a novel technique to compute dominions, called priority promotion, has been proposed, which is based on the notions of quasi dominion, a relaxed form of dominion, and dominion space. The underlying framework is general enough to accommodate different instantiations of the solution procedure, whose correctness is ensured by the nature of the space itself. In this paper we propose a new such instantiation, called delayed promotion, that tries to reduce the possible exponential behaviours exhibited by the original method in the worst case. The resulting procedure not only often outperforms the original priority promotion approach, but so far no exponential worst case is known.
Games for Topological Fixpoint Logic
Venue: arXiv cs.LO 2016
Year: 2016

Topological fixpoint logics are a family of logics that admits topological models and where the fixpoint operators are defined with respect to the topological interpretations. Here we consider a topological fixpoint logic for relational structures based on Stone spaces, where the fixpoint operators are interpreted via clopen sets. We develop a game-theoretic semantics for this logic. First we introduce games characterising clopen fixpoints of monotone operators on Stone spaces. These fixpoint games allow us to characterise the semantics for our topological fixpoint logic using a two-player graph game. Adequacy of this game is the main result of our paper. Finally, we define bisimulations for the topological structures under consideration and use our game semantics to prove that the truth of a formula of our topological fixpoint logic is bisimulation-invariant.
Alternation Is Strict For Higher-Order Modal Fixpoint Logic
Venue: arXiv cs.LO 2016
Year: 2016

We study the expressive power of Alternating Parity Krivine Automata (APKA), which provide operational semantics to Higher-Order Modal Fixpoint Logic (HFL). APKA consist of ordinary parity automata extended by a variation of the Krivine Abstract Machine. We show that the number and parity of priorities available to an APKA form a proper hierarchy of expressive power as in the modal mu-calculus. This also induces a strict alternation hierarchy on HFL. The proof follows Arnold's (1999) encoding of runs into trees and subsequent use of the Banach Fixpoint Theorem.
Cycle Detection in Computation Tree Logic
Venue: arXiv cs.LO 2016
Year: 2016

Temporal logic is a very powerful formalism deeply investigated and used in formal system design and verification. Its application usually reduces to solving specific decision problems such as model checking and satisfiability. In these kind of problems, the solution often requires detecting some specific properties over cycles. For instance, this happens when using classic techniques based on automata, game-theory, SCC decomposition, and the like. Surprisingly, no temporal logics have been considered so far with the explicit ability of talking about cycles. In this paper we introduce Cycle-CTL*, an extension of the classical branching-time temporal logic CTL* along with cycle quantifications in order to predicate over cycles. This logic turns out to be very expressive. Indeed, we prove that it strictly extends CTL* and is orthogonal to mu-calculus. We also give an evidence of its usefulness by providing few examples involving non-regular properties. We investigate the model checking problem for Cycle-CTL* and show that it is PSPACE-Complete as for CTL*. We also study the satisfiability problem for the existential-cycle fragment of the logic and show that it is solvable in 2ExpTime. This result makes use of an automata-theoretic approach along with novel ad-hoc definitions of bisimulation and tree-like unwinding.
Certification of Prefixed Tableau Proofs for Modal Logic
Venue: arXiv cs.LO 2016
Year: 2016

Different theorem provers tend to produce proof objects in different formats and this is especially the case for modal logics, where several deductive formalisms (and provers based on them) have been presented. This work falls within the general project of establishing a common specification language in order to certify proofs given in a wide range of deductive formalisms. In particular, by using a translation from the modal language into a first-order polarized language and a checker whose small kernel is based on a classical focused sequent calculus, we are able to certify modal proofs given in labeled sequent calculi, prefixed tableaux and free-variable prefixed tableaux. We describe the general method for the logic K, present its implementation in a prolog-like language, provide some examples and discuss how to extend the approach to other normal modal logics
ADWISERv2: A Plug-and-play Controller for Managing TCP Transfers in IEEE~802.11 Infrastructure WLANs with Multiple Access Points
Venue: arXiv cs.NI 2016
Year: 2016

In this paper, we present a generic plug-and-play controller that ensures fair and efficient operation of IEEE~802.11 infrastructure wireless local area networks with multiple co-channel access points, without any change to hardware/firmware of the network devices. Our controller addresses performance issues of TCP transfers in multi-AP WLANs, by overlaying a coarse time-slicing scheduler on top of a cascaded fair queuing scheduler. The time slices and queue weights, used in our controller, are obtained from the solution of a constrained utility optimization formulation. A study of the impact of coarse time-slicing on TCP is also presented in this paper. We present an improved algorithm for adaptation of the service rate of the fair queuing scheduler and provide experimental results to illustrate its efficacy. We also present the changes that need to be incorporated to the proposed approach, to handle short-lived and interactive TCP flows. Finally, we report the results of experiments performed on a real testbed, demonstrating the efficacy of our controller.
Quick and energy-efficient Bayesian computing of binocular disparity using stochastic digital signals
Venue: arXiv cs.CV 2016
Year: 2016

Reconstruction of the tridimensional geometry of a visual scene using the binocular disparity information is an important issue in computer vision and mobile robotics, which can be formulated as a Bayesian inference problem. However, computation of the full disparity distribution with an advanced Bayesian model is usually an intractable problem, and proves computationally challenging even with a simple model. In this paper, we show how probabilistic hardware using distributed memory and alternate representation of data as stochastic bitstreams can solve that problem with high performance and energy efficiency. We put forward a way to express discrete probability distributions using stochastic data representations and perform Bayesian fusion using those representations, and show how that approach can be applied to diparity computation. We evaluate the system using a simulated stochastic implementation and discuss possible hardware implementations of such architectures and their potential for sensorimotor processing and robotics.
3D Face Reconstruction by Learning from Synthetic Data
Venue: arXiv cs.CV 2016
Year: 2016

Fast and robust three-dimensional reconstruction of facial geometric structure from a single image is a challenging task with numerous applications. Here, we introduce a learning-based approach for reconstructing a three-dimensional face from a single image. Recent face recovery methods rely on accurate localization of key characteristic points. In contrast, the proposed approach is based on a Convolutional-Neural-Network (CNN) which extracts the face geometry directly from its image. Although such deep architectures outperform other models in complex computer vision problems, training them properly requires a large dataset of annotated examples. In the case of three-dimensional faces, currently, there are no large volume data sets, while acquiring such big-data is a tedious task. As an alternative, we propose to generate random, yet nearly photo-realistic, facial images for which the geometric form is known. The suggested model successfully recovers facial shapes from real images, even for faces with extreme expressions and under various lighting conditions.
An Adaptive Psychoacoustic Model for Automatic Speech Recognition
Venue: arXiv cs.CL 2016
Year: 2016

Compared with automatic speech recognition (ASR), the human auditory system is more adept at handling noise-adverse situations, including environmental noise and channel distortion. To mimic this adeptness, auditory models have been widely incorporated in ASR systems to improve their robustness. This paper proposes a novel auditory model which incorporates psychoacoustics and otoacoustic emissions (OAEs) into ASR. In particular, we successfully implement the frequency-dependent property of psychoacoustic models and effectively improve resulting system performance. We also present a novel double-transform spectrum-analysis technique, which can qualitatively predict ASR performance for different noise types. Detailed theoretical analysis is provided to show the effectiveness of the proposed algorithm. Experiments are carried out on the AURORA2 database and show that the word recognition rate using our proposed feature extraction method is significantly increased over the baseline. Given models trained with clean speech, our proposed method achieves up to 85.39% word recognition accuracy on noisy data.