OpenRaiser/Intern-Atlas huggingface dataset:
Games for Bisimulations and Abstraction
Venue: arXiv cs.LO 2017
Year: 2017

Weak bisimulations are typically used in process algebras where silent steps are used to abstract from internal behaviours. They facilitate relating implementations to specifications. When an implementation fails to conform to its specification, pinpointing the root cause can be challenging. In this paper we provide a generic characterisation of branching-, delayed-, $η$- and weak-bisimulation as a game between Spoiler and Duplicator, offering an operational understanding of the relations. We show how such games can be used to assist in diagnosing non-conformance between implementation and specification. Moreover, we show how these games can be extended to distinguish divergences.
Directional Training and Fast Sector-based Processing Schemes for mmWave Channels
Venue: arXiv cs.IT 2017
Year: 2017

We consider a single-cell scenario involving a single base station (BS) with a massive array serving multi-antenna terminals in the downlink of a mmWave channel. We present a class of multiuser user MIMO schemes, which rely on uplink training from the user terminals, and on uplink/downlink channel reciprocity. The BS employs virtual sector-based processing according to which, user-channel estimation and data transmission are performed in parallel over non-overlapping angular sectors. The uplink training schemes we consider are non-orthogonal, that is, we allow multiple users to transmit pilots on the same pilot dimension (thereby potentially interfering with one another). Elementary processing allows each sector to determine the subset of user channels that can be resolved on the sector (effectively pilot contamination free) and, thus, the subset of users that can be served by the sector. This allows resolving multiple users on the same pilot dimension at different sectors, thereby increasing the overall multiplexing gains of the system. Our analysis and simulations reveal that, by using appropriately designed directional training beams at the user terminals, the sector-based transmission schemes we present can yield substantial spatial multiplexing and ergodic user-rates improvements with respect to their orthogonal-training counterparts.
On the Compositionality of Quantitative Information Flow
Venue: arXiv cs.LO 2017
Year: 2017

Information flow is the branch of security that studies the leakage of information due to correlation between secrets and observables. Since in general such correlation cannot be avoided completely, it is important to quantify the leakage. The most followed approaches to defining appropriate measures are those based on information theory. In particular, one of the most successful approaches is the recently proposed $g$-leakage framework, which encompasses most of the information-theoretic ones. A problem with $g$-leakage, however, is that it is defined in terms of a minimization problem, which, in the case of large systems, can be computationally rather heavy. In this paper we study the case in which the channel associated to the system can be decomposed into simpler channels, which typically happens when the observables consist of multiple components. Our main contribution is the derivation of bounds on the (multiplicative version of) $g$-leakage of the whole system in terms of the $g$-leakages of its components. We also consider the particular cases of min-entropy leakage and of parallel channels, generalizing and systematizing results from the literature. We demonstrate the effectiveness of our method and evaluate the precision of our bounds using examples.
A Memory Bandwidth-Efficient Hybrid Radix Sort on GPUs
Venue: arXiv cs.DB 2017
Year: 2017

Sorting is at the core of many database operations, such as index creation, sort-merge joins, and user-requested output sorting. As GPUs are emerging as a promising platform to accelerate various operations, sorting on GPUs becomes a viable endeavour. Over the past few years, several improvements have been proposed for sorting on GPUs, leading to the first radix sort implementations that achieve a sorting rate of over one billion 32-bit keys per second. Yet, state-of-the-art approaches are heavily memory bandwidth-bound, as they require substantially more memory transfers than their CPU-based counterparts. Our work proposes a novel approach that almost halves the amount of memory transfers and, therefore, considerably lifts the memory bandwidth limitation. Being able to sort two gigabytes of eight-byte records in as little as 50 milliseconds, our approach achieves a 2.32-fold improvement over the state-of-the-art GPU-based radix sort for uniform distributions, sustaining a minimum speed-up of no less than a factor of 1.66 for skewed distributions. To address inputs that either do not reside on the GPU or exceed the available device memory, we build on our efficient GPU sorting approach with a pipelined heterogeneous sorting algorithm that mitigates the overhead associated with PCIe data transfers. Comparing the end-to-end sorting performance to the state-of-the-art CPU-based radix sort running 16 threads, our heterogeneous approach achieves a 2.06-fold and a 1.53-fold improvement for sorting 64 GB key-value pairs with a skewed and a uniform distribution, respectively.
Multiple-Speaker Localization Based on Direct-Path Features and Likelihood Maximization with Spatial Sparsity Regularization
Venue: arXiv cs.SD 2017
Year: 2017

This paper addresses the problem of multiple-speaker localization in noisy and reverberant environments, using binaural recordings of an acoustic scene. A Gaussian mixture model (GMM) is adopted, whose components correspond to all the possible candidate source locations defined on a grid. After optimizing the GMM-based objective function, given an observed set of binaural features, both the number of sources and their locations are estimated by selecting the GMM components with the largest priors. This is achieved by enforcing a sparse solution, thus favoring a small number of speakers with respect to the large number of initial candidate source locations. An entropy-based penalty term is added to the likelihood, thus imposing sparsity over the set of GMM priors. In addition, the direct-path relative transfer function (DP-RTF) is used to build robust binaural features. The DP-RTF, recently proposed for single-source localization, was shown to be robust to reverberations, since it encodes inter-channel information corresponding to the direct-path of sound propagation. In this paper, we extend the DP-RTF estimation to the case of multiple sources. In the short-time Fourier transform domain, a consistency test is proposed to check whether a set of consecutive frames is associated to the same source or not. Reliable DP-RTF features are selected from the frames that pass the consistency test to be used for source localization. Experiments carried out using both simulation data and real data gathered with a robotic head confirm the efficiency of the proposed multi-source localization method.
Capacity-Achieving Rate-Compatible Polar Codes for General Channels
Venue: arXiv cs.IT 2017
Year: 2017

We present a rate-compatible polar coding scheme that achieves the capacity of any family of channels. Our solution generalizes the previous results [1], [2] that provide capacity-achieving rate-compatible polar codes for a degraded family of channels. The motivation for our extension comes from the fact that in many practical scenarios, e.g., MIMO systems and non-Gaussian interference, the channels cannot be ordered by degradation. The main technical contribution of this paper consists in removing the degradation condition. To do so, we exploit the ideas coming from the construction of universal polar codes. Our scheme possesses the usual attractive features of polar codes: low complexity code construction, encoding, and decoding; super-polynomial scaling of the error probability with the block length; and absence of error floors. On the negative side, the scaling of the gap to capacity with the block length is slower than in standard polar codes, and we prove an upper bound on the scaling exponent.
Feasible Interpolation for QBF Resolution Calculi
Venue: arXiv cs.CC 2017
Year: 2017

In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or expansion-based solving. This both provides the first general lower bound method for QBF proof systems as well as largely extends the scope of classical feasible interpolation. We apply our technique to obtain new exponential lower bounds to all resolution-based QBF systems for a new class of QBF formulas based on the clique problem. Finally, we show how feasible interpolation relates to the recently established lower bound method based on strategy extraction.
Hierarchical Overlapping Clustering of Network Data Using Cut Metrics
Venue: arXiv cs.SI 2017
Year: 2017

A novel method to obtain hierarchical and overlapping clusters from network data -i.e., a set of nodes endowed with pairwise dissimilarities- is presented. The introduced method is hierarchical in the sense that it outputs a nested collection of groupings of the node set depending on the resolution or degree of similarity desired, and it is overlapping since it allows nodes to belong to more than one group. Our construction is rooted on the facts that a hierarchical (non-overlapping) clustering of a network can be equivalently represented by a finite ultrametric space and that a convex combination of ultrametrics results in a cut metric. By applying a hierarchical (non-overlapping) clustering method to multiple dithered versions of a given network and then convexly combining the resulting ultrametrics, we obtain a cut metric associated to the network of interest. We then show how to extract a hierarchical overlapping clustering structure from the aforementioned cut metric. Furthermore, the so-called overlapping function is presented as a tool for gaining insights about the data by identifying meaningful resolutions of the obtained hierarchical structure. Additionally, we explore hierarchical overlapping quasi-clustering methods that preserve the asymmetry of the data contained in directed networks. Finally, the presented method is illustrated via synthetic and real-world classification problems including handwritten digit classification and authorship attribution of famous plays.
Flat ORAM: A Simplified Write-Only Oblivious RAM Construction for Secure Processors
Venue: arXiv cs.AR 2017
Year: 2017

Oblivious RAM (ORAM) is a cryptographic primitive which obfuscates the access patterns to a storage thereby preventing privacy leakage. So far in the current literature, only `fully functional' ORAMs are widely studied which can protect, at a cost of considerable performance penalty, against the strong adversaries who can monitor all read and write operations. However, recent research has shown that information can still be leaked even if only the write access pattern (not reads) is visible to the adversary. For such weaker adversaries, a fully functional ORAM turns out to be an overkill causing unnecessary overheads. Instead, a simple `write-only' ORAM is sufficient, and, more interestingly, is preferred as it can offer far more performance and energy efficiency than a fully functional ORAM. In this work, we present Flat ORAM: an efficient write-only ORAM scheme which outperforms the closest existing write-only ORAM called HIVE. HIVE suffers from performance bottlenecks while managing the memory occupancy information vital for correctness of the protocol. Flat ORAM resolves these bottlenecks by introducing a simple idea of Occupancy Map (OccMap) which efficiently manages the memory occupancy information resulting in far better performance. Our simulation results show that, on average, Flat ORAM only incurs a moderate slowdown of $3\times$ over the insecure DRAM for memory intensive benchmarks among Splash2 and $1.6\times$ for SPEC06. Compared to HIVE, Flat ORAM offers $50\%$ performance gain on average and up to $80\%$ energy savings.
Crowd Guilds: Worker-led Reputation and Feedback on Crowdsourcing Platforms
Venue: arXiv cs.HC 2017
Year: 2017

Crowd workers are distributed and decentralized. While decentralization is designed to utilize independent judgment to promote high-quality results, it paradoxically undercuts behaviors and institutions that are critical to high-quality work. Reputation is one central example: crowdsourcing systems depend on reputation scores from decentralized workers and requesters, but these scores are notoriously inflated and uninformative. In this paper, we draw inspiration from historical worker guilds (e.g., in the silk trade) to design and implement crowd guilds: centralized groups of crowd workers who collectively certify each other's quality through double-blind peer assessment. A two-week field experiment compared crowd guilds to a traditional decentralized crowd work model. Crowd guilds produced reputation signals more strongly correlated with ground-truth worker quality than signals available on current crowd working platforms, and more accurate than in the traditional model.
LZ-End Parsing in Compressed Space
Venue: arXiv cs.DS 2017
Year: 2017

We present an algorithm that constructs the LZ-End parsing (a variation of LZ77) of a given string of length $n$ in $O(n\log\ell)$ expected time and $O(z + \ell)$ space, where $z$ is the number of phrases in the parsing and $\ell$ is the length of the longest phrase. As an option, we can fix $\ell$ (e.g., to the size of RAM) thus obtaining a reasonable LZ-End approximation with the same functionality and the length of phrases restricted by $\ell$. This modified algorithm constructs the parsing in streaming fashion in one left to right pass on the input string w.h.p. and performs one right to left pass to verify the correctness of the result. Experimentally comparing this version to other LZ77-based analogs, we show that it is of practical interest.
Low-effort place recognition with WiFi fingerprints using deep learning
Venue: arXiv cs.RO 2017
Year: 2017

Using WiFi signals for indoor localization is the main localization modality of the existing personal indoor localization systems operating on mobile devices. WiFi fingerprinting is also used for mobile robots, as WiFi signals are usually available indoors and can provide rough initial position estimate or can be used together with other positioning systems. Currently, the best solutions rely on filtering, manual data analysis, and time-consuming parameter tuning to achieve reliable and accurate localization. In this work, we propose to use deep neural networks to significantly lower the work-force burden of the localization system design, while still achieving satisfactory results. Assuming the state-of-the-art hierarchical approach, we employ the DNN system for building/floor classification. We show that stacked autoencoders allow to efficiently reduce the feature space in order to achieve robust and precise classification. The proposed architecture is verified on the publicly available UJIIndoorLoc dataset and the results are compared with other solutions.
Hierarchical compositional feature learning
Venue: arXiv cs.LG 2017
Year: 2017

We introduce the hierarchical compositional network (HCN), a directed generative model able to discover and disentangle, without supervision, the building blocks of a set of binary images. The building blocks are binary features defined hierarchically as a composition of some of the features in the layer immediately below, arranged in a particular manner. At a high level, HCN is similar to a sigmoid belief network with pooling. Inference and learning in HCN are very challenging and existing variational approximations do not work satisfactorily. A main contribution of this work is to show that both can be addressed using max-product message passing (MPMP) with a particular schedule (no EM required). Also, using MPMP as an inference engine for HCN makes new tasks simple: adding supervision information, classifying images, or performing inpainting all correspond to clamping some variables of the model to their known values and running MPMP on the rest. When used for classification, fast inference with HCN has exactly the same functional form as a convolutional neural network (CNN) with linear activations and binary weights. However, HCN's features are qualitatively very different.
Spectrum sharing in energy harvesting cognitive radio networks: A cross-layer perspective
Venue: arXiv cs.IT 2017
Year: 2017

In the paper, we present a cross-layer perspective on data transmission in energy harvesting cognitive radio networks (CRNs). The delay optimal power allocation is studied while taking into account the randomness of harvested energy, data generation, channel state and the grid price. To guarantee primary user (PU)'s transmission, its Signal-Interference-Ratio (SIR) should be no less than a threshold. Each user, including PU as well as secondary user (SU), has energy harvesting devices, and the PU can also purchases the grid power. Each user is rational and selfish to minimize its own the buffer delay. We formulate a stochastic Stackelberg game in a bilevel manner. After decoupling via rewriting the objective and constraints, an equivalent tractable reconstruction is derived. First, we give a distributive algorithm to obtain the Nash equilibrium (NE) of the lower level SUs' noncooperative stochastic game. Thereafter, the stochastic Stackelberg game is discussed under the circumstances that there is no information exchange between PU and SU. Distributed iterative algorithms are designed. Furthermore, a distributive online algorithm is proposed. Finally, simulations are carried out to verify the correctness and demonstrate the effectiveness of proposed algorithms.
Recursive Regression with Neural Networks: Approximating the HJI PDE Solution
Venue: arXiv cs.LG 2017
Year: 2017

The majority of methods used to compute approximations to the Hamilton-Jacobi-Isaacs partial differential equation (HJI PDE) rely on the discretization of the state space to perform dynamic programming updates. This type of approach is known to suffer from the curse of dimensionality due to the exponential growth in grid points with the state dimension. In this work we present an approximate dynamic programming algorithm that computes an approximation of the solution of the HJI PDE by alternating between solving a regression problem and solving a minimax problem using a feedforward neural network as the function approximator. We find that this method requires less memory to run and to store the approximation than traditional gridding methods, and we test it on a few systems of two, three and six dimensions.
New CRT sequence sets for a collision channel without feedback
Venue: arXiv cs.IT 2017
Year: 2017

Protocol sequences are binary and periodic sequences used for deterministic multiple access in a collision channel without feedback. In this paper, we focus on user-irrepressible (UI) protocol sequences that can guarantee a positive individual throughput per sequence period with probability one for a slot-synchronous channel, regardless of the delay offsets among the users. As the sequence period has a fundamental impact on the worst-case channel access delay, a common objective of designing UI sequences is to make the sequence period as short as possible. Consider a communication channel that is shared by $M$ active users, and assume that each protocol sequence has a constant Hamming weight $w$. To attain a better delay performance than previously known UI sequences, this paper presents a CRTm construction of UI sequences with $w=M+1$, which is a variation of the previously known CRT construction. For all non-prime $M\geq 8$, our construction produces the shortest known sequence period and the shortest known worst-case delay of UI sequences. Numerical results show that the new construction enjoys a better average delay performance than the optimal random access scheme and other constructions with the same sequence period, in a variety of traffic conditions. In addition, we derive an asymptotic lower bound on the minimum sequence period for $w=M+1$ if the sequence structure satisfies some technical conditions, called equi-difference, and prove the tightness of this lower bound by using the CRTm construction.
Massive Machine Type Communication with Data Aggregation and Resource Scheduling
Venue: arXiv cs.IT 2017
Year: 2017

To enable massive machine type communication (mMTC), data aggregation is a promising approach to reduce the congestion caused by a massive number of machine type devices (MTDs). In this work, we consider a two-phase cellular-based mMTC network where MTDs transmit to aggregators (i.e., aggregation phase) and the aggregated data is then relayed to base stations (i.e., relaying phase). Due to the limited resources, the aggregators not only aggregate data, but also schedule resources among MTDs. We consider two scheduling schemes: random resource scheduling (RRS) and channel-aware resource scheduling (CRS). By leveraging the stochastic geometry, we present a tractable analytical framework to investigate the signal-to-interference ratio (SIR) for each phase, thereby computing the MTD success probability, the average number of successful MTDs and probability of successful channel utilization, which are the key metrics characterizing the overall mMTC performance. Our numerical results show that, although the CRS outperforms the RRS in terms of SIR at the aggregation phase, the simpler RRS has almost the same performance as the CRS for most cases with regards to the overall mMTC performance. Furthermore, the provision of more resources at the aggregation phase is not always beneficial to the mMTC performance.
Primal-Dual Optimization for Fluids
Venue: arXiv cs.GR 2017
Year: 2017

We apply a novel optimization scheme from the image processing and machine learning areas, a fast Primal-Dual method, to achieve controllable and realistic fluid simulations. While our method is generally applicable to many problems in fluid simulations, we focus on the two topics of fluid guiding and separating solid-wall boundary conditions. Each problem is posed as an optimization problem and solved using our method, which contains acceleration schemes tailored to each problem. In fluid guiding, we are interested in partially guiding fluid motion to exert control while preserving fluid characteristics. With our method, we achieve explicit control over both large-scale motions and small-scale details which is valuable for many applications, such as level-of-detail adjustment (after running the coarse simulation), spatially varying guiding strength, domain modification, and resimulation with different fluid parameters. For the separating solid-wall boundary conditions problem, our method effectively eliminates unrealistic artifacts of fluid crawling up solid walls and sticking to ceilings, requiring few changes to existing implementations. We demonstrate the fast convergence of our Primal-Dual method with a variety of test cases for both model problems.