OpenRaiser/Intern-Atlas huggingface dataset:
RFID Security Using Lightweight Mutual Authentication And Ownership Transfer Protocol
Venue: arXiv cs.CR 2012
Year: 2012

In recent years, radio frequency identification technology has moved into the mainstream applications that help to speed up handling of manufactured goods and materials. RFID tags are divided into two classes: active and passive. Active tag requires a power source that's why its cost is more than passive tags. However, the low-cost RFID tags are facing new challenges to security and privacy. Some solutions utilize expensive cryptographic primitives such as hash or encryption functions, and some lightweight approaches have been reported to be not secure. This paper describes a lightweight Mutual authentication and ownership transfer protocol utilizing minimalistic cryptography using Physically Unclonable Functions (PUF) and Linear Feedback Shift Registers (LFSR). PUFs and LFSRs are very efficient in hardware and particularly suitable for the low-cost RFID tags. To functioning security in low cost RFID tag minimum gate requirement is 2000 gates. To implement security protocols using PUF and LFSR functions need only approx 800 gates. In this paper it is explained how we can authenticate and transfer ownership of low cost RFID tag securely using LFSR and PUF as compared to existing solutions based on hash functions.
ROSA Analyser: An automatized approach to analyse processes of ROSA
Venue: arXiv cs.SE 2012
Year: 2012

In this work we present the first version of ROSA Analyser, a tool designed to get closer to a fully automatic process of analysing the behaviour of a system specified as a process of the Markovian Process Algebra ROSA. In this first development stage, ROSA Analyser is able to generate the Labelled Transition System, according to ROSA Operational Semantics. ROSA Analyser performance starts with the Syntactic Analysis so generating a layered structure, suitable to then, apply the Operational Semantics Transition rules in the easier way. ROSA Analyser is able to recognize some states identities deeper than the Syntactic ones. This is the very first step in the way to reduce the size of the LTS and then to avoid the state explosion problem, so making this task more tractable. For the sake of better illustrating the usefulness of ROSA Analyser, a case study is also provided within this work.
Design and Performance Analysis of hybrid adders for high speed arithmetic circuit
Venue: arXiv cs.AR 2012
Year: 2012

Adder cells using Gate Diffusion Technique (GDI) & PTL-GDI technique are described in this paper. GDI technique allows reducing power consumption, propagation delay and low PDP (power delay product) whereas Pass Transistor Logic (PTL) reduces the count of transistors used to make different logic gates, by eliminating redundant transistors. Performance comparison with various Hybrid Adder is been presented. In this paper, we propose two new designs based on GDI & PTL techniques, which is found to be much more power efficient in comparison with existing design technique. Only 10 transistors are used to implement the SUM & CARRY function for both the designs. The SUM and CARRY cell are implemented in a cascaded way i.e. firstly the XOR cell is implemented and then using XOR as input SUM as well as CARRY cell is implemented. For Proposed GDI adder the SUM as well as CARRY cell is designed using GDI technique. On the other hand in Proposed PTL-GDI adder the SUM cell is constructed using PTL technique and the CARRY cell is designed using GDI technique. The advantages of both the designs are discussed. The significance of these designs is substantiated by the simulation results obtained from Cadence Virtuoso 180nm environment.
Performance Enhancement Factors of ERP Projects in a Telecom Public Sector Organization of Pakistan : An Exploratory Study
Venue: arXiv cs.CY 2012
Year: 2012

Public sector organizations are treated in a different manner, as Information technology/information system has become necessity in a highly competitive environment. Importance of information systems is becoming more and more vital as the global technology adoption is in progress. ERP projects are considered as one of the most important and critical area of technology especially in public sector organizations where cost effectiveness and operational efficiency is prioritized on profits. A lot of research studies have been made on ERP projects but mostly on critical success factors (CSFs) and other managerial issues. This ongoing research mainly focuses upon the performance of ERP software in public sector organizations by thoroughly going through one of the largest most public sector organizations of Pakistan. Though ERP projects are handled by experienced consultants in addition to the support of vendor companies but because of its features and functional complexity and mismatch with the organizational processes, different managerial and technical issues arise during and after its implementation. This study investigates the performance of ERP system in a large public sector organization of Pakistan; five most critical technical factors, which can lead the whole project towards success or failure, have been dug out. This exploratory study i.e. extensive literature review and a case study includes survey and interviews which later on investigated through their application in a public sector organization in Pakistan.
Real Root Isolation of Polynomial Equations Based on Hybrid Computation
Venue: arXiv cs.SC 2012
Year: 2012

A new algorithm for real root isolation of polynomial equations based on hybrid computation is presented in this paper. Firstly, the approximate (complex) zeros of the given polynomial equations are obtained via homotopy continuation method. Then, for each approximate zero, an initial box relying on the Kantorovich theorem is constructed, which contains the corresponding accurate zero. Finally, the Krawczyk interval iteration with interval arithmetic is applied to the initial boxes so as to check whether or not the corresponding approximate zeros are real and to obtain the real root isolation boxes. Meanwhile, an empirical construction of initial box is provided for higher performance. Our experiments on many benchmarks show that the new hybrid method is more efficient, compared with the traditional symbolic approaches.
Tracking Tetrahymena Pyriformis Cells using Decision Trees
Venue: arXiv cs.CV 2012
Year: 2012

Matching cells over time has long been the most difficult step in cell tracking. In this paper, we approach this problem by recasting it as a classification problem. We construct a feature set for each cell, and compute a feature difference vector between a cell in the current frame and a cell in a previous frame. Then we determine whether the two cells represent the same cell over time by training decision trees as our binary classifiers. With the output of decision trees, we are able to formulate an assignment problem for our cell association task and solve it using a modified version of the Hungarian algorithm.
Formal Verification of Monad Transformers
Venue: arXiv cs.LO 2012
Year: 2012

We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or type quantification; instead, we rely on a domain-theoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses. We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes.
Design for Distributed Moroccan Hospital Pharmacy Information Environment with Service Oriented Architecture
Venue: arXiv cs.SE 2012
Year: 2012

In the last five years, Moroccan e-health system has focused on improving the quality of patient care services by making use of advanced Information and Communications Technologies (ICT) solutions. In actual fact, achieving runtime and efficient information sharing, through large-scale distributed environments such as e-health system, is not a trivial task. It seems to present many issues due to the heterogeneity and complex nature of data resources. This concerns, in particular, Moroccan Hospital Pharmacy Information System (HPIS) which needs to interact with several disparate medical information systems. Service Oriented Architecture (SOA) offers solution that is both flexible and practical to effectively address the problem of interoperability of e-health systems. In this paper, we discuss the limits and challenges of the current Moroccan information system intended for hospital pharmacy. We therefore propose a global Web services-based e-health architecture for integrating different heterogeneous blocks and various data resources of this system. We also present a solution to secure Web services communication using WS-SecurityPolicy.
Verifying an algorithm computing Discrete Vector Fields for digital imaging
Venue: arXiv cs.AI 2012
Year: 2012

In this paper, we present a formalization of an algorithm to construct admissible discrete vector fields in the Coq theorem prover taking advantage of the SSReflect library. Discrete vector fields are a tool which has been welcomed in the homological analysis of digital images since it provides a procedure to reduce the amount of information but preserving the homological properties. In particular, thanks to discrete vector fields, we are able to compute, inside Coq, homological properties of biomedical images which otherwise are out of the reach of this system.
On the Sum Capacity of the Discrete Memoryless Interference Channel with One-Sided Weak Interference and Mixed Interference
Venue: arXiv cs.IT 2012
Year: 2012

The sum capacity of a class of discrete memoryless interference channels is determined. This class of channels is defined analogous to the Gaussian Z-interference channel with weak interference; as a result, the sum capacity is achieved by letting the transceiver pair subject to the interference communicates at a rate such that its message can be decoded at the unintended receiver using single user detection. Moreover, this class of discrete memoryless interference channels is equivalent in capacity region to certain discrete degraded interference channels. This allows the construction of a capacity outer-bound using the capacity region of associated degraded broadcast channels. The same technique is then used to determine the sum capacity of the discrete memoryless interference channel with mixed interference. The above results allow one to determine sum capacities or capacity regions of several new discrete memoryless interference channels.
MDS and Self-dual Codes over Rings
Venue: arXiv cs.IT 2012
Year: 2012

In this paper we give the structure of constacyclic codes over formal power series and chain rings. We also present necessary and sufficient conditions on the existence of MDS codes over principal ideal rings. These results allow for the construction of infinite families of MDS self-dual codes over finite chain rings, formal power series and principal ideal rings.
An Approach to Model Interest for Planetary Rover through Dezert-Smarandache Theory
Venue: arXiv cs.AI 2012
Year: 2012

In this paper, we propose an approach for assigning an interest level to the goals of a planetary rover. Assigning an interest level to goals, allows the rover autonomously to transform and reallocate the goals. The interest level is defined by data-fusing payload and navigation information. The fusion yields an "interest map", that quantifies the level of interest of each area around the rover. In this way the planner can choose the most interesting scientific objectives to be analyzed, with limited human intervention, and reallocates its goals autonomously. The Dezert-Smarandache Theory of Plausible and Paradoxical Reasoning was used for information fusion: this theory allows dealing with vague and conflicting data. In particular, it allows us directly to model the behavior of the scientists that have to evaluate the relevance of a particular set of goals. The paper shows an application of the proposed approach to the generation of a reliable interest map.
Robust Mission Design Through Evidence Theory and Multi-Agent Collaborative Search
Venue: arXiv cs.CE 2012
Year: 2012

In this paper, the preliminary design of a space mission is approached introducing uncertainties on the design parameters and formulating the resulting reliable design problem as a multiobjective optimization problem. Uncertainties are modelled through evidence theory and the belief, or credibility, in the successful achievement of mission goals is maximised along with the reliability of constraint satisfaction. The multiobjective optimisation problem is solved through a novel algorithm based on the collaboration of a population of agents in search for the set of highly reliable solutions. Two typical problems in mission analysis are used to illustrate the proposed methodology.
Isabelle/jEdit --- a Prover IDE within the PIDE framework
Venue: arXiv cs.LO 2012
Year: 2012

PIDE is a general framework for document-oriented prover interaction and integration, based on a bilingual architecture that combines ML and Scala. The overall aim is to connect LCF-style provers like Isabelle (or Coq or HOL) with sophisticated front-end technology on the JVM platform, overcoming command-line interaction at last. The present system description specifically covers Isabelle/jEdit as part of the official release of Isabelle2011-1 (October 2011). It is a concrete Prover IDE implementation based on Isabelle/PIDE library modules (implemented in Scala) on the one hand, and the well-known text editor framework of jEdit (implemented in Java) on the other hand. The interaction model of our Prover IDE follows the idea of continuous proof checking: the theory source text is annotated by semantic information by the prover as it becomes available incrementally. This works via an asynchronous protocol that neither blocks the editor nor stops the prover from exploiting parallelism on multi-core hardware. The jEdit GUI provides standard metaphors for augmented text editing (highlighting, squiggles, tooltips, hyperlinks etc.) that we have instrumented to render the formal content from the prover context. Further refinement of the jEdit display engine via suitable plugins and fonts approximates mathematical rendering in the text buffer, including symbols from the TeX repertoire, and sub-/superscripts. Isabelle/jEdit is presented here both as a usable interface for current Isabelle, and as a reference application to inspire further projects based on PIDE.
Optimal Selection of Assets Investing Composition Plan based on Grey Multi Objective Programming method
Venue: arXiv cs.CE 2012
Year: 2012

The problem for selection of appropriate assets investing composition projects such as assets rationalization plays an important role in promotion of business systems. We consider the assets investing composition plan problems subject to grey multiobjective programming with the grey inequality constraints. In this paper, we show in detail the entire process of the application from modeling the case problem to generating its solution. To solve the grey multi objective programming problem, we then develop and apply an algorithm of grey multiple objective programming by weighting method and an algorithm of grey multiple objective programming based on q -positioned programming method. These algorithms all regard as of great importance uncertainty (greyness) at grey multiobjective programming and simple and easy the calculating process. The calculating examples of paper also show ability and effectiveness of algorithms.
HMRF-EM-image: Implementation of the Hidden Markov Random Field Model and its Expectation-Maximization Algorithm
Venue: arXiv cs.CV 2012
Year: 2012

In this project, we study the hidden Markov random field (HMRF) model and its expectation-maximization (EM) algorithm. We implement a MATLAB toolbox named HMRF-EM-image for 2D image segmentation using the HMRF-EM framework. This toolbox also implements edge-prior-preserving image segmentation, and can be easily reconfigured for other problems, such as 3D image segmentation.
A unified approach to truthful scheduling on related machines
Venue: arXiv cs.DS 2012
Year: 2012

We present a unified framework for designing deterministic monotone polynomial time approximation schemes (PTAS's) for a wide class of scheduling problems on uniformly related machines. This class includes (among others) minimizing the makespan, maximizing the minimum load, and minimizing the l_p norm of the machine loads vector. Previously, this kind of result was only known for the makespan objective. Monotone algorithms have the property that an increase in the speed of a machine cannot decrease the amount of work assigned to it. The key idea of our novel method is to show that for goal functions that are sufficiently well-behaved functions of the machine loads, it is possible to compute in polynomial time a highly structured nearly optimal schedule. Monotone approximation schemes have an important role in the emerging area of algorithmic mechanism design. In the game-theoretical setting of these scheduling problems there is a social goal, which is one of the objective functions that we study. Each machine is controlled by a selfish single-parameter agent, where its private information is its cost of processing a unit sized job, which is also the inverse of the speed of its machine. Each agent wishes to maximize its own profit, defined as the payment it receives from the mechanism minus its cost for processing all jobs assigned to it, and places a bid which corresponds to its private information. For each one of the problems, we show that we can calculate payments that guarantee truthfulness in an efficient manner. Thus, there exists a dominant strategy where agents report their true speeds, and we show the existence of a truthful mechanism which can be implemented in polynomial time, where the social goal is approximated within a factor of 1+epsilon for every epsilon>0.
Classification of Approaches and Challenges of Frequent Subgraphs Mining in Biological Networks
Venue: arXiv cs.AI 2012
Year: 2012

Understanding the structure and dynamics of biological networks is one of the important challenges in system biology. In addition, increasing amount of experimental data in biological networks necessitate the use of efficient methods to analyze these huge amounts of data. Such methods require to recognize common patterns to analyze data. As biological networks can be modeled by graphs, the problem of common patterns recognition is equivalent with frequent sub graph mining in a set of graphs. In this paper, at first the challenges of frequent subgrpahs mining in biological networks are introduced and the existing approaches are classified for each challenge. then the algorithms are analyzed on the basis of the type of the approach they apply for each of the challenges.
Designing various component analysis at will
Venue: arXiv cs.CV 2012
Year: 2012

This paper provides a generic framework of component analysis (CA) methods introducing a new expression for scatter matrices and Gram matrices, called Generalized Pairwise Expression (GPE). This expression is quite compact but highly powerful: The framework includes not only (1) the standard CA methods but also (2) several regularization techniques, (3) weighted extensions, (4) some clustering methods, and (5) their semi-supervised extensions. This paper also presents quite a simple methodology for designing a desired CA method from the proposed framework: Adopting the known GPEs as templates, and generating a new method by combining these templates appropriately.
Erasure Coding for Real-Time Streaming
Venue: arXiv cs.IT 2012
Year: 2012

We consider a real-time streaming system where messages are created sequentially at the source, and are encoded for transmission to the receiver over a packet erasure link. Each message must subsequently be decoded at the receiver within a given delay from its creation time. The goal is to construct an erasure correction code that achieves the maximum message size when all messages must be decoded by their respective deadlines under a specified set of erasure patterns (erasure model). We present an explicit intrasession code construction that is asymptotically optimal under erasure models containing a limited number of erasures per coding window, per sliding window, and containing erasure bursts of a limited length.
OGCOSMO: An auxiliary tool for the study of the Universe within hierarchical scenario of structure formation
Venue: arXiv cs.CE 2012
Year: 2012

In this work is presented the software OGCOSMO. This program was written using high level design methodology (HLDM), that is based on the use of very high level (VHL) programing language as main, and the use of the intermediate level (IL) language only for the critical processing time. The languages used are PYTHON (VHL) and FORTRAN (IL). The core of OGCOSMO is a package called OGC{\_}lib. This package contains a group of modules for the study of cosmological and astrophysical processes, such as: comoving distance, relation between redshift and time, cosmic star formation rate, number density of dark matter haloes and mass function of supermassive black holes (SMBHs). The software is under development and some new features will be implemented for the research of stochastic background of gravitational waves (GWs) generated by: stellar collapse to form black holes, binary systems of SMBHs. Even more, we show that the use of HLDM with PYTHON and FORTRAN is a powerful tool for producing astrophysical softwares.
Joint Filter Design of Alternate MIMO AF Relaying Networks with Interference Alignment
Venue: arXiv cs.IT 2012
Year: 2012

We study in this paper a two-hop relaying network consisting of one source, one destination, and three amplify-and-forward (AF) relays operating in a half-duplex mode. In order to compensate for the inherent loss of capacity pre-log factor 1/2 in a half-duplex mode, we consider alternate transmission protocol among three relays where two relays and the other relay alternately forward messages from source to destination. We consider a multiple-antenna environment where all nodes have $M$ antennas. Aligning the inter-relay interference due to the alternate transmission is utilized to make additional degrees of freedom (DOFs) and recover the pre-log factor loss. It is shown that the proposed relaying scheme can achieve $\frac{3M}{4}$ DOFs compared with the $\frac{M}{2}$ DOFs of conventional AF relaying. In addition, suboptimal linear filter designs for a source and three relays are proposed to maximize the system achievable sum-rate for different fading scenarios when the destination utilizes a linear minimum mean-square error filter for decoding. We verify from our selected numerical results that the proposed filter designs give significant improvement over a naive filter or conventional relaying schemes.