OpenRaiser/Intern-Atlas huggingface dataset:
Efficient CTL Verification via Horn Constraints Solving
Venue: arXiv cs.LO 2016
Year: 2016

The use of temporal logics has long been recognised as a fundamental approach to the formal specification and verification of reactive systems. In this paper, we take on the problem of automatically verifying a temporal property, given by a CTL formula, for a given (possibly infinite-state) program. We propose a method based on encoding the problem as a set of Horn constraints. The method takes a program, modeled as a transition system, and a property given by a CTL formula as input. It first generates a set of forall-exists quantified Horn constraints and well-foundedness constraints by exploiting the syntactic structure of the CTL formula. Then, the generated set of constraints are solved by applying an off-the-shelf Horn constraints solving engine. The program is said to satisfy the property if and only if the generated set of constraints has a solution. We demonstrate the practical promises of the method by applying it on a set of challenging examples. Although our method is based on a generic Horn constraint solving engine, it is able to outperform state-of-art methods specialised for CTL verification.
Solving non-linear Horn clauses using a linear Horn clause solver
Venue: arXiv cs.PL 2016
Year: 2016

In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion of tree dimension, which we apply to a set of non-linear clauses, yielding a set whose derivation trees have bounded dimension. Such a set of clauses can be linearised. The main algorithm then proceeds by applying the linearisation transformation and solver for linear Horn clauses to a sequence of sets of clauses with successively increasing dimension bound. The approach is then further developed by using a solution of clauses of lower dimension to (partially) linearise clauses of higher dimension. We constructed a prototype implementation of this approach and performed some experiments on a set of verification problems, which shows some promise.
Selecting Algorithms for Black Box Matrices: Checking for Matrix Properties That Can Simplify Computations
Venue: arXiv cs.NA 2016
Year: 2016

Processes to automate the selection of appropriate algorithms for various matrix computations are described. In particular, processes to check for, and certify, various matrix properties of black box matrices are presented. These include sparsity patterns and structural properties that allow "superfast" algorithms to be used in place of black-box algorithms. Matrix properties that hold generically, and allow the use of matrix preconditioning to be reduced or eliminated, can also be checked for and certified - notably including in the small-field case, where this presently has the greatest impact on the efficiency of the computation.
Number representations and term rewriting
Venue: arXiv cs.LO 2016
Year: 2016

In this paper we examine a number of term rewriting system for integer number representations, building further upon the datatype defining systems described in [2]. In particular, we look at automated methods for proving confluence and termination in binary and decimal term rewriting systems for both append and tree constructor functions. We find that some of these term rewriting systems are not strongly terminating, which we resolve with minor changes to these systems. Moreover, most of the term rewriting systems discussed do not exhibit the confluence property, which seems more difficult to resolve.
Black Box Linear Algebra: Extending Wiedemann's Analysis of a Sparse Matrix Preconditioner for Computations over Small Fields
Venue: arXiv cs.NA 2016
Year: 2016

Wiedemann's paper, introducing his algorithm for sparse and structured matrix computations over arbitrary fields, also presented a pair of matrix preconditioners for computations over small fields. The analysis of the second of these is extended in order to provide more explicit statements of the expected number of nonzero entries in the matrices obtained as well as bounds on the probability that such matrices have maximal rank. This is part of ongoing work to establish that this matrix preconditioner can also be used to bound the number of nontrivial nilpotent blocks in the Jordan normal form of a preconditioned matrix, in such a way that one can also sample uniformly from the null space of the originally given matrix. If successful this will result in a black box algorithm for the type of matrix computation required when using the number field sieve for integer factorization that is provably reliable and - by a small factor - asymptotically more efficient than alternative techniques that make use of other matrix preconditioners or require computations over field extensions.
Automatic Environmental Sound Recognition: Performance versus Computational Cost
Venue: arXiv cs.SD 2016
Year: 2016

In the context of the Internet of Things (IoT), sound sensing applications are required to run on embedded platforms where notions of product pricing and form factor impose hard constraints on the available computing power. Whereas Automatic Environmental Sound Recognition (AESR) algorithms are most often developed with limited consideration for computational cost, this article seeks which AESR algorithm can make the most of a limited amount of computing power by comparing the sound classification performance em as a function of its computational cost. Results suggest that Deep Neural Networks yield the best ratio of sound classification accuracy across a range of computational costs, while Gaussian Mixture Models offer a reasonable accuracy at a consistently small cost, and Support Vector Machines stand between both in terms of compromise between accuracy and computational cost.
Best-case Analysis of MergeSort with an Application to the Sum of Digits Problem, A manuscript (MS) v2
Venue: arXiv cs.DM 2016
Year: 2016

An exact formula \[ B(n) = \frac{n}{2}(\lfloor \lg n \rfloor + 1) - \sum _{k=0} ^{\lfloor \lg n \rfloor} 2^k Zigzag(\frac{n}{2^{k+1}}), \] where \[ Zigzag (x) = \min (x - \lfloor x \rfloor, \lceil x \rceil - x), \] for the minimal number $ B(n) $ of comparisons of keys performed by $ {\tt MergeSort} $ on an $ n $-element array is derived and analyzed. The said formula is less complex than any other known formula for the same and can be evaluated in $ O(\log ^{c}) $ time, where $ c $ is a constant. It is shown that there is no closed-form formula for the above. Since the recurrence relation for the minimal number of comparisons of keys for $ {\tt MergeSort} $ is identical with a recurrence relation for the number of 1s in binary expansions of all integers between $ 0 $ and $ n $ (exclusively), the above results extend to the sum of binary digits problem.
Identification of promising research directions using machine learning aided medical literature analysis
Venue: arXiv cs.CL 2016
Year: 2016

The rapidly expanding corpus of medical research literature presents major challenges in the understanding of previous work, the extraction of maximum information from collected data, and the identification of promising research directions. We present a case for the use of advanced machine learning techniques as an aide in this task and introduce a novel methodology that is shown to be capable of extracting meaningful information from large longitudinal corpora, and of tracking complex temporal changes within it.
Core spaces, sector spaces and fan spaces: a topological approach to domain theory
Venue: arXiv cs.LO 2016
Year: 2016

We present old and new characterizations of core spaces, alias worldwide web spaces, originally defined by the existence of supercompact neighborhood bases. The patch spaces of core spaces, obtained by joining the original topology with a second topology having the dual specialization order, are the so-called sector spaces, which have good convexity and separation properties and determine the original space. The category of core spaces is shown to be concretely isomorphic to the category of fan spaces; these are certain quasi-ordered spaces having neighborhood bases of so-called fans, obtained by deleting a finite number of principal filters from a principal filter. This approach has useful consequences for domain theory. In fact, endowed with the Scott topology, the continuous domains are nothing but the sober core spaces, and endowed with the Lawson topology, they are the corresponding fan spaces. We generalize the characterization of continuous lattices as meet-continuous lattices with T$_2$ Lawson topology and extend the Fundamental Theorem of Compact Semilattices to non-complete structures. Finally, we investigate cardinal invariants like density and weight of the involved objects.
Embedding LTE-U within Wi-Fi Bands for Spectrum Efficiency Improvement
Venue: arXiv cs.IT 2016
Year: 2016

Driven by growing spectrum shortage, Long-term Evolution in unlicensed spectrum (LTE-U) has recently been proposed as a new paradigm to deliver better performance and experience for mobile users by extending the LTE protocol to unlicensed spectrum. In the paper, we first present a comprehensive overview of the LTE-U technology, and discuss the practical challenges it faces. We summarize the existing LTE-U operation modes and analyze several means for LTE-U coexistence with Wi-Fi medium access control protocols. We further propose a novel hyper access-point (HAP) that integrates the functionalities of LTE small cell base station and commercial Wi-Fi AP for deployment by cellular network operators. Our proposed LTE-U access embedding within the Wi-Fi protocol is non-disruptive to unlicensed Wi-Fi nodes and demonstrates performance benefits as a seamless and novel LTE and Wi-Fi coexistence technology in unlicensed band. We provide results to demonstrate the performances advantage of this novel LTE-U proposal.
Stochastic Recursive Inclusions with Non-Additive Iterate-Dependent Markov Noise
Venue: arXiv cs.SY 2016
Year: 2016

In this paper we study the asymptotic behavior of stochastic approximation schemes with set-valued drift function and non-additive iterate-dependent Markov noise. We show that a linearly interpolated trajectory of such a recursion is an asymptotic pseudotrajectory for the flow of a limiting differential inclusion obtained by averaging the set-valued drift function of the recursion w.r.t. the stationary distributions of the Markov noise. The limit set theorem in [1] is then used to characterize the limit sets of the recursion in terms of the dynamics of the limiting differential inclusion. We then state two variants of the Markov noise assumption under which the analysis of the recursion is similar to the one presented in this paper. Scenarios where our recursion naturally appears are presented as applications. These include controlled stochastic approximation, subgradient descent, approximate drift problem and analysis of discontinuous dynamics all in the presence of non-additive iterate-dependent Markov noise.
Exploiting Multi-modal Curriculum in Noisy Web Data for Large-scale Concept Learning
Venue: arXiv cs.CV 2016
Year: 2016

Learning video concept detectors automatically from the big but noisy web data with no additional manual annotations is a novel but challenging area in the multimedia and the machine learning community. A considerable amount of videos on the web are associated with rich but noisy contextual information, such as the title, which provides weak annotations or labels about the video content. To leverage the big noisy web labels, this paper proposes a novel method called WEbly-Labeled Learning (WELL), which is established on the state-of-the-art machine learning algorithm inspired by the learning process of human. WELL introduces a number of novel multi-modal approaches to incorporate meaningful prior knowledge called curriculum from the noisy web videos. To investigate this problem, we empirically study the curriculum constructed from the multi-modal features of the videos collected from YouTube and Flickr. The efficacy and the scalability of WELL have been extensively demonstrated on two public benchmarks, including the largest multimedia dataset and the largest manually-labeled video set. The comprehensive experimental results demonstrate that WELL outperforms state-of-the-art studies by a statically significant margin on learning concepts from noisy web video data. In addition, the results also verify that WELL is robust to the level of noisiness in the video data. Notably, WELL trained on sufficient noisy web labels is able to achieve a comparable accuracy to supervised learning methods trained on the clean manually-labeled data.
Cyber Attack Surface Analysis of Advanced Metering Infrastructure
Venue: arXiv cs.CR 2016
Year: 2016

Cyber attacks on critical infrastructure have been an issue of importance in industry over the past several years, as well as a focus of academic research. Cyber attacks of various types and magnitude have been on the rise targeted specifically at power grids. A successful attack on the power grid could result in significant impacts including grid shutdown, cascading failures, damage to the infrastructure, and potential harm to people. Power grid infrastructure are critical in nature, they enable operations for residential, commercial, industrial, and government users across critical infrastructure such as water, communication, banking, transportation, manufacturing, and more. The compromise of these operations introduces threats, which span from economic to public safety. The Advanced Metering Infrastructure (AMI) is now being rapidly deployed throughout the power grid, and is an enabling technology for smart grid. Identifying the attack surface is a necessary step in achieving cyber security in smart grids and AMI. The purpose of this paper is to quantify and examine the cyber attack surface of AMI in order to lay the foundation for mitigating approaches to AMI cyber security.
Coordinated Optimization at a Hydro Generating Plant by Software Agents
Venue: arXiv cs.SY 2016
Year: 2016

The architecture is developed for incorporating a software agent into the existing control system of a river-based hydro generating plant. The software agent will utilize a rule-based system for ease of integration. Optimization for increased power production is presented, initially for a single generating unit. An enhancement to facilitate the constraints of river level and flow by an external user as well as the goals of corporate dispatching is then developed through the existing SCADA system. Finally, expansion to coordinate multiple hydro units at a single location is presented.
New Software Metrics for Evaluation and Comparison of Advanced Power Management Systems
Venue: arXiv cs.SE 2016
Year: 2016

A set of software metrics for the evaluation of power management systems (PMSs) is presented. Such systems for managing power need to be autonomous, scalable, low in complexity, and comprised of portable algorithms in order to be well applied across the varying implementations that utilize power systems. Although similar metrics exist for software in general, their definitions do not readily lend themselves to the unique characteristics of power management systems or systems of similar architecture.
Gland Instance Segmentation by Deep Multichannel Neural Networks
Venue: arXiv cs.CV 2016
Year: 2016

In this paper, we propose a new image instance segmentation method that segments individual glands (instances) in colon histology images. This is a task called instance segmentation that has recently become increasingly important. The problem is challenging since not only do the glands need to be segmented from the complex background, they are also required to be individually identified. Here we leverage the idea of image-to-image prediction in recent deep learning by building a framework that automatically exploits and fuses complex multichannel information, regional, location and boundary patterns in gland histology images. Our proposed system, deep multichannel framework, alleviates heavy feature design due to the use of convolutional neural networks and is able to meet multifarious requirement by altering channels. Compared to methods reported in the 2015 MICCAI Gland Segmentation Challenge and other currently prevalent methods of instance segmentation, we observe state-of-the-art results based on a number of evaluation metrics.
Fully Dynamic de Bruijn Graphs
Venue: arXiv cs.DS 2016
Year: 2016

We present a space- and time-efficient fully dynamic implementation de Bruijn graphs, which can also support fixed-length jumbled pattern matching.
Sparse Representation-Based Classification: Orthogonal Least Squares or Orthogonal Matching Pursuit?
Venue: arXiv cs.CV 2016
Year: 2016

Spare representation of signals has received significant attention in recent years. Based on these developments, a sparse representation-based classification (SRC) has been proposed for a variety of classification and related tasks, including face recognition. Recently, a class dependent variant of SRC was proposed to overcome the limitations of SRC for remote sensing image classification. Traditionally, greedy pursuit based method such as orthogonal matching pursuit (OMP) are used for sparse coefficient recovery due to their simplicity as well as low time-complexity. However, orthogonal least square (OLS) has not yet been widely used in classifiers that exploit the sparse representation properties of data. Since OLS produces lower signal reconstruction error than OMP under similar conditions, we hypothesize that more accurate signal estimation will further improve the classification performance of classifiers that exploiting the sparsity of data. In this paper, we present a classification method based on OLS, which implements OLS in a classwise manner to perform the classification. We also develop and present its kernelized variant to handle nonlinearly separable data. Based on two real-world benchmarking hyperspectral datasets, we demonstrate that class dependent OLS based methods outperform several baseline methods including traditional SRC and the support vector machine classifier.
Adaptive control for trailing arm suspension with hydraulic cylinder spring under practical constraints
Venue: arXiv cs.SY 2016
Year: 2016

This paper presents an adaptive control strategy with LQ control of a quarter-car, which is ameliorated to smoothly follow the dynamically changing reference arm angle, in order to omit the heave sensor in this study. Linearized plant parameters are initially derived from model equation and then estimated by online estimator. LQ control method provides optimal control effort with corresponding estimated plant parameters. The results of the simulation are depicted in time domain. Weighted RMS values of the consequences are suggested to assess the efficiency of the controller. Different road conditions are considered in order to reveal the performance of the controller in detail.
Rotation-k Affine-Power-Affine-like Multiple Substitution-Boxes for Secure Communication
Venue: arXiv cs.CR 2016
Year: 2016

Substitution boxes with thorough cryptographic strengths are essential for the development of strong encryption systems. They are the only portions capable of inducing nonlinearity in symmetric encryption systems. Bijective substitution boxes having both high nonlinearities and high algebraic complexities are the most desirable to thwart linear, differential and algebraic attacks. In this paper, a method of constructing algebraically complex and cryptographically potent multiple substitution boxes is proposed. The multiple substitution boxes are synthesized by applying the concept of rotation-k approach on the affine-power-affine structure. It is shown that the rotation-k approach inherits all the features of affine-power-affine structure. Performance assessment of all the proposed substitution boxes is done against nonlinearity, strict avalanche criteria, bits independent criteria, differential probability, linear approximation probability and algebraic complexity. It has been found that the proposed substitution boxes have outstanding cryptographic characteristics and outperform the various recent substitution boxes.
A Markov Chain Model for the Decoding Probability of Sparse Network Coding
Venue: arXiv cs.NI 2016
Year: 2016

Random Linear Network Coding (RLNC) has been proved to offer an efficient communication scheme, leveraging an interesting robustness against packet losses. However, it suffers from a high computational complexity and some novel approaches, which follow the same idea, have been recently proposed. One of such solutions is Tunable Sparse Network Coding (TSNC), where only few packets are combined in each transmissions. The amount of data packets to be combined in each transmissions can be set from a density parameter/distribution, which could be eventually adapted. In this work we present an analytical model that captures the performance of SNC on an accurate way. We exploit an absorbing Markov process where the states are defined by the number of useful packets received by the decoder, i.e the decoding matrix rank, and the number of non-zero columns at such matrix. The model is validated by means of a thorough simulation campaign, and the difference between model and simulation is negligible. A mean square error less than $4 \cdot 10^{-4}$ in the worst cases. We also include in the comparison some of more general bounds that have been recently used, showing that their accuracy is rather poor. The proposed model would enable a more precise assessment of the behavior of sparse network coding techniques. The last results show that the proposed analytical model can be exploited by the TSNC techniques in order to select by the encoder the best density as the transmission evolves.
Algorithmic Trading: A brief, computational finance case study on data centre FPGAs
Venue: arXiv cs.DC 2016
Year: 2016

Increasingly FPGAs will be deployed at scale due to the need for increased need for power efficient computation and improved high level synthesis tool flows, creating a new category of device: data centre FPGAs. A method for using these FPGAs is to identify what proportion of a given workload would benefit from being implemented upon the available FPGAs while minimising communication off-chip. As part of the implementation of these tasks, care should be taken in identifying the parallel execution mode, task or pipeline parallelism that should be used. When considering a case study of computational finance tasks, a benchmark workload of Heston and Black-Scholes-based options implemented using OpenCL and OpenSPL, the benefit of this method of using data centre FPGAs is illustrated. These devices deliver latency performance close to that of workstation grade GPUs, while requiring considerably less energy, resulting in 30% more floating point operations per Joule of energy consumed.