OpenRaiser/Intern-Atlas huggingface dataset:
PMI-based MIMO OFDM PHY Integrated Key Exchange (P-MOPI) Scheme
Venue: arXiv cs.IT 2011
Year: 2011

In the literature, J.-P. Cheng et al. have proposed the MIMO-OFDM PHY integrated (MOPI) scheme for achieving physical-layer security in practice without using any cryptographic ciphers. The MOPI scheme uses channel sounding and physical-layer network coding (PNC) to prevent eavesdroppers from learning the channel state information (CSI). Nevertheless, due to the use of multiple antennas for PNC at transmitter and beamforming at receiver, it is not possible to have spatial multiplexing nor use space-time codes in our previous MOPI scheme. In this paper, we propose a variant of the MOPI scheme, called P-MOPI, that works with a cryptographic cipher and utilizes precoding matrix index (PMI) as an efficient key-exchange mechanism. With channel sounding, the PMI is only known between the transmitter and the legal receiver. The shared key can then be used, e.g., as the seed to generate pseudo random bit sequences for securing subsequent transmissions using a stream cipher. By applying the same techniques at independent subcarriers of the OFDM system, the P-MOPI scheme easily allows two communicating parties to exchange over 100 secret bits. As a result, not only secure communication but also the MIMO gain can be guaranteed by using the P-MOPI scheme.
Reconciling Compressive Sampling Systems for Spectrally-sparse Continuous-time Signals
Venue: arXiv cs.IT 2011
Year: 2011

The Random Demodulator (RD) and the Modulated Wideband Converter (MWC) are two recently proposed compressed sensing (CS) techniques for the acquisition of continuous-time spectrally-sparse signals. They extend the standard CS paradigm from sampling discrete, finite dimensional signals to sampling continuous and possibly infinite dimensional ones, and thus establish the ability to capture these signals at sub-Nyquist sampling rates. The RD and the MWC have remarkably similar structures (similar block diagrams), but their reconstruction algorithms and signal models strongly differ. To date, few results exist that compare these systems, and owing to the potential impacts they could have on spectral estimation in applications like electromagnetic scanning and cognitive radio, we more fully investigate their relationship in this paper. We show that the RD and the MWC are both based on the general concept of random filtering, but employ significantly different sampling functions. We also investigate system sensitivities (or robustness) to sparse signal model assumptions. Lastly, we show that "block convolution" is a fundamental aspect of the MWC, allowing it to successfully sample and reconstruct block-sparse (multiband) signals. Based on this concept, we propose a new acquisition system for continuous-time signals whose amplitudes are block sparse. The paper includes detailed time and frequency domain analyses of the RD and the MWC that differ, sometimes substantially, from published results.
Networking
Venue: arXiv cs.NI 2011
Year: 2011

This paper discusses an efficient approach to design and implement a highly available peer- to-peer system irrespective of peer timing and churn.
Effective Privacy Amplification for Secure Classical Communications
Venue: arXiv cs.CR 2011
Year: 2011

We study the practical effectiveness of privacy amplification for classical key-distribution schemes. We find that in contrast to quantum key distribution schemes, the high fidelity of the raw key generated in classical systems allow the users to always sift a secure shorter key if they have an upper bound on the eavesdropper probability to correctly guess the exchanged key-bits. The number of privacy amplification iterations needed to achieve information leak of 10^-8 in existing classical communicators is 2 or 3 resulting in a corresponding slowdown 4 to 8. We analyze the inherent tradeoff between the number of iterations and the security of the raw key. This property which is unique to classical key distribution systems render them highly useful for practical, especially for noisy channels where sufficiently low quantum bit error ratios are difficult to achieve.
On Making Directed Graphs Eulerian
Venue: arXiv cs.DM 2011
Year: 2011

A directed graph is called Eulerian, if it contains a tour that traverses every arc in the graph exactly once. We study the problem of Eulerian extension (EE) where a directed multigraph G and a weight function is given and it is asked whether G can be made Eulerian by adding arcs whose total weight does not exceed a given threshold. This problem is motivated through applications in vehicle routing and flowshop scheduling. However, EE is NP-hard and thus we use the parameterized complexity framework to analyze it. In parameterized complexity, the running time of algorithms is considered not only with respect to input length, but also with respect to other properties of the input - called "parameters". Dorn et. al. proved that EE can be solved in O(4^k n^4) time, where k denotes the parameter "number of arcs that have to be added". In this thesis, we analyze EE with respect to the (smaller) parameters "number c of connected components in the input graph" and "sum b over indeg(v) - outdeg(v) for all vertices v in the input graph where this value is positive". We prove that there is an algorithm for EE whose running time is polynomial except for the term 4^(c log(bc^2)). To obtain this result, we make several observations about the sets of arcs that have to be added to the input graph in order to make it Eulerian. We build upon these observations to restate EE in a matching context. This matching formulation of EE might be an important tool to solve the question of whether EE can be solved within running time whose superpolynomial part depends only on c. We also consider polynomial time preprocessing routines for EE and show that these routines cannot yield instances whose size depends polynomially only on either of the parameters b, c, k unless coNP is contained in NP/poly.
Building a Chaotic Proved Neural Network
Venue: arXiv cs.AI 2011
Year: 2011

Chaotic neural networks have received a great deal of attention these last years. In this paper we establish a precise correspondence between the so-called chaotic iterations and a particular class of artificial neural networks: global recurrent multi-layer perceptrons. We show formally that it is possible to make these iterations behave chaotically, as defined by Devaney, and thus we obtain the first neural networks proven chaotic. Several neural networks with different architectures are trained to exhibit a chaotical behavior.
Meaning Negotiation as Inference
Venue: arXiv cs.AI 2011
Year: 2011

Meaning negotiation (MN) is the general process with which agents reach an agreement about the meaning of a set of terms. Artificial Intelligence scholars have dealt with the problem of MN by means of argumentations schemes, beliefs merging and information fusion operators, and ontology alignment but the proposed approaches depend upon the number of participants. In this paper, we give a general model of MN for an arbitrary number of agents, in which each participant discusses with the others her viewpoint by exhibiting it in an actual set of constraints on the meaning of the negotiated terms. We call this presentation of individual viewpoints an angle. The agents do not aim at forming a common viewpoint but, instead, at agreeing about an acceptable common angle. We analyze separately the process of MN by two agents (\emph{bilateral} or \emph{pairwise} MN) and by more than two agents (\emph{multiparty} MN), and we use game theoretic models to understand how the process develops in both cases: the models are Bargaining Game for bilateral MN and English Auction for multiparty MN. We formalize the process of reaching such an agreement by giving a deduction system that comprises of rules that are consistent and adequate for representing MN.
Equality, Quasi-Implicit Products, and Large Eliminations
Venue: arXiv cs.PL 2011
Year: 2011

This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including implicit arguments, are dropped during reduction of terms. We develop the metatheory for an undecidable version of the system with unannotated terms. We then devise a decidable system with annotated terms, justified in terms of the unannotated system. Finally, we show how the approach can be extended to account for large eliminations, using what we call quasi-implicit products.
Solutions for the MIMO Gaussian Wiretap Channel with a Cooperative Jammer
Venue: arXiv cs.IT 2011
Year: 2011

We study the Gaussian MIMO wiretap channel with a transmitter, a legitimate receiver, an eavesdropper and an external helper, each equipped with multiple antennas. The transmitter sends confidential messages to its intended receiver, while the helper transmits jamming signals independent of the source message to confuse the eavesdropper. The jamming signal is assumed to be treated as noise at both the intended receiver and the eavesdropper. We obtain a closed-form expression for the structure of the artificial noise covariance matrix that guarantees no decrease in the secrecy capacity of the wiretap channel. We also describe how to find specific realizations of this covariance matrix expression that provide good secrecy rate performance, even when there is no non-trivial null space between the helper and the intended receiver. Unlike prior work, our approach considers the general MIMO case, and is not restricted to SISO or MISO scenarios.
A Context-theoretic Framework for Compositionality in Distributional Semantics
Venue: arXiv cs.CL 2011
Year: 2011

Techniques in which words are represented as vectors have proved useful in many applications in computational linguistics, however there is currently no general semantic formalism for representing meaning in terms of vectors. We present a framework for natural language semantics in which words, phrases and sentences are all represented as vectors, based on a theoretical analysis which assumes that meaning is determined by context. In the theoretical analysis, we define a corpus model as a mathematical abstraction of a text corpus. The meaning of a string of words is assumed to be a vector representing the contexts in which it occurs in the corpus model. Based on this assumption, we can show that the vector representations of words can be considered as elements of an algebra over a field. We note that in applications of vector spaces to representing meanings of words there is an underlying lattice structure; we interpret the partial ordering of the lattice as describing entailment between meanings. We also define the context-theoretic probability of a string, and, based on this and the lattice structure, a degree of entailment between strings. We relate the framework to existing methods of composing vector-based representations of meaning, and show that our approach generalises many of these, including vector addition, component-wise multiplication, and the tensor product.
A Secure Web-Based File Exchange Server: Software Requirements Specification Document
Venue: arXiv cs.CR 2011
Year: 2011

This document presents brief software specification of a secure file exchange system prototype involving mutual authentication of the users via their browser and the application server with PKI-based certificates as credentials, the use of LDAP for credential management, and authentication between the application and database servers to maintain a high level of trust between all parties.
Minimum k-way cut of bounded size is fixed-parameter tractable
Venue: arXiv cs.DM 2011
Year: 2011

We consider a the minimum k-way cut problem for unweighted graphs with a size bound s on the number of cut edges allowed. Thus we seek to remove as few edges as possible so as to split a graph into k components, or report that this requires cutting more than s edges. We show that this problem is fixed-parameter tractable (FPT) in s. More precisely, for s=O(1), our algorithm runs in quadratic time while we have a different linear time algorithm for planar graphs and bounded genus graphs. Our tractability result stands in contrast to known W[1] hardness of related problems. Without the size bound, Downey et al.[2003] proved that the minimum k-way cut problem is W[1] hard in k even for simple unweighted graphs. Downey et al. asked about the status for planar graphs. Our result implies tractability in k for the planar graphs since the minimum k-way cut of a planar graph is of size at most 6k (more generally, we get tractability in k for any graph class with k-way cuts of size limited by is a function of k, e.g., bounded degree graphs, or simple graphs with an excluded minor). A simple reduction shows that vertex cuts are at least as hard as edge cuts, so the minimum k-way vertex cut is also W[1] hard in terms of k. Marx [2004] proved that finding a minimum k-way vertex cut of size s is also W[1] hard in s. Marx asked about the FPT status with edge cuts, which we prove tractable here. We are not aware of any other cut problem where the vertex version is W[1] hard but the edge version is FPT.
Numerical Evaluation of Algorithmic Complexity for Short Strings: A Glance into the Innermost Structure of Randomness
Venue: arXiv cs.IT 2011
Year: 2011

We describe an alternative method (to compression) that combines several theoretical and experimental results to numerically approximate the algorithmic (Kolmogorov-Chaitin) complexity of all $\sum_{n=1}^82^n$ bit strings up to 8 bits long, and for some between 9 and 16 bits long. This is done by an exhaustive execution of all deterministic 2-symbol Turing machines with up to 4 states for which the halting times are known thanks to the Busy Beaver problem, that is 11019960576 machines. An output frequency distribution is then computed, from which the algorithmic probability is calculated and the algorithmic complexity evaluated by way of the (Levin-Zvonkin-Chaitin) coding theorem.
The Structure of First-Order Causality (extended version)
Venue: arXiv cs.LO 2011
Year: 2011

Game semantics describe the interactive behavior of proofs by interpreting formulas as games on which proofs induce strategies. Such a semantics is introduced here for capturing dependencies induced by quantifications in first-order propositional logic. One of the main difficulties that has to be faced during the elaboration of this kind of semantics is to characterize definable strategies, that is strategies which actually behave like a proof. This is usually done by restricting the model to strategies satisfying subtle combinatorial conditions, whose preservation under composition is often difficult to show. Here, we present an original methodology to achieve this task, which requires to combine advanced tools from game semantics, rewriting theory and categorical algebra. We introduce a diagrammatic presentation of the monoidal category of definable strategies of our model, by the means of generators and relations: those strategies can be generated from a finite set of atomic strategies and the equality between strategies admits a finite axiomatization, this equational structure corresponding to a polarized variation of the notion of bialgebra. This work thus bridges algebra and denotational semantics in order to reveal the structure of dependencies induced by first-order quantifiers, and lays the foundations for a mechanized analysis of causality in programming languages.
List decoding of a class of affine variety codes
Venue: arXiv cs.IT 2011
Year: 2011

Consider a polynomial $F$ in $m$ variables and a finite point ensemble $S=S_1 \times ... \times S_m$. When given the leading monomial of $F$ with respect to a lexicographic ordering we derive improved information on the possible number of zeros of $F$ of multiplicity at least $r$ from $S$. We then use this information to design a list decoding algorithm for a large class of affine variety codes.
Jancar's formal system for deciding bisimulation of first-order grammars and its non-soundness
Venue: arXiv cs.FL 2011
Year: 2011

We construct an example of proof within the main formal system from arXiv:1010.4760v3, which is intended to capture the bisimulation equivalence for non-deterministic first-order grammars, and show that its conclusion is semantically false. We then locate and analyze the flawed argument in the soundness (meta)-proof of the above reference.
Simulation of Self-Assembly in the Abstract Tile Assembly Model with ISU TAS
Venue: arXiv cs.MS 2011
Year: 2011

Since its introduction by Erik Winfree in 1998, the abstract Tile Assembly Model (aTAM) has inspired a wealth of research. As an abstract model for tile based self-assembly, it has proven to be remarkably powerful and expressive in terms of the structures which can self-assemble within it. As research has progressed in the aTAM, the self-assembling structures being studied have become progressively more complex. This increasing complexity, along with a need for standardization of definitions and tools among researchers, motivated the development of the Iowa State University Tile Assembly Simulator (ISU TAS). ISU TAS is a graphical simulator and tile set editor for designing and building 2-D and 3-D aTAM tile assembly systems and simulating their self-assembly. This paper reviews the features and functionality of ISU TAS and describes how it can be used to further research into the complexities of the aTAM. Software and source code are available at http://www.cs.iastate.edu/~lnsa.
Highlights from the SOAP project survey. What Scientists Think about Open Access Publishing
Venue: arXiv cs.DL 2011
Year: 2011

The SOAP (Study of Open Access Publishing) project has run a large-scale survey of the attitudes of researchers on, and the experiences with, open access publishing. Around forty thousands answers were collected across disciplines and around the world, showing an overwhelming support for the idea of open access, while highlighting funding and (perceived) quality as the main barriers to publishing in open access journals. This article serves as an introduction to the survey and presents this and other highlights from a preliminary analysis of the survey responses. To allow a maximal re-use of the information collected by this survey, the data are hereby released under a CC0 waiver, so to allow libraries, publishers, funding agencies and academics to further analyse risks and opportunities, drivers and barriers, in the transition to open access publishing.
A Novel Unified Expression for the Capacity and Bit Error Probability of Wireless Communication Systems over Generalized Fading Channels
Venue: arXiv cs.IT 2011
Year: 2011

Analysis of the average binary error probabilities (ABEP) and average capacity (AC) of wireless communications systems over generalized fading channels have been considered separately in the past. This paper introduces a novel moment generating function (MGF)-based \emph{unified expression} for the ABEP and AC of single and multiple link communication with maximal ratio combining. In addition, this paper proposes the hyper-Fox's H fading model as a unified fading distribution of a majority of the well-known generalized fading models. As such, we offer a generic unified performance expression that can be easily calculated and that is applicable to a wide variety of fading scenarios. The mathematical formalism is illustrated with some selected numerical examples that validate the correctness of our newly derived results.
Succincter Text Indexing with Wildcards
Venue: arXiv cs.DS 2011
Year: 2011

We study the problem of indexing text with wildcard positions, motivated by the challenge of aligning sequencing data to large genomes that contain millions of single nucleotide polymorphisms (SNPs)---positions known to differ between individuals. SNPs modeled as wildcards can lead to more informed and biologically relevant alignments. We improve the space complexity of previous approaches by giving a succinct index requiring $(2 + o(1))n \log σ+ O(n) + O(d \log n) + O(k \log k)$ bits for a text of length $n$ over an alphabet of size $σ$ containing $d$ groups of $k$ wildcards. A key to the space reduction is a result we give showing how any compressed suffix array can be supplemented with auxiliary data structures occupying $O(n) + O(d \log \frac{n}{d})$ bits to also support efficient dictionary matching queries. The query algorithm for our wildcard index is faster than previous approaches using reasonable working space. More importantly our new algorithm greatly reduces the query working space to $O(d m + m \log n)$ bits. We note that compared to previous results this reduces the working space by two orders of magnitude when aligning short read data to the Human genome.
Interactive Learning Based Realizability and 1-Backtracking Games
Venue: arXiv cs.LO 2011
Year: 2011

We prove that interactive learning based classical realizability (introduced by Aschieri and Berardi for first order arithmetic) is sound with respect to Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy for the 1-Backtracking version of Tarski games. We also give examples of realizer and winning strategy extraction for some classical proofs. We also sketch some ongoing work about how to extend our notion of realizability in order to obtain completeness with respect to Coquand semantics, when it is restricted to 1-Backtracking games.
Superdeduction in Lambda-Bar-Mu-Mu-Tilde
Venue: arXiv cs.LO 2011
Year: 2011

Superdeduction is a method specially designed to ease the use of first-order theories in predicate logic. The theory is used to enrich the deduction system with new deduction rules in a systematic, correct and complete way. A proof-term language and a cut-elimination reduction already exist for superdeduction, both based on Christian Urban's work on classical sequent calculus. However the computational content of Christian Urban's calculus is not directly related to the (lambda-calculus based) Curry-Howard correspondence. In contrast the Lambda bar mu mu tilde calculus is a lambda-calculus for classical sequent calculus. This short paper is a first step towards a further exploration of the computational content of superdeduction proofs, for we extend the Lambda bar mu mu tilde calculus in order to obtain a proofterm langage together with a cut-elimination reduction for superdeduction. We also prove strong normalisation for this extension of the Lambda bar mu mu tilde calculus.
Dialectica Interpretation with Marked Counterexamples
Venue: arXiv cs.LO 2011
Year: 2011

Goedel's functional "Dialectica" interpretation can be used to extract functional programs from non-constructive proofs in arithmetic by employing two sorts of higher-order witnessing terms: positive realisers and negative counterexamples. In the original interpretation decidability of atoms is required to compute the correct counterexample from a set of candidates. When combined with recursion, this choice needs to be made for every step in the extracted program, however, in some special cases the decision on negative witnesses can be calculated only once. We present a variant of the interpretation in which the time complexity of extracted programs can be improved by marking the chosen witness and thus avoiding recomputation. The achieved effect is similar to using an abortive control operator to interpret computational content of non-constructive principles.