OpenRaiser/Intern-Atlas huggingface dataset:
Tree Buffers
Venue: arXiv cs.DS 2015
Year: 2015

In runtime verification, the central problem is to decide if a given program execution violates a given property. In online runtime verification, a monitor observes a program's execution as it happens. If the program being observed has hard real-time constraints, then the monitor inherits them. In the presence of hard real-time constraints it becomes a challenge to maintain enough information to produce error traces, should a property violation be observed. In this paper we introduce a data structure, called tree buffer, that solves this problem in the context of automata-based monitors: If the monitor itself respects hard real-time constraints, then enriching it by tree buffers makes it possible to provide error traces, which are essential for diagnosing defects. We show that tree buffers are also useful in other application domains. For example, they can be used to implement functionality of capturing groups in regular expressions. We prove optimal asymptotic bounds for our data structure, and validate them using empirical data from two sources: regular expression searching through Wikipedia, and runtime verification of execution traces obtained from the DaCapo test suite.
On the Lovász Theta function for Independent Sets in Sparse Graphs
Venue: arXiv cs.DS 2015
Year: 2015

We consider the maximum independent set problem on graphs with maximum degree~$d$. We show that the integrality gap of the Lovász $\vartheta$-function based SDP is $\widetilde{O}(d/\log^{3/2} d)$. This improves on the previous best result of $\widetilde{O}(d/\log d)$, and almost matches the integrality gap of $\widetilde{O}(d/\log^2 d)$ recently shown for stronger SDPs, namely those obtained using poly-$(\log(d))$ levels of the $SA^+$ semidefinite hierarchy. The improvement comes from an improved Ramsey-theoretic bound on the independence number of $K_r$-free graphs for large values of $r$. We also show how to obtain an algorithmic version of the above-mentioned $SA^+$-based integrality gap result, via a coloring algorithm of Johansson. The resulting approximation guarantee of $\widetilde{O}(d/\log^2 d)$ matches the best unique-games-based hardness result up to lower-order poly-$(\log\log d)$ factors.
Partial Order Reduction for Security Protocols
Venue: arXiv cs.CR 2015
Year: 2015

Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g., anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools. In this paper, we overcome this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.
Rover-to-Orbiter Communication in Mars: Taking Advantage of the Varying Topology
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we study the communication problem from rovers on Mars' surface to Mars-orbiting satellites. We first justify that, to a good extent, the rover-to-orbiter communication problem can be modelled as communication over a $2 \times 2$ X-channel with the network topology varying over time. For such a fading X-channel where transmitters are only aware of the time-varying topology but not the time-varying channel state (i.e., no CSIT), we propose coding strategies that code across topologies, and develop upper bounds on the sum degrees-of-freedom (DoF) that is shown to be tight under certain pattern of the topology variation. Furthermore we demonstrate that the proposed scheme approximately achieves the ergodic sum-capacity of the network. Using the proposed coding scheme, we numerically evaluate the ergodic rate gain over a time-division-multiple-access (TDMA) scheme for Rayleigh and Rice fading channels. We also numerically demonstrate that with practical orbital parameters, a 9.6% DoF gain, as well as more than 11.6% throughput gain can be achieved for a rover-to-orbiter communication network.
Design and Implementation of an Integrated Information System to Support Scientific Research
Venue: arXiv cs.DL 2015
Year: 2015

Computerization of research activities led to the creation of large specialized information resources, platforms, services and software to support scientific research. However, their shortcomings do not allow to fully realizing the comprehensive support of scientific activity, and the absence of a single entry point to divide the scientific community fragmented groups interests. The article based on analysing the existing solutions and approaches to the tools of information and communication technologies of various types of scientific activity, and taking into account the research lifecycle proposed and formulated the basic principles of designing and implementing an integrated information system to support scientific research.
Rooted Cycle Bases
Venue: arXiv cs.DS 2015
Year: 2015

A cycle basis in an undirected graph is a minimal set of simple cycles whose symmetric differences include all Eulerian subgraphs of the given graph. We define a rooted cycle basis to be a cycle basis in which all cycles contain a specified root edge, and we investigate the algorithmic problem of constructing rooted cycle bases. We show that a given graph has a rooted cycle basis if and only if the root edge belongs to its 2-core and the 2-core is 2-vertex-connected, and that constructing such a basis can be performed efficiently. We show that in an unweighted or positively weighted graph, it is possible to find the minimum weight rooted cycle basis in polynomial time. Additionally, we show that it is NP-complete to find a fundamental rooted cycle basis (a rooted cycle basis in which each cycle is formed by combining paths in a fixed spanning tree with a single additional edge) but that the problem can be solved by a fixed-parameter-tractable algorithm when parameterized by clique-width.
Algorithmic statistics revisited
Venue: arXiv cs.IT 2015
Year: 2015

The mission of statistics is to provide adequate statistical hypotheses (models) for observed data. But what is an "adequate" model? To answer this question, one needs to use the notions of algorithmic information theory. It turns out that for every data string $x$ one can naturally define "stochasticity profile", a curve that represents a trade-off between complexity of a model and its adequacy. This curve has four different equivalent definitions in terms of (1)~randomness deficiency, (2)~minimal description length, (3)~position in the lists of simple strings and (4)~Kolmogorov complexity with decompression time bounded by busy beaver function. We present a survey of the corresponding definitions and results relating them to each other.
Vector Linear Error Correcting Index Codes and Discrete Polymatroids
Venue: arXiv cs.IT 2015
Year: 2015

The connection between index coding and matroid theory have been well studied in the recent past. El Rouayheb et al. established a connection between multi linear representation of matroids and wireless index coding. Muralidharan and Rajan showed that a vector linear solution to an index coding problem exists if and only if there exists a representable discrete polymatroid satisfying certain conditions. Recently index coding with erroneous transmission was considered by Dau et al.. Error correcting index codes in which all receivers are able to correct a fixed number of errors was studied. In this paper we consider a more general scenario in which each receiver is able to correct a desired number of errors, calling such index codes differential error correcting index codes. We show that vector linear differential error correcting index code exists if and only if there exists a representable discrete polymatroid satisfying certain conditions
On the Number of Optimal Index Codes
Venue: arXiv cs.IT 2015
Year: 2015

In Index coding there is a single sender with multiple messages and multiple receivers each wanting a different set of messages and knowing a different set of messages a priori. The Index Coding problem is to identify the minimum number of transmissions (optimal length) to be made so that all receivers can decode their wanted messages using the transmitted symbols and their respective prior information and also the codes with optimal length. Recently it was shown that different optimal length codes perform differently in a wireless channel. Towards identifying the best optimal length index code one needs to know the number of optimal length index codes. In this paper we present results on the number of optimal length index codes making use of the representation of an index coding problem by an equivalent network code. We give the minimum number of codes possible with the optimal length. This is done using a simpler algebraic formulation of the problem compared to the approach of Koetter and Medard.
Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions
Venue: arXiv cs.PL 2015
Year: 2015

In this paper we turn the spotlight on a class of lexicographic ranking functions introduced by Bradley, Manna and Sipma in a seminal CAV 2005 paper, and establish for the first time the complexity of some problems involving the inference of such functions for linear-constraint loops (without precondition). We show that finding such a function, if one exists, can be done in polynomial time in a way which is sound and complete when the variables range over the rationals (or reals). We show that when variables range over the integers, the problem is harder -- deciding the existence of a ranking function is coNP-complete. Next, we study the problem of minimizing the number of components in the ranking function (a.k.a. the dimension). This number is interesting in contexts like computing iteration bounds and loop parallelization. Surprisingly, and unlike the situation for some other classes of lexicographic ranking functions, we find that even deciding whether a two-component ranking function exists is harder than the unrestricted problem: NP-complete over the rationals and $Σ^P_2$-complete over the integers.
Resource Management and Cell Planning in Millimeter-Wave Overlaid Ultra-Dense Cellular Networks
Venue: arXiv cs.NI 2015
Year: 2015

This paper proposes a cellular network exploiting millimeter-wave (mmWave) and ultra-densified base stations (BSs) to achieve the far-reaching 5G aim in downlink average rate. The mmWave overlaid network however incurs a pitfall that its ample data rate is only applicable for downlink transmissions due to the implementation difficulty at mobile users, leading to an immense difference between uplink and downlink rates. We therefore turn our attention not only to maximize downlink rate but also to ensure the minimum uplink rate. With this end, we firstly derive the mmWave overlaid ultra-dense cellular network spectral efficiencies for both uplink and downlink cases in closed forms by using stochastic geometry via a lower bound approximation. In a practical scenario, such tractable results of the proposed network reveal that incumbent micro-wave ($μ$Wave) cellular resource should be mostly dedicated to uplink transmissions in order to correspond with the mmWave downlink rate improvement. Furthermore, increasing uplink rate via $μ$Wave BS densification cannot solely cope with the mmWave downlink/uplink rate asymmetry, and thus requires additional $μ$Wave spectrum in 5G cellular networks.
Adaptive stochastic resonance based on output autocorrelations
Venue: arXiv cs.IT 2015
Year: 2015

Successful detection of weak signals is a universal challenge for numerous technical and biological systems and crucially limits signal transduction and transmission. Stochastic resonance (SR) has been identified to have the potential to tackle this problem, namely to enable non-linear systems to detect small, otherwise sub-threshold signals by means of added non-zero noise. This has been demonstrated within a wide range of systems in physical, technological and biological contexts. Based on its ubiquitous importance, numerous theoretical and technical approaches aim at an optimization of signal transduction based on SR. Several quantities like mutual information, signal-to-noise-ratio, or the cross-correlation between input stimulus and resulting detector response have been used to determine optimal noise intensities for SR. The fundamental shortcoming with all these measures is that knowledge of the signal to be detected is required to compute them. This dilemma prevents the use of adaptive SR procedures in any application where the signal to be detected is unknown. We here show that the autocorrelation function (AC) of the detector response fundamentally overcomes this drawback. For a simplified model system, the equivalence of the output AC with the measures mentioned above is proven analytically. In addition, we test our approach numerically for a variety of systems comprising different input signals and different types of detectors. The results indicate a strong similarity between mutual information and output AC in terms of the optimal noise intensity for SR. Hence, using the output AC to adaptively vary the amount of added noise in order to maximize information transmission via SR might be a fundamental processing principle in nature, in particular within neural systems which could be implemented in future technical applications.
Density Criteria for the Identification of Linear Time-Varying Systems
Venue: arXiv cs.IT 2015
Year: 2015

This paper addresses the problem of identifying a linear time-varying (LTV) system characterized by a (possibly infinite) discrete set of delays and Doppler shifts. We prove that stable identifiability is possible if the upper uniform Beurling density of the delay-Doppler support set is strictly smaller than 1/2 and stable identifiability is impossible for densities strictly larger than 1/2. The proof of this density theorem reveals an interesting relation between LTV system identification and interpolation in the Bargmann-Fock space. Finally, we introduce a subspace method for solving the system identification problem at hand.
Conservativity of embeddings in the lambda Pi calculus modulo rewriting (long version)
Venue: arXiv cs.LO 2015
Year: 2015

The lambda Pi calculus can be extended with rewrite rules to embed any functional pure type system. In this paper, we show that the embedding is conservative by proving a relative form of normalization, thus justifying the use of the lambda Pi calculus modulo rewriting as a logical framework for logics based on pure type systems. This result was previously only proved under the condition that the target system is normalizing. Our approach does not depend on this condition and therefore also works when the source system is not normalizing.
Constructions of Fast-Decodable Distributed Space-Time Codes
Venue: arXiv cs.IT 2015
Year: 2015

Fast-decodable distributed space-time codes are constructed by adapting the iterative code construction introduced in [1] to the N -relay multiple-input multiple-output channel, leading to the first fast-decodable distributed space-time codes for more than one antenna per user. Explicit constructions are provided alongside with a performance comparison to non-iterated (non-) fast-decodable codes.
Hybrid Genetic Algorithm and Lasso Test Approach for Inferring Well Supported Phylogenetic Trees based on Subsets of Chloroplastic Core Genes
Venue: arXiv cs.AI 2015
Year: 2015

The amount of completely sequenced chloroplast genomes increases rapidly every day, leading to the possibility to build large scale phylogenetic trees of plant species. Considering a subset of close plant species defined according to their chloroplasts, the phylogenetic tree that can be inferred by their core genes is not necessarily well supported, due to the possible occurrence of "problematic" genes (i.e., homoplasy, incomplete lineage sorting, horizontal gene transfers, etc.) which may blur phylogenetic signal. However, a trustworthy phylogenetic tree can still be obtained if the number of problematic genes is low, the problem being to determine the largest subset of core genes that produces the best supported tree. To discard problematic genes and due to the overwhelming number of possible combinations, we propose an hybrid approach that embeds both genetic algorithms and statistical tests. Given a set of organisms, the result is a pipeline of many stages for the production of well supported phylogenetic trees. The proposal has been applied to different cases of plant families, leading to encouraging results for these families.
Iteratively Reweighted $\ell_1$ Approaches to Sparse Composite Regularization
Venue: arXiv cs.IT 2015
Year: 2015

Motivated by the observation that a given signal $\boldsymbol{x}$ admits sparse representations in multiple dictionaries $\boldsymbolΨ_d$ but with varying levels of sparsity across dictionaries, we propose two new algorithms for the reconstruction of (approximately) sparse signals from noisy linear measurements. Our first algorithm, Co-L1, extends the well-known lasso algorithm from the L1 regularizer $\|\boldsymbol{Ψx}\|_1$ to composite regularizers of the form $\sum_d λ_d \|\boldsymbolΨ_d \boldsymbol{x}\|_1$ while self-adjusting the regularization weights $λ_d$. Our second algorithm, Co-IRW-L1, extends the well-known iteratively reweighted L1 algorithm to the same family of composite regularizers. We provide several interpretations of both algorithms: i) majorization-minimization (MM) applied to a non-convex log-sum-type penalty, ii) MM applied to an approximate $\ell_0$-type penalty, iii) MM applied to Bayesian MAP inference under a particular hierarchical prior, and iv) variational expectation-maximization (VEM) under a particular prior with deterministic unknown parameters. A detailed numerical study suggests that our proposed algorithms yield significantly improved recovery SNR when compared to their non-composite L1 and IRW-L1 counterparts.
Multi-swarm PSO algorithm for the Quadratic Assignment Problem: a massive parallel implementation on the OpenCL platform
Venue: arXiv cs.NE 2015
Year: 2015

This paper presents a multi-swarm PSO algorithm for the Quadratic Assignment Problem (QAP) implemented on OpenCL platform. Our work was motivated by results of time efficiency tests performed for single-swarm algorithm implementation that showed clearly that the benefits of a parallel execution platform can be fully exploited, if the processed population is large. The described algorithm can be executed in two modes: with independent swarms or with migration. We discuss the algorithm construction, as well as we report results of tests performed on several problem instances from the QAPLIB library. During the experiments the algorithm was configured to process large populations. This allowed us to collect statistical data related to values of goal function reached by individual particles. We use them to demonstrate on two test cases that although single particles seem to behave chaotically during the optimization process, when the whole population is analyzed, the probability that a particle will select a near-optimal solution grows.
Convolutional Neural Network-Based Image Representation for Visual Loop Closure Detection
Venue: arXiv cs.RO 2015
Year: 2015

Deep convolutional neural networks (CNN) have recently been shown in many computer vision and pattern recog- nition applications to outperform by a significant margin state- of-the-art solutions that use traditional hand-crafted features. However, this impressive performance is yet to be fully exploited in robotics. In this paper, we focus one specific problem that can benefit from the recent development of the CNN technology, i.e., we focus on using a pre-trained CNN model as a method of generating an image representation appropriate for visual loop closure detection in SLAM (simultaneous localization and mapping). We perform a comprehensive evaluation of the outputs at the intermediate layers of a CNN as image descriptors, in comparison with state-of-the-art image descriptors, in terms of their ability to match images for detecting loop closures. The main conclusions of our study include: (a) CNN-based image representations perform comparably to state-of-the-art hand- crafted competitors in environments without significant lighting change, (b) they outperform state-of-the-art competitors when lighting changes significantly, and (c) they are also significantly faster to extract than the state-of-the-art hand-crafted features even on a conventional CPU and are two orders of magnitude faster on an entry-level GPU.
PBF: A New Privacy-Aware Billing Framework for Online Electric Vehicles with Bidirectional Auditability
Venue: arXiv cs.CR 2015
Year: 2015

Recently an online electric vehicle (OLEV) concept has been introduced, where vehicles are propelled through the wirelessly transmitted electrical power from the infrastructure installed under the road while moving. The absence of secure-and-fair billing is one main hurdle to widely adopt this promising technology. This paper introduces a secure and privacy-aware fair billing framework for OLEV on the move through the charging plates installed under the road. We first propose two extreme lightweight mutual authentication mechanisms, a direct authentication and a hash chain-based authentication between vehicles and the charging plates that can be used for different vehicular speeds on the road. Second we propose a secure and privacy-aware wireless power transfer on move for the vehicles with bidirectional auditability guarantee by leveraging game-theoretic approach. Each charging plate transfers a fixed amount of energy to the vehicle and bills the vehicle in a privacy-aware way accordingly. Our protocol guarantees secure, privacy-aware, and fair billing mechanism for the OLEVs while receiving electric power from the road. Moreover our proposed framework can play a vital role in eliminating the security and privacy challenges in the deployment of power transfer technology to the OLEVs.
Viewpoint distortion compensation in practical surveillance systems
Venue: arXiv cs.CV 2015
Year: 2015

Our aim is to estimate the perspective-effected geometric distortion of a scene from a video feed. In contrast to all previous work we wish to achieve this using from low-level, spatio-temporally local motion features used in commercial semi-automatic surveillance systems. We: (i) describe a dense algorithm which uses motion features to estimate the perspective distortion at each image locus and then polls all such local estimates to arrive at the globally best estimate, (ii) present an alternative coarse algorithm which subdivides the image frame into blocks, and uses motion features to derive block-specific motion characteristics and constrain the relationships between these characteristics, with the perspective estimate emerging as a result of a global optimization scheme, and (iii) report the results of an evaluation using nine large sets acquired using existing close-circuit television (CCTV) cameras. Our findings demonstrate that both of the proposed methods are successful, their accuracy matching that of human labelling using complete visual data.