OpenRaiser/Intern-Atlas huggingface dataset:
Exploiting Similarities among Languages for Machine Translation
Venue: arXiv cs.CL 2013
Year: 2013

Dictionaries and phrase tables are the basis of modern statistical machine translation systems. This paper develops a method that can automate the process of generating and extending dictionaries and phrase tables. Our method can translate missing word and phrase entries by learning language structures based on large monolingual data and mapping between languages from small bilingual data. It uses distributed representation of words and learns a linear mapping between vector spaces of languages. Despite its simplicity, our method is surprisingly effective: we can achieve almost 90% precision@5 for translation of words between English and Spanish. This method makes little assumption about the languages, so it can be used to extend and refine dictionaries and translation tables for any language pairs.
The Set Partitions: Solution for the sharing secret keys
Venue: arXiv cs.CR 2013
Year: 2013

Confidentiality was and will always remain a critical need in the exchanges either between persons or the official parties. Recently, cryptology has made a jump, from classical form to the quantum one, we talk about quantum cryptography. This theory, although is perfectly safe, there are still binding limits of implementation. In this paper, we developed a new cryptographic protocol, called BCB12 protocol, which will be used to provide random keys shared via a classical channel, using the set partitions. Each key can be long enough that the plain text in question, in purpose, for instance, to hide then to transmit the secret information using the Vernam cipher.
Modeling and Evaluating Performance of Routing Operations in Proactive Routing Protocols
Venue: arXiv cs.NI 2013
Year: 2013

To ensure seamless communication in wireless multi-hop networks, certain classes of routing protocols are defined. This vary paper, is based upon proactive routing protocols for Wireless multihop networks. Initially, we discuss Destination Sequence Distance Vector (DSDV), Fish-eye State Routing (FSR) and Optimized Link State Routing (OLSR), precisely followed by mathematical frame work of control overhead regarding proactive natured routing protocols. Finally, extensive simulations are done using NS 2 respecting above mentioned routing protocols covering mobility and scalability issues. Said protocols are compared under mobile and dense environments to conclude our performance analysis.
Routing Directions: Keeping it Fast and Simple
Venue: arXiv cs.DS 2013
Year: 2013

The problem of providing meaningful routing directions over road networks is of great importance. In many real-life cases, the fastest route may not be the ideal choice for providing directions in written, spoken text, or for an unfamiliar neighborhood, or in cases of emergency. Rather, it is often more preferable to offer "simple" directions that are easy to memorize, explain, understand or follow. However, there exist cases where the simplest route is considerably longer than the fastest. This paper tries to address this issue, by finding near-simplest routes which are as short as possible and near-fastest routes which are as simple as possible. Particularly, we focus on efficiency, and propose novel algorithms, which are theoretically and experimentally shown to be significantly faster than existing approaches.
A fully automatic problem solver with human-style output
Venue: arXiv cs.AI 2013
Year: 2013

This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians. The program is part of a more general project, which we also discuss.
Cable-Driven Robots with Wireless Control Capability for Pedagogical Illustration in Science
Venue: arXiv cs.RO 2013
Year: 2013

Science teaching in secondary schools is often abstract for students. Even if some experiments can be conducted in classrooms, mainly for chemistry or some physics fields, mathematics is not an experimental science. Teachers have to convince students that theorems have practical implications. We present teachers an original and easy-to-use pedagogical tool: a cable-driven robot with a Web-based remote control interface. The robot implements several scientific concepts such as 3D-geometry and kinematics. The remote control enables the teacher to move freely in the classroom.
Log-space counter is useful for unary languages by help of a constant-size quantum register
Venue: arXiv cs.CC 2013
Year: 2013

The minimum amount of resources to recognize a nonregular language is a fundamental research topic in theoretical computer science which has been examined for different kinds of resources and many different models. In this note, we focus on unary languages and space complexity on counters. Our model is two-way one-counter automaton with quantum and classical states (2QCCA), which is a two-way finite automaton with one-counter (2DCA) augmented with a fixed size quantum register or a two-way finite automaton with quantum and classical states (2QCFA) augmented with a classical counter. It is known that any 2DCA using a sublinear space on its counter can recognize only regular languages \cite{DG82B}. In this note, we show that bounded-error 2QCCAs can recognize a non-regular unary language by using logarithmic space on its counters for the members. Note that it is still an open problem whether bounded-error 2QCFA can recognize a non-regular unary language.
A Robust Information Source Estimator with Sparse Observations
Venue: arXiv cs.SI 2013
Year: 2013

In this paper, we consider the problem of locating the information source with sparse observations. We assume that a piece of information spreads in a network following a heterogeneous susceptible-infected-recovered (SIR) model and that a small subset of infected nodes are reported, from which we need to find the source of the information. We adopt the sample path based estimator developed in [1], and prove that on infinite trees, the sample path based estimator is a Jordan infection center with respect to the set of observed infected nodes. In other words, the sample path based estimator minimizes the maximum distance to observed infected nodes. We further prove that the distance between the estimator and the actual source is upper bounded by a constant independent of the number of infected nodes with a high probability on infinite trees. Our simulations on tree networks and real world networks show that the sample path based estimator is closer to the actual source than several other algorithms.
Approximation Theory and the Design of Fast Algorithms
Venue: arXiv cs.DS 2013
Year: 2013

We survey key techniques and results from approximation theory in the context of uniform approximations to real functions such as e^{-x}, 1/x, and x^k. We then present a selection of results demonstrating how such approximations can be used to speed up primitives crucial for the design of fast algorithms for problems such as simulating random walks, graph partitioning, solving linear system of equations, computing eigenvalues and combinatorial approaches to solve semi-definite programs.
Distributed coordination of self-organizing mechanisms in communication networks
Venue: arXiv cs.NI 2013
Year: 2013

The fast development of the Self-Organizing Network (SON) technology in mobile networks renders the problem of coordinating SON functionalities operating simultaneously critical. SON functionalities can be viewed as control loops that may need to be coordinated to guarantee conflict free operation, to enforce stability of the network and to achieve performance gain. This paper proposes a distributed solution for coordinating SON functionalities. It uses Rosen's concave games framework in conjunction with convex optimization. The SON functionalities are modeled as linear Ordinary Differential Equation (ODE)s. The stability of the system is first evaluated using a basic control theory approach. The coordination solution consists in finding a linear map (called coordination matrix) that stabilizes the system of SON functionalities. It is proven that the solution remains valid in a noisy environment using Stochastic Approximation. A practical example involving three different SON functionalities deployed in Base Stations (BSs) of a Long Term Evolution (LTE) network demonstrates the usefulness of the proposed method.
Securing the IEEE 802.16 OFDM WiMAX PHYSICAL AND MAC Layer Using STBC Coding and Encryption
Venue: arXiv cs.CR 2013
Year: 2013

This work proposes model design in securing the IEEE 802.16 WiMAX Physical and MAC layer, using Orthogonal Frequency Division Multiplexing (OFDM) and STBC model. Typically, it addresses the physical and MAC layer security concerns, using a Space Time Block Coding (STBC), link encryption, and Message Authentication Code (MAC) technique. The model conforms to Multiple Input Single Output (MISO) fading channels which model two or more transmitters and a receiver in multiuser environment. The two fading link parameters are assumed to be same. Channel estimate for each link, in combination to the received signal is based on Reed Solomon Convolution Coding (RS-CC) algorithm, which occurs as a result of the Space-Time Diversity Combiner block. In addition the model explore using communication blocks to measure and display bit error rate after encryption algorithm and Message Authentication Code (MAC) have been adapted in Forward Error Correction (FEC) mode. Channel SNR and estimation in rate ID is applied. The final results shows authentication, and the Reed-Solomon decoding of the final information or data received.
3-extra connectivity of 3-ary n-cube networks
Venue: arXiv cs.DM 2013
Year: 2013

Let G be a connected graph and S be a set of vertices. The h-extra connectivity of G is the cardinality of a minimum set S such that G-S is disconnected and each component of G-S has at least h+1 vertices. The h-extra connectivity is an important parameter to measure the reliability and fault tolerance ability of large interconnection networks. The h-extra connectivity for h=1,2 of k-ary n-cube are gotten by Hsieh et al. in [Theoretical Computer Science, 443 (2012) 63-69] for k>=4 and Zhu et al. in [Theory of Computing Systems, arxiv.org/pdf/1105.0991v1 [cs.DM] 5 May 2011] for k=3. In this paper, we show that the h-extra connectivity of the 3-ary n-cube networks for h=3 is equal to 8n-12, where n>=3.
An ant colony optimization algorithm for job shop scheduling problem
Venue: arXiv cs.AI 2013
Year: 2013

The nature has inspired several metaheuristics, outstanding among these is Ant Colony Optimization (ACO), which have proved to be very effective and efficient in problems of high complexity (NP-hard) in combinatorial optimization. This paper describes the implementation of an ACO model algorithm known as Elitist Ant System (EAS), applied to a combinatorial optimization problem called Job Shop Scheduling Problem (JSSP). We propose a method that seeks to reduce delays designating the operation immediately available, but considering the operations that lack little to be available and have a greater amount of pheromone. The performance of the algorithm was evaluated for problems of JSSP reference, comparing the quality of the solutions obtained regarding the best known solution of the most effective methods. The solutions were of good quality and obtained with a remarkable efficiency by having to make a very low number of objective function evaluations.
A Proof System with Names for Modal Mu-calculus
Venue: arXiv cs.LO 2013
Year: 2013

Fixpoints are an important ingredient in semantics, abstract interpretation and program logics. Their addition to a logic can add considerable expressive power. One general issue is how to define proof systems for such logics. Here we examine proof systems for modal logic with fixpoints. We present a tableau proof system for checking validity of formulas which uses names to keep track of unfoldings of fixpoint variables as devised by Jungteerapanich.
Abstract Interpretation as a Programming Language
Venue: arXiv cs.PL 2013
Year: 2013

In David Schmidt's PhD work he explored the use of denotational semantics as a programming language. It was part of an effort to not only treat formal semantics as specifications but also as interpreters and input to compiler generators. The semantics itself can be seen as a program and one may examine different programming styles and ways to represent states. Abstract interpretation is primarily a technique for derivation and specification of program analysis. As with denotational semantics we may also view abstract interpretations as programs and examine the implementation. The main focus in this paper is to show that results from higher-order strictness analysis may be used more generally as fixpoint operators for higher-order functions over lattices and thus provide a technique for immediate implementation of a large class of abstract interpretations. Furthermore, it may be seen as a programming paradigm and be used to write programs in a circular style.
Online partial evaluation of sheet-defined functions
Venue: arXiv cs.PL 2013
Year: 2013

We present a spreadsheet implementation, extended with sheet-defined functions, that allows users to define functions using only standard spreadsheet concepts such as cells, formulas and references, requiring no new syntax. This implements an idea proposed by Peyton-Jones and others. As the main contribution of this paper, we then show how to add an online partial evaluator for such sheet-defined functions. The result is a higher-order functional language that is dynamically typed, in keeping with spreadsheet traditions, and an interactive platform for function definition and function specialization. We describe an implementation of these ideas, present some performance data from microbenchmarks, and outline desirable improvements and extensions.
Abstraction and Learning for Infinite-State Compositional Verification
Venue: arXiv cs.LO 2013
Year: 2013

Despite many advances that enable the application of model checking techniques to the verification of large systems, the state-explosion problem remains the main challenge for scalability. Compositional verification addresses this challenge by decomposing the verification of a large system into the verification of its components. Recent techniques use learning-based approaches to automate compositional verification based on the assume-guarantee style reasoning. However, these techniques are only applicable to finite-state systems. In this work, we propose a new framework that interleaves abstraction and learning to perform automated compositional verification of infinite-state systems. We also discuss the role of learning and abstraction in the related context of interface generation for infinite-state components.
A Simple Semantics and Static Analysis for Stack Inspection
Venue: arXiv cs.PL 2013
Year: 2013

The Java virtual machine and the .NET common language runtime feature an access control mechanism specified operationally in terms of run-time stack inspection. We give a denotational semantics in "eager" form, and show that it is equivalent to the "lazy" semantics using stack inspection. We give a static analysis of safety, i.e., the absence of security errors, that is simpler than previous proposals. We identify several program transformations that can be used to remove run-time checks. We give complete, detailed proofs for safety of the analysis and for the transformations, exploiting compositionality of the eager semantics.
A Survey on Product Operators in Abstract Interpretation
Venue: arXiv cs.LO 2013
Year: 2013

The aim of this paper is to provide a general overview of the product operators introduced in the literature as a tool to enhance the analysis accuracy in the Abstract Interpretation framework. In particular we focus on the Cartesian and reduced products, as well as on the reduced cardinal power, an under-used technique whose features deserve to be stressed for their potential impact in practical applications.
Iterable Forward Reachability Analysis of Monitor-DPNs
Venue: arXiv cs.LO 2013
Year: 2013

There is a close connection between data-flow analysis and model checking as observed and studied in the nineties by Steffen and Schmidt. This indicates that automata-based analysis techniques developed in the realm of infinite-state model checking can be applied as data-flow analyzers that interpret complex control structures, which motivates the development of such analysis techniques for ever more complex models. One approach proposed by Esparza and Knoop is based on computation of predecessor or successor sets for sets of automata configurations. Our goal is to adapt and exploit this approach for analysis of multi-threaded Java programs. Specifically, we consider the model of Monitor-DPNs for concurrent programs. Monitor-DPNs precisely model unbounded recursion, dynamic thread creation, and synchronization via well-nested locks with finite abstractions of procedure- and thread-local state. Previous work on this model showed how to compute regular predecessor sets of regular configurations and tree-regular successor sets of a fixed initial configuration. By combining and extending different previously developed techniques we show how to compute tree-regular successor sets of tree-regular sets. Thereby we obtain an iterable, lock-sensitive forward reachability analysis. We implemented the analysis for Java programs and applied it to information flow control and data race detection.
Closing a Gap in the Complexity of Refinement Modal Logic
Venue: arXiv cs.LO 2013
Year: 2013

Refinement Modal Logic (RML), which was recently introduced by Bozzelli et al., is an extension of classical modal logic which allows one to reason about a changing model. In this paper we study computational complexity questions related to this logic, settling a number of open problems. Specifically, we study the complexity of satisfiability for the existential fragment of RML, a problem posed by Bozzelli, van Ditmarsch and Pinchinat. Our main result is a tight PSPACE upper bound for this problem, which we achieve by introducing a new tableau system. As a direct consequence, we obtain a tight characterization of the complexity of RML satisfiability for any fixed number of alternations of refinement quantifiers. Additionally, through a simple reduction we establish that the model checking problem for RML is PSPACE-complete, even for formulas with a single quantifier.
JRC EuroVoc Indexer JEX - A freely available multi-label categorisation tool
Venue: arXiv cs.CL 2013
Year: 2013

EuroVoc (2012) is a highly multilingual thesaurus consisting of over 6,700 hierarchically organised subject domains used by European Institutions and many authorities in Member States of the European Union (EU) for the classification and retrieval of official documents. JEX is JRC-developed multi-label classification software that learns from manually labelled data to automatically assign EuroVoc descriptors to new documents in a profile-based category-ranking task. The JEX release consists of trained classifiers for 22 official EU languages, of parallel training data in the same languages, of an interface that allows viewing and amending the assignment results, and of a module that allows users to re-train the tool on their own document collections. JEX allows advanced users to change the document representation so as to possibly improve the categorisation result through linguistic pre-processing. JEX can be used as a tool for interactive EuroVoc descriptor assignment to increase speed and consistency of the human categorisation process, or it can be used fully automatically. The output of JEX is a language-independent EuroVoc feature vector lending itself also as input to various other Language Technology tasks, including cross-lingual clustering and classification, cross-lingual plagiarism detection, sentence selection and ranking, and more.
DGT-TM: A freely Available Translation Memory in 22 Languages
Venue: arXiv cs.CL 2013
Year: 2013

The European Commission's (EC) Directorate General for Translation, together with the EC's Joint Research Centre, is making available a large translation memory (TM; i.e. sentences and their professionally produced translations) covering twenty-two official European Union (EU) languages and their 231 language pairs. Such a resource is typically used by translation professionals in combination with TM software to improve speed and consistency of their translations. However, this resource has also many uses for translation studies and for language technology applications, including Statistical Machine Translation (SMT), terminology extraction, Named Entity Recognition (NER), multilingual classification and clustering, and many more. In this reference paper for DGT-TM, we introduce this new resource, provide statistics regarding its size, and explain how it was produced and how to use it.
Adaptive model predictive control with exploring property for constrained linear systems that uses basis function model parametrization
Venue: arXiv cs.SY 2013
Year: 2013

This manuscript contains technical details of recent results developed by the authors on adaptive model predictive control for constrained linear systems that exhibits exploring property and uses basis function model parametrization.
Development of Comprehensive Devnagari Numeral and Character Database for Offline Handwritten Character Recognition
Venue: arXiv cs.CV 2013
Year: 2013

In handwritten character recognition, benchmark database plays an important role in evaluating the performance of various algorithms and the results obtained by various researchers. In Devnagari script, there is lack of such official benchmark. This paper focuses on the generation of offline benchmark database for Devnagari handwritten numerals and characters. The present work generated 5137 and 20305 isolated samples for numeral and character database, respectively, from 750 writers of all ages, sex, education, and profession. The offline sample images are stored in TIFF image format as it occupies less memory. Also, the data is presented in binary level so that memory requirement is further reduced. It will facilitate research on handwriting recognition of Devnagari script through free access to the researchers.
On the asymptotic hyperstability of switched systems
Venue: arXiv cs.SY 2013
Year: 2013

Asymptotic hyperstability is achievable under certain switching laws if at least one of the feed-forward parameterization: 1) possesses a strictly positive real transfer function, 2) a minimum residence time interval is respected for each activation time interval of such a parameterization, and 3) a maximum allowable residence time interval is guaranteed for all active parameterization which is not positive real.
Alternating Turing machines for inductive languages
Venue: arXiv cs.LO 2013
Year: 2013

We show that alternating Turing machines, with a novel and natural definition of acceptance, accept precisely the inductive (Pi-1-1) languages. Total alternating machines, that either accept or reject each input, accept precisely the hyper-elementary (Delta-1-1) languages. Moreover, bounding the permissible number of alternations yields a characterization of the levels of the arithmetical hierarchy. Notably, these results use simple finite computing devices, with finitary and discrete operational semantics, and neither the results nor their proofs make any use of transfinite ordinals. Our characterizations elucidate the analogy between the polynomial-time hierarchy and the arithmetical hierarchy, as well as between their respective limits, namely polynomial-space and Pi-1-1.