OpenRaiser/Intern-Atlas huggingface dataset:
Robust image reconstruction from multi-view measurements
Venue: arXiv cs.CV 2013
Year: 2013

We propose a novel method to accurately reconstruct a set of images representing a single scene from few linear multi-view measurements. Each observed image is modeled as the sum of a background image and a foreground one. The background image is common to all observed images but undergoes geometric transformations, as the scene is observed from different viewpoints. In this paper, we assume that these geometric transformations are represented by a few parameters, e.g., translations, rotations, affine transformations, etc.. The foreground images differ from one observed image to another, and are used to model possible occlusions of the scene. The proposed reconstruction algorithm estimates jointly the images and the transformation parameters from the available multi-view measurements. The ideal solution of this multi-view imaging problem minimizes a non-convex functional, and the reconstruction technique is an alternating descent method built to minimize this functional. The convergence of the proposed algorithm is studied, and conditions under which the sequence of estimated images and parameters converges to a critical point of the non-convex functional are provided. Finally, the efficiency of the algorithm is demonstrated using numerical simulations for applications such as compressed sensing or super-resolution.
Machine Learning in Proof General: Interfacing Interfaces
Venue: arXiv cs.AI 2013
Year: 2013

We present ML4PG - a machine learning extension for Proof General. It allows users to gather proof statistics related to shapes of goals, sequences of applied tactics, and proof tree structures from the libraries of interactive higher-order proofs written in Coq and SSReflect. The gathered data is clustered using the state-of-the-art machine learning algorithms available in MATLAB and Weka. ML4PG provides automated interfacing between Proof General and MATLAB/Weka. The results of clustering are used by ML4PG to provide proof hints in the process of interactive proof development.
An Interactive Graph-Based Automation Assistant: A Case Study to Manage the GIPSY's Distributed Multi-tier Run-Time System
Venue: arXiv cs.DC 2013
Year: 2013

The GIPSY system provides a framework for a distributed multi-tier demand-driven evaluation of heterogeneous programs, in which certain tiers can generate demands, while others can respond to demands to work on them. They are connected through a virtual network that can be flexibly reconfigured at run-time. Although the demand generator components were originally designed specifically for the eductive (demand-driven) evaluation of Lucid intensional programs, the GIPSY's run-time's flexible framework design enables it to perform the execution of various kinds of programs that can be evaluated using the demand-driven computational model. Management of the GISPY networks has become a tedious (although scripted) task that took manual command-line console to do, which does not scale for large experiments. Therefore a new component has been designed and developed to allow users to represent, visualize, and interactively create, configure and seamlessly manage such a network as a graph. Consequently, this work presents a Graphical GMT Manager, an interactive graph-based assistant component for the GIPSY network creation and configuration management. Besides allowing the management of the nodes and tiers (mapped to hosts where store, workers, and generators reside), it lets the user to visually control the network parameters and the interconnection between computational nodes at run-time. In this paper we motivate and present the key features of this newly implemented graph-based component. We give the graph representation details, mapping of the graph nodes to tiers, tier groups, and specific commands. We provide the requirements and design specification of the tool and its implementation. Then we detail and discuss some experimental results.
Polynomial functions of degree 20 which are APN infinitely often
Venue: arXiv cs.IT 2013
Year: 2013

We give all the polynomials functions of degree 20 which are APN over an infinity of field extensions and show they are all CCZ-equivalent to the function $x^5$, which is a new step in proving the conjecture of Aubry, McGuire and Rodier.
Phenomenology Tools on Cloud Infrastructures using OpenStack
Venue: arXiv cs.DC 2013
Year: 2013

We present a new environment for computations in particle physics phenomenology employing recent developments in cloud computing. On this environment users can create and manage "virtual" machines on which the phenomenology codes/tools can be deployed easily in an automated way. We analyze the performance of this environment based on "virtual" machines versus the utilization of "real" physical hardware. In this way we provide a qualitative result for the influence of the host operating system on the performance of a representative set of applications for phenomenology calculations.
Distributed Rate Allocation in Inter-Session Network Coding
Venue: arXiv cs.NI 2013
Year: 2013

In this work, we propose a distributed rate allocation algorithm that minimizes the average decoding delay for multimedia clients in inter-session network coding systems. We consider a scenario where the users are organized in a mesh network and each user requests the content of one of the available sources. We propose a novel distributed algorithm where network users determine the coding operations and the packet rates to be requested from the parent nodes, such that the decoding delay is minimized for all the clients. A rate allocation problem is solved by every user, which seeks the rates that minimize the average decoding delay for its children and for itself. Since the optimization problem is a priori non-convex, we introduce the concept of equivalent packet flows, which permits to estimate the expected number of packets that every user needs to collect for decoding. We then decompose our original rate allocation problem into a set of convex subproblems, which are eventually combined to obtain an effective approximate solution to the delay minimization problem. The results demonstrate that the proposed scheme eliminates the bottlenecks and reduces the decoding delay experienced by users with limited bandwidth resources. We validate the performance of our distributed rate allocation algorithm in different video streaming scenarios using the NS-3 network simulator. We show that our system is able to take benefit of inter-session network coding for simultaneous delivery of video sessions in networks with path diversity.
Relaying Protocols for Wireless Energy Harvesting and Information Processing
Venue: arXiv cs.IT 2013
Year: 2013

An emerging solution for prolonging the lifetime of energy constrained relay nodes in wireless networks is to avail the ambient radio-frequency (RF) signal and to simultaneously harvest energy and process information. In this paper, an amplify-and-forward (AF) relaying network is considered, where an energy constrained relay node harvests energy from the received RF signal and uses that harvested energy to forward the source information to the destination. Based on the time switching and power splitting receiver architectures, two relaying protocols, namely, i) time switching-based relaying (TSR) protocol and ii) power splitting-based relaying (PSR) protocol are proposed to enable energy harvesting and information processing at the relay. In order to determine the throughput, analytical expressions for the outage probability and the ergodic capacity are derived for delay-limited and delay-tolerant transmission modes, respectively. The numerical analysis provides practical insights into the effect of various system parameters, such as energy harvesting time, power splitting ratio, source transmission rate, source to relay distance, noise power, and energy harvesting efficiency, on the performance of wireless energy harvesting and information processing using AF relay nodes. In particular, the TSR protocol outperforms the PSR protocol in terms of throughput at relatively low signal-to-noise-ratios and high transmission rate.
Reinforcement learning for port-Hamiltonian systems
Venue: arXiv cs.SY 2013
Year: 2013

Passivity-based control (PBC) for port-Hamiltonian systems provides an intuitive way of achieving stabilization by rendering a system passive with respect to a desired storage function. However, in most instances the control law is obtained without any performance considerations and it has to be calculated by solving a complex partial differential equation (PDE). In order to address these issues we introduce a reinforcement learning approach into the energy-balancing passivity-based control (EB-PBC) method, which is a form of PBC in which the closed-loop energy is equal to the difference between the stored and supplied energies. We propose a technique to parameterize EB-PBC that preserves the systems's PDE matching conditions, does not require the specification of a global desired Hamiltonian, includes performance criteria, and is robust to extra non-linearities such as control input saturation. The parameters of the control law are found using actor-critic reinforcement learning, enabling learning near-optimal control policies satisfying a desired closed-loop energy landscape. The advantages are that near-optimal controllers can be generated using standard energy shaping techniques and that the solutions learned can be interpreted in terms of energy shaping and damping injection, which makes it possible to numerically assess stability using passivity theory. From the reinforcement learning perspective, our proposal allows for the class of port-Hamiltonian systems to be incorporated in the actor-critic framework, speeding up the learning thanks to the resulting parameterization of the policy. The method has been successfully applied to the pendulum swing-up problem in simulations and real-life experiments.
Normalized Compression Distance of Multisets with Applications
Venue: arXiv cs.CV 2013
Year: 2013

Normalized compression distance (NCD) is a parameter-free, feature-free, alignment-free, similarity measure between a pair of finite objects based on compression. However, it is not sufficient for all applications. We propose an NCD of finite multisets (a.k.a. multiples) of finite objects that is also a metric. Previously, attempts to obtain such an NCD failed. We cover the entire trajectory from theoretical underpinning to feasible practice. The new NCD for multisets is applied to retinal progenitor cell classification questions and to related synthetically generated data that were earlier treated with the pairwise NCD. With the new method we achieved significantly better results. Similarly for questions about axonal organelle transport. We also applied the new NCD to handwritten digit recognition and improved classification accuracy significantly over that of pairwise NCD by incorporating both the pairwise and NCD for multisets. In the analysis we use the incomputable Kolmogorov complexity that for practical purposes is approximated from above by the length of the compressed version of the file involved, using a real-world compression program. Index Terms--- Normalized compression distance, multisets or multiples, pattern recognition, data mining, similarity, classification, Kolmogorov complexity, retinal progenitor cells, synthetic data, organelle transport, handwritten character recognition
Programming CUDA and OpenCL: A Case Study Using Modern C++ Libraries
Venue: arXiv cs.MS 2013
Year: 2013

We present a comparison of several modern C++ libraries providing high-level interfaces for programming multi- and many-core architectures on top of CUDA or OpenCL. The comparison focuses on the solution of ordinary differential equations and is based on odeint, a framework for the solution of systems of ordinary differential equations. Odeint is designed in a very flexible way and may be easily adapted for effective use of libraries such as Thrust, MTL4, VexCL, or ViennaCL, using CUDA or OpenCL technologies. We found that CUDA and OpenCL work equally well for problems of large sizes, while OpenCL has higher overhead for smaller problems. Furthermore, we show that modern high-level libraries allow to effectively use the computational resources of many-core GPUs or multi-core CPUs without much knowledge of the underlying technologies.
Dialectics of Knowledge Representation in a Granular Rough Set Theory
Venue: arXiv cs.AI 2013
Year: 2013

The concepts of rough and definite objects are relatively more determinate than those of granules and granulation in general rough set theory (RST) [1]. Representation of rough objects can however depend on the dialectical relation between granulation and definiteness. In this research, we make this exact in the context of RST over proto-transitive approximation spaces. This approach can be directly extended to many other types of RST. These are used for formulating an extended concept of knowledge interpretation (KI)(relative the situation for classical RST) and the problem of knowledge representation (KR) is solved. These will be of direct interest in granular KR in RST as developed by the present author [2] and of rough objects in general. In [3], these have already been used for five different semantics by the present author. This is an extended version of [4] with key examples and more results.
The Complexity of Infinitely Repeated Alternating Move Games
Venue: arXiv cs.GT 2013
Year: 2013

We consider infinite duration alternating move games. These games were previously studied by Roth, Balcan, Kalai and Mansour. They presented an FPTAS for computing an approximated equilibrium, and conjectured that there is a polynomial algorithm for finding an exact equilibrium. We extend their study in two directions: (1) We show that finding an exact equilibrium, even for two-player zero-sum games, is polynomial time equivalent to finding a winning strategy for a (two-player) mean-payoff game on graphs. The existence of a polynomial algorithm for the latter is a long standing open question in computer science. Our hardness result for two-player games suggests that two-player alternating move games are harder to solve than two-player simultaneous move games, while the work of Roth et al., suggests that for $k\geq 3$, $k$-player games are easier to analyze in the alternating move setting. (2) We show that optimal equilibriums (with respect to the social welfare metric) can be obtained by pure strategies, and we present an FPTAS for computing a pure approximated equilibrium that is $δ$-optimal with respect to the social welfare metric. This result extends the previous work by presenting an FPTAS that finds a much more desirable approximated equilibrium. We also show that if there is a polynomial algorithm for mean-payoff games on graphs, then there is a polynomial algorithm that computes an optimal exact equilibrium, and hence, (two-player) mean-payoff games on graphs are inter-reducible with $k$-player alternating move games, for any $k\geq 2$.
PALS-Based Analysis of an Airplane Multirate Control System in Real-Time Maude
Venue: arXiv cs.LO 2013
Year: 2013

Distributed cyber-physical systems (DCPS) are pervasive in areas such as aeronautics and ground transportation systems, including the case of distributed hybrid systems. DCPS design and verification is quite challenging because of asynchronous communication, network delays, and clock skews. Furthermore, their model checking verification typically becomes unfeasible due to the huge state space explosion caused by the system's concurrency. The PALS ("physically asynchronous, logically synchronous") methodology has been proposed to reduce the design and verification of a DCPS to the much simpler task of designing and verifying its underlying synchronous version. The original PALS methodology assumes a single logical period, but Multirate PALS extends it to deal with multirate DCPS in which components may operate with different logical periods. This paper shows how Multirate PALS can be applied to formally verify a nontrivial multirate DCPS. We use Real-Time Maude to formally specify a multirate distributed hybrid system consisting of an airplane maneuvered by a pilot who turns the airplane according to a specified angle through a distributed control system. Our formal analysis revealed that the original design was ineffective in achieving a smooth turning maneuver, and led to a redesign of the system that satisfies the desired correctness properties. This shows that the Multirate PALS methodology is not only effective for formal DCPS verification, but can also be used effectively in the DCPS design process, even before properties are verified.
MDM: A Mode Diagram Modeling Framework
Venue: arXiv cs.LO 2013
Year: 2013

Periodic control systems used in spacecrafts and automotives are usually period-driven and can be decomposed into different modes with each mode representing a system state observed from outside. Such systems may also involve intensive computing in their modes. Despite the fact that such control systems are widely used in the above-mentioned safety-critical embedded domains, there is lack of domain-specific formal modelling languages for such systems in the relevant industry. To address this problem, we propose a formal visual modeling framework called mode diagram as a concise and precise way to specify and analyze such systems. To capture the temporal properties of periodic control systems, we provide, along with mode diagram, a property specification language based on interval logic for the description of concrete temporal requirements the engineers are concerned with. The statistical model checking technique can then be used to verify the mode diagram models against desired properties. To demonstrate the viability of our approach, we have applied our modelling framework to some real life case studies from industry and helped detect two design defects for some spacecraft control systems.
On Two Infinite Families of Pairing Bijections
Venue: arXiv cs.MS 2013
Year: 2013

We describe two general mechanisms for producing pairing bijections (bijective functions defined from N x N to N). The first mechanism, using n-adic valuations results in parameterized algorithms generating a countable family of distinct pairing bijections. The second mechanism, using characteristic functions of subsets of N provides 2^N distinct pairing bijections. Mechanisms to combine such pairing functions and their application to generate families of permutations of N are also described. The paper uses a small subset of the functional language Haskell to provide type checked executable specifications of all the functions defined in a literate programming style. The self-contained Haskell code extracted from the paper is available at http://logic.cse.unt.edu/tarau/research/2012/infpair.hs .
Sensing as a Service and Big Data
Venue: arXiv cs.CY 2013
Year: 2013

Internet of Things (IoT) will comprise billions of devices that can sense, communicate, compute and potentially actuate. Data streams coming from these devices will challenge the traditional approaches to data management and contribute to the emerging paradigm of big data. This paper discusses emerging Internet of Things (IoT) architecture, large scale sensor network applications, federating sensor networks, sensor data and related context capturing techniques, challenges in cloud-based management, storing, archiving and processing of sensor data.
Efficient Solutions for Weighted Sum Rate Maximization in Multicellular Networks With Channel Uncertainties
Venue: arXiv cs.IT 2013
Year: 2013

The important problem of weighted sum rate maximization (WSRM) in a multicellular environment is intrinsically sensitive to channel estimation errors. In this paper, we study ways to maximize the weighted sum rate in a linearly precoded multicellular downlink system where the receivers are equipped with a single antenna. With perfect channel information available at the base stations, we first present a novel fast converging algorithm that solves the WSRM problem. Then, the assumption is relaxed to the case where the error vectors in the channel estimates are assumed to lie in an uncertainty set formed by the intersection of finite ellipsoids. As our main contributions, we present two procedures to solve the intractable nonconvex robust designs based on the worst case principle. The proposed iterative algorithms solve the semidefinite programs in each of their steps and provably converge to a locally optimal solution of the robust WSRM problem. The proposed approaches are numerically compared against each other to ascertain their robustness towards channel estimation imperfections. The results clearly indicate the performance gain compared to the case when channel uncertainties are ignored in the design process. For certain scenarios, we also quantify the gap between the proposed approximations and exact solutions.
Increasing Security in Cloud Environment
Venue: arXiv cs.CR 2013
Year: 2013

The concept of cloud computing was introduced to meet the increase in demand for new application for a project, and to provide a large storage facility whenever or wherever a user needs it. The cloud system facility helped many industries as well as individual users to get authentic software at a very low cost. But with this new system comes the major concern of security, as the connection to the cloud is through the web and the data and application availability need to be handled for each client. The paper describes the various security measures that can be added in isolation or in combination for securing data transmission, server and client.
Chaotic Analog-to-Information Conversion with Chaotic State Modulation
Venue: arXiv cs.IT 2013
Year: 2013

Chaotic compressive sensing is a nonlinear framework for compressive sensing. Along the framework, this paper proposes a chaotic analog-to-information converter, chaotic modulation, to acquire and reconstruct band-limited sparse analog signals at sub-Nyquist rate. In the chaotic modulation, the sparse signal is randomized through state modulation of continuous-time chaotic system and one state output is sampled as compressive measurements. The reconstruction is achieved through the estimation of the sparse coefficients with principle of chaotic impulsive synchronization and Lp-norm regularized nonlinear least squares. The concept of supreme local Lyapunov exponents (SLLE) is introduced to study the reconstructablity. It is found that the sparse signals are reconstructable, if the largest SLLE of the error dynamical system is negative. As examples, the Lorenz system and Liu system excited by the sparse multi-tone signals are taken to illustrate the principle and the performance.
Word Storms: Multiples of Word Clouds for Visual Comparison of Documents
Venue: arXiv cs.IR 2013
Year: 2013

Word clouds are a popular tool for visualizing documents, but they are not a good tool for comparing documents, because identical words are not presented consistently across different clouds. We introduce the concept of word storms, a visualization tool for analysing corpora of documents. A word storm is a group of word clouds, in which each cloud represents a single document, juxtaposed to allow the viewer to compare and contrast the documents. We present a novel algorithm that creates a coordinated word storm, in which words that appear in multiple documents are placed in the same location, using the same color and orientation, in all of the corresponding clouds. In this way, similar documents are represented by similar-looking word clouds, making them easier to compare and contrast visually. We evaluate the algorithm in two ways: first, an automatic evaluation based on document classification; and second, a user study. The results confirm that unlike standard word clouds, a coordinated word storm better allows for visual comparison of documents.