OpenRaiser/Intern-Atlas huggingface dataset:
LMEEC: Layered Multi-Hop Energy Efficient Cluster-based Routing Protocol for Wireless Sensor Networks
Venue: arXiv cs.NI 2012
Year: 2012

In this paper, we propose LMEEC, a cluster-based routing protocol with low energy consumption for wireless sensor networks. Our protocol is based on a strategy which aims to provide a more reasonable exploitation of the selected nodes (cluster-heads) energy. Simulation results show the effectiveness of LMEEC in decreasing the energy consumption, and in prolonging the network lifetime, compared to LEACH.
Umgebungserfassungssystem fuer mobile Roboter (environment logging system for mobile autonomous robots)
Venue: arXiv cs.RO 2012
Year: 2012

This diploma thesis describes the theoretical bases, the conception of the module and the final result of the development process in application. for the environment logging with a small mobile robot for interiors should be sketched an economical alternative to the expensive laser scanners. the structure, color or the material of the objects in the radius of action, as well as the environment brightness and illuminating are to have thereby no influence on the results of measurement.
On the Dynamic Qualitative Behaviour of Universal Computation
Venue: arXiv cs.CC 2012
Year: 2012

We explore the possible connections between the dynamic behaviour of a system and Turing universality in terms of the system's ability to (effectively) transmit and manipulate information. Some arguments will be provided using a defined compression-based transition coefficient which quantifies the sensitivity of a system to being programmed. In the same spirit, a list of conjectures concerning the ability of Busy Beaver Turing machines to perform universal computation will be formulated. The main working hypothesis is that universality is deeply connected to the qualitative behaviour of a system, particularly to its ability to react to external stimulus--as it needs to be programmed--and to its capacity for transmitting this information.
Computer Runtimes and the Length of Proofs: On an Algorithmic Probabilistic Application to Waiting Times in Automatic Theorem Proving
Venue: arXiv cs.CC 2012
Year: 2012

This paper is an experimental exploration of the relationship between the runtimes of Turing machines and the length of proofs in formal axiomatic systems. We compare the number of halting Turing machines of a given size to the number of provable theorems of first-order logic of a given size, and the runtime of the longest-running Turing machine of a given size to the proof length of the most-difficult-to-prove theorem of a given size. It is suggested that theorem provers are subject to the same non-linear tradeoff between time and size as computer programs are, affording the possibility of determining optimal timeouts and waiting times in automatic theorem proving. I provide the statistics for some small choices of parameters for both of these systems.
Wireless Network-Coded Accumulate-Compute and Forward Two-Way Relaying
Venue: arXiv cs.IT 2012
Year: 2012

The design of modulation schemes for the physical layer network-coded two way wireless relaying scenario is considered. It was observed by Koike-Akino et al. for the two way relaying scenario, that adaptively changing the network coding map used at the relay according to the channel conditions greatly reduces the impact of multiple access interference which occurs at the relay during the MA Phase and all these network coding maps should satisfy a requirement called exclusive law. We extend this approach to an Accumulate-Compute and Forward protocol which employs two phases: Multiple Access (MA) phase consisting of two channel uses with independent messages in each channel use, and Broadcast (BC) phase having one channel use. Assuming that the two users transmit points from the same 4-PSK constellation, every such network coding map that satisfies the exclusive law can be represented by a Latin Square with side 16, and conversely, this relationship can be used to get the network coding maps satisfying the exclusive law. Two methods of obtaining this network coding map to be used at the relay are discussed. Using the structural properties of the Latin Squares for a given set of parameters, the problem of finding all the required maps is reduced to finding a small set of maps. Having obtained all the Latin Squares, the set of all possible channel realizations is quantized, depending on which one of the Latin Squares obtained optimizes the performance. The quantization thus obtained, is shown to be the same as the one obtained in [7] for the 2-stage bidirectional relaying.
Approximations of the Euclidean distance by chamfer distances
Venue: arXiv cs.IT 2012
Year: 2012

Chamfer distances play an important role in the theory of distance transforms. Though the determination of the exact Euclidean distance transform is also a well investigated area, the classical chamfering method based upon "small" neighborhoods still outperforms it e.g. in terms of computation time. In this paper we determine the best possible maximum relative error of chamfer distances under various boundary conditions. In each case some best approximating sequences are explicitly given. Further, because of possible practical interest, we give all best approximating sequences in case of small (i.e. 5 by 5 and 7 by 7) neighborhoods.
Termination of Nondeterministic Quantum Programs
Venue: arXiv cs.LO 2012
Year: 2012

We define a language-independent model of nondeterministic quantum programs in which a quantum program consists of a finite set of quantum processes. These processes are represented by quantum Markov chains over the common state space. An execution of a nondeterministic quantum program is modeled by a sequence of actions of individual processes. These actions are described by super-operators on the state Hilbert space. At each step of an execution, a process is chosen nondeterministically to perform the next action. A characterization of reachable space and a characterization of diverging states of a nondeterministic quantum program are presented. We establish a zero-one law for termination probability of the states in the reachable space of a nondeterministic quantum program. A combination of these results leads to a necessary and sufficient condition for termination of nondeterministic quantum programs. Based on this condition, an algorithm is found for checking termination of nondeterministic quantum programs within a fixed finite-dimensional state space. A striking difference between nondeterministic classical and quantum programs is shown by example: it is possible that each of several quantum programs simulates the same classical program which terminates with probability 1, but the nondeterministic program consisting of them terminates with probability 0 due to the interference carried in the execution of them.
Sciduction: Combining Induction, Deduction, and Structure for Verification and Synthesis
Venue: arXiv cs.LO 2012
Year: 2012

Even with impressive advances in automated formal methods, certain problems in system verification and synthesis remain challenging. Examples include the verification of quantitative properties of software involving constraints on timing and energy consumption, and the automatic synthesis of systems from specifications. The major challenges include environment modeling, incompleteness in specifications, and the complexity of underlying decision problems. This position paper proposes sciduction, an approach to tackle these challenges by integrating inductive inference, deductive reasoning, and structure hypotheses. Deductive reasoning, which leads from general rules or concepts to conclusions about specific problem instances, includes techniques such as logical inference and constraint solving. Inductive inference, which generalizes from specific instances to yield a concept, includes algorithmic learning from examples. Structure hypotheses are used to define the class of artifacts, such as invariants or program fragments, generated during verification or synthesis. Sciduction constrains inductive and deductive reasoning using structure hypotheses, and actively combines inductive and deductive reasoning: for instance, deductive techniques generate examples for learning, and inductive reasoning is used to guide the deductive engines. We illustrate this approach with three applications: (i) timing analysis of software; (ii) synthesis of loop-free programs, and (iii) controller synthesis for hybrid systems. Some future applications are also discussed.
Secure SQL Server - Enabling Secure Access to Remote Relational Data
Venue: arXiv cs.CY 2012
Year: 2012

The Secure SQL Server - SecSS, is a technology primarily developed to enable self-service governance of states, as described in (Paulin 2012). Self-service governance is a novel model of governance that rejects service-based public administration and instead proposes that governed subjects manage their legal relations in a self-service manner, based on ad-hoc determination of eligibilities. In this article we describe the prototype SecSS and its evaluation in a complex governmental scenario.
Formalization of semantic network of image constructions in electronic content
Venue: arXiv cs.CL 2012
Year: 2012

A formal theory based on a binary operator of directional associative relation is constructed in the article and an understanding of an associative normal form of image constructions is introduced. A model of a commutative semigroup, which provides a presentation of a sentence as three components of an interrogative linguistic image construction, is considered.
Turing Machines and Understanding Computational Complexity
Venue: arXiv cs.CC 2012
Year: 2012

We describe the Turing Machine, list some of its many influences on the theory of computation and complexity of computations, and illustrate its importance.
Novel Relations between the Ergodic Capacity and the Average Bit Error Rate
Venue: arXiv cs.IT 2012
Year: 2012

Ergodic capacity and average bit error rate have been widely used to compare the performance of different wireless communication systems. As such recent scientific research and studies revealed strong impact of designing and implementing wireless technologies based on these two performance indicators. However and to the best of our knowledge, the direct links between these two performance indicators have not been explicitly proposed in the literature so far. In this paper, we propose novel relations between the ergodic capacity and the average bit error rate of an overall communication system using binary modulation schemes for signaling with a limited bandwidth and operating over generalized fading channels. More specifically, we show that these two performance measures can be represented in terms of each other, without the need to know the exact end-to-end statistical characterization of the communication channel. We validate the correctness and accuracy of our newly proposed relations and illustrated their usefulness by considering some classical examples.
Upper Bound on the Capacity of Gaussian Channels with Noisy Feedback
Venue: arXiv cs.IT 2012
Year: 2012

We consider an additive Gaussian channel with additive Gaussian noise feedback. We derive an upper bound on the n-block capacity (defined by Cover [1]). It is shown that this upper bound can be obtained by solving a convex optimization problem. With stationarity assumptions on Gaussian noise processes, we characterize the limit of the n-block upper bound and prove that this limit is the upper bound of the noisy feedback (shannon) capacity.
Per-antenna Constant Envelope Precoding for Large Multi-User MIMO Systems
Venue: arXiv cs.IT 2012
Year: 2012

We consider the multi-user MIMO broadcast channel with $M$ single-antenna users and $N$ transmit antennas under the constraint that each antenna emits signals having constant envelope (CE). The motivation for this is that CE signals facilitate the use of power-efficient RF power amplifiers. Analytical and numerical results show that, under certain mild conditions on the channel gains, for a fixed $M$, array gain is achievable even under the stringent per-antenna CE constraint (essentially, for a fixed $M$, at sufficiently large $N$ the total transmitted power can be reduced with increasing $N$ while maintaining a fixed information rate to each user). Simulations for the i.i.d. Rayleigh fading channel show that the total transmit power can be reduced linearly with increasing $N$ (i.e., an O(N) array gain). We also propose a precoding scheme which finds near-optimal CE signals to be transmitted, and has O(MN) complexity. Also, in terms of the total transmit power required to achieve a fixed desired information sum-rate, despite the stringent per-antenna CE constraint, the proposed CE precoding scheme performs close to the sum-capacity achieving scheme for an average-only total transmit power constrained channel.
Customers Behavior Modeling by Semi-Supervised Learning in Customer Relationship Management
Venue: arXiv cs.LG 2012
Year: 2012

Leveraging the power of increasing amounts of data to analyze customer base for attracting and retaining the most valuable customers is a major problem facing companies in this information age. Data mining technologies extract hidden information and knowledge from large data stored in databases or data warehouses, thereby supporting the corporate decision making process. CRM uses data mining (one of the elements of CRM) techniques to interact with customers. This study investigates the use of a technique, semi-supervised learning, for the management and analysis of customer-related data warehouse and information. The idea of semi-supervised learning is to learn not only from the labeled training data, but to exploit also the structural information in additionally available unlabeled data. The proposed semi-supervised method is a model by means of a feed-forward neural network trained by a back propagation algorithm (multi-layer perceptron) in order to predict the category of an unknown customer (potential customers). In addition, this technique can be used with Rapid Miner tools for both labeled and unlabeled data.
Theoretical Modeling and Simulation of Phase-Locked Loop (PLL) for Clock Data Recovery (CDR)
Venue: arXiv cs.AR 2012
Year: 2012

Modern communication and computer systems require rapid (Gbps), efficient and large bandwidth data transfers. Agressive scaling of digital integrated systems allow buses and communication controller circuits to be integrated with the microprocessor on the same chip. The Peripheral Component Interconnect Express (PCIe) protocol handles all communcation between the central processing unit (CPU) and hardware devices. PCIe buses require efficient clock data recovery circuits (CDR) to recover clock signals embedded in data during transmission. This paper describes the theoretical modeling and simulation of a phase-locked loop (PLL) used in a CDR circuit. A simple PLL architecture for a 5 GHz CDR circuit is proposed and elaborated in this work. Simulations were carried out using a Hardware Description Language, Verilog- AMS. The effect of jitter on the proposed design is also simulated and evaluated in this work. It was found that the proposed design is robust against both input and VCO jitter.
A type reduction theory for systems with replicated components
Venue: arXiv cs.LO 2012
Year: 2012

The Parameterised Model Checking Problem asks whether an implementation Impl(t) satisfies a specification Spec(t) for all instantiations of parameter t. In general, t can determine numerous entities: the number of processes used in a network, the type of data, the capacities of buffers, etc. The main theme of this paper is automation of uniform verification of a subclass of PMCP with the parameter of the first kind, i.e. the number of processes in the network. We use CSP as our formalism. We present a type reduction theory, which, for a given verification problem, establishes a function ϕthat maps all (sufficiently large) instantiations T of the parameter to some fixed type T^ and allows us to deduce that if Spec(T^) is refined by ϕ(Impl(T)), then (subject to certain assumptions) Spec(T) is refined by Impl(T). The theory can be used in practice by combining it with a suitable abstraction method that produces a t-independent process Abstr that is refined by ϕ(Impl(T)) for all sufficiently large T. Then, by testing (with a model checker) if the abstract model Abstr refines Spec(T^), we can deduce a positive answer to the original uniform verification problem. The type reduction theory relies on symbolic representation of process behaviour. We develop a symbolic operational semantics for CSP processes that satisfy certain normality requirements, and we provide a set of translation rules that allow us to concretise symbolic transition graphs. Based on this, we prove results that allow us to infer behaviours of a process instantiated with uncollapsed types from known behaviours of the same process instantiated with a reduced type. One of the main advantages of our symbolic operational semantics and the type reduction theory is their generality, which makes them applicable in a wide range of settings.
Stochastic Loss Aversion for Random Medium Access
Venue: arXiv cs.GT 2012
Year: 2012

We consider a slotted-ALOHA LAN with loss-averse, noncooperative greedy users. To avoid non-Pareto equilibria, particularly deadlock, we assume probabilistic loss-averse behavior. This behavior is modeled as a modulated white noise term, in addition to the greedy term, creating a diffusion process modeling the game. We observe that when player's modulate with their throughput, a more efficient exploration of play-space results, and so finding a Pareto equilibrium is more likely over a given interval of time.
On Polynomial Remainder Codes
Venue: arXiv cs.IT 2012
Year: 2012

Polynomial remainder codes are a large class of codes derived from the Chinese remainder theorem that includes Reed-Solomon codes as a special case. In this paper, we revisit these codes and study them more carefully than in previous work. We explicitly allow the code symbols to be polynomials of different degrees, which leads to two different notions of weight and distance. Algebraic decoding is studied in detail. If the moduli are not irreducible, the notion of an error locator polynomial is replaced by an error factor polynomial. We then obtain a collection of gcd-based decoding algorithms, some of which are not quite standard even when specialized to Reed-Solomon codes.
Investigating the Awareness of Applying the Important Web Application Development and Measurement Practices in Small Software Firms
Venue: arXiv cs.SE 2012
Year: 2012

This paper aims to discuss the pilot study and analysis of the current development and measurement practices in Jordanian small software firms. It is conducted because most developers build web applications without using any specific development method and don't know how to integrate the suitable measurements inside the process to improve and reduce defect, time and rework of the development life cycle. Furthermore the objectives of this pilot study are firstly; determine the real characteristics of small software firms in Jordan. Secondly, investigate the current development and measurement practices. Thirdly, examine the need of new development methodology for building web application in small software firms. Consequently, Pilot survey was conducted in Jordanian small software firms. Descriptive statistics analysis was used to rank the development and measurements methods according to their importance. This paper presents the data, analysis and finding based on pilot survey. These actual findings of this survey will contribute to build new methodology for developing web applications in small software firms taking to account how to integrate the suitable measurement program to the whole development process and also will provide useful information to those who are doing research in the same area.
Recognizing Bangla Grammar using Predictive Parser
Venue: arXiv cs.CL 2012
Year: 2012

We describe a Context Free Grammar (CFG) for Bangla language and hence we propose a Bangla parser based on the grammar. Our approach is very much general to apply in Bangla Sentences and the method is well accepted for parsing a language of a grammar. The proposed parser is a predictive parser and we construct the parse table for recognizing Bangla grammar. Using the parse table we recognize syntactical mistakes of Bangla sentences when there is no entry for a terminal in the parse table. If a natural language can be successfully parsed then grammar checking from this language becomes possible. The proposed scheme is based on Top down parsing method and we have avoided the left recursion of the CFG using the idea of left factoring.
Improvement of Anomoly Detection Algorithms in Hyperspectral Images using Discrete Wavelet Transform
Venue: arXiv cs.OH 2012
Year: 2012

Recently anomaly detection (AD) has become an important application for target detection in hyperspectral remotely sensed images. In many applications, in addition to high accuracy of detection we need a fast and reliable algorithm as well. This paper presents a novel method to improve the performance of current AD algorithms. The proposed method first calculates Discrete Wavelet Transform (DWT) of every pixel vector of image using Daubechies4 wavelet. Then, AD algorithm performs on four bands of "Wavelet transform" matrix which are the approximation of main image. In this research some benchmark AD algorithms including Local RX, DWRX and DWEST have been implemented on Airborne Visible/Infrared Imaging Spectrometer (AVIRIS) hyperspectral datasets. Experimental results demonstrate significant improvement of runtime in proposed method. In addition, this method improves the accuracy of AD algorithms because of DWT's power in extracting approximation coefficients of signal, which contain the main behaviour of signal, and abandon the redundant information in hyperspectral image data.
Reflection Scan: an Off-Path Attack on TCP
Venue: arXiv cs.CR 2012
Year: 2012

The paper demonstrates how traffic load of a shared packet queue can be exploited as a side channel through which protected information leaks to an off-path attacker. The attacker sends to a victim a sequence of identical spoofed segments. The victim responds to each segment in the sequence (the sequence is reflected by the victim) if the segments satisfy a certain condition tested by the attacker. The responses do not reach the attacker directly, but induce extra load on a routing queue shared between the victim and the attacker. Increased processing time of packets traversing the queue reveal that the tested condition was true. The paper concentrates on the TCP, but the approach is generic and can be effective against other protocols that allow to construct requests which are conditionally answered by the victim. A proof of concept was created to assess applicability of the method in real-life scenarios.