OpenRaiser/Intern-Atlas huggingface dataset:
On the Minimum Mean $p$-th Error in Gaussian Noise Channels and its Applications
Venue: arXiv cs.IT 2016
Year: 2016

The problem of estimating an arbitrary random vector from its observation corrupted by additive white Gaussian noise, where the cost function is taken to be the Minimum Mean $p$-th Error (MMPE), is considered. The classical Minimum Mean Square Error (MMSE) is a special case of the MMPE. Several bounds, properties and applications of the MMPE are derived and discussed. The optimal MMPE estimator is found for Gaussian and binary input distributions. Properties of the MMPE as a function of the input distribution, SNR and order $p$ are derived. In particular, it is shown that the MMPE is a continuous function of $p$ and SNR. These results are possible in view of interpolation and change of measure bounds on the MMPE. The `Single-Crossing-Point Property' (SCPP) that bounds the MMSE for all SNR values {\it above} a certain value, at which the MMSE is known, together with the I-MMSE relationship is a powerful tool in deriving converse proofs in information theory. By studying the notion of conditional MMPE, a unifying proof (i.e., for any $p$) of the SCPP is shown. A complementary bound to the SCPP is then shown, which bounds the MMPE for all SNR values {\it below} a certain value, at which the MMPE is known. As a first application of the MMPE, a bound on the conditional differential entropy in terms of the MMPE is provided, which then yields a generalization of the Ozarow-Wyner lower bound on the mutual information achieved by a discrete input on a Gaussian noise channel. As a second application, the MMPE is shown to improve on previous characterizations of the phase transition phenomenon that manifests, in the limit as the length of the capacity achieving code goes to infinity, as a discontinuity of the MMSE as a function of SNR. As a final application, the MMPE is used to show bounds on the second derivative of mutual information, that tighten previously known bounds.
The Effects of Cultural dimensions and Demographic Characteristics on E-learning Acceptance
Venue: arXiv cs.CY 2016
Year: 2016

This study aims to develop and test an amalgamated conceptual framework based on Technology Acceptance Model (TAM) and other models from social psychology, such as theory of reasoned action and TAM2 that captures the salient factors influencing the user adoption and acceptance of web-based learning systems. This framework has been applied to the study of higher educational institutions in the context of developing as well as developed countries (e.g. Lebanon and UK). Additionally, the framework investigates the moderating effect of Hofstedes four cultural dimensions at the individual level and a set of individual differences (age, gender, experience and educational level) on the key determinants that affect the behavioral intention to use e-learning. A total of 1197 questionnaires were received from students who were using web-based learning systems at higher educational institutions in Lebanon and the UK with opposite scores on cultural dimensions. Confirmatory Factor Analysis (CFA) was used to perform reliability and validity checks, and Structural Equation Modeling (SEM) in conjunction with multi-group analysis method was used to test the hypothesized conceptual model. Our findings suggest that individual, social, cultural and organizational factors are important to consider in explaining students behavioral intention and usage of e-learning environments. The findings of this research contribute to the literature by validating and supporting the applicability of our extended TAM in the Lebanese and British contexts and provide several prominent implications to both theory and practice on the individual, organizational and societal levels.
Optimal Locally Repairable Systematic Codes Based on Packings
Venue: arXiv cs.IT 2016
Year: 2016

Locally repairable codes are desirable for distributed storage systems to improve the repair efficiency. In this paper, we first build a bridge between locally repairable code and packing. As an application of this bridge, some optimal locally repairable codes can be obtained by packings, which gives optimal locally repairable codes with flexible parameters.
Translating Scala Programs to Isabelle/HOL
Venue: arXiv cs.LO 2016
Year: 2016

We present a trustworthy connection between the Leon verification system and the Isabelle proof assistant. Leon is a system for verifying functional Scala programs. It uses a variety of automated theorem provers (ATPs) to check verification conditions (VCs) stemming from the input program. Isabelle, on the other hand, is an interactive theorem prover used to verify mathematical specifications using its own input language Isabelle/Isar. Users specify (inductive) definitions and write proofs about them manually, albeit with the help of semi-automated tactics. The integration of these two systems allows us to exploit Isabelle's rich standard library and give greater confidence guarantees in the correctness of analysed programs.
On Sampling and Greedy MAP Inference of Constrained Determinantal Point Processes
Venue: arXiv cs.DS 2016
Year: 2016

Subset selection problems ask for a small, diverse yet representative subset of the given data. When pairwise similarities are captured by a kernel, the determinants of submatrices provide a measure of diversity or independence of items within a subset. Matroid theory gives another notion of independence, thus giving rise to optimization and sampling questions about Determinantal Point Processes (DPPs) under matroid constraints. Partition constraints, as a special case, arise naturally when incorporating additional labeling or clustering information, besides the kernel, in DPPs. Finding the maximum determinant submatrix under matroid constraints on its row/column indices has been previously studied. However, the corresponding question of sampling from DPPs under matroid constraints has been unresolved, beyond the simple cardinality constrained k-DPPs. We give the first polynomial time algorithm to sample exactly from DPPs under partition constraints, for any constant number of partitions. We complement this by a complexity theoretic barrier that rules out such a result under general matroid constraints. Our experiments indicate that partition-constrained DPPs offer more flexibility and more diversity than k-DPPs and their naive extensions, while being reasonably efficient in running time. We also show that a simple greedy initialization followed by local search gives improved approximation guarantees for the problem of MAP inference from k- DPPs on well-conditioned kernels. Our experiments show that this improvement is significant for larger values of k, supporting our theoretical result.
Lattice Structure of Variable Precision Rough Sets
Venue: arXiv cs.AI 2016
Year: 2016

The main purpose of this paper is to study the lattice structure of variable precision rough sets. The notion of variation in precision of rough sets have been further extended to variable precision rough set with variable classification error and its algebraic properties are also studied.
GUICop: Approach and Toolset for Specification-based GUI Testing
Venue: arXiv cs.SE 2016
Year: 2016

Oracles used for testing graphical user interface (GUI) programs are required to take into consideration complicating factors such as variations in screen resolution or color scheme when comparing observed GUI elements to expected GUI elements. Researchers proposed fuzzy comparison rules and computationally expensive image processing techniques to tame the comparison process since otherwise the naive matching comparison would be too constraining and consequently impractical. Alternatively, this paper proposes GUICop, a novel approach with a supporting toolset that takes (1) a GUI program and (2) user-defined GUI specifications characterizing the rendering behavior of the GUI elements, and checks whether the execution traces of the program satisfy the specifications. GUICop comprises the following: 1) a GUI Specification Language; 2) a Driver; 3) Instrumented GUI Libraries; 4) a Solver; and 5) a Code Weaver. The user defines the specifications of the subject GUI program using the GUI Specification Language. The Driver traverses the GUI structure of the program and generates events that drive its execution. The Instrumented GUI Libraries capture the GUI execution trace, i.e., information about the positions and visibility of the GUI elements. And the Solver, enabled by code injected by the Code Weaver, checks whether the traces satisfy the specifications. GUICop was successfully evaluated using four open source GUI applications that included eight defects, namely, Jajuk, Gason, JEdit, and TerpPaint.
Urban Social Media Inequality: Definition, Measurements, and Application
Venue: arXiv cs.SI 2016
Year: 2016

Social media content shared today in cities, such as Instagram images, their tags and descriptions, is the key form of contemporary city life. It tells people where activities and locations that interest them are and it allows them to share their urban experiences and self-representations. Therefore, any analysis of urban structures and cultures needs to consider social media activity. In our paper, we introduce the novel concept of social media inequality. This concept allows us to quantitatively compare patterns in social media activities between parts of a city, a number of cities, or any other spatial areas. We define this concept using an analogy with the concept of economic inequality. Economic inequality indicates how some economic characteristics or material resources, such as income, wealth or consumption are distributed in a city, country or between countries. Accordingly, we can define social media inequality as the measure of the distribution of characteristics from social media content shared in a particular geographic area or between areas. An example of such characteristics is the number of photos shared by all users of a social network such as Instagram in a given city or city area, or the content of these photos. We propose that the standard inequality measures used in other disciplines, such as the Gini coefficient, can also be used to characterize social media inequality. To test our ideas, we use a dataset of 7,442,454 public geo-coded Instagram images shared in Manhattan during five months (March-July) in 2014, and also selected data for 287 Census tracts in Manhattan. We compare patterns in Instagram sharing for locals and for visitors for all tracts, and also for hours in a 24-hour cycle. We also look at relations between social media inequality and socio-economic inequality using selected indicators for Census tracts.
Untrimmed Video Classification for Activity Detection: submission to ActivityNet Challenge
Venue: arXiv cs.CV 2016
Year: 2016

Current state-of-the-art human activity recognition is focused on the classification of temporally trimmed videos in which only one action occurs per frame. We propose a simple, yet effective, method for the temporal detection of activities in temporally untrimmed videos with the help of untrimmed classification. Firstly, our model predicts the top k labels for each untrimmed video by analysing global video-level features. Secondly, frame-level binary classification is combined with dynamic programming to generate the temporally trimmed activity proposals. Finally, each proposal is assigned a label based on the global label, and scored with the score of the temporal activity proposal and the global score. Ultimately, we show that untrimmed video classification models can be used as stepping stone for temporal detection.
Tubelets: Unsupervised action proposals from spatiotemporal super-voxels
Venue: arXiv cs.CV 2016
Year: 2016

This paper considers the problem of localizing actions in videos as a sequences of bounding boxes. The objective is to generate action proposals that are likely to include the action of interest, ideally achieving high recall with few proposals. Our contributions are threefold. First, inspired by selective search for object proposals, we introduce an approach to generate action proposals from spatiotemporal super-voxels in an unsupervised manner, we call them Tubelets. Second, along with the static features from individual frames our approach advantageously exploits motion. We introduce independent motion evidence as a feature to characterize how the action deviates from the background and explicitly incorporate such motion information in various stages of the proposal generation. Finally, we introduce spatiotemporal refinement of Tubelets, for more precise localization of actions, and pruning to keep the number of Tubelets limited. We demonstrate the suitability of our approach by extensive experiments for action proposal quality and action localization on three public datasets: UCF Sports, MSR-II and UCF101. For action proposal quality, our unsupervised proposals beat all other existing approaches on the three datasets. For action localization, we show top performance on both the trimmed videos of UCF Sports and UCF101 as well as the untrimmed videos of MSR-II.
Fast and robust mesh generation on the sphere Application to coastal domains
Venue: arXiv cs.CG 2016
Year: 2016

This paper presents a fast an robust mesh generation procedure that is able to generate meshes of the earth system (ocean and continent) in matters of seconds. Our algorithm takes as input a standard shape-file i.e. geospatial vector data format for geographic information system (GIS) software. The input is initially coarsened in order to automatically remove unwanted channels that are under a desired resolution. A valid non-overlapping 1D mesh is then created on the sphere using the Euclidian coordinates system $x,y,z$. A modified Delaunay kernel is then proposed that enables to generate meshes on the sphere in a straightforward manner without parametrization. One of the main difficulty in dealing with geographical data is the over-sampled nature of coastline representations. We propose here an algorithm that automatically unrefines coastline data. Small features are automatically removed while always keeping a valid (non-overlapping) geometrical representation of the domain. A Delaunay refinement procedure is subsequently applied to the domain. The refinement scheme is also multi-threaded at a fine grain level, allowing to generate about a million points per second on 8 threads. Examples of meshes of the Baltic sea as well as of the global ocean are presented.
Extreme Scaling of Supercomputing with Stranded Power: Costs and Capabilities
Venue: arXiv cs.DC 2016
Year: 2016

Power consumption (supply, heat, cost) and associated carbon emissions (environmental impact) are increasingly critical challenges in scaling supercomputing to Exascale and beyond. We proposes to exploit stranded power, renewable energy that has no value to the power grid, for scaling supercomputers, Zero-Carbon Cloud (ZCCloud), and showing that stranded power can be employed effectively to expand computing [1]. We build on those results with a new analysis of stranded power, characterizing temporal, geographic, and interval properties. We simulate production supercomputing workloads and model datacenter total-cost-of-ownership (TCO), assessing the costs and capabilities of stranded-power based supercomputing. Results show that the ZCCloud approach is cost-effective today in regions with high cost power. The ZCCloud approach reduces TCO by 21-45%, and improves cost-effectiveness up to 34%. We study many scenarios. With higher power price, cheaper computing hardware and higher system power density, benefits rise to 55%, 97% and 116% respectively. Finally, we study future extreme-scale systems, showing that beyond terascale, projected power requirements in excess of 100MW make ZCCloud up to 45% lower cost, for a fixed budget, increase peak PFLOPS achievable by 80%.
Argumentation Models for Cyber Attribution
Venue: arXiv cs.AI 2016
Year: 2016

A major challenge in cyber-threat analysis is combining information from different sources to find the person or the group responsible for the cyber-attack. It is one of the most important technical and policy challenges in cyber-security. The lack of ground truth for an individual responsible for an attack has limited previous studies. In this paper, we take a first step towards overcoming this limitation by building a dataset from the capture-the-flag event held at DEFCON, and propose an argumentation model based on a formal reasoning framework called DeLP (Defeasible Logic Programming) designed to aid an analyst in attributing a cyber-attack. We build models from latent variables to reduce the search space of culprits (attackers), and show that this reduction significantly improves the performance of classification-based approaches from 37% to 62% in identifying the attacker.
Sapo: Reachability Computation and Parameter Synthesis of Polynomial Dynamical Systems
Venue: arXiv cs.SY 2016
Year: 2016

Sapo is a C++ tool for the formal analysis of polynomial dynamical systems. Its main features are: 1) Reachability computation, i.e., the calculation of the set of states reachable from a set of initial conditions, and 2) Parameter synthesis, i.e., the refinement of a set of parameters so that the system satisfies a given specification. Sapo can represent reachable sets as unions of boxes, parallelotopes, or parallelotope bundles (symbolic representation of polytopes). Sets of parameters are represented with polytopes while specifications are formalized as Signal Temporal Logic (STL) formulas.
Large Scale GPU Accelerated PPMLR-MHD Simulations for Space Weather Forecast
Venue: arXiv cs.DC 2016
Year: 2016

PPMLR-MHD is a new magnetohydrodynamics (MHD) model used to simulate the interactions of the solar wind with the magnetosphere, which has been proved to be the key element of the space weather cause-and-effect chain process from the Sun to Earth. Compared to existing MHD methods, PPMLR-MHD achieves the advantage of high order spatial accuracy and low numerical dissipation. However, the accuracy comes at a cost. On one hand, this method requires more intensive computation. On the other hand, more boundary data is subject to be transferred during the process of simulation.s In this work, we present a parallel hybrid solution of the PPMLR-MHD model implemented using the computing capabilities of both CPUs and GPUs. We demonstrate that our optimized implementation alleviates the data transfer overhead by using GPU Direct technology and can scale up to 151 processes and achieve significant performance gains by distributing the workload among the CPUs and GPUs on Titan at Oak Ridge National Laboratory. The performance results show that our implementation is fast enough to carry out highly accurate MHD simulations in real time.
Towards Trustworthy Refactoring in Erlang
Venue: arXiv cs.PL 2016
Year: 2016

Tool-assisted refactoring transformations must be trustworthy if programmers are to be confident in applying them on arbitrarily extensive and complex code in order to improve style or efficiency. We propose a simple, high-level but rigorous, notation for defining refactoring transformations in Erlang, and show that this notation provides an extensible, verifiable and executable specification language for refactoring. To demonstrate the applicability of our approach, we show how to define and verify a number of example refactorings in the system.
Program Transformation to Identify List-Based Parallel Skeletons
Venue: arXiv cs.PL 2016
Year: 2016

Algorithmic skeletons are used as building-blocks to ease the task of parallel programming by abstracting the details of parallel implementation from the developer. Most existing libraries provide implementations of skeletons that are defined over flat data types such as lists or arrays. However, skeleton-based parallel programming is still very challenging as it requires intricate analysis of the underlying algorithm and often uses inefficient intermediate data structures. Further, the algorithmic structure of a given program may not match those of list-based skeletons. In this paper, we present a method to automatically transform any given program to one that is defined over a list and is more likely to contain instances of list-based skeletons. This facilitates the parallel execution of a transformed program using existing implementations of list-based parallel skeletons. Further, by using an existing transformation called distillation in conjunction with our method, we produce transformed programs that contain fewer inefficient intermediate data structures.
Resiliency with Aggregate Computing: State of the Art and Roadmap
Venue: arXiv cs.PL 2016
Year: 2016

One of the difficulties in developing collective adaptive systems is the challenge of simultaneously engineering both the desired resilient behaviour of the collective and the details of its implementation on individual devices. Aggregate computing simplifies this problem by separating these aspects into different layers of abstraction by means of a unifying notion of computational field and a functional computational model. We review the state of the art in aggregate computing, discuss the various resiliency properties it supports, and develop a roadmap of foundational problems still needing to be addressed in the continued development of this emerging discipline.
A Formal Framework for Modeling Trust and Reputation in Collective Adaptive Systems
Venue: arXiv cs.LO 2016
Year: 2016

Trust and reputation models for distributed, collaborative systems have been studied and applied in several domains, in order to stimulate cooperation while preventing selfish and malicious behaviors. Nonetheless, such models have received less attention in the process of specifying and analyzing formally the functionalities of the systems mentioned above. The objective of this paper is to define a process algebraic framework for the modeling of systems that use (i) trust and reputation to govern the interactions among nodes, and (ii) communication models characterized by a high level of adaptiveness and flexibility. Hence, we propose a formalism for verifying, through model checking techniques, the robustness of these systems with respect to the typical attacks conducted against webs of trust.
Rates of DNA Sequence Profiles for Practical Values of Read Lengths
Venue: arXiv cs.IT 2016
Year: 2016

A recent study by one of the authors has demonstrated the importance of profile vectors in DNA-based data storage. We provide exact values and lower bounds on the number of profile vectors for finite values of alphabet size $q$, read length $\ell$, and word length $n$.Consequently, we demonstrate that for $q\ge 2$ and $n\le q^{\ell/2-1}$, the number of profile vectors is at least $q^{κn}$ with $κ$ very close to one.In addition to enumeration results, we provide a set of efficient encoding and decoding algorithms for each of two particular families of profile vectors.
On Channel Resolvability in Presence of Feedback
Venue: arXiv cs.IT 2016
Year: 2016

We study the problem of generating an approximately i.i.d. string at the output of a discrete memoryless channel using a limited amount of randomness at its input in presence of causal noiseless feedback. Feedback does not decrease the channel resolution, the minimum entropy rate required to achieve an accurate approximation of an i.i.d. output string. However, we show that, at least over a binary symmetric channel, a significantly larger resolvability exponent (the exponential decay rate of the divergence between the output distribution and product measure), compared to the best known achievable resolvability exponent in a system without feedback, is possible. We show that by employing a variable-length resolvability scheme and using an average number of coin-flips per channel use, the average divergence between the distribution of the output sequence and product measure decays exponentially fast in the average length of output sequence with an exponent equal to $[R-I(U;V)]^+$ where $I(U;V)$ is the mutual information developed across the channel.