OpenRaiser/Intern-Atlas huggingface dataset:
Modular SIMD arithmetic in Mathemagix
Venue: arXiv cs.MS 2014
Year: 2014

Modular integer arithmetic occurs in many algorithms for computer algebra, cryptography, and error correcting codes. Although recent microprocessors typically offer a wide range of highly optimized arithmetic functions, modular integer operations still require dedicated implementations. In this article, we survey existing algorithms for modular integer arithmetic, and present detailed vectorized counterparts. We also present several applications, such as fast modular Fourier transforms and multiplication of integer polynomials and matrices. The vectorized algorithms have been implemented in C++ inside the free computer algebra and analysis system Mathemagix. The performance of our implementation is illustrated by various benchmarks.
Showing invariance compositionally for a process algebra for network protocols
Venue: arXiv cs.LO 2014
Year: 2014

This paper presents the mechanization of a process algebra for Mobile Ad hoc Networks and Wireless Mesh Networks, and the development of a compositional framework for proving invariant properties. Mechanizing the core process algebra in Isabelle/HOL is relatively standard, but its layered structure necessitates special treatment. The control states of reactive processes, such as nodes in a network, are modelled by terms of the process algebra. We propose a technique based on these terms to streamline proofs of inductive invariance. This is not sufficient, however, to state and prove invariants that relate states across multiple processes (entire networks). To this end, we propose a novel compositional technique for lifting global invariants stated at the level of individual nodes to networks of nodes.
Measuring Atmospheric Scattering from Digital Images of Urban Scenery using Temporal Polarization-Based Vision
Venue: arXiv cs.CV 2014
Year: 2014

Particulate Matter (PM) is a form of air pollution that visually degrades urban scenery and is hazardous to human health and the environment. Current monitoring devices are limited in measuring average PM over large areas. Quantifying the visual effects of haze in digital images of urban scenery and correlating these effects to PM levels is a vital step in more practically monitoring our environment. Current image haze extraction algorithms remove haze from the scene for the sole purpose of enhancing vision. We present two algorithms which bridge the gap between image haze extraction and environmental monitoring. We provide a means of measuring atmospheric scattering from images of urban scenery by incorporating temporal knowledge. In doing so, we also present a method of recovering an accurate depthmap of the scene and recovering the scene without the visual effects of haze. We compare our algorithm to three known haze removal methods. The algorithms are composed of an optimization over a model of haze formation in images and an optimization using a constraint of constant depth over a sequence of images taken over time. These algorithms not only measure atmospheric scattering, but also recover a more accurate depthmap and dehazed image. The measurements of atmospheric scattering this research produces, can be directly correlated to PM levels and therefore pave the way to monitoring the health of the environment by visual means. Accurate atmospheric sensing from digital images is a challenging and under-researched problem. This work provides an important step towards a more practical and accurate visual means of measuring PM from digital images.
Diffusion Adaptation Strategies for Distributed Estimation over Gaussian Markov Random Fields
Venue: arXiv cs.SY 2014
Year: 2014

The aim of this paper is to propose diffusion strategies for distributed estimation over adaptive networks, assuming the presence of spatially correlated measurements distributed according to a Gaussian Markov random field (GMRF) model. The proposed methods incorporate prior information about the statistical dependency among observations, while at the same time processing data in real-time and in a fully decentralized manner. A detailed mean-square analysis is carried out in order to prove stability and evaluate the steady-state performance of the proposed strategies. Finally, we also illustrate how the proposed techniques can be easily extended in order to incorporate thresholding operators for sparsity recovery applications. Numerical results show the potential advantages of using such techniques for distributed learning in adaptive networks deployed over GMRF.
A Framework for Exploring Non-Linear Functional Connectivity and Causality in the Human Brain: Mutual Connectivity Analysis (MCA) of Resting-State Functional MRI with Convergent Cross-Mapping and Non-Metric Clustering
Venue: arXiv cs.NE 2014
Year: 2014

We present a computational framework for analysis and visualization of non-linear functional connectivity in the human brain from resting state functional MRI (fMRI) data for purposes of recovering the underlying network community structure and exploring causality between network components. Our proposed methodology of non-linear mutual connectivity analysis (MCA) involves two computational steps. First, the pair-wise cross-prediction performance between resting state fMRI pixel time series within the brain is evaluated. The underlying network structure is subsequently recovered from the affinity matrix constructed through MCA using non-metric network partitioning/clustering with the so-called Louvain method. We demonstrate our methodology in the task of identifying regions of the motor cortex associated with hand movement on resting state fMRI data acquired from eight slice locations in four subjects. For comparison, we also localized regions of the motor cortex through a task-based fMRI sequence involving a finger-tapping stimulus paradigm. Finally, we integrate convergent cross mapping (CCM) into the first step of MCA for investigating causality between regions of the motor cortex. Results regarding causation between regions of the motor cortex revealed a significant directional variability and were not readily interpretable in a consistent manner across all subjects. However, our results on whole-slice fMRI analysis demonstrate that MCA-based model-free recovery of regions associated with the primary motor cortex and supplementary motor area are in close agreement with localization of similar regions achieved with a task-based fMRI acquisition. Thus, we conclude that our computational framework MCA can extract and visualize valuable information concerning the underlying network structure and causation between different regions of the brain in resting state fMRI.
Correct-by-design Control Synthesis for Multilevel Converters using State Space Decomposition
Venue: arXiv cs.SY 2014
Year: 2014

High-power converters based on elementary switching cells are more and more used in the industry of power electronics owing to various advantages such as lower voltage stress and reduced power loss. However, the complexity of controlling such converters is a major challenge that the power manufacturing industry has to face with. The synthesis of industrial switching controllers relies today on heuristic rules and empiric simulation. The state of the system is not guaranteed to stay within the limits that are admissible for its correct electrical behavior. We show here how to apply a formal method in order to synthesize a correct-by-design control that guarantees that the power converter will always stay within a predefined safe zone of variations for its input parameters. The method is applied in order to synthesize a correct-by-design control for 5-level and 7-level power converters with a flying capacitor topology. We check the validity of our approach by numerical simulations for 5 and 7 levels. We also perform physical experimentations using a prototype built by SATIE laboratory for 5 levels.
Experience using Coloured Petri Nets to Model Railway Interlocking Tables
Venue: arXiv cs.SE 2014
Year: 2014

Interlocking tables are the functional specification defining the routes on which the passage of the train is allowed. Associated with the route, the states and actions of all related signalling equipment are also specified. It is well-known that designing and verifying the interlocking tables are labour intensive, tedious and prone to errors. To assist the verification process and detect errors rapidly, we formally model and analyse the interlocking tables using Coloured Petri Nets (CPNs). Although a large interlocking table can be easily modelled, analysing the model is rather difficult due to the state explosion problem and undesired safe deadlocks. The safe deadlocks are when no train collides but the train traffic cannot proceed any further. For ease of analysis we incorporate automatic route setting and automatic route cancelling functions into the model. These help reducing the number of the deadlocks. We also exploit the new features of CPN Tools; prioritized transitions; inhibitor arcs; and reset arcs. These help reducing the size of the state spaces. We also include a fail safe specification called flank protection into the interlocking model.
Verified Subtyping with Traits and Mixins
Venue: arXiv cs.PL 2014
Year: 2014

Traits allow decomposing programs into smaller parts and mixins are a form of composition that resemble multiple inheritance. Unfortunately, in the presence of traits, programming languages like Scala give up on subtyping relation between objects. In this paper, we present a method to check subtyping between objects based on entailment in separation logic. We implement our method as a domain specific language in Scala and apply it on the Scala standard library. We have verified that 67% of mixins used in the Scala standard library do indeed conform to subtyping between the traits that are used to build them.
VR-Stepper: A Do-It-Yourself Game Interface For Locomotion In Virtual Environments
Venue: arXiv cs.HC 2014
Year: 2014

Compared to real world tasks, completing tasks in a virtual environment (VE) seldom involves the whole spectrum of skills the human body offers. User input in a VE is commonly accomplished through simple finger gestures, such as walking in a scene by simply pressing a button, even if this kind of interaction is not very suitable. In order to create a more intuitive and natural interaction, diverse projects try to tackle the problem of locomotion in VEs by trying to enable a natural walking movement, which is also supposed to increase the level of immersion. Existing solutions such as treadmills are still expensive and need additional fixation of the body. In this paper, we describe a simple and inexpensive way to build a useful locomotion interface using a conventional sports stepper and an Arduino. This device enables control in a VE by walking-in-place and without the need for any additional fixation gadgets. We conducted a user study with 10 participants to evaluate the impression on the joy and ease of use, immersion and reliability in comparison to other interfaces used for locomotion, such as the Wii Balance Board and a Wand Joystick. We found out that the stepper is experienced slightly better in terms of immersion and joy of use. Furthermore, found that pressing buttons on a Joystick was perceived to be more reliable.
An iterative approach to Hough transform without re-voting
Venue: arXiv cs.CV 2014
Year: 2014

Many bone shapes in the human skeleton are characterized by profiles that can be associated to equations of algebraic curves. Fixing the parameters in the curve equation, by means of a classical pattern recognition procedure like the Hough transform technique, it is then possible to associate an equation to a specific bone profile. However, most skeleton districts are more accurately described by piecewise defined curves. This paper utilizes an iterative approach of the Hough transform without re-voting, to provide an efficient procedure for describing the profile of a bone in the human skeleton as a collection of different but continuously attached curves.
A Generalized Write Channel Model for Bit-Patterned Media Recording
Venue: arXiv cs.IT 2014
Year: 2014

In this paper, we propose a generalized write channel model for bit-patterned media recording by considering all sources of errors causing some extra disturbances during write process, in addition to data dependent write synchronization errors. We investigate information-theoretic bounds for this new model according to various input distributions and also compare it numerically to the last proposed model.
Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations
Venue: arXiv cs.LO 2014
Year: 2014

We introduce a new class of graph transformation systems in which rewrite rules can be guarded by universally quantified conditions on the neighbourhood of nodes. These conditions are defined via special graph patterns which may be transformed by the rule as well. For the new class for graph rewrite rules, we provide a symbolic procedure working on minimal representations of upward closed sets of configurations. We prove correctness and effectiveness of the procedure by a categorical presentation of rewrite rules as well as the involved order, and using results for well-structured transition systems. We apply the resulting procedure to the analysis of the Distributed Dining Philosophers protocol on an arbitrary network structure.
Analysis of Democratic Voting Principles used in Distributed Greedy Algorithms
Venue: arXiv cs.IT 2014
Year: 2014

A key aspect for any greedy pursuit algorithm used in compressed sensing is a good support-set detection method. For distributed compressed sensing, we consider a setup where many sensors measure sparse signals that are correlated via the existence of a signals' intersection support-set. This intersection support-set is called the joint support-set. Estimation of the joint support-set has a high impact on the performance of a distributed greedy pursuit algorithm. This estimation can be achieved by exchanging local support-set estimates followed by a (consensus) voting method. In this paper we endeavor for a probabilistic analysis of two democratic voting principle that we call majority and consensus voting. In our analysis, we first model the input/output relation of a greedy algorithm (executed locally in a sensor) by a single parameter known as probability of miss. Based on this model, we analyze the voting principles and prove that the democratic voting principle has a merit to detect the joint support-set.
Generating Asymptotically Non-Terminating Initial Values for Linear Programs
Venue: arXiv cs.DM 2014
Year: 2014

We present the notion of asymptotically non-terminating initial variable values for linear loop programs. Those values are directly associated to initial variable values for which the corresponding program does not terminate. Our theoretical contributions provide us with powerful computational methods for automatically generating sets of asymptotically non-terminating initial variable values. Such sets are represented symbolically and exactly by a semi-linear space, e.g., characterized by conjunctions and disjunctions of linear equalities and inequalities. Moreover, by taking their complements, we obtain a precise under-approximation of the set of inputs for which the program does terminate. We can then reduce the termination problem of linear programs to the emptiness check of a specific set of asymptotically non-terminating initial variable values. Our static input data analysis is not restricted only to programs where the variables are interpreted over the reals. We extend our approach and provide new decidability results for the termination problem of affine integer and rational programs.
Proving termination with transition invariants of height omega
Venue: arXiv cs.LO 2014
Year: 2014

The Termination Theorem by Podelski and Rybalchenko states that the reduction relations which are terminating from any initial state are exactly the reduction relations whose transitive closure, restricted to the accessible states, is included in some finite union of well-founded relations. An alternative statement of the theorem is that terminating reduction relations are precisely those having a "disjunctively well-founded transition invariant". From this result the same authors and Byron Cook designed an algorithm checking a sufficient condition for termination for a while-if program. The algorithm looks for a disjunctively well-founded transition invariant, made of well-founded relations of height omega, and if it finds it, it deduces the termination for the while-if program using the Termination Theorem. This raises an interesting question: What is the status of reduction relations having a disjunctively well-founded transition invariant where each relation has height omega? An answer to this question can lead to a characterization of the set of while-if programs which the termination algorithm can prove to be terminating. The goal of this work is to prove that they are exactly the set of reduction relations having height omega^n for some n < omega. Besides, if all the relations in the transition invariant are primitive recursive and the reduction relation is the graph of the restriction to some primitive recursive set of a primitive recursive map, then a final state is computable by some primitive recursive map in the initial state. As a corollary we derive that the set of functions, having at least one implementation in Podelski Rybalchenko while-if language with a well-founded disjunctively transition invariant where each relation has height omega, is exactly the set of primitive recursive functions.
Ark: A Real-World Consensus Implementation
Venue: arXiv cs.DC 2014
Year: 2014

Ark is an implementation of a consensus algorithm similar to Paxos and Raft, designed as an improvement over the existing consensus algorithm used by MongoDB and TokuMX. Ark was designed from first principles, improving on the election algorithm used by TokuMX, to fix deficiencies in MongoDB's consensus algorithms that can cause data loss. It ultimately has many similarities with Raft, but diverges in a few ways, mainly to support other features like chained replication and unacknowledged writes.
Collaborative Filtering Ensemble for Personalized Name Recommendation
Venue: arXiv cs.IR 2014
Year: 2014

Out of thousands of names to choose from, picking the right one for your child is a daunting task. In this work, our objective is to help parents making an informed decision while choosing a name for their baby. We follow a recommender system approach and combine, in an ensemble, the individual rankings produced by simple collaborative filtering algorithms in order to produce a personalized list of names that meets the individual parents' taste. Our experiments were conducted using real-world data collected from the query logs of 'nameling' (nameling.net), an online portal for searching and exploring names, which corresponds to the dataset released in the context of the ECML PKDD Discover Challenge 2013. Our approach is intuitive, easy to implement, and features fast training and prediction steps.
Design and Analysis of RS Sort
Venue: arXiv cs.DS 2014
Year: 2014

This paper introduces a new comparison base stable sorting algorithm, named RS sort. RS Sort involves only the comparison of pair of elements in an array which ultimately sorts the array and does not involve the comparison of each element with every other element. RS sort tries to build upon the relationship established between the elements in each pass. Suppose there is an array containing three elements a1, a2, a3 and if a relationship exist such that a1<a2 and a2<a3 then it can be established that a1<a3 and so there is no need to compare a1 and a3. Sorting is a fundamental operation in computer science. RS sort is analyzed both theoretically and empirically. We have performed its Empirical analysis and compared its performance with the well-known quick sort for various input types.
Compressed Subspace Matching on the Continuum
Venue: arXiv cs.IT 2014
Year: 2014

We consider the general problem of matching a subspace to a signal in R^N that has been observed indirectly (compressed) through a random projection. We are interested in the case where the collection of K-dimensional subspaces is continuously parameterized, i.e. naturally indexed by an interval from the real line, or more generally a region of R^D. Our main results show that if the dimension of the random projection is on the order of K times a geometrical constant that describes the complexity of the collection, then the match obtained from the compressed observation is nearly as good as one obtained from a full observation of the signal. We give multiple concrete examples of collections of subspaces for which this geometrical constant can be estimated, and discuss the relevance of the results to the general problems of template matching and source localization.
A Comparative Analysis for Determining the Optimal Path using PSO and GA
Venue: arXiv cs.NI 2014
Year: 2014

Significant research has been carried out recently to find the optimal path in network routing. Among them, the evolutionary algorithm approach is an area where work is carried out extensively. We in this paper have used particle swarm optimization (PSO) and genetic algorithm (GA) for finding the optimal path and the concept of region based network is introduced along with the use of indirect encoding. We demonstrate the advantage of fitness value and hop count in both PSO and GA. A comparative study of PSO and genetic algorithm (GA) is carried out, and it was found that PSO converged to arrive at the optimal path much faster than GA.
Practical Kernel-Based Reinforcement Learning
Venue: arXiv cs.LG 2014
Year: 2014

Kernel-based reinforcement learning (KBRL) stands out among reinforcement learning algorithms for its strong theoretical guarantees. By casting the learning problem as a local kernel approximation, KBRL provides a way of computing a decision policy which is statistically consistent and converges to a unique solution. Unfortunately, the model constructed by KBRL grows with the number of sample transitions, resulting in a computational cost that precludes its application to large-scale or on-line domains. In this paper we introduce an algorithm that turns KBRL into a practical reinforcement learning tool. Kernel-based stochastic factorization (KBSF) builds on a simple idea: when a transition matrix is represented as the product of two stochastic matrices, one can swap the factors of the multiplication to obtain another transition matrix, potentially much smaller, which retains some fundamental properties of its precursor. KBSF exploits such an insight to compress the information contained in KBRL's model into an approximator of fixed size. This makes it possible to build an approximation that takes into account both the difficulty of the problem and the associated computational cost. KBSF's computational complexity is linear in the number of sample transitions, which is the best one can do without discarding data. Moreover, the algorithm's simple mechanics allow for a fully incremental implementation that makes the amount of memory used independent of the number of sample transitions. The result is a kernel-based reinforcement learning algorithm that can be applied to large-scale problems in both off-line and on-line regimes. We derive upper bounds for the distance between the value functions computed by KBRL and KBSF using the same data. We also illustrate the potential of our algorithm in an extensive empirical study in which KBSF is applied to difficult tasks based on real-world data.