OpenRaiser/Intern-Atlas huggingface dataset:
A necessary and sufficient condition for two relations to induce the same definable set family
Venue: arXiv cs.AI 2013
Year: 2013

In Pawlak rough sets, the structure of the definable set families is simple and clear, but in generalizing rough sets, the structure of the definable set families is a bit more complex. There has been much research work focusing on this topic. However, as a fundamental issue in relation based rough sets, under what condition two relations induce the same definable set family has not been discussed. In this paper, based on the concept of the closure of relations, we present a necessary and sufficient condition for two relations to induce the same definable set family.
Fully Homomorphic Encryption Scheme with Symmetric Keys
Venue: arXiv cs.CR 2013
Year: 2013

Homomorphic encryption has largely been studied in context of public key cryptosystems. But there are applications which inherently would require symmetric keys. We propose a symmetric key encryption scheme with fully homomorphic evaluation capabilities. The operations are matrix based, that is the scheme consists of mapping the operations on integers to operations on matrix. We also include a protocol which uses the proposed scheme for private data processing in clouds.
Algorithmes auto-stabilisants pour la construction d'arbres couvrants et la gestion d'entités autonomes
Venue: arXiv cs.DC 2013
Year: 2013

In the context of large-scale networks, the consideration of faults is an evident necessity. This document is focussing on the self-stabilizing approach which aims at conceiving algorithms "repairing themselves" in case of transient faults, that is of faults implying an arbitrary modification of the states of the processes. The document focuses on two different contexts, covering the major part of my research work these last years. The first part of the document is dedicated to the design and analysis of self-stabilizing algorithms for networks of processes. The second part of the document is dedicated to the design and analysis of self-stabilizing algorithms for autonomous entities (i.e., software agents, robots, etc.) moving in a network.
Saturation of Concurrent Collapsible Pushdown Systems
Venue: arXiv cs.FL 2013
Year: 2013

Multi-stack pushdown systems are a well-studied model of concurrent computation using threads with first-order procedure calls. While, in general, reachability is undecidable, there are numerous restrictions on stack behaviour that lead to decidability. To model higher-order procedures calls, a generalisation of pushdown stacks called collapsible pushdown stacks are required. Reachability problems for multi-stack collapsible pushdown systems have been little studied. Here, we study ordered, phase-bounded and scope-bounded multi-stack collapsible pushdown systems using saturation techniques, showing decidability of control state reachability and giving a regular representation of all configurations that can reach a given control state.
Testing Graph Isotopy on Surfaces
Venue: arXiv cs.CG 2013
Year: 2013

We investigate the following problem: Given two embeddings G_1 and G_2 of the same abstract graph G on an orientable surface S, decide whether G_1 and G_2 are isotopic; in other words, whether there exists a continuous family of embeddings between G_1 and G_2. We provide efficient algorithms to solve this problem in two models. In the first model, the input consists of the arrangement of G_1 (resp., G_2) with a fixed graph cellularly embedded on S; our algorithm is linear in the input complexity, and thus, optimal. In the second model, G_1 and G_2 are piecewise-linear embeddings in the plane minus a finite set of points; our algorithm runs in O(n^{3/2}\log n) time, where n is the complexity of the input. The graph isotopy problem is a natural variation of the homotopy problem for closed curves on surfaces and on the punctured plane, for which algorithms have been given by various authors; we use some of these algorithms as a subroutine. As a by-product, we reprove the following mathematical characterization, first observed by Ladegaillerie (1984): Two graph embeddings are isotopic if and only if they are homotopic and congruent by an oriented homeomorphism.
Efficient Algorithms for Computing Rational First Integrals and Darboux Polynomials of Planar Polynomial Vector Fields
Venue: arXiv cs.SC 2013
Year: 2013

We present fast algorithms for computing rational first integrals with bounded degree of a planar polynomial vector field. Our approach is inspired by an idea of Ferragut and Giacomini. We improve upon their work by proving that rational first integrals can be computed via systems of linear equations instead of systems of quadratic equations. This leads to a probabilistic algorithm with arithmetic complexity $\bigOsoft(N^{2 ω})$ and to a deterministic algorithm solving the problem in $\bigOsoft(d^2N^{2 ω+1})$ arithmetic operations, where $N$ denotes the given bound for the degree of the rational first integral, and where $d \leq N$ is the degree of the vector field, and $ω$ the exponent of linear algebra. We also provide a fast heuristic variant which computes a rational first integral, or fails, in $\bigOsoft(N^{ω+2})$ arithmetic operations. By comparison, the best previous algorithm uses at least $d^{ω+1}\, N^{4ω+4}$ arithmetic operations. We then show how to apply a similar method to the computation of Darboux polynomials. The algorithms are implemented in a Maple package which is available to interested readers with examples showing its efficiency.
Lemma Mining over HOL Light
Venue: arXiv cs.AI 2013
Year: 2013

Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informal mathematical practice, only a tiny fraction of such statements is named and re-used in later proofs by formal mathematicians. In this work, we suggest and implement criteria defining the estimated usefulness of the HOL Light lemmas for proving further theorems. We use these criteria to mine the large inference graph of all lemmas in the core HOL Light library, adding thousands of the best lemmas to the pool of named statements that can be re-used in later proofs. The usefulness of the new lemmas is then evaluated by comparing the performance of automated proving of the core HOL Light theorems with and without such added lemmas.
Emergency and Normal Navigation in Confined Spaces
Venue: arXiv cs.OH 2013
Year: 2013

Emergency navigation algorithms direct evacuees to exits when disastrous events such as fire take place. Due to the spread of hazards, latency in information updating and unstable flows of civilians, emergency evacuation is absolutely a complex transshipment problem involving numerous sources and multiple destinations. Previous algorithms which commonly need either a full graph search or a convergence process suffer from high computational and communication overheads. This research report surveys the current emergency navigation algorithms and adapts the concept of Cognitive Packet Network (CPN) to the context of emergency evacuation. By using random neural networks, the CPN based algorithm can explore optimal routes rapidly and adaptively in a highly dynamic emergency environment with low expense. Simultaneously, in emergency situations there are typically different categories of evacuees such as people of different age groups. However, current algorithms only consider "normal" evacuees and do not meet the specific requirements of diverse evacuees. Our algorithms make use of the flexibility of CPN which can operate with different user-defined goals to customize appropriate paths for each category. The CPN algorithm is simulated in a graph based discrete-event simulator and Dijkstra's shortest path algorithm is taken as reference. The results show that the CPN algorithm reaches the performance of ideal path-finding algorithm and quality of service is improved by using specific goal functions for diverse categories of evacuees. Finally, we present a future plan for further research.
Improved Spectrum Mobility using Virtual Reservation in Collaborative Cognitive Radio Networks
Venue: arXiv cs.NI 2013
Year: 2013

Cognitive radio technology would enable a set of secondary users (SU) to opportunistically use the spectrum licensed to a primary user (PU). On the appearance of this PU on a specific frequency band, any SU occupying this band should free it for PUs. Typically, SUs may collaborate to reduce the impact of cognitive users on the primary network and to improve the performance of the SUs. In this paper, we propose and analyze the performance of virtual reservation in collaborative cognitive networks. Virtual reservation is a novel link maintenance strategy that aims to maximize the throughput of the cognitive network through full spectrum utilization. Our performance evaluation shows significant improvements not only in the SUs blocking and forced termination probabilities but also in the throughput of cognitive users.
Towards Gigayear Storage Using a Silicon-Nitride/Tungsten Based Medium
Venue: arXiv cs.ET 2013
Year: 2013

Current digital data storage systems are able to store huge amounts of data. Even though the data density of digital information storage has increased tremendously over the last few decades, the data longevity is limited to only a few decades. If we want to preserve anything about the human race which can outlast the human race itself, we require a data storage medium designed to last for 1 million to 1 billion years. In this paper a medium is investigated consisting of tungsten encapsulated by siliconnitride which, according to elevated temperature tests, will last for well over the suggested time.
Depth-dependent Parallel Visualization with 3D Stylized Dense Tubes
Venue: arXiv cs.DC 2013
Year: 2013

We present a parallel visualization algorithm for the illustrative rendering of depth-dependent stylized dense tube data at interactive frame rates. While this computation could be efficiently performed on a GPU device, we target a parallel framework to enable it to be efficiently running on an ordinary multi-core CPU platform which is much more available than GPUs for common users. Our approach is to map the depth information in each tube onto each of the visual dimensions of shape, color, texture, value, and size on the basis of Bertin's semiology theory. The purpose is to enable more legible displays in the dense tube environments. A major contribution of our work is an efficient and effective parallel depthordering algorithm that makes use of the message passing interface (MPI) with VTK. We evaluated our framework with visualizations of depth-stylized tubes derived from 3D diffusion tensor MRI data by comparing its efficiency with several other alternative parallelization platforms running the same computations. As our results show, the parallelization framework we proposed can efficiently render highly dense 3D data sets like the tube data and thus is useful as a complement to parallel visualization environments that rely on GPUs.
Filter-And-Forward Relay Design for MIMO-OFDM Systems
Venue: arXiv cs.IT 2013
Year: 2013

In this paper, the filter-and-forward (FF) relay design for multiple-input multiple-output (MIMO) orthogonal frequency-division multiplexing (OFDM) systems is considered. Due to the considered MIMO structure, the problem of joint design of the linear MIMO transceiver at the source and the destination and the FF relay at the relay is considered. As the design criterion, the minimization of weighted sum mean-square-error (MSE) is considered first, and the joint design in this case is approached based on alternating optimization that iterates between optimal design of the FF relay for a given set of MIMO precoder and decoder and optimal design of the MIMO precoder and decoder for a given FF relay filter. Next, the joint design problem for rate maximization is considered based on the obtained result regarding weighted sum MSE and the existing result regarding the relationship between weighted MSE minimization and rate maximization. Numerical results show the effectiveness of the proposed FF relay design and significant performance improvement by FF relays over widely-considered simple AF relays for MIMO-ODFM systems.
10 Inventions on special type of keyboards -A study based on US patents
Venue: arXiv cs.HC 2013
Year: 2013

A keyboard is the most important input device for a computer. It is used with various types and sizes of computer. But the same standard keyboard will not work efficiently with different types of computers at different environments. There is a need to develop special keyboards to meet special requirements. This article illustrates 10 inventions on special types of keyboards. The special keyboard are used in special computers or computers used for special purposes. A special keyboard is to be understood as a keyboard having features beyond a normal keyboard. The example of special keyboards are, a children's keyboard which may be colorful and attractive, a keyboard in public place need to be more robust, the keyboard in a palmtop may have less number of keys, the keyboard for a game station may have special attachments, a multimedia keyboard may have CD ROM and speakers, a wireless keyboard may have remote control features, a touch sensitive keyboard may have sensors on the keys and so on.
Ehrenfeucht-Fraisse Games on Omega-Terms
Venue: arXiv cs.FL 2013
Year: 2013

Fragments of first-order logic over words can often be characterized in terms of finite monoids or finite semigroups. Usually these algebraic descriptions yield decidability of the question whether a given regular language is definable in a particular fragment. An effective algebraic characterization can be obtained from identities of so-called omega-terms. In order to show that a given fragment satisfies some identity of omega-terms, one can use Ehrenfeucht-Fraisse games on word instances of the omega-terms. The resulting proofs often require a significant amount of book-keeping with respect to the constants involved. In this paper we introduce Ehrenfeucht-Fraisse games on omega-terms. To this end we assign a labeled linear order to every omega-term. Our main theorem shows that a given fragment satisfies some identity of omega-terms if and only if Duplicator has a winning strategy for the game on the resulting linear orders. This allows to avoid the book-keeping. As an application of our main result, we show that one can decide in exponential time whether all aperiodic monoids satisfy some given identity of omega-terms, thereby improving a result of McCammond (Int. J. Algebra Comput., 2001).
New Identities Relating Wild Goppa Codes
Venue: arXiv cs.IT 2013
Year: 2013

For a given support $L \in \mathbb{F}_{q^m}^n$ and a polynomial $g\in \mathbb{F}_{q^m}[x]$ with no roots in $\mathbb{F}_{q^m}$, we prove equality between the $q$-ary Goppa codes $Γ_q(L,N(g)) = Γ_q(L,N(g)/g)$ where $N(g)$ denotes the norm of $g$, that is $g^{q^{m-1}+\cdots +q+1}.$ In particular, for $m=2$, that is, for a quadratic extension, we get $Γ_q(L,g^q) = Γ_q(L,g^{q+1})$. If $g$ has roots in $\mathbb{F}_{q^m}$, then we do not necessarily have equality and we prove that the difference of the dimensions of the two codes is bounded above by the number of distinct roots of $g$ in $\mathbb{F}_{q^m}$. These identities provide numerous code equivalences and improved designed parameters for some families of classical Goppa codes.
Bayesian Estimation of White Matter Atlas from High Angular Resolution Diffusion Imaging
Venue: arXiv cs.CV 2013
Year: 2013

We present a Bayesian probabilistic model to estimate the brain white matter atlas from high angular resolution diffusion imaging (HARDI) data. This model incorporates a shape prior of the white matter anatomy and the likelihood of individual observed HARDI datasets. We first assume that the atlas is generated from a known hyperatlas through a flow of diffeomorphisms and its shape prior can be constructed based on the framework of large deformation diffeomorphic metric mapping (LDDMM). LDDMM characterizes a nonlinear diffeomorphic shape space in a linear space of initial momentum uniquely determining diffeomorphic geodesic flows from the hyperatlas. Therefore, the shape prior of the HARDI atlas can be modeled using a centered Gaussian random field (GRF) model of the initial momentum. In order to construct the likelihood of observed HARDI datasets, it is necessary to study the diffeomorphic transformation of individual observations relative to the atlas and the probabilistic distribution of orientation distribution functions (ODFs). To this end, we construct the likelihood related to the transformation using the same construction as discussed for the shape prior of the atlas. The probabilistic distribution of ODFs is then constructed based on the ODF Riemannian manifold. We assume that the observed ODFs are generated by an exponential map of random tangent vectors at the deformed atlas ODF. Hence, the likelihood of the ODFs can be modeled using a GRF of their tangent vectors in the ODF Riemannian manifold. We solve for the maximum a posteriori using the Expectation-Maximization algorithm and derive the corresponding update equations. Finally, we illustrate the HARDI atlas constructed based on a Chinese aging cohort of 94 adults and compare it with that generated by averaging the coefficients of spherical harmonics of the ODF across subjects.
GPU-Framework for Teamwork Action Recognition
Venue: arXiv cs.DC 2013
Year: 2013

Real time processing for teamwork action recognition is a challenge, due to complex computational models to achieve high system performance. Hence, this paper proposes a framework based on Graphical Processing Units (GPUs) to achieve a significant speed up in the performance of role based activity recognition of teamwork. The framework can be applied in various fields, especially athletic and military applications. Furthermore, the framework can be customized for many action recognition applications. The paper presents the stages of the framework where GPUs are the main tool for performance improvement. The speedup is achieved by performing video processing and Machine learning algorithms on GPU. Video processing and machine learning algorithms covers all computations involved in our framework. Video processing tasks on involves GPU implementation of Motion detection, segmentation and object tracking algorithms. In addition, our framework is integrated with GPUCV, a GPU version of OpenCV functions. Machine learning tasks are supported under our framework with GPU implementations of Support Vector Machine (SVM) for object classification and feature discretization, Hidden Marcov Model (HMM) for activity recognition phase, and ID3 algorithm for role recognition of team members. The system was tested against UC-Teamwork dataset and speedup of 20X has been achieved on NVidia 9500GT graphics card (32 500MHZ processors).
A Kalman Filtering approach of improved precision for fault diagnosis in distributed parameter systems
Venue: arXiv cs.SY 2013
Year: 2013

The Derivative-free nonlinear Kalman Filter is proposed for state estimation and fault diagnosis in distributed parameter systems and particularly in dynamical systems described by partial differential equations of the nonlinear wave type. At a first stage, a nonlinear filtering approach for estimating the dynamics of a 1D nonlinear wave equation, from measurements provided from a small number of sensors is developed. It is shown that the numerical solution of the associated partial differential equation results into a set of nonlinear ordinary differential equations. With the application of diffeomorphism that is based on differential flatness theory it is shown that an equivalent description of the system is obtained in the linear canonical (Brunovsky) form. This transformation enables to obtain local estimates about the state vector of the system through the application of the standard Kalman Filter recursion. At a second stage, the local statistical approach to fault diagnosis is used to perform fault diagnosis for the distributed parameters system by processing with elaborated statistical tools the differences (residuals) between the output of the Kalman Filter and the measurements obtained from the distributed parameter system. Optimal selection of the fault threshold is succeeded by using the local statistical approach to fault diagnosis. The efficiency of the proposed filtering approach for performing fault diagnosis in distributed parameters systems is confirmed through simulation experiments.
Finding the Largest Disk Containing a Query Point in Logarithmic Time with Linear Storage
Venue: arXiv cs.CG 2013
Year: 2013

Let D be a set of n disks in the plane. We present a data structure of size O(n) that can compute, for any query point q, the largest disk in D that contains q, in O(log n) time. The structure can be constructed in O(n log^3 n) time. The optimal storage and query time of the structure improve several recent solutions by Augustine et al. and by Kaplan and Sharir.
QEMU/CPC: Static Analysis and CPS Conversion for Safe, Portable, and Efficient Coroutines
Venue: arXiv cs.PL 2013
Year: 2013

Coroutines and events are two common abstractions for writing concurrent programs. Because coroutines are often more convenient, but events more portable and efficient, it is natural to want to translate the former into the latter. CPC is such a source-to-source translator for C programs, based on a partial conversion into continuation-passing style (CPS conversion) of functions annotated as cooperative. In this article, we study the application of the CPC translator to QEMU, an open-source machine emulator which also uses annotated coroutine functions for concurrency. We first propose a new type of annotations to identify functions which never cooperate, and we introduce CoroCheck, a tool for the static analysis and inference of cooperation annotations. Then, we improve the CPC translator, defining CPS conversion as a calling convention for the C language, with support for indirect calls to CPS-converted function through function pointers. Finally, we apply CoroCheck and CPC to QEMU (750 000 lines of C code), fixing hundreds of missing annotations and comparing performance of the translated code with existing implementations of coroutines in QEMU. Our work shows the importance of static annotation checking to prevent actual concurrency bugs, and demonstrates that CPS conversion is a flexible, portable, and efficient compilation technique, even for very large programs written in an imperative language.
An Algebraic Framework for Compositional Program Analysis
Venue: arXiv cs.PL 2013
Year: 2013

The purpose of a program analysis is to compute an abstract meaning for a program which approximates its dynamic behaviour. A compositional program analysis accomplishes this task with a divide-and-conquer strategy: the meaning of a program is computed by dividing it into sub-programs, computing their meaning, and then combining the results. Compositional program analyses are desirable because they can yield scalable (and easily parallelizable) program analyses. This paper presents algebraic framework for designing, implementing, and proving the correctness of compositional program analyses. A program analysis in our framework defined by an algebraic structure equipped with sequencing, choice, and iteration operations. From the analysis design perspective, a particularly interesting consequence of this is that the meaning of a loop is computed by applying the iteration operator to the loop body. This style of compositional loop analysis can yield interesting ways of computing loop invariants that cannot be defined iteratively. We identify a class of algorithms, the so-called path-expression algorithms [Tarjan1981,Scholz2007], which can be used to efficiently implement analyses in our framework. Lastly, we develop a theory for proving the correctness of an analysis by establishing an approximation relationship between an algebra defining a concrete semantics and an algebra defining an analysis.