OpenRaiser/Intern-Atlas huggingface dataset:
Reducing Weak to Strong Bisimilarity in CCP
Venue: arXiv cs.PL 2012
Year: 2012

Concurrent constraint programming (ccp) is a well-established model for concurrency that singles out the fundamental aspects of asynchronous systems whose agents (or processes) evolve by posting and querying (partial) information in a global medium. Bisimilarity is a standard behavioural equivalence in concurrency theory. However, only recently a well-behaved notion of bisimilarity for ccp, and a ccp partition refinement algorithm for deciding the strong version of this equivalence have been proposed. Weak bisimiliarity is a central behavioural equivalence in process calculi and it is obtained from the strong case by taking into account only the actions that are observable in the system. Typically, the standard partition refinement can also be used for deciding weak bisimilarity simply by using Milner's reduction from weak to strong bisimilarity; a technique referred to as saturation. In this paper we demonstrate that, because of its involved labeled transitions, the above-mentioned saturation technique does not work for ccp. We give an alternative reduction from weak ccp bisimilarity to the strong one that allows us to use the ccp partition refinement algorithm for deciding this equivalence.
Coherent Minimisation: Towards efficient tamper-proof compilation
Venue: arXiv cs.PL 2012
Year: 2012

Automata representing game-semantic models of programs are meant to operate in environments whose input-output behaviour is constrained by the rules of a game. This can lead to a notion of equivalence between states which is weaker than the conventional notion of bisimulation, since not all actions are available to the environment. An environment which attempts to break the rules of the game is, effectively, mounting a low-level attack against a system. In this paper we show how (and why) to enforce game rules in games-based hardware synthesis and how to use this weaker notion of equivalence, called coherent equivalence, to aggressively minimise automata.
Partial Degree Bounded Edge Packing Problem with Arbitrary Bounds
Venue: arXiv cs.DS 2012
Year: 2012

We study the Partial Degree Bounded Edge Packing (PDBEP) problem introduced in [5] by Zhang. They have shown that this problem is NP-Hard even for uniform degree constraint. They also presented approximation algorithms for the case when all the vertices have degree constraint of 1 and 2 with approximation ratio of 2 and 32=11 respectively. In this work we study general degree constraint case (arbitrary degree constraint for each vertex) and present two combinatorial approximation algorithms with approximation factors 4 and 2. We also study integer program based solution and present an iterative rounding algorithm with approximation factor 3/(1 - ε)^2 for any positive ε. Next we study the same problem with weighted edges. In this case we present an O(log n) approximation algorithm. Zhang has given an exact O(n^2) complexity algorithm for trees in case of uniform degree constraint. We improve their result by giving O(nlog n) complexity exact algorithm for trees with general degree constraint.
Elaboration of global quality standards for natural and low energy cooling in French tropical island buildings
Venue: arXiv cs.CE 2012
Year: 2012

Electric load profiles of tropical islands in developed countries are characterised by morning, midday and evening peaks arising from all year round high power demand in the commercial and residential sectors, due mostly to air conditioning appliances and bad thermal conception of the building. The work presented in this paper has led to the conception of a global quality standards obtained through optimized bioclimatic urban planning and architectural design, the use of passive cooling architectural components, natural ventilation and energy efficient systems such as solar water heaters. We evaluated, with the aid of an airflow and thermal building simulation software (CODYRUN), the impact of each technical solution on thermal comfort within the building. These technical solutions have been implemented in 280 new pilot dwelling projects through the year 1996.
Advanced Bloom Filter Based Algorithms for Efficient Approximate Data De-Duplication in Streams
Venue: arXiv cs.IR 2012
Year: 2012

Applications involving telecommunication call data records, web pages, online transactions, medical records, stock markets, climate warning systems, etc., necessitate efficient management and processing of such massively exponential amount of data from diverse sources. De-duplication or Intelligent Compression in streaming scenarios for approximate identification and elimination of duplicates from such unbounded data stream is a greater challenge given the real-time nature of data arrival. Stable Bloom Filters (SBF) addresses this problem to a certain extent. . In this work, we present several novel algorithms for the problem of approximate detection of duplicates in data streams. We propose the Reservoir Sampling based Bloom Filter (RSBF) combining the working principle of reservoir sampling and Bloom Filters. We also present variants of the novel Biased Sampling based Bloom Filter (BSBF) based on biased sampling concepts. We also propose a randomized load balanced variant of the sampling Bloom Filter approach to efficiently tackle the duplicate detection. In this work, we thus provide a generic framework for de-duplication using Bloom Filters. Using detailed theoretical analysis we prove analytical bounds on the false positive rate, false negative rate and convergence rate of the proposed structures. We exhibit that our models clearly outperform the existing methods. We also demonstrate empirical analysis of the structures using real-world datasets (3 million records) and also with synthetic datasets (1 billion records) capturing various input distributions.
Online Learning for Ground Trajectory Prediction
Venue: arXiv cs.AI 2012
Year: 2012

This paper presents a model based on an hybrid system to numerically simulate the climbing phase of an aircraft. This model is then used within a trajectory prediction tool. Finally, the Covariance Matrix Adaptation Evolution Strategy (CMA-ES) optimization algorithm is used to tune five selected parameters, and thus improve the accuracy of the model. Incorporated within a trajectory prediction tool, this model can be used to derive the order of magnitude of the prediction error over time, and thus the domain of validity of the trajectory prediction. A first validation experiment of the proposed model is based on the errors along time for a one-time trajectory prediction at the take off of the flight with respect to the default values of the theoretical BADA model. This experiment, assuming complete information, also shows the limit of the model. A second experiment part presents an on-line trajectory prediction, in which the prediction is continuously updated based on the current aircraft position. This approach raises several issues, for which improvements of the basic model are proposed, and the resulting trajectory prediction tool shows statistically significantly more accurate results than those of the default model.
Compositional Verification of Evolving Software Product Lines
Venue: arXiv cs.SE 2012
Year: 2012

This paper presents a novel approach to the design verification of Software Product Lines(SPL). The proposed approach assumes that the requirements and designs are modeled as finite state machines with variability information. The variability information at the requirement and design levels are expressed differently and at different levels of abstraction. Also the proposed approach supports verification of SPL in which new features and variability may be added incrementally. Given the design and requirements of an SPL, the proposed design verification method ensures that every product at the design level behaviorally conforms to a product at the requirement level. The conformance procedure is compositional in the sense that the verification of an entire SPL consisting of multiple features is reduced to the verification of the individual features. The method has been implemented and demonstrated in a prototype tool SPLEnD (SPL Engine for Design Verification) on a couple of fairly large case studies.
GMM-Based Hidden Markov Random Field for Color Image and 3D Volume Segmentation
Venue: arXiv cs.CV 2012
Year: 2012

In this project, we first study the Gaussian-based hidden Markov random field (HMRF) model and its expectation-maximization (EM) algorithm. Then we generalize it to Gaussian mixture model-based hidden Markov random field. The algorithm is implemented in MATLAB. We also apply this algorithm to color image segmentation problems and 3D volume segmentation problems.
Natural Language Understanding Based on Semantic Relations between Sentences
Venue: arXiv cs.CL 2012
Year: 2012

In this paper, we define event expression over sentences of natural language and semantic relations between events. Based on this definition, we formally consider text understanding process having events as basic unit.
Analysis of Large-scale Traffic Dynamics using Non-negative Tensor Factorization
Venue: arXiv cs.LG 2012
Year: 2012

In this paper, we present our work on clustering and prediction of temporal dynamics of global congestion configurations in large-scale road networks. Instead of looking into temporal traffic state variation of individual links, or of small areas, we focus on spatial congestion configurations of the whole network. In our work, we aim at describing the typical temporal dynamic patterns of this network-level traffic state and achieving long-term prediction of the large-scale traffic dynamics, in a unified data-mining framework. To this end, we formulate this joint task using Non-negative Tensor Factorization (NTF), which has been shown to be a useful decomposition tools for multivariate data sequences. Clustering and prediction are performed based on the compact tensor factorization results. Experiments on large-scale simulated data illustrate the interest of our method with promising results for long-term forecast of traffic evolution.
SMML estimators for 1-dimensional continuous data
Venue: arXiv cs.IT 2012
Year: 2012

A method is given for calculating the strict minimum message length (SMML) estimator for 1-dimensional exponential families with continuous sufficient statistics. A set of $n$ equations are found that the $n$ cut-points of the SMML estimator must satisfy. These equations can be solved using Newton's method and this approach is used to produce new results and to replicate results that C. S. Wallace obtained using his boundary rules for the SMML estimator. A rigorous proof is also given that, despite being composed of step functions, the posterior probability corresponding to the SMML estimator is a continuous function of the data.
Fourier Domain Beamforming for Medical Ultrasound
Venue: arXiv cs.IT 2012
Year: 2012

Sonography techniques use multiple transducer elements for tissue visualization. Signals detected at each element are sampled prior to digital beamforming. The required sampling rates are up to 4 times the Nyquist rate of the signal and result in considerable amount of data, that needs to be stored and processed. A developed technique, based on the finite rate of innovation model, compressed sensing (CS) and Xampling ideas, allows to reduce the number of samples needed to reconstruct an image comprised of strong reflectors. A significant drawback of this method is its inability to treat speckle, which is of significant importance in medical imaging. Here we build on previous work and show explicitly how to perform beamforming in the Fourier domain. Beamforming in frequency exploits the low bandwidth of the beamformed signal and allows to bypass the oversampling dictated by digital implementation of beamforming in time. We show that this allows to obtain the same beamformed image as in standard beamforming but from far fewer samples. Finally, we present an analysis based CS-technique that allows for further reduction in sampling rate, using only a portion of the beamformed signal's bandwidth, namely, sampling the signal at sub-Nyquist rates. We demonstrate our methods on in vivo cardiac ultrasound data and show that reductions up to 1/25 over standard beamforming rates are possible.
D'Event-B vers UML/OCL en passant par UML/EM-OCL
Venue: arXiv cs.SE 2012
Year: 2012

To overcome the limitations of both approaches classical and formal for the development of complex software, we proposed a hybrid approach combining the formal approach (Event-B) and the classical approach (UML/OCL). Upstream phases of our approach include: Rewriting the requirements document, Refinement strategy, Abstract specification and Horizontal refinement. We have shown the feasibility of our approach on a case study: An Electronic Hotel Key System (SCEH). The problem of transition from the formal (Event-B) to the semi-formal (UML/OCL) is processed through our extension to OCL (EM-OCL).
Balance properties of Arnoux-Rauzy words
Venue: arXiv cs.FL 2012
Year: 2012

The paper deals with balances and imbalances in Arnoux-Rauzy words. We provide sufficient conditions for $C$-balancedness, but our results indicate that even a characterization of 2-balanced Arnoux-Rauzy words on a 3-letter alphabet is not immediate.
Cumulative Sum Algorithm for Detecting SYN Flooding Attacks
Venue: arXiv cs.NI 2012
Year: 2012

SYN flooding attacks generate enormous packets by a large number of agents and can easily exhaust the computing and communication resources of a victim within a short period of time. In this paper, we propose a lightweight method for detecting SYN flooding attack by non-parametric cumulative sum algorithm. We experiment with real SYN flooding attack data set in order to evaluate our method. The results show that our method can detect SYN flooding attack very well.
A Modal Characterization of Alternating Approximate Bisimilarity
Venue: arXiv cs.LO 2012
Year: 2012

Recently, alternating transition systems are adopted to describe control systems with disturbances and their finite abstract systems. In order to capture the equivalence relation between these systems, a notion of alternating approximate bisimilarity is introduced. This paper aims to establish a modal characterization for alternating approximate bisimilarity. Moreover, based on this result, we provide a link between specifications satisfied by the samples of control systems with disturbances and their finite abstractions.
Performance Evaluation of an Orthogonal Frequency Division Multiplexing based Wireless Communication System with implementation of Least Mean Square Equalization technique
Venue: arXiv cs.IT 2012
Year: 2012

Orthogonal Frequency Division Multiplexing (OFDM) has recently been applied in wireless communication systems due to its high data rate transmission capability with high bandwidth efficiency and its robustness to multi-path delay. Fading is the one of the major aspect which is considered in the receiver. To cancel the effect of fading, channel estimation and equalization procedure must be done at the receiver before data demodulation. This paper mainly deals with pilot based channel estimation techniques for OFDM communication over frequency selective fading channels. This paper proposes a specific approach to channel equalization for Orthogonal Frequency Division Multiplex (OFDM) systems. Inserting an equalizer realized as an adaptive system before the FFT processing, the influence of variable delay and multi path could be mitigated in order to remove or reduce considerably the guard interval and to gain some spectral efficiency. The adaptive algorithm is based on adaptive filtering with averaging (AFA) for parameter update. Based on the development of a model of the OFDM system, through extensive computer simulations, we investigate the performance of the channel equalized system. The results show much higher convergence and adaptation rate compared to one of the most frequently used algorithms - Least Mean Squares (LMS).
Bibliometric Networks
Venue: arXiv cs.DL 2012
Year: 2012

This text is based on a translation of a chapter in a handbook about network analysis (published in German) where we tried to make beginners familiar with some basic notions and recent developments of network analysis applied to bibliometric issues (Havemann and Scharnhorst 2010). We have added some recent references.
A Neural Network Approach to ECG Denoising
Venue: arXiv cs.CE 2012
Year: 2012

We propose an ECG denoising method based on a feed forward neural network with three hidden layers. Particulary useful for very noisy signals, this approach uses the available ECG channels to reconstruct a noisy channel. We tested the method, on all the records from Physionet MIT-BIH Arrhythmia Database, adding electrode motion artifact noise. This denoising method improved the perfomance of publicly available ECG analysis programs on noisy ECG signals. This is an offline method that can be used to remove noise from very corrupted Holter records.
Development of a new model to predict indoor daylighting: Integration in CODYRUN software and validation
Venue: arXiv cs.CE 2012
Year: 2012

Many models exist in the scientific literature for determining indoor daylighting values. They are classified in three categories: numerical, simplified and empirical models. Nevertheless, each of these categories of models are not convenient for every application. Indeed, the numerical model requires high calculation time; conditions of use of the simplified models are limited, and experimental models need not only important financial resources but also a perfect control of experimental devices (e.g. scale model), as well as climatic characteristics of the location (e.g. in situ experiment). In this article, a new model based on a combination of multiple simplified models is established. The objective is to improve this category of model. The originality of our paper relies on the coupling of several simplified models of indoor daylighting calculations. The accuracy of the simulation code, introduced into CODYRUN software to simulate correctly indoor illuminance, is then verified. Besides, the software consists of a numerical building simulation code, developed in the Physics and Mathematical Engineering Laboratory for Energy and Environment (P.I.M.E.N.T) at the University of Reunion. Initially dedicated to the thermal, airflow and hydrous phenomena in the buildings, the software has been completed for the calculation of indoor daylighting. New models and algorithms - which rely on a semi-detailed approach - will be presented in this paper. In order to validate the accuracy of the integrated models, many test cases have been considered as analytical, inter-software comparisons and experimental comparisons. In order to prove the accuracy of the new model - which can properly simulate the illuminance - a confrontation between the results obtained from the software (developed in this research paper) and the major made at a given place is described in details. A new statistical indicator to appreciate the margins of errors - named RSD (Reliability of Software Degrees) - is also be defined.
Program Verification in the presence of complex numbers, functions with branch cuts etc
Venue: arXiv cs.SC 2012
Year: 2012

In considering the reliability of numerical programs, it is normal to "limit our study to the semantics dealing with numerical precision" (Martel, 2005). On the other hand, there is a great deal of work on the reliability of programs that essentially ignores the numerics. The thesis of this paper is that there is a class of problems that fall between these two, which could be described as "does the low-level arithmetic implement the high-level mathematics". Many of these problems arise because mathematics, particularly the mathematics of the complex numbers, is more difficult than expected: for example the complex function log is not continuous, writing down a program to compute an inverse function is more complicated than just solving an equation, and many algebraic simplification rules are not universally valid. The good news is that these problems are theoretically capable of being solved, and are practically close to being solved, but not yet solved, in several real-world examples. However, there is still a long way to go before implementations match the theoretical possibilities.
Development of an Anti-collision Model for Vehicles
Venue: arXiv cs.SY 2012
Year: 2012

The Anti Collision device is a detection device meant to be incorporated into cars for the purpose of safety. As opposed to the anti collision devices present in the market today, this system is not designed to control the vehicle. Instead, it serves as an alert in the face of imminent collision. The device is intended to find a way to implement a minimum spacing for cars in traffic in an affordable way. It would also achieve safety for the passengers of a moving car. The device is made up of an infrared transmitter and receiver. Also incorporated into it is an audio visual alarm to work in with the receiver and effectively alert the driver and/or the passengers. To achieve this design, 555 timers coupled both as astable and monostable circuits were used along with a 38 KHz Square Pulse generator. The device works by sending out streams of infrared radiation and when these rays are seen by the other equipped vehicle, both are meant to take the necessary precaution to avert a collision. The device would still sound an alarm even though it is not receiving infrared beams from the oncoming vehicle. This is due to reflection of its own infrared beams. At the end of the design and testing process, overall system was implemented with a constructed work, tested working and perfectly functional.
Concurrent object-oriented development with behavioral design patterns
Venue: arXiv cs.SE 2012
Year: 2012

The development of concurrent applications is challenging because of the complexity of concurrent designs and the hazards of concurrent programming. Architectural modeling using the Unified Modeling Language (UML) can support the development process, but the problem of mapping the model to a concurrent implementation remains. This paper addresses this problem by defining a scheme to map concurrent UML designs to a concurrent object-oriented program. Using the COMET method for the architectural design of concurrent object-oriented systems, each component and connector is annotated with a stereotype indicating its behavioral design pattern. For each of these patterns, a reference implementation is provided using SCOOP, a concurrent object-oriented programming model. We evaluate this development process using a case study of an ATM system, obtaining a fully functional implementation based on the systematic mapping of the individual patterns. Given the strong execution guarantees of the SCOOP model, which is free of data races by construction, this development method eliminates a source of intricate concurrent programming errors.
Online Forum Thread Retrieval using Pseudo Cluster Selection and Voting Techniques
Venue: arXiv cs.IR 2012
Year: 2012

Online forums facilitate knowledge seeking and sharing on the Web. However, the shared knowledge is not fully utilized due to information overload. Thread retrieval is one method to overcome information overload. In this paper, we propose a model that combines two existing approaches: the Pseudo Cluster Selection and the Voting Techniques. In both, a retrieval system first scores a list of messages and then ranks threads by aggregating their scored messages. They differ on what and how to aggregate. The pseudo cluster selection focuses on input, while voting techniques focus on the aggregation method. Our combined models focus on the input and the aggregation methods. The result shows that some combined models are statistically superior to baseline methods.