OpenRaiser/Intern-Atlas huggingface dataset:
A Monadic Formalization of ML5
Venue: arXiv cs.PL 2010
Year: 2010

ML5 is a programming language for spatially distributed computing, based on a Curry-Howard correspondence with the modal logic S5. Despite being designed by a correspondence with S5 modal logic, the ML5 programming language differs from the logic in several ways. In this paper, we explain these discrepancies between ML5 and S5 by translating ML5 into a slightly different logic: intuitionistic S5 extended with a lax modality that encapsulates effectful computations in a monad. This translation both explains the existing ML5 design and suggests some simplifications and generalizations. We have formalized our translation within the Agda proof assistant. Rather than formalizing lax S5 as a proof theory, we \emph{embed} it as a universe within the the dependently typed host language, with the universe elimination given by implementing the modal logic's Kripke semantics. This representation technique saves us the work of defining a proof theory for the logic and proving it correct, and additionally allows us to inherit the equational theory of the meta-language, which can be exploited in proving that the semantics validates the operational semantics of ML5.
Quantum function computation using sublogarithmic space (abstract & poster)
Venue: arXiv cs.CC 2010
Year: 2010

We prove that quantum Turing machines are strictly superior to probabilistic Turing machines in function computation for any space bound $ o(\log(n)) $.
Direct vs. Two-Step Approach for Unique Word Generation in UW-OFDM
Venue: arXiv cs.IT 2010
Year: 2010

Unique word OFDM is a novel technique for constructing OFDM symbols, that has many advantages over cyclic prefix OFDM. In this paper we investigate two different approaches for the generation of an OFDM symbol containing a unique word in its time domain representation. The two-step and the direct approach seem very similar at first sight, but actually produce completely different OFDM symbols. Also the overall system's bit error ratio differs significantly for the two approaches. We will prove these propositions analytically, and we will give simulation results for further illustration.
Linear Transceiver Design for Interference Alignment: Complexity and Computation
Venue: arXiv cs.IT 2010
Year: 2010

Consider a MIMO interference channel whereby each transmitter and receiver are equipped with multiple antennas. The basic problem is to design optimal linear transceivers (or beamformers) that can maximize system throughput. The recent work [1] suggests that optimal beamformers should maximize the total degrees of freedom and achieve interference alignment in high SNR. In this paper we first consider the interference alignment problem in spatial domain and prove that the problem of maximizing the total degrees of freedom for a given MIMO interference channel is NP-hard. Furthermore, we show that even checking the achievability of a given tuple of degrees of freedom for all receivers is NP-hard when each receiver is equipped with at least three antennas. Interestingly, the same problem becomes polynomial time solvable when each transmit/receive node is equipped with no more than two antennas. Finally, we propose a distributed algorithm for transmit covariance matrix design, while assuming each receiver uses a linear MMSE beamformer. The simulation results show that the proposed algorithm outperforms the existing interference alignment algorithms in terms of system throughput.
Open, Closed, and Shared Access Femtocells in the Downlink
Venue: arXiv cs.NI 2010
Year: 2010

A fundamental choice in femtocell deployments is the set of users which are allowed to access each femtocell. Closed access restricts the set to specifically registered users, while open access allows any mobile subscriber to use any femtocell. Which one is preferable depends strongly on the distance between the macrocell base station (MBS) and femtocell. The main results of the paper are lemmas which provide expressions for the SINR distribution for various zones within a cell as a function of this MBS-femto distance. The average sum throughput (or any other SINR-based metric) of home users and cellular users under open and closed access can be readily determined from these expressions. We show that unlike in the uplink, the interests of home and cellular users are in conflict, with home users preferring closed access and cellular users preferring open access. The conflict is most pronounced for femtocells near the cell edge, when there are many cellular users and fewer femtocells. To mitigate this conflict, we propose a middle way which we term shared access in which femtocells allocate an adjustable number of time-slots between home and cellular users such that a specified minimum rate for each can be achieved. The optimal such sharing fraction is derived. Analysis shows that shared access achieves at least the overall throughput of open access while also satisfying rate requirements, while closed access fails for cellular users and open access fails for the home user.
PC 2 Phone Event Announcer
Venue: arXiv cs.NI 2010
Year: 2010

Nowadays, mobile phones are indispensable devices; it has become a trend now that college and university students are owners of such devices and this particular factor plays a very important role behind the coming up with the proposed system. "PC 2 Phone event Announcer", is the name of the new proposed system suggested to solve the existing communication problem between the College staff and students. As the name suggests, it can be deduced that the system will involve computers and phones, more specifically mobile phones.
Efficient Indexing of the BitTorrent Distributed Hash Table
Venue: arXiv cs.NI 2010
Year: 2010

The following paper presents various methods and implementation techniques used to harvest metadata efficiently from a Kademlia Distributed Hashtable (DHT) as used in the BitTorrent P2P network to build an index of publicly available files in the BitTorrent ecosystem. The indexer design makes various tradeoffs between throughput and fairness towards other DHT nodes while also being scaleable in a distributed environment.
Totally Corrective Multiclass Boosting with Binary Weak Learners
Venue: arXiv cs.LG 2010
Year: 2010

In this work, we propose a new optimization framework for multiclass boosting learning. In the literature, AdaBoost.MO and AdaBoost.ECC are the two successful multiclass boosting algorithms, which can use binary weak learners. We explicitly derive these two algorithms' Lagrange dual problems based on their regularized loss functions. We show that the Lagrange dual formulations enable us to design totally-corrective multiclass algorithms by using the primal-dual optimization technique. Experiments on benchmark data sets suggest that our multiclass boosting can achieve a comparable generalization capability with state-of-the-art, but the convergence speed is much faster than stage-wise gradient descent boosting. In other words, the new totally corrective algorithms can maximize the margin more aggressively.
Contracting the Facebook API
Venue: arXiv cs.SE 2010
Year: 2010

In recent years, there has been an explosive growth in the popularity of online social networks such as Facebook. In a new twist, third party developers are now able to create their own web applications which plug into Facebook and work with Facebook's "social" data, enabling the entire Facebook user base of more than 400 million active users to use such applications. These client applications can contain subtle errors that can be hard to debug if they misuse the Facebook API. In this paper we present an experience report on applying Microsoft's new code contract system for the .NET framework to the Facebook API.We wrote contracts for several classes in the Facebook API wrapper which allows Microsoft .NET developers to implement Facebook applications. We evaluated the usefulness of these contracts during implementation of a new Facebook application. Our experience indicates that having code contracts provides a better and quicker software development experience.
Improved Iterative Techniques to Compensate for Interpolation Distortions
Venue: arXiv cs.MM 2010
Year: 2010

In this paper a novel hybrid approach for compensating the distortion of any interpolation has been proposed. In this hybrid method, a modular approach was incorporated in an iterative fashion. By using this approach we can get drastic improvement with less computational complexity. The extension of the proposed approach to two dimensions was also studied. Both the simulation results and mathematical analyses confirmed the superiority of the hybrid method. The proposed method was also shown to be robust against additive noise.
Portability of Prolog programs: theory and case-studies
Venue: arXiv cs.PL 2010
Year: 2010

(Non-)portability of Prolog programs is widely considered as an important factor in the lack of acceptance of the language. Since 1995, the core of the language is covered by the ISO standard 13211-1. Since 2007, YAP and SWI-Prolog have established a basic compatibility framework. This article describes and evaluates this framework. The aim of the framework is running the same code on both systems rather than migrating an application. We show that today, the portability within the family of Edinburgh/Quintus derived Prolog implementations is good enough to allow for maintaining portable real-world applications.
A General Analog Network Coding for Wireless Systems with Fading and Noisy Channels
Venue: arXiv cs.NI 2010
Year: 2010

It has been recently brought into spotlight that through the exploitation of network coding concepts at physical-layer, the interference property of the wireless media can be proven to be a blessing in disguise. Nonetheless, most of the previous studies on this subject have either held unrealistic assumptions about the network properties, thus making them basically theoretical, or have otherwise been limited to fairly simple network topologies. We, on the other hand, believe to have devised a novel scheme, called Real Amplitude Scaling (RAS), that relaxes the aforementioned restrictions, and works with a wider range of network topologies and in circumstances that are closer to practice, for instance in lack of symbol-level synchronization and in the presence of noise, channel distortion and severe interference from other sources. The simulation results confirmed the superior performance of the proposed method in low SNRs, as well as the high SNR limits, where the effect of quantization error in the digital techniques becomes comparable to the channel.
Casting of the WAM as an EAM
Venue: arXiv cs.PL 2010
Year: 2010

Logic programming provides a very high-level view of programming, which comes at the cost of some execution efficiency. Improving performance of logic programs is thus one of the holy grails of Prolog system implementations and a wide range of approaches have historically been taken towards this goal. Designing computational models that both exploit the available parallelism in a given application and that try hard to reduce the explored search space has been an ongoing line of research for many years. These goals in particular have motivated the design of several computational models, one of which is the Extended Andorra Model (EAM). In this paper, we present a preliminary specification and implementation of the EAM with Implicit Control, the WAM2EAM, which supplies regular WAM instructions with an EAM-centered interpretation.
A memory-efficient data structure representing exact-match overlap graphs with application for next generation DNA assembly
Venue: arXiv cs.DS 2010
Year: 2010

An exact-match overlap graph of $n$ given strings of length $\ell$ is an edge-weighted graph in which each vertex is associated with a string and there is an edge $(x,y)$ of weight $ω= \ell - |ov_{max}(x,y)|$ if and only if $ω\leq λ$, where $|ov_{max}(x,y)|$ is the length of $ov_{max}(x,y)$ and $λ$ is a given threshold. In this paper, we show that the exact-match overlap graphs can be represented by a compact data structure that can be stored using at most $(2λ-1 )(2\lceil\log n\rceil + \lceil\logλ\rceil)n$ bits with a guarantee that the basic operation of accessing an edge takes $O(\log λ)$ time. Exact-match overlap graphs have been broadly used in the context of DNA assembly and the \emph{shortest super string problem} where the number of strings $n$ ranges from a couple of thousands to a couple of billions, the length $\ell$ of the strings is from 25 to 1000, depending on DNA sequencing technologies. However, many DNA assemblers using overlap graphs are facing a major problem of constructing and storing them. Especially, it is impossible for these DNA assemblers to handle the huge amount of data produced by the next generation sequencing technologies where the number of strings $n$ is usually very large ranging from hundred million to a couple of billions. In fact, to our best knowledge there is no DNA assemblers that can handle such a large number of strings. Fortunately, with our compact data structure, the major problem of constructing and storing overlap graphs is practically solved since it only requires linear time and and linear memory. As a result, it opens the door of possibilities to build a DNA assembler that can handle large-scale datasets efficiently.
Van Wijngaarden grammars, metamorphism and K-ary malwares
Venue: arXiv cs.CR 2010
Year: 2010

Grammars are used to describe sentences structure, thanks to some sets of rules, which depends on the grammar type. A classification of grammars has been made by Noam Chomsky, which led to four well-known types. Yet, there are other types of grammars, which do not exactly fit in Chomsky's classification, such as the two-level grammars. As their name suggests it, the main idea behind these grammars is that they are composed of two grammars. Van Wijngaarden grammars, particularly, are such grammars. They are interesting by their power (expressiveness), which can be the same, under some hypotheses, as the most powerful grammars of Chomsky's classification, i.e. Type 0 grammars. Another point of interest is their relative conciseness and readability. Van Wijngaarden grammars can describe static and dynamic semantic of a language. So, by using them as a generative engine, it is possible to generate a possibly infinite set of words, while assuring us that they all have the same semantic. Moreover, they can describe K-ary codes, by describing the semantic of each components of a code.
Modeling and Analyzing Adaptive User-Centric Systems in Real-Time Maude
Venue: arXiv cs.SE 2010
Year: 2010

Pervasive user-centric applications are systems which are meant to sense the presence, mood, and intentions of users in order to optimize user comfort and performance. Building such applications requires not only state-of-the art techniques from artificial intelligence but also sound software engineering methods for facilitating modular design, runtime adaptation and verification of critical system requirements. In this paper we focus on high-level design and analysis, and use the algebraic rewriting language Real-Time Maude for specifying applications in a real-time setting. We propose a generic component-based approach for modeling pervasive user-centric systems and we show how to analyze and prove crucial properties of the system architecture through model checking and simulation. For proving time-dependent properties we use Metric Temporal Logic (MTL) and present analysis algorithms for model checking two subclasses of MTL formulas: time-bounded response and time-bounded safety MTL formulas. The underlying idea is to extend the Real-Time Maude model with suitable clocks, to transform the MTL formulas into LTL formulas over the extended specification, and then to use the LTL model checker of Maude. It is shown that these analyses are sound and complete for maximal time sampling. The approach is illustrated by a simple adaptive advertising scenario in which an adaptive advertisement display can react to actions of the users in front of the display.
A Rewriting-Logic-Based Technique for Modeling Thermal Systems
Venue: arXiv cs.LO 2010
Year: 2010

This paper presents a rewriting-logic-based modeling and analysis technique for physical systems, with focus on thermal systems. The contributions of this paper can be summarized as follows: (i) providing a framework for modeling and executing physical systems, where both the physical components and their physical interactions are treated as first-class citizens; (ii) showing how heat transfer problems in thermal systems can be modeled in Real-Time Maude; (iii) giving the implementation in Real-Time Maude of a basic numerical technique for executing continuous behaviors in object-oriented hybrid systems; and (iv) illustrating these techniques with a set of incremental case studies using realistic physical parameters, with examples of simulation and model checking analyses.
Distributed Interference Cancellation in Multiple Access Channel with Transmitter Cooperation
Venue: arXiv cs.IT 2010
Year: 2010

We consider a two-user Gaussian multiple access channel with two independent additive white Gaussian interferences. Each interference is known to exactly one transmitter non-causally. Transmitters are allowed to cooperate through finite-capacity links. The capacity region is characterized to within 3 and 1.5 bits for the stronger user and the weaker user respectively, regardless of channel parameters. As a by-product, we characterize the capacity region of the case without cooperation to within 1 and 0.5 bits for the stronger user and the weaker user respectively. These results are based on a layered modulo-lattice transmission architecture which realizes distributed interference cancellation.
Performance Analysis of Estimation of Distribution Algorithm and Genetic Algorithm in Zone Routing Protocol
Venue: arXiv cs.NE 2010
Year: 2010

In this paper, Estimation of Distribution Algorithm (EDA) is used for Zone Routing Protocol (ZRP) in Mobile Ad-hoc Network (MANET) instead of Genetic Algorithm (GA). It is an evolutionary approach, and used when the network size grows and the search space increases. When the destination is outside the zone, EDA is applied to find the route with minimum cost and time. The implementation of proposed method is compared with Genetic ZRP, i.e., GZRP and the result demonstrates better performance for the proposed method. Since the method provides a set of paths to the destination, it results in load balance to the network. As both EDA and GA use random search method to reach the optimal point, the searching cost reduced significantly, especially when the number of data is large.
A PTAS for Scheduling with Tree Assignment Restrictions
Venue: arXiv cs.DS 2010
Year: 2010

Scheduling with assignment restrictions is an important special case of scheduling unrelated machines which has attracted much attention in the recent past. While a lower bound on approximability of 3/2 is known for its most general setting, subclasses of the problem admit polynomial-time approximation schemes. This note provides a PTAS for tree-like hierarchical structures, improving on a recent 4/3-approximation by Huo and Leung.
A Cluster Based Replication Architecture for Load Balancing in Peer-to-Peer Content Distribution
Venue: arXiv cs.NI 2010
Year: 2010

In P2P systems, large volumes of data are declustered naturally across a large number of peers. But it is very difficult to control the initial data distribution because every user has the freedom to share any data with other users. The system scalability can be improved by distributing the load across multiple servers which is proposed by replication. The large scale content distribution systems were improved broadly using the replication techniques. The demanded contents can be brought closer to the clients by multiplying the source of information geographically, which in turn reduce both the access latency and the network traffic. In addition to this, due to the intrinsic dynamism of the P2P environment, static data distribution cannot be expected to guarantee good load balancing. If the hot peers become bottleneck, it leads to increased user response time and significant performance degradation of the system. Hence an effective load balancing mechanism is necessary in such cases and it can be attained efficiently by intelligent data replication. In this paper, we propose a cluster based replication architecture for load-balancing in peer-to-peer content distribution systems. In addition to an intelligent replica placement technique, it also consists of an effective load balancing technique. In the intelligent replica placement technique, peers are grouped into strong and weak clusters based on their weight vector which comprises available capacity, CPU speed, access latency and memory size. In order to achieve complete load balancing across the system, an intracluster and inter-cluster load balancing algorithms are proposed. We are able to show that our proposed architecture attains less latency and better throughput with reduced bandwidth usage, through the simulation results.
An Algorithm to Extract Rules from Artificial Neural Networks for Medical Diagnosis Problems
Venue: arXiv cs.NE 2010
Year: 2010

Artificial neural networks (ANNs) have been successfully applied to solve a variety of classification and function approximation problems. Although ANNs can generally predict better than decision trees for pattern classification problems, ANNs are often regarded as black boxes since their predictions cannot be explained clearly like those of decision trees. This paper presents a new algorithm, called rule extraction from ANNs (REANN), to extract rules from trained ANNs for medical diagnosis problems. A standard three-layer feedforward ANN with four-phase training is the basis of the proposed algorithm. In the first phase, the number of hidden nodes in ANNs is determined automatically by a constructive algorithm. In the second phase, irrelevant connections and input nodes are removed from trained ANNs without sacrificing the predictive accuracy of ANNs. The continuous activation values of the hidden nodes are discretized by using an efficient heuristic clustering algorithm in the third phase. Finally, rules are extracted from compact ANNs by examining the discretized activation values of the hidden nodes. Extensive experimental studies on three benchmark classification problems, i.e. breast cancer, diabetes and lenses, demonstrate that REANN can generate high quality rules from ANNs, which are comparable with other methods in terms of number of rules, average number of conditions for a rule, and predictive accuracy.
Novel Codes Family for Modified Spectral-Amplitude-Coding OCDMA Systems and Performance Analysis
Venue: arXiv cs.IT 2010
Year: 2010

In this paper a novel family of codes for modified spectral-amplitude-coding optical code division multiple access (SAC-OCDMA) is introduced. The proposed codes exist for more number of processing gains comparing to the previously reported codes. In the network using these codes, the number of users can be extended without any essential changes in the previous transmitters. In this study, we propose a construction method for these codes and compare their performance with previously reported codes.