OpenRaiser/Intern-Atlas huggingface dataset:
Revisiting Timed Specification Theory II : Realisability
Venue: arXiv cs.LO 2013
Year: 2013

In this paper we present an assume-guarantee specification theory (aka interface theory from [14]) for modular synthesis and verification of real-time systems with critical timing constraints. It is a further step of our earlier work [10] which achieved an elegant algebraic specification theory for real-time systems endowed with the capability to freeze time. In this paper we relinquish such (unrealisable) capability and target more realistic systems without the ability to stop time. Our theory, in a combined process-algebraic and reactive-synthesis style, provides the operations of parallel composition for system integration, logical conjunction/disjunction for viewpoint fusion and independent development, and quotient for incremental synthesis. We show that a substitutive refinement preorder, which is a coarsening of the pre-congruence in [10], constitutes the weakest pre-congruence preserving freedom of incompatibility errors. The coarsening requires a shift in the focus of our theory to a more game-theoretical treatment, where the coarsening constitutes a reactive synthesis game named normalisation and is efficiently implementable by a novel local bot-backpropagation algorithm. Previously, timed concurrent games have been studied in [1,14,13], where one of the key concern is the removal of time-blocking strategies by applying blame assignment [13]. Our timed games also have the issue of time-blocking strategies, which may arise through the composition of specifications. However, due to our distinctively different formulation of timed games, we have discovered another elegant solution to the problem without blame assignment. Our solution utilises a second reactive synthesis game called realisation, which is dual to normalisation and implementable by the dual local top-backpropagation algorithm.
MDMP: Managed Data Message Passing
Venue: arXiv cs.DC 2013
Year: 2013

MDMP is a new parallel programming approach that aims to provide users with an easy way to add parallelism to programs, optimise the message passing costs of traditional scientific simulation algorithms, and enable existing MPI-based parallel programs to be optimised and extended without requiring the whole code to be re-written from scratch. MDMP utilises a directives based approach to enable users to specify what communications should take place in the code, and then implements those communications for the user in an optimal manner using both the information provided by the user and data collected from instrumenting the code and gathering information on the data to be communicated. This work will present the basic concepts and functionality of MDMP and discuss the performance that can be achieved using our prototype implementation of MDMP on some model scientific simulation applications.
Machine Translation Systems in India
Venue: arXiv cs.CL 2013
Year: 2013

Machine Translation is the translation of one natural language into another using automated and computerized means. For a multilingual country like India, with the huge amount of information exchanged between various regions and in different languages in digitized format, it has become necessary to find an automated process from one language to another. In this paper, we take a look at the various Machine Translation System in India which is specifically built for the purpose of translation between the Indian languages. We discuss the various approaches taken for building the machine translation system and then discuss some of the Machine Translation Systems in India along with their features.
An Interpreter for Quantum Circuits
Venue: arXiv cs.LO 2013
Year: 2013

This paper describes an ACL2 interpreter for "netlists" describing quantum circuits. Several quantum gates are implemented, including the Hadamard gate H, which rotates vectors by 45 degrees, necessitating the use of irrational numbers, at least at the logical level. Quantum measurement presents an especially difficult challenge, because it requires precise comparisons of irrational numbers and the use of random numbers. This paper does not address computation with irrational numbers or the generation of random numbers, although future work includes the development of pseudo-random generators for ACL2.
Normal type-2 Fuzzy Rational B-Spline Curve
Venue: arXiv cs.GR 2013
Year: 2013

In this paper, we proposed a new form of type-2 fuzzy data points(T2FDPs) that is normal type-2 data points(NT2FDPs). These brand-new forms of data were defined by using the definition of normal type-2 triangular fuzzy number(NT2TFN). Then, we applied fuzzification(alpha-cut) and type-reduction processes towards NT2FDPs after they had been redefined based on the situation of NT2FDPs. Furthermore, we redefine the defuzzification definition along with the new definitions of fuzzification process and type-reduction method to obtain crisp type-2 fuzzy solution data points. For all these processes from the defining the NT2FDPs to defuzzification of NT2FDPs, we demonstrate through curve representation by using the rational B-spline curve function as the example form modeling these NT2FDPs.
Priority Based Pre-emptive Task Scheduling for Android Operating System
Venue: arXiv cs.OH 2013
Year: 2013

Android mobile operating system which is based on Linux Kernel 2.6, has open source license and adaptability to user driven applications. As all other operating systems it has all the basic features like process scheduling, memory management, process management etc associated with it. Any mobile platform works smoothly when the process scheduling is performed in a proper way. Ideal platform is that in which no resource conflict occurs. Thus scheduling in every manner is essential for the operating system to adapt itself with the requirement of a particular application. In this paper, priority based pre-emptive task scheduling is proposed for the SMS application. The idea is to define High priority to required contacts, for ex. Contact numbers of parents or teachers will be given High priority. If in case, any SMS from these High priority contacts is received, the application would flash the SMS on the active screen and redirect this High priority SMS to the Priority Inbox.
Adaptive Mode Selection and Power Allocation in Bidirectional Buffer-aided Relay Networks
Venue: arXiv cs.IT 2013
Year: 2013

In this paper, we consider the problem of sum rate maximization in a bidirectional relay network with fading. Hereby, user 1 and user 2 communicate with each other only through a relay, i.e., a direct link between user 1 and user 2 is not present. In this network, there exist six possible transmission modes: four point-to-point modes (user 1-to-relay, user 2-to-relay, relay-to-user 1, relay-to-user 2), a multiple access mode (both users to the relay), and a broadcast mode (the relay to both users). Most existing protocols assume a fixed schedule of using a subset of the aforementioned transmission modes, as a result, the sum rate is limited by the capacity of the weakest link associated with the relay in each time slot. Motivated by this limitation, we develop a protocol which is not restricted to adhere to a predefined schedule for using the transmission modes. Therefore, all transmission modes of the bidirectional relay network can be used adaptively based on the instantaneous channel state information (CSI) of the involved links. To this end, the relay has to be equipped with two buffers for the storage of the information received from users 1 and 2, respectively. For the considered network, given a total average power budget for all nodes, we jointly optimize the transmission mode selection and power allocation based on the instantaneous CSI in each time slot for sum rate maximization. Simulation results show that the proposed protocol outperforms existing protocols for all signal-to-noise ratios (SNRs). Specifically, we obtain a considerable gain at low SNRs due to the adaptive power allocation and at high SNRs due to the adaptive mode selection.
A Novel Cluster Validation Approach on Pso-Pac Mechanism in Ad Hoc Network
Venue: arXiv cs.NI 2013
Year: 2013

The ad hoc network places a vital role in contemporary days communication scenario. This network performance gets up while the clustering phenomenon has been incorporated. The cluster formation using the vital parameters is incredible on deciding the efficiency level of the clustered ad hoc networks. The PSO-PAC mechanism forms clusters based on swarm intelligence by considering energy as crucial parameter. This optimized cluster helps to suits the applications where the energy parameter plays a key role. The clusters formed by this mechanism may not ascertain the compactness of the clusters. Thus, this paper proposes D-PAC as an index based validation mechanism to be handled on clusters formed using PSO-PAC. The cluster formation and validation mechanism have been implemented using OMNET++ simulator.
Exploration of Speech enabled System for English
Venue: arXiv cs.HC 2013
Year: 2013

This paper presents exploration of speech enable operating systems, software, and applications. It begins with a description of how such systems work, and the level of accuracy that can be expected. It explains the applications of speech recognition technology in different areas education, medical, mobile computing, railway reservation, dictation, and web browsing. A brief comparison of the operating systems supported for voice, speech recognition software or tool. It gives the brief introduction about the potential of voice/speech recognition software. It explains the feature of different speech enable Operating system and speech recognition software. Windows speech recognition have many innovative features for Windows operating system and efficiently assist the computer to control, dictate, navigate, selecting the words, sending emails and correcting the words or sentences. It also explains the benefits and issue related to speech technology. In last era speech recognition technology grew tremendously. There are large number of companies who are working in these area and developing software for the people who are not able to control the system through keyboard or mouse such as physically impaired and senior citizens. This paper gives a brief introduction of speech enabled OS and speech recognition software.
Revealing social networks of spammers through spectral clustering
Venue: arXiv cs.SI 2013
Year: 2013

To date, most studies on spam have focused only on the spamming phase of the spam cycle and have ignored the harvesting phase, which consists of the mass acquisition of email addresses. It has been observed that spammers conceal their identity to a lesser degree in the harvesting phase, so it may be possible to gain new insights into spammers' behavior by studying the behavior of harvesters, which are individuals or bots that collect email addresses. In this paper, we reveal social networks of spammers by identifying communities of harvesters with high behavioral similarity using spectral clustering. The data analyzed was collected through Project Honey Pot, a distributed system for monitoring harvesting and spamming. Our main findings are (1) that most spammers either send only phishing emails or no phishing emails at all, (2) that most communities of spammers also send only phishing emails or no phishing emails at all, and (3) that several groups of spammers within communities exhibit coherent temporal behavior and have similar IP addresses. Our findings reveal some previously unknown behavior of spammers and suggest that there is indeed social structure between spammers to be discovered.
Lightweight LCP Construction for Next-Generation Sequencing Datasets
Venue: arXiv cs.DS 2013
Year: 2013

The advent of "next-generation" DNA sequencing (NGS) technologies has meant that collections of hundreds of millions of DNA sequences are now commonplace in bioinformatics. Knowing the longest common prefix array (LCP) of such a collection would facilitate the rapid computation of maximal exact matches, shortest unique substrings and shortest absent words. CPU-efficient algorithms for computing the LCP of a string have been described in the literature, but require the presence in RAM of large data structures. This prevents such methods from being feasible for NGS datasets. In this paper we propose the first lightweight method that simultaneously computes, via sequential scans, the LCP and BWT of very large collections of sequences. Computational results on collections as large as 800 million 100-mers demonstrate that our algorithm scales to the vast sequence collections encountered in human whole genome sequencing experiments.
A Comparative Study of Web Services Composition Networks
Venue: arXiv cs.SE 2013
Year: 2013

Web services growth makes the composition process a hard task to solve. This numerous interacting elements can be adequately represented by a network. Discovery and composition can benefit from the knowledge of the network structure. In this paper, we investigate the topological properties of two models of syntactic and semantic Web services composition networks: dependency and interaction. Results show that they share a similar organization characterized by the small-world property, a heavy-tailed degree distribution and a low transitivity value. Furthermore, the networks are disassortative.
The operad of wiring diagrams: formalizing a graphical language for databases, recursion, and plug-and-play circuits
Venue: arXiv cs.DB 2013
Year: 2013

Wiring diagrams, as seen in digital circuits, can be nested hierarchically and thus have an aspect of self-similarity. We show that wiring diagrams form the morphisms of an operad $\mcT$, capturing this self-similarity. We discuss the algebra $\Rel$ of mathematical relations on $\mcT$, and in so doing use wiring diagrams as a graphical language with which to structure queries on relational databases. We give the example of circuit diagrams as a special case. We move on to show how plug-and-play devices and also recursion can be formulated in the operadic framework as well. Throughout we include many examples and figures.
Relevance distributions across Bradford Zones: Can Bradfordizing improve search?
Venue: arXiv cs.IR 2013
Year: 2013

The purpose of this paper is to describe the evaluation of the effectiveness of the bibliometric technique Bradfordizing in an information retrieval (IR) scenario. Bradfordizing is used to re-rank topical document sets from conventional abstracting & indexing (A&I) databases into core and more peripheral document zones. Bradfordized lists of journal articles and monographs will be tested in a controlled scenario consisting of different A&I databases from social and political sciences, economics, psychology and medical science, 164 standardized IR topics and intellectual assessments of the listed documents. Does Bradfordizing improve the ratio of relevant documents in the first third (core) compared to the second and last third (zone 2 and zone 3, respectively)? The IR tests show that relevance distributions after re-ranking improve at a significant level if documents in the core are compared with documents in the succeeding zones. After Bradfordizing of document pools, the core has a significant better average precision than zone 2, zone 3 and baseline. This paper should be seen as an argument in favour of alternative non-textual (bibliometric) re-ranking methods which can be simply applied in text-based retrieval systems and in particular in A&I databases.
Feasibility Analysis of Low Cost Graphical Processing Units for Electromagnetic Field Simulations by Finite Difference Time Domain Method
Venue: arXiv cs.DC 2013
Year: 2013

Among several techniques available for solving Computational Electromagnetics (CEM) problems, the Finite Difference Time Domain (FDTD) method is one of the best suited approaches when a parallelized hardware platform is used. In this paper we investigate the feasibility of implementing the FDTD method using the NVIDIA GT 520, a low cost Graphical Processing Unit (GPU), for solving the differential form of Maxwell's equation in time domain. Initially a generalized benchmarking problem of bandwidth test and another benchmarking problem of 'matrix left division is discussed for understanding the correlation between the problem size and the performance on the CPU and the GPU respectively. This is further followed by the discussion of the FDTD method, again implemented on both, the CPU and the GT520 GPU. For both of the above comparisons, the CPU used is Intel E5300, a low cost dual core CPU.
On the Ratio of Revenue to Welfare in Single-Parameter Mechanism Design
Venue: arXiv cs.GT 2013
Year: 2013

What fraction of the potential social surplus in an environment can be extracted by a revenue-maximizing monopolist? We investigate this problem in Bayesian single-parameter environments with independent private values. The precise answer to the question obviously depends on the particulars of the environment: the feasibility constraint and the distributions from which the bidders' private values are sampled. Rather than solving the problem in particular special cases, our work aims to provide universal lower bounds on the revenue-to-welfare ratio that hold under the most general hypotheses that allow for non-trivial such bounds. Our results can be summarized as follows. For general feasibility constraints, the revenue-to-welfare ratio is at least a constant times the inverse-square-root of the number of agents, and this is tight up to constant factors. For downward-closed feasibility constraints, the revenue-to-welfare ratio is bounded below by a constant. Both results require the bidders' distributions to satisfy hypotheses somewhat stronger than regularity; we show that the latter result cannot avoid this requirement.
On Achievable Rates for Channels with Mismatched Decoding
Venue: arXiv cs.IT 2013
Year: 2013

The problem of mismatched decoding for discrete memoryless channels is addressed. A mismatched cognitive multiple-access channel is introduced, and an inner bound on its capacity region is derived using two alternative encoding methods: superposition coding and random binning. The inner bounds are derived by analyzing the average error probability of the code ensemble for both methods and by a tight characterization of the resulting error exponents. Random coding converse theorems are also derived. A comparison of the achievable regions shows that in the matched case, random binning performs as well as superposition coding, i.e., the region achievable by random binning is equal to the capacity region. The achievability results are further specialized to obtain a lower bound on the mismatch capacity of the single-user channel by investigating a cognitive multiple access channel whose achievable sum-rate serves as a lower bound on the single-user channel's capacity. In certain cases, for given auxiliary random variables this bound strictly improves on the achievable rate derived by Lapidoth.
CONATION: English Command Input/Output System for Computers
Venue: arXiv cs.HC 2013
Year: 2013

In this information technology age, a convenient and user friendly interface is required to operate the computer system on very fast rate. In the human being, speech being a natural mode of communication has potential to being a fast and convenient mode of interaction with computer. Speech recognition will play an important role in taking technology to them. It is the need of this era to access the information within seconds. This paper describes the design and development of speaker independent and English command interpreted system for computers. HMM model is used to represent the phoneme like speech commands. Experiments have been done on real world data and system has been trained in normal condition for real world subject.
On Flexible Web Services Composition Networks
Venue: arXiv cs.SE 2013
Year: 2013

The semantic Web service community develops efforts to bring semantics to Web service descriptions and allow automatic discovery and composition. However, there is no widespread adoption of such descriptions yet, because semantically defining Web services is highly complicated and costly. As a result, production Web services still rely on syntactic descriptions, key-word based discovery and predefined compositions. Hence, more advanced research on syntactic Web services is still ongoing. In this work we build syntactic composition Web services networks with three well known similarity metrics, namely Levenshtein, Jaro and Jaro-Winkler. We perform a comparative study on the metrics performance by studying the topological properties of networks built from a test collection of real-world descriptions. It appears Jaro-Winkler finds more appropriate similarities and can be used at higher thresholds. For lower thresholds, the Jaro metric would be preferable because it detect less irrelevant relationships.
Monitoring Student Activity in Collaborative Software Development
Venue: arXiv cs.CY 2013
Year: 2013

This paper presents data analysis from a course on Software Engineering in an effort to identify metrics and techniques that would allow instructor to act proactively and identify patterns of low engagement and inefficient peer collaboration. Over the last two terms, 106 students in their second year of studies formed 20 groups and worked collaboratively to develop video games. Throughout the lab, students have to use a variety of tools for managing and developing their projects, such as software version control, static analysis tools, wikis, mailing lists, etc. The students are also supported by weekly meetings with teaching assistants and instructors regarding group progress, code quality, and management issues. Through these meetings and their interactions with the software tools, students leave a detailed trace of data related to their individual engagement and their collaboration behavior in their groups. The paper provides discussion on the different source of data that can be monitored, and present preliminary results on how these data can be used to analyze students' activity.
An Optimal Mastermind (4,7) Strategy and More Results in the Expected Case
Venue: arXiv cs.GT 2013
Year: 2013

This paper presents an optimal strategy for solving the 4 peg-7 color Mastermind MM(4,7) in the expected case (4.676) along with optimal strategies or upper bounds for other values. The program developed is using a depth-first branch and bound algorithm relying on tight upper bound, dynamic lower bound evaluation and guess equivalence to prune symmetric tree branches.
Optimal Fully Electric Vehicle load balancing with an ADMM algorithm in Smartgrids
Venue: arXiv cs.SY 2013
Year: 2013

In this paper we present a system architecture and a suitable control methodology for the load balancing of Fully Electric Vehicles at Charging Station (CS). Within the proposed architecture, control methodologies allow to adapt Distributed Energy Resources (DER) generation profiles and active loads to ensure economic benefits to each actor. The key aspect is the organization in two levels of control: at local level a Load Area Controller (LAC) optimally calculates the FEVs charging sessions, while at higher level a Macro Load Area Aggregator (MLAA) provides DER with energy production profiles, and LACs with energy withdrawal profiles. Proposed control methodologies involve the solution of a Walrasian market equilibrium and the design of a distributed algorithm.
Towards User Profile Modelling in Recommender System
Venue: arXiv cs.IR 2013
Year: 2013

The notion of profile appeared in the 1970s decade, which was mainly due to the need to create custom applications that could be adapted to the user. In this paper, we treat the different aspects of the user's profile, defining it, profile, its features and its indicators of interest, and then we describe the different approaches of modelling and acquiring the user's interests.