OpenRaiser/Intern-Atlas huggingface dataset:
Connectivity of Boolean Satisfiability
Venue: arXiv cs.CC 2015
Year: 2015

For Boolean satisfiability problems, the structure of the solution space is characterized by the solution graph, where the vertices are the solutions, and two solutions are connected iff they differ in exactly one variable. For this implicitly defined graph, we here study the st-connectivity and connectivity problems. Building on the work of Gopalan et al. ("The Connectivity of Boolean Satisfiability: Computational and Structural Dichotomies", 2006/2009), we first investigate satisfiability problems given by CSPs, more exactly CNF(S)-formulas with constants (as considered in Schaefer's famous 1978 dichotomy theorem); we prove a computational dichotomy for the st-connectivity problem, asserting that it is either solvable in polynomial time or PSPACE-complete, and an aligned structural dichotomy, asserting that the maximal diameter of connected components is either linear in the number of variables, or can be exponential; further, we show a trichotomy for the connectivity problem, asserting that it is either in P, coNP-complete, or PSPACE-complete. Next we investigate two important variants: CNF(S)-formulas without constants, and partially quantified formulas; in both cases, we prove analogous dichotomies for st-connectivity and the diameter; for for the connectivity problem, we show a trichotomy in the case of quantified formulas, while in the case of formulas without constants, we identify fragments of a possible trichotomy. Finally, we consider the connectivity issues for B-formulas, which are arbitrarily nested formulas built from some fixed set B of connectives, and for B-circuits, which are Boolean circuits where the gates are from some finite set B; we prove a common dichotomy for both connectivity problems and the diameter; for partially quantified B-formulas, we show an analogous dichotomy.
Characteristic Formulae for Session Types (extended version)
Venue: arXiv cs.LO 2015
Year: 2015

Subtyping is a crucial ingredient of session type theory and its applications, notably to programming language implementations. In this paper, we study effective ways to check whether a session type is a subtype of another by applying a characteristic formulae approach to the problem. Our core contribution is an algorithm to generate a modal mu-calculus formula that characterises all the supertypes (or subtypes) of a given type. Subtyping checks can then be off-loaded to model checkers, thus incidentally yielding an efficient algorithm to check safety of session types, soundly and completely. We have implemented our theory and compared its cost with other classical subtyping algorithms.
Using MapReduce for Large-scale Medical Image Analysis
Venue: arXiv cs.DC 2015
Year: 2015

The growth of the amount of medical image data produced on a daily basis in modern hospitals forces the adaptation of traditional medical image analysis and indexing approaches towards scalable solutions. The number of images and their dimensionality increased dramatically during the past 20 years. We propose solutions for large-scale medical image analysis based on parallel computing and algorithm optimization. The MapReduce framework is used to speed up and make possible three large-scale medical image processing use-cases: (i) parameter optimization for lung texture segmentation using support vector machines, (ii) content-based medical image indexing, and (iii) three-dimensional directional wavelet analysis for solid texture classification. A cluster of heterogeneous computing nodes was set up in our institution using Hadoop allowing for a maximum of 42 concurrent map tasks. The majority of the machines used are desktop computers that are also used for regular office work. The cluster showed to be minimally invasive and stable. The runtimes of each of the three use-case have been significantly reduced when compared to a sequential execution. Hadoop provides an easy-to-employ framework for data analysis tasks that scales well for many tasks but requires optimization for specific tasks.
On the Value and Limits of Multi-level Energy Consumption Static Analysis for Deeply Embedded Single and Multi-threaded Programs
Venue: arXiv cs.PL 2015
Year: 2015

There is growing interest in lowering the energy consumption of computation. Energy transparency is a concept that makes a program's energy consumption visible from software to hardware through the different system layers. Such transparency can enable energy optimizations at each layer and between layers, and help both programmers and operating systems make energy aware decisions. The common methodology of extracting the energy consumption of a program is through direct measurement of the target hardware. This usually involves specialized equipment and knowledge most programmers do not have. In this paper, we examine how existing methods for static resource analysis and energy modeling can be utilized to perform Energy Consumption Static Analysis (ECSA) for deeply embedded programs. To investigate this, we have developed ECSA techniques that work at the instruction set level and at a higher level, the LLVM IR, through a novel mapping technique. We apply our ECSA to a comprehensive set of mainly industrial benchmarks, including single-threaded and also multi-threaded embedded programs from two commonly used concurrency patterns, task farms and pipelines. We compare our ECSA results to hardware measurements and predictions obtained based on simulation traces. We discuss a number of application scenarios for which ECSA results can provide energy transparency and conclude with a set of new research questions for future work.
Intelligent Financial Fraud Detection Practices: An Investigation
Venue: arXiv cs.CR 2015
Year: 2015

Financial fraud is an issue with far reaching consequences in the finance industry, government, corporate sectors, and for ordinary consumers. Increasing dependence on new technologies such as cloud and mobile computing in recent years has compounded the problem. Traditional methods of detection involve extensive use of auditing, where a trained individual manually observes reports or transactions in an attempt to discover fraudulent behaviour. This method is not only time consuming, expensive and inaccurate, but in the age of big data it is also impractical. Not surprisingly, financial institutions have turned to automated processes using statistical and computational methods. This paper presents a comprehensive investigation on financial fraud detection practices using such data mining methods, with a particular focus on computational intelligence-based techniques. Classification of the practices based on key aspects such as detection algorithm used, fraud type investigated, and success rate have been covered. Issues and challenges associated with the current practices and potential future direction of research have also been identified.
Implementation of Experimental Test Bed to Evaluate Security in Cellular Networks
Venue: arXiv cs.CR 2015
Year: 2015

The wide development of inter connectivity of cellular networks with the internet network has made them to be vulnerable. This exposure of the cellular networks to internet has increased threats to customer end equipment as well as the carrier infrastructure.
On the Dominating Set Problem in Random Graphs
Venue: arXiv cs.DS 2015
Year: 2015

In this paper, we study the {\sc Dominating Set} problem in random graphs. In a random graph, each pair of vertices are joined by an edge with a probability of $p$, where $p$ is a positive constant less than $1$. We show that, given a random graph in $n$ vertices, a minimum dominating set in the graph can be computed in expected $2^{O(\log_{2}^{2}{n})}$ time. For the parameterized dominating set problem, we show that it cannot be solved in expected $O(f(k)n^{c})$ time unless the minimum dominating set problem can be approximated within a ratio of $o(\log_{2}n)$ in expected polynomial time, where $f(k)$ is a function of the parameter $k$ and $c$ is a constant independent of $n$ and $k$. In addition, we show that the parameterized dominating set problem can be solved in expected $O(f(k)n^{c})$ time when the probability $p$ depends on $n$ and equals to $\frac{1}{g(n)}$, where $g(n)< n$ is a monotonously increasing function of $n$ and its value approaches infinity when $n$ approaches infinity.
An Efficient Implementation for WalkSAT
Venue: arXiv cs.AI 2015
Year: 2015

Stochastic local search (SLS) algorithms have exhibited great effectiveness in finding models of random instances of the Boolean satisfiability problem (SAT). As one of the most widely known and used SLS algorithm, WalkSAT plays a key role in the evolutions of SLS for SAT, and also hold state-of-the-art performance on random instances. This work proposes a novel implementation for WalkSAT which decreases the redundant calculations leading to a dramatically speeding up, thus dominates the latest version of WalkSAT including its advanced variants.
Some Notes on Temporal Justification Logic
Venue: arXiv cs.LO 2015
Year: 2015

Justification logics are modal-like logics with the additional capability of recording the reason, or justification, for modalities in syntactic structures, called justification terms. Justification logics can be seen as explicit counterparts to modal logic. The behavior and interaction of agents in distributed system is often modeled using logics of knowledge and time. In this paper, we sketch some preliminary ideas on how the modal knowledge part of such logics of knowledge and time could be replaced with an appropriate justification logic.
A Framework for Distributed Deep Learning Layer Design in Python
Venue: arXiv cs.LG 2015
Year: 2015

In this paper, a framework for testing Deep Neural Network (DNN) design in Python is presented. First, big data, machine learning (ML), and Artificial Neural Networks (ANNs) are discussed to familiarize the reader with the importance of such a system. Next, the benefits and detriments of implementing such a system in Python are presented. Lastly, the specifics of the system are explained, and some experimental results are presented to prove the effectiveness of the system.
Safe Control under Uncertainty
Venue: arXiv cs.SY 2015
Year: 2015

Controller synthesis for hybrid systems that satisfy temporal specifications expressing various system properties is a challenging problem that has drawn the attention of many researchers. However, making the assumption that such temporal properties are deterministic is far from the reality. For example, many of the properties the controller has to satisfy are learned through machine learning techniques based on sensor input data. In this paper, we propose a new logic, Probabilistic Signal Temporal Logic (PrSTL), as an expressive language to define the stochastic properties, and enforce probabilistic guarantees on them. We further show how to synthesize safe controllers using this logic for cyber-physical systems under the assumption that the stochastic properties are based on a set of Gaussian random variables. One of the key distinguishing features of PrSTL is that the encoded logic is adaptive and changes as the system encounters additional data and updates its beliefs about the latent random variables that define the safety properties. We demonstrate our approach by synthesizing safe controllers under the PrSTL specifications for multiple case studies including control of quadrotors and autonomous vehicles in dynamic environments.
Depth Extraction from Videos Using Geometric Context and Occlusion Boundaries
Venue: arXiv cs.CV 2015
Year: 2015

We present an algorithm to estimate depth in dynamic video scenes. We propose to learn and infer depth in videos from appearance, motion, occlusion boundaries, and geometric context of the scene. Using our method, depth can be estimated from unconstrained videos with no requirement of camera pose estimation, and with significant background/foreground motions. We start by decomposing a video into spatio-temporal regions. For each spatio-temporal region, we learn the relationship of depth to visual appearance, motion, and geometric classes. Then we infer the depth information of new scenes using piecewise planar parametrization estimated within a Markov random field (MRF) framework by combining appearance to depth learned mappings and occlusion boundary guided smoothness constraints. Subsequently, we perform temporal smoothing to obtain temporally consistent depth maps. To evaluate our depth estimation algorithm, we provide a novel dataset with ground truth depth for outdoor video scenes. We present a thorough evaluation of our algorithm on our new dataset and the publicly available Make3d static image dataset.
Varieties of Unranked Tree Languages
Venue: arXiv cs.FL 2015
Year: 2015

We study varieties that contain unranked tree languages over all alphabets. Trees are labeled with symbols from two alphabets, an unranked operator alphabet and an alphabet used for leaves only. Syntactic algebras of unranked tree languages are defined similarly as for ranked tree languages, and an unranked tree language is shown to be recognizable iff its syntactic algebra is regular, i.e., a finite unranked algebra in which the operations are defined by regular languages over its set of elements. We establish a bijective correspondence between varieties of unranked tree languages and varieties of regular algebras. For this, we develop a basic theory of unranked algebras in which algebras over all operator alphabets are considered together. Finally, we show that the natural unranked counterparts of several general varieties of ranked tree languages form varieties in our sense. This work parallels closely the theory of general varieties of ranked tree languages and general varieties of finite algebras, but many nontrivial modifications are required. For example, principal varieties as the basic building blocks of varieties of tree languages have to be replaced by what we call quasi-principal varieties, and we device a general scheme for defining these by certain systems of congruences.
PMU-Based Estimation of Dynamic State Jacobian Matrix
Venue: arXiv cs.SY 2015
Year: 2015

In this paper, a hybrid measurement and model-based method is proposed which can estimate the dynamic state Jacobian matrix in near real-time. The proposed method is computationally efficient and robust to the variation of network topology. Since the estimated Jacobian matrix carries significant information on system dynamics and states, it can be utilized in various applications. In particular, two application of the estimated Jacobian matrix in online oscillation analysis, stability monitoring and control are illustrated with numerical examples. In addition, a side-product of the proposed method can facilitate model validation by approximating the damping of generators.
RRH clustering and transmit precoding for interference-limited 5G CRAN downlink
Venue: arXiv cs.IT 2015
Year: 2015

In this work, we consider cloud RAN architecture and focus on the downlink of an antenna domain (AD) exposed to external interference from neighboring ADs. With system sum-rate as performance metric, and assuming that perfect channel state information is available at the aggregation node (AN), we implement i) a greedy user association algorithm, and ii) a greedy remote radio-head (RRH) clustering algorithm at the AN. We then vary the size of individual RRH clusters, and evaluate and compare the sum-rate gains due to two distinct transmit precoding schemes namely i) zero forcing beamforming (ZFBF), ii) coordinated beamforming (CB), when exposed to external interference of same kind. From system-level simulation results, we learn that in an interference-limited regime: i) RRH clustering helps, i.e., {\it cost-adjusted} performance when RRHs cooperate is superior to the performance when they don't, ii) for transmit precoding, the CB scheme is to be preferred over the ZFBF scheme. Finally, we discuss in detail the cost of RRH clustering, i.e., the piloting overhead (and the elements driving it), incorporate its impact on system sum-rate, and discuss its implications on the baseband processing capabilities of the RRHs.
Faster Exact and Parameterized Algorithm for Feedback Vertex Set in Tournaments
Venue: arXiv cs.DS 2015
Year: 2015

A tournament is a directed graph T such that every pair of vertices are connected by an arc. A feedback vertex set is a set S of vertices in T such that T - S is acyclic. In this article we consider the Feedback Vertex Set problem in tournaments. Here input is a tournament T and integer k, and the task is to determine whether T has a feedback vertex set of size at most k. We give a new algorithm for Feedback Vertex Set in Tournaments. The running time of our algorithm is upper bounded by O(1.618^k + n^{O(1)}) and by O(1.46^n). Thus our algorithm simultaneously improves over the fastest known parameterized algorithm for the problem by Dom et al. running in time O(2^kk^{O(1)} + n^{O(1)}), and the fastest known exact exponential time algorithm by Gaspers and Mnich with running time O(1.674^n). On the way to prove our main result we prove a new partitioning theorem for undirected graphs. In particular we show that the vertices of any undirected m-edge graph of maximum degree d can be colored white or black in such a way that for each of the two colors, the number of edges with both endpoints of that color is between m/4-d/2 and m/4+d/4.
Full Duplex Assisted Inter-cell Interference Cancellation in Heterogeneous Networks
Venue: arXiv cs.IT 2015
Year: 2015

The paper studies the suppression of cross-tier inter-cell interference (ICI) generated by a macro base station (MBS) to pico user equipments (PUEs) in heterogeneous networks (HetNets). Different from existing ICI avoidance schemes such as enhanced ICI cancellation (eICIC) and coordinated beamforming, which generally operate at the MBS, we propose a full duplex (FD) assisted ICI cancellation (fICIC) scheme, which can operate at each pico BS (PBS) individually and is transparent to the MBS. The basic idea of the fICIC is to apply FD technique at the PBS such that the PBS can send the desired signals and forward the listened cross-tier ICI simultaneously to PUEs. We first consider the narrowband single-user case, where the MBS serves a single macro UE and each PBS serves a single PUE. We obtain the closed-form solution of the optimal fICIC scheme, and analyze its asymptotical performance in ICI-dominated scenario. We then investigate the general narrowband multi-user case, where both MBS and PBSs serve multiple UEs. We devise a low-complexity algorithm to optimize the fICIC aimed at maximizing the downlink sum rate of the PUEs subject to user fairness constraint. Finally, the generalization of the fICIC to wideband systems is investigated. Simulations validate the analytical results and demonstrate the advantages of the fICIC on mitigating cross-tier ICI.
Expanders via Local Edge Flips
Venue: arXiv cs.DS 2015
Year: 2015

Designing distributed and scalable algorithms to improve network connectivity is a central topic in peer-to-peer networks. In this paper we focus on the following well-known problem: given an $n$-node $d$-regular network for $d=Ω(\log n)$, we want to design a decentralized, local algorithm that transforms the graph into one that has good connectivity properties (low diameter, expansion, etc.) without affecting the sparsity of the graph. To this end, Mahlmann and Schindelhauer introduced the random "flip" transformation, where in each time step, a random pair of vertices that have an edge decide to `swap a neighbor'. They conjectured that performing $O(n d)$ such flips at random would convert any connected $d$-regular graph into a $d$-regular expander graph, with high probability. However, the best known upper bound for the number of steps is roughly $O(n^{17} d^{23})$, obtained via a delicate Markov chain comparison argument. Our main result is to prove that a natural instantiation of the random flip produces an expander in at most $O(n^2 d^2 \sqrt{\log n})$ steps, with high probability. Our argument uses a potential-function analysis based on the matrix exponential, together with the recent beautiful results on the higher-order Cheeger inequality of graphs. We also show that our technique can be used to analyze another well-studied random process known as the `random switch', and show that it produces an expander in $O(n d)$ steps with high probability.
An O(log k log^2 n)-competitive Randomized Algorithm for the k-Sever Problem
Venue: arXiv cs.DS 2015
Year: 2015

In this paper, we show that there is an O(log k log^2 n)-competitive randomized algorithm for the k-sever problem on any metric space with n points, which improved the previous best competitive ratio O(log^2 k log^3 n log log n) by Nikhil Bansal et al. (FOCS 2011, pages 267-276).
Research on Anonymization and De-anonymization in the Bitcoin System
Venue: arXiv cs.CR 2015
Year: 2015

The Bitcoin system is an anonymous, decentralized crypto-currency. There are some deanonymizating techniques to cluster Bitcoin addresses and to map them to users' identifications in the two research directions of Analysis of Transaction Chain (ATC) and Analysis of Bitcoin Protocol and Network (ABPN). Nowadays, there are also some anonymization methods such as coin-mixing and transaction remote release (TRR) to cover the relationship between Bitcoin address and the user. This paper studies anonymization and de-anonymization technologies and proposes some directions for further research.
Automation of Smartphone Traffic Generation in a Virtualized Environment
Venue: arXiv cs.NI 2015
Year: 2015

Scalable and comprehensive analysis of rapidly evolving mobile device application traffic is extremely important but a challenging problem for the Deep Packet Inspection (DPI) engines to perform effective policy management. We present a test framework in which a test driver can automate/orchestrate traffic generation by invoking appropriate method (intent) of real mobile applications (as opposed to traffic replay) in regression or functional testing of mobile application traffic analysis engines in a virtualized environment, without real hardware. We demonstrate the concept by automating a real-time Skype call through a DPI engine in a virtual test setup using Android VMs.
Optimal Caching Placement for D2D Assisted Wireless Caching Networks
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we devise the optimal caching placement to maximize the offloading probability for a two-tier wireless caching system, where the helpers and a part of users have caching ability. The offloading comes from the local caching, D2D sharing and the helper transmission. In particular, to maximize the offloading probability we reformulate the caching placement problem for users and helpers into a difference of convex (DC) problem which can be effectively solved by DC programming. Moreover, we analyze the two extreme cases where there is only help-tier caching network and only user-tier. Specifically, the placement problem for the helper-tier caching network is reduced to a convex problem, and can be effectively solved by the classical water-filling method. We notice that users and helpers prefer to cache popular contents under low node density and prefer to cache different contents evenly under high node density. Simulation results indicate a great performance gain of the proposed caching placement over existing approaches.