OpenRaiser/Intern-Atlas huggingface dataset:
Efficient Algorithms for Time- and Cost-Bounded Probabilistic Model Checking
Venue: arXiv cs.LO 2016
Year: 2016

In the design of probabilistic timed systems, bounded requirements concerning behaviour that occurs within a given time, energy, or more generally cost budget are of central importance. Traditionally, such requirements have been model-checked via a reduction to the unbounded case by unfolding the model according to the cost bound. This exacerbates the state space explosion problem and significantly increases runtime. In this paper, we present three new algorithms to model-check time- and cost-bounded properties for Markov decision processes and probabilistic timed automata that avoid unfolding. They are based on a modified value iteration process, on an enumeration of schedulers, and on state elimination techniques. We can now obtain results for any cost bound on a single state space no larger than for the corresponding unbounded or expected-value property. In particular, we can naturally compute the cumulative distribution function at no overhead. We evaluate the applicability and compare the performance of our new algorithms and their implementation on a number of case studies from the literature.
Time-Invariant Spatially Coupled Low-Density Parity-Check Codes with Small Constraint Length
Venue: arXiv cs.IT 2016
Year: 2016

We consider a special family of SC-LDPC codes, that is, time-invariant LDPCC codes, which are known in the literature for a long time. Codes of this kind are usually designed by starting from QC block codes, and applying suitable unwrapping procedures. We show that, by directly designing the LDPCC code syndrome former matrix without the constraints of the underlying QC block code, it is possible to achieve smaller constraint lengths with respect to the best solutions available in the literature. We also find theoretical lower bounds on the syndrome former constraint length for codes with a specified minimum length of the local cycles in their Tanner graphs. For this purpose, we exploit a new approach based on a numerical representation of the syndrome former matrix, which generalizes over a technique we already used to study a special subclass of the codes here considered.
Naughton's Wisconsin Bibliography: A Brief Guide
Venue: arXiv cs.GL 2016
Year: 2016

Over nearly three decades at the University of Wisconsin, Jeff Naughton has left an indelible mark on computer science. He has been a global leader of the database research field, deepening its core and pushing its boundaries. Many of Naughton's ideas were translated directly into practice in commercial and open-source systems. But software comes and goes. In the end, it is the ideas themselves that have had impact, ideas written down in papers. Naughton has been a prolific scholar over the last thirty years, with over 175 publications in his bibliography, covering a wide range of topics. This document does not attempt to enumerate or even summarize the wealth of ideas that Naughton has published over the course of his academic career--the task is too daunting. Instead, the best this short note aims to do is to serve as a rough map of the territory: something to help other researchers navigate the wide spaces of Naughton's work.
Spectrum Sharing in mmWave Cellular Networks via Cell Association, Coordination, and Beamforming
Venue: arXiv cs.IT 2016
Year: 2016

This paper investigates the extent to which spectrum sharing in mmWave networks with multiple cellular operators is a viable alternative to traditional dedicated spectrum allocation. Specifically, we develop a general mathematical framework by which to characterize the performance gain that can be obtained when spectrum sharing is used, as a function of the underlying beamforming, operator coordination, bandwidth, and infrastructure sharing scenarios. The framework is based on joint beamforming and cell association optimization, with the objective of maximizing the long-term throughput of the users. Our asymptotic and non-asymptotic performance analyses reveal five key points: (1) spectrum sharing with light on-demand intra- and inter-operator coordination is feasible, especially at higher mmWave frequencies (for example, 73 GHz), (2) directional communications at the user equipment substantially alleviate the potential disadvantages of spectrum sharing (such as higher multiuser interference), (3) large numbers of antenna elements can reduce the need for coordination and simplify the implementation of spectrum sharing, (4) while inter-operator coordination can be neglected in the large-antenna regime, intra-operator coordination can still bring gains by balancing the network load, and (5) critical control signals among base stations, operators, and user equipment should be protected from the adverse effects of spectrum sharing, for example by means of exclusive resource allocation. The results of this paper, and their extensions obtained by relaxing some ideal assumptions, can provide important insights for future standardization and spectrum policy.
A Short Proof for Gap Independence of Simultaneous Iteration
Venue: arXiv cs.NA 2016
Year: 2016

This note provides a very short proof of a spectral gap independent property of the simultaneous iterations algorithm for finding the top singular space of a matrix. See Rokhlin-Szlam-Tygert-2009, Halko-Martinsson-Tropp-2011 and Musco-Musco-2015. The proof is terse but completely self contained and should be accessible to the linear algebra savvy reader.
Full characterization of generalized bent functions as (semi)-bent spaces, their dual, and the Gray image
Venue: arXiv cs.IT 2016
Year: 2016

In difference to many recent articles that deal with generalized bent (gbent) functions $f:\mathbb{Z}_2^n \rightarrow \mathbb{Z}_q$ for certain small valued $q\in \{4,8,16 \}$, we give a complete description of these functions for both $n$ even and odd and for any $q=2^k$ in terms of both the necessary and sufficient conditions their component functions need to satisfy. This enables us to completely characterize gbent functions as algebraic objects, namely as affine spaces of bent or semi-bent functions with interesting additional properties, which we in detail describe. We also specify the dual and the Gray image of gbent functions for $q=2^k$. We discuss the subclass of gbent functions which corresponds to relative difference sets, which we call $\mathbb{Z}_q$-bent functions, and point out that they correspond to a class of vectorial bent functions. The property of being $\mathbb{Z}_q$-bent is much stronger than the standard concept of a gbent function. We analyse two examples of this class of functions.
Robust Image Descriptors for Real-Time Inter-Examination Retargeting in Gastrointestinal Endoscopy
Venue: arXiv cs.CV 2016
Year: 2016

For early diagnosis of malignancies in the gastrointestinal tract, surveillance endoscopy is increasingly used to monitor abnormal tissue changes in serial examinations of the same patient. Despite successes with optical biopsy for in vivo and in situ tissue characterisation, biopsy retargeting for serial examinations is challenging because tissue may change in appearance between examinations. In this paper, we propose an inter-examination retargeting framework for optical biopsy, based on an image descriptor designed for matching between endoscopic scenes over significant time intervals. Each scene is described by a hierarchy of regional intensity comparisons at various scales, offering tolerance to long-term change in tissue appearance whilst remaining discriminative. Binary coding is then used to compress the descriptor via a novel random forests approach, providing fast comparisons in Hamming space and real-time retargeting. Extensive validation conducted on 13 in vivo gastrointestinal videos, collected from six patients, show that our approach outperforms state-of-the-art methods.
Resource Provisioning and Profit Maximization for Transcoding in Information Centric Networking
Venue: arXiv cs.MM 2016
Year: 2016

Adaptive bitrate streaming (ABR) has been widely adopted to support video streaming services over heterogeneous devices and varying network conditions. With ABR, each video content is transcoded into multiple representations in different bitrates and resolutions. However, video transcoding is computing intensive, which requires the transcoding service providers to deploy a large number of servers for transcoding the video contents published by the content producers. As such, a natural question for the transcoding service provider is how to provision the computing resource for transcoding the video contents while maximizing service profit. To address this problem, we design a cloud video transcoding system by taking the advantage of cloud computing technology to elastically allocate computing resource. We propose a method for jointly considering the task scheduling and resource provisioning problem in two timescales, and formulate the service profit maximization as a two-timescale stochastic optimization problem. We derive some approximate policies for the task scheduling and resource provisioning. Based on our proposed methods, we implement our open source cloud video transcoding system Morph and evaluate its performance in a real environment. The experiment results demonstrate that our proposed method can reduce the resource consumption and achieve a higher profit compared with the baseline schemes.
Recurrent Exponential-Family Harmoniums without Backprop-Through-Time
Venue: arXiv cs.LG 2016
Year: 2016

Exponential-family harmoniums (EFHs), which extend restricted Boltzmann machines (RBMs) from Bernoulli random variables to other exponential families (Welling et al., 2005), are generative models that can be trained with unsupervised-learning techniques, like contrastive divergence (Hinton et al. 2006; Hinton, 2002), as density estimators for static data. Methods for extending RBMs--and likewise EFHs--to data with temporal dependencies have been proposed previously (Sutskever and Hinton, 2007; Sutskever et al., 2009), the learning procedure being validated by qualitative assessment of the generative model. Here we propose and justify, from a very different perspective, an alternative training procedure, proving sufficient conditions for optimal inference under that procedure. The resulting algorithm can be learned with only forward passes through the data--backprop-through-time is not required, as in previous approaches. The proof exploits a recent result about information retention in density estimators (Makin and Sabes, 2015), and applies it to a "recurrent EFH" (rEFH) by induction. Finally, we demonstrate optimality by simulation, testing the rEFH: (1) as a filter on training data generated with a linear dynamical system, the position of which is noisily reported by a population of "neurons" with Poisson-distributed spike counts; and (2) with the qualitative experiments proposed by Sutskever et al. (2009).
Bacterial foraging optimization based brain magnetic resonance image segmentation
Venue: arXiv cs.CV 2016
Year: 2016

Segmentation partitions an image into its constituent parts. It is essentially the pre-processing stage of image analysis and computer vision. In this work, T1 and T2 weighted brain magnetic resonance images are segmented using multilevel thresholding and bacterial foraging optimization (BFO) algorithm. The thresholds are obtained by maximizing the between class variance (multilevel Otsu method) of the image. The BFO algorithm is used to optimize the threshold searching process. The edges are then obtained from the thresholded image by comparing the intensity of each pixel with its eight connected neighbourhood. Post processing is performed to remove spurious responses in the segmented image. The proposed segmentation technique is evaluated using edge detector evaluation parameters such as figure of merit, Rand Index and variation of information. The proposed brain MR image segmentation technique outperforms the traditional edge detectors such as canny and sobel.
Automatic TM Cleaning through MT and POS Tagging: Autodesk's Submission to the NLP4TM 2016 Shared Task
Venue: arXiv cs.CL 2016
Year: 2016

We describe a machine learning based method to identify incorrect entries in translation memories. It extends previous work by Barbu (2015) through incorporating recall-based machine translation and part-of-speech-tagging features. Our system ranked first in the Binary Classification (II) task for two out of three language pairs: English-Italian and English-Spanish.
A Geometric Approach to Color Image Regularization
Venue: arXiv cs.CV 2016
Year: 2016

We present a new vectorial total variation method that addresses the problem of color consistent image filtering. Our approach is inspired from the double-opponent cell representation in the human visual cortex. Existing methods of vectorial total variation regularizers have insufficient (or no) coupling between the color channels and thus may introduce color artifacts. We address this problem by introducing a novel coupling between the color channels related to a pullback-metric from the opponent space to the data (RGB color) space. Our energy is a non-convex, non-smooth higher-order vectorial total variation approach and promotes color consistent image filtering via a coupling term. For a convex variant, we show well-posedness and existence of a solution in the space of vectorial bounded variation. For the higher-order scheme we employ a half-quadratic strategy, which model the non-convex energy terms as the infimum of a sequence of quadratic functions. In experiments, we elaborate on traditional image restoration applications of inpainting, deblurring and denoising. Regarding the latter, we demonstrate state of the art restoration quality with respect to structure coherence and color consistency.
Computation of the Similarity Class of the p-Curvature
Venue: arXiv cs.SC 2016
Year: 2016

The $p$-curvature of a system of linear differential equations in positive characteristic $p$ is a matrix that measures how far the system is from having a basis of polynomial solutions. We show that the similarity class of the $p$-curvature can be determined without computing the $p$-curvature itself. More precisely, we design an algorithm that computes the invariant factors of the $p$-curvature in time quasi-linear in $\sqrt p$. This is much less than the size of the $p$-curvature, which is generally linear in $p$. The new algorithm allows to answer a question originating from the study of the Ising model in statistical physics.
Hardware-Based ADMM-LP Decoding
Venue: arXiv cs.IT 2016
Year: 2016

In this paper we present an FPGA-based implementation of linear programming (LP) decoding. LP decoding frames error correction as an optimization problem. This is in contrast to variants of belief propagation (BP) decoding that view error correction as a problem of graphical inference. There are many advantages to taking the optimization perspective: convergence guarantees, improved performance in certain regimes, and a methodology for incorporating the latest developments in optimization techniques. However, LP decoding, when implemented with standard LP solvers, does not easily scale to the blocklengths of modern error-correction codes. In earlier work, we showed that by drawing on decomposition methods from optimization theory, specifically the alternating direction method of multipliers (ADMM), we could build an LP decoding solver that was competitive with BP, both in terms of performance and speed. We also observed empirically that LP decoders have much better high-SNR performance in the "error floor" regime, a trait of particular relevance to optical transport and storage applications. While our previous implementation was in floating point, in this paper we report initial results of a fixed-point, hardware-based realization of our ADMM-LP decoder.
Modeling and performance evaluation of stealthy false data injection attacks on smart grid in the presence of corrupted measurements
Venue: arXiv cs.CR 2016
Year: 2016

The false data injection (FDI) attack cannot be detected by the traditional anomaly detection techniques used in the energy system state estimators. In this paper, we demonstrate how FDI attacks can be constructed blindly, i.e., without system knowledge, including topological connectivity and line reactance information. Our analysis reveals that existing FDI attacks become detectable (consequently unsuccessful) by the state estimator if the data contains grossly corrupted measurements such as device malfunction and communication errors. The proposed sparse optimization based stealthy attacks construction strategy overcomes this limitation by separating the gross errors from the measurement matrix. Extensive theoretical modeling and experimental evaluation show that the proposed technique performs more stealthily (has less relative error) and efficiently (fast enough to maintain time requirement) compared to other methods on IEEE benchmark test systems.
Localizing by Describing: Attribute-Guided Attention Localization for Fine-Grained Recognition
Venue: arXiv cs.CV 2016
Year: 2016

A key challenge in fine-grained recognition is how to find and represent discriminative local regions. Recent attention models are capable of learning discriminative region localizers only from category labels with reinforcement learning. However, not utilizing any explicit part information, they are not able to accurately find multiple distinctive regions. In this work, we introduce an attribute-guided attention localization scheme where the local region localizers are learned under the guidance of part attribute descriptions. By designing a novel reward strategy, we are able to learn to locate regions that are spatially and semantically distinctive with reinforcement learning algorithm. The attribute labeling requirement of the scheme is more amenable than the accurate part location annotation required by traditional part-based fine-grained recognition methods. Experimental results on the CUB-200-2011 dataset demonstrate the superiority of the proposed scheme on both fine-grained recognition and attribute recognition.
FIT A Fog Computing Device for Speech TeleTreatments
Venue: arXiv cs.CY 2016
Year: 2016

There is an increasing demand for smart fogcomputing gateways as the size of cloud data is growing. This paper presents a Fog computing interface (FIT) for processing clinical speech data. FIT builds upon our previous work on EchoWear, a wearable technology that validated the use of smartwatches for collecting clinical speech data from patients with Parkinson's disease (PD). The fog interface is a low-power embedded system that acts as a smart interface between the smartwatch and the cloud. It collects, stores, and processes the speech data before sending speech features to secure cloud storage. We developed and validated a working prototype of FIT that enabled remote processing of clinical speech data to get speech clinical features such as loudness, short-time energy, zero-crossing rate, and spectral centroid. We used speech data from six patients with PD in their homes for validating FIT. Our results showed the efficacy of FIT as a Fog interface to translate the clinical speech processing chain (CLIP) from a cloud-based backend to a fog-based smart gateway.
Piece-wise quadratic approximations of arbitrary error functions for fast and robust machine learning
Venue: arXiv cs.LG 2016
Year: 2016

Most of machine learning approaches have stemmed from the application of minimizing the mean squared distance principle, based on the computationally efficient quadratic optimization methods. However, when faced with high-dimensional and noisy data, the quadratic error functionals demonstrated many weaknesses including high sensitivity to contaminating factors and dimensionality curse. Therefore, a lot of recent applications in machine learning exploited properties of non-quadratic error functionals based on $L_1$ norm or even sub-linear potentials corresponding to quasinorms $L_p$ ($0<p<1$). The back side of these approaches is increase in computational cost for optimization. Till so far, no approaches have been suggested to deal with {\it arbitrary} error functionals, in a flexible and computationally efficient framework. In this paper, we develop a theory and basic universal data approximation algorithms ($k$-means, principal components, principal manifolds and graphs, regularized and sparse regression), based on piece-wise quadratic error potentials of subquadratic growth (PQSQ potentials). We develop a new and universal framework to minimize {\it arbitrary sub-quadratic error potentials} using an algorithm with guaranteed fast convergence to the local or global error minimum. The theory of PQSQ potentials is based on the notion of the cone of minorant functions, and represents a natural approximation formalism based on the application of min-plus algebra. The approach can be applied in most of existing machine learning methods, including methods of data approximation and regularized and sparse regression, leading to the improvement in the computational cost/accuracy trade-off. We demonstrate that on synthetic and real-life datasets PQSQ-based machine learning methods achieve orders of magnitude faster computational performance than the corresponding state-of-the-art methods.
ImageCL: An Image Processing Language for Performance Portability on Heterogeneous Systems
Venue: arXiv cs.DC 2016
Year: 2016

Modern computer systems typically conbine multicore CPUs with accelerators like GPUs for inproved performance and energy efficiency. However, these sys- tems suffer from poor performance portability, code tuned for one device must be retuned to achieve high performance on another. Image processing is increas- ing in importance , with applications ranging from seismology and medicine to Photoshop. Based on our experience with medical image processing, we propose ImageCL, a high-level domain-specific language and source-to-source compiler, targeting heterogeneous hardware. ImageCL resembles OpenCL, but abstracts away per- formance optimization details, allowing the programmer to focus on algorithm development, rather than performance tuning. The latter is left to our source-to- source compiler and auto-tuner. From high-level ImageCL kernels, our source- to-source compiler can generate multiple OpenCL implementations with different optimizations applied. We rely on auto-tuning rather than machine models or ex- pert programmer knowledge to determine which optimizations to apply, making our tuning procedure highly robust. Furthermore, we can generate high perform- ing implementations for different devices from a single source code, thereby im- proving performance portability. We evaluate our approach on three image processing benchmarks, on different GPU and CPU devices, and are able to outperform other state of the art solutions in several cases, achieving speedups of up to 4.57x.
Big(ger) Sets: decomposed delta CRDT Sets in Riak
Venue: arXiv cs.DB 2016
Year: 2016

CRDT[24] Sets as implemented in Riak[6] perform poorly for writes, both as cardinality grows, and for sets larger than 500KB[25]. Riak users wish to create high cardinality CRDT sets, and expect better than O(n) performance for individual insert and remove operations. By decomposing a CRDT set on disk, and employing delta-replication[2], we can achieve far better performance than just delta replication alone: relative to the size of causal metadata, not the cardinality of the set, and we can support sets that are 100s times the size of Riak sets, while still providing the same level of consistency. There is a trade-off in read performance but we expect it is mitigated by enabling queries on sets.