OpenRaiser/Intern-Atlas huggingface dataset:
Hardware Impairments in Large-scale MISO Systems: Energy Efficiency, Estimation, and Capacity Limits
Venue: arXiv cs.IT 2013
Year: 2013

The use of large-scale antenna arrays has the potential to bring substantial improvements in energy efficiency and/or spectral efficiency to future wireless systems, due to the greatly improved spatial beamforming resolution. Recent asymptotic results show that by increasing the number of antennas one can achieve a large array gain and at the same time naturally decorrelate the user channels; thus, the available energy can be focused very accurately at the intended destinations without causing much inter-user interference. Since these results rely on asymptotics, it is important to investigate whether the conventional system models are still reasonable in the asymptotic regimes. This paper analyzes the fundamental limits of large-scale multiple-input single-output (MISO) communication systems using a generalized system model that accounts for transceiver hardware impairments. As opposed to the case of ideal hardware, we show that these practical impairments create finite ceilings on the estimation accuracy and capacity of large-scale MISO systems. Surprisingly, the performance is only limited by the hardware at the single-antenna user terminal, while the impact of impairments at the large-scale array vanishes asymptotically. Furthermore, we show that an arbitrarily high energy efficiency can be achieved by reducing the power while increasing the number of antennas.
Broadcast Channel Games: Equilibrium Characterization and a MIMO MAC-BC Game Duality
Venue: arXiv cs.IT 2013
Year: 2013

The emergence of heterogeneous decentralized networks without a central controller, such as device-to-device communication systems, has created the need for new problem frameworks to design and analyze the performance of such networks. As a key step towards such an analysis for general networks, this paper examines the strategic behavior of \emph{receivers} in a Gaussian broadcast channel (BC) and \emph{transmitters} in a multiple access channel (MAC) with sum power constraints (sum power MAC) using the framework of non-cooperative game theory. These signaling scenarios are modeled as generalized Nash equilibrium problems (GNEPs) with jointly convex and coupled constraints and the existence and uniqueness of equilibrium achieving strategies and equilibrium utilities are characterized for both the Gaussian BC and the sum power MAC. The relationship between Pareto-optimal boundary points of the capacity region and the generalized Nash equilibria (GNEs) are derived for the several special cases and in all these cases it is shown that all the GNEs are Pareto-optimal, demonstrating that there is no loss in efficiency when players adopt strategic behavior in these scenarios. Several key equivalence relations are derived and used to demonstrate a game-theoretic duality between the Gaussian MAC and the Gaussian BC. This duality allows a parametrized computation of the equilibria of the BC in terms of the equilibria of the MAC and paves the way to translate several MAC results to the dual BC scenario.
Nouvelle approche de recommandation personnalisee dans les folksonomies basee sur le profil des utilisateurs
Venue: arXiv cs.IR 2013
Year: 2013

In folksonomies, users use to share objects (movies, books, bookmarks, etc.) by annotating them with a set of tags of their own choice. With the rise of the Web 2.0 age, users become the core of the system since they are both the contributors and the creators of the information. Yet, each user has its own profile and its own ideas making thereby the strength as well as the weakness of folksonomies. Indeed, it would be helpful to take account of users' profile when suggesting a list of tags and resources or even a list of friends, in order to make a personal recommandation, instead of suggesting the more used tags and resources in the folksonomy. In this paper, we consider users' profile as a new dimension of a folksonomy classically composed of three dimensions <users, tags, ressources> and we propose an approach to group users with equivalent profiles and equivalent interests as quadratic concepts. Then, we use such structures to propose our personalized recommendation system of users, tags and resources according to each user's profile. Carried out experiments on two real-world datasets, i.e., MovieLens and BookCrossing highlight encouraging results in terms of precision as well as a good social evaluation.
An upper bound of Singleton type for componentwise products of linear codes
Venue: arXiv cs.IT 2013
Year: 2013

We give an upper bound that relates the minimum weight of a nonzero componentwise product of codewords from some given number of linear codes, with the dimensions of these codes. Its shape is a direct generalization of the classical Singleton bound.
Tight Kernel Bounds for Problems on Graphs with Small Degeneracy
Venue: arXiv cs.DS 2013
Year: 2013

In this paper we consider kernelization for problems on d-degenerate graphs, i.e. graphs such that any subgraph contains a vertex of degree at most $d$. This graph class generalizes many classes of graphs for which effective kernelization is known to exist, e.g. planar graphs, H-minor free graphs, and H-topological-minor free graphs. We show that for several natural problems on d-degenerate graphs the best known kernelization upper bounds are essentially tight.
Noncoherent Trellis Coded Quantization: A Practical Limited Feedback Technique for Massive MIMO Systems
Venue: arXiv cs.IT 2013
Year: 2013

Accurate channel state information (CSI) is essential for attaining beamforming gains in single-user (SU) multiple-input multiple-output (MIMO) and multiplexing gains in multi-user (MU) MIMO wireless communication systems. State-of-the-art limited feedback schemes, which rely on pre-defined codebooks for channel quantization, are only appropriate for a small number of transmit antennas and low feedback overhead. In order to scale informed transmitter schemes to emerging massive MIMO systems with a large number of transmit antennas at the base station, one common approach is to employ time division duplexing (TDD) and to exploit the implicit feedback obtained from channel reciprocity. However, most existing cellular deployments are based on frequency division duplexing (FDD), hence it is of great interest to explore backwards compatible massive MIMO upgrades of such systems. For a fixed feedback rate per antenna, the number of codewords for quantizing the channel grows exponentially with the number of antennas, hence generating feedback based on look-up from a standard vector quantized codebook does not scale. In this paper, we propose noncoherent trellis-coded quantization (NTCQ), whose encoding complexity scales linearly with the number of antennas. The approach exploits the duality between source encoding in a Grassmannian manifold and noncoherent sequence detection. Furthermore, since noncoherent detection can be realized near-optimally using a bank of coherent detectors, we obtain a low-complexity implementation of NTCQ encoding using an off-the-shelf Viterbi algorithm applied to standard trellis coded quantization. We also develop advanced NTCQ schemes which utilize various channel properties such as temporal/spatial correlations. Simulation results show the proposed NTCQ and its extensions can achieve near-optimal performance with moderate complexity and feedback overhead.
Surface Reconstruction from Scattered Point via RBF Interpolation on GPU
Venue: arXiv cs.DC 2013
Year: 2013

In this paper we describe a parallel implicit method based on radial basis functions (RBF) for surface reconstruction. The applicability of RBF methods is hindered by its computational demand, that requires the solution of linear systems of size equal to the number of data points. Our reconstruction implementation relies on parallel scientific libraries and is supported for massively multi-core architectures, namely Graphic Processor Units (GPUs). The performance of the proposed method in terms of accuracy of the reconstruction and computing time shows that the RBF interpolant can be very effective for such problem.
A Characterization of Approximation Resistance
Venue: arXiv cs.CC 2013
Year: 2013

A predicate f:{-1,1}^k -> {0,1} with ρ(f) = \frac{|f^{-1}(1)|}{2^k} is called {\it approximation resistant} if given a near-satisfiable instance of CSP(f), it is computationally hard to find an assignment that satisfies at least ρ(f)+Ω(1) fraction of the constraints. We present a complete characterization of approximation resistant predicates under the Unique Games Conjecture. We also present characterizations in the {\it mixed} linear and semi-definite programming hierarchy and the Sherali-Adams linear programming hierarchy. In the former case, the characterization coincides with the one based on UGC. Each of the two characterizations is in terms of existence of a probability measure with certain symmetry properties on a natural convex polytope associated with the predicate.
Memory Efficient Decoders using Spatially Coupled Quasi-Cyclic LDPC Codes
Venue: arXiv cs.IT 2013
Year: 2013

In this paper we propose the construction of Spatially Coupled Low-Density Parity-Check (SC-LDPC) codes using a periodic time-variant Quasi-Cyclic (QC) algorithm. The QC based approach is optimized to obtain memory efficiency in storing the parity-check matrix in the decoders. A hardware model of the parity-check storage units has been designed for Xilinx FPGA to compare the logic and memory requirements for various approaches. It is shown that the proposed QC SC-LDPC code (with optimization) can be stored with reasonable logic resources and without the need of block memory in the FPGA. In addition, a significant improvement in the processing speed is also achieved.
Math-Net.Ru as a Digital Archive of the Russian Mathematical Knowledge from the XIX Century to Today
Venue: arXiv cs.DL 2013
Year: 2013

The main goal of the project Math-Net.Ru is to collect scientific publications in Russian and Soviet mathematics journals since their foundation to today and the authors of these publications into a single database and to provide access to full-text articles for broad international mathematical community. Leading Russian mathematics journals have been comprehensively digitized dating back to the first volumes.
Validity of a clinical decision rule based alert system for drug dose adjustment in patients with renal failure intended to improve pharmacists' analysis of medication orders in hospitals
Venue: arXiv cs.AI 2013
Year: 2013

Objective: The main objective of this study was to assess the diagnostic performances of an alert system integrated into the CPOE/EMR system for renally cleared drug dosing control. The generated alerts were compared with the daily routine practice of pharmacists as part of the analysis of medication orders. Materials and Methods: The pharmacists performed their analysis of medication orders as usual and were not aware of the alert system interventions that were not displayed for the purpose of the study neither to the physician nor to the pharmacist but kept with associate recommendations in a log file. A senior pharmacist analyzed the results of medication order analysis with and without the alert system. The unit of analysis was the drug prescription line. The primary study endpoints were the detection of drug-dose prescription errors and inter-rater reliability between the alert system and the pharmacists in the detection of drug dose error. Results: The alert system fired alerts in 8.41% (421/5006) of cases: 5.65% (283/5006) exceeds max daily dose alerts and 2.76% (138/5006) under dose alerts. The alert system and the pharmacists showed a relatively poor concordance: 0.106 (CI 95% [0.068, 0.144]). According to the senior pharmacist review, the alert system fired more appropriate alerts than pharmacists, and made fewer errors than pharmacists in analyzing drug dose prescriptions: 143 for the alert system and 261 for the pharmacists. Unlike the alert system, most diagnostic errors made by the pharmacists were false negatives. The pharmacists were not able to analyze a significant number (2097; 25.42%) of drug prescription lines because understaffing. Conclusion: This study strongly suggests that an alert system would be complementary to the pharmacists activity and contribute to drug prescription safety.
Formal Mathematics on Display: A Wiki for Flyspeck
Venue: arXiv cs.MS 2013
Year: 2013

The Agora system is a prototype "Wiki for Formal Mathematics", with an aim to support developing and documenting large formalizations of mathematics in a proof assistant. The functions implemented in Agora include in-browser editing, strong AI/ATP proof advice, verification, and HTML rendering. The HTML rendering contains hyperlinks and provides on-demand explanation of the proof state for each proof step. In the present paper we show the prototype Flyspeck Wiki as an instance of Agora for HOL Light formalizations. The wiki can be used for formalizations of mathematics and for writing informal wiki pages about mathematics. Such informal pages may contain islands of formal text, which is used here for providing an initial cross-linking between Hales's informal Flyspeck book, and the formal Flyspeck development. The Agora platform intends to address distributed wiki-style collaboration on large formalization projects, in particular both the aspect of immediate editing, verification and rendering of formal code, and the aspect of gradual and mutual refactoring and correspondence of the initial informal text and its formalization. Here, we highlight these features within the Flyspeck Wiki.
Escaping the Trap of too Precise Topic Queries
Venue: arXiv cs.DL 2013
Year: 2013

At the very center of digital mathematics libraries lie controlled vocabularies which qualify the {\it topic} of the documents. These topics are used when submitting a document to a digital mathematics library and to perform searches in a library. The latter are refined by the use of these topics as they allow a precise classification of the mathematics area this document addresses. However, there is a major risk that users employ too precise topics to specify their queries: they may be employing a topic that is only "close-by" but missing to match the right resource. We call this the {\it topic trap}. Indeed, since 2009, this issue has appeared frequently on the i2geo.net platform. Other mathematics portals experience the same phenomenon. An approach to solve this issue is to introduce tolerance in the way queries are understood by the user. In particular, the approach of including fuzzy matches but this introduces noise which may prevent the user of understanding the function of the search engine. In this paper, we propose a way to escape the topic trap by employing the navigation between related topics and the count of search results for each topic. This supports the user in that search for close-by topics is a click away from a previous search. This approach was realized with the i2geo search engine and is described in detail where the relation of being {\it related} is computed by employing textual analysis of the definitions of the concepts fetched from the Wikipedia encyclopedia.
Graphic lambda calculus
Venue: arXiv cs.LO 2013
Year: 2013

We introduce and study graphic lambda calculus, a visual language which can be used for representing untyped lambda calculus, but it can also be used for computations in emergent algebras or for representing Reidemeister moves of locally planar tangle diagrams.
Lightweight Contention Management for Efficient Compare-and-Swap Operations
Venue: arXiv cs.DC 2013
Year: 2013

Many concurrent data-structure implementations use the well-known compare-and-swap (CAS) operation, supported in hardware by most modern multiprocessor architectures for inter-thread synchronization. A key weakness of the CAS operation is the degradation in its performance in the presence of memory contention. In this work we study the following question: can software-based contention management improve the efficiency of hardware-provided CAS operations? Our performance evaluation establishes that lightweight contention management support can greatly improve performance under medium and high contention levels while typically incurring only small overhead when contention is low.
Agent Based Intelligent Alert System for Smart-Phones
Venue: arXiv cs.HC 2013
Year: 2013

The paper deals with the design of an agent which modifies and enhances the various alert systems in the smartphones. The actions of the agent includes sorting the notifications abiding to human thinking, helping the user to have a safe conversation, assisting in tracking back the reach-ability status of the caller when needed, conveying the user about the notifications in times of situations like drained battery and smartly alerting the user in situations like sleeping. The agent uses the information gathered from a survey, to modify the existing methods of alerts and produce alerts which abide by the human cognitive responses.
Calculation of geometric characteristics of land cover and urban canyon for multi-scale parameterization of megalopolis meteorological models
Venue: arXiv cs.OH 2013
Year: 2013

The results of studies on the development of computational techniques for geometric and thematic characteristics of the underlying surface and urban canyon are presented. These characteristics are intended for parameterization of the local model of energy-mass exchange between the surface layer of the atmosphere and the surface of the active layer of the underlying urban areas (cities). Multiscale database of parameters of the underlying surface with a resolution of 200, 500 and 1000 meters is obtained. The use of micro-meteorology models that take into account the specificity of the urban environment, coupled with mesoscale prognostic models will significantly improve the sound quality of the meteorological fields and local operational weather forecasting in the metropolitan areas where considering the hydrometeorological situation is particularly important.
Modelling and Refinement in CODA
Venue: arXiv cs.SE 2013
Year: 2013

This paper provides an overview of the CODA framework for modelling and refinement of component-based embedded systems. CODA is an extension of Event-B and UML-B and is supported by a plug-in for the Rodin toolset. CODA augments Event-B with constructs for component-based modelling including components, communications ports, port connectors, timed communications and timing triggers. Component behaviour is specified through a combination of UML-B state machines and Event-B. CODA communications and timing are given an Event-B semantics through translation rules. Refinement is based on Event-B refinement and allows layered construction of CODA models in a consistent way.
Refining SCJ Mission Specifications into Parallel Handler Designs
Venue: arXiv cs.LO 2013
Year: 2013

Safety-Critical Java (SCJ) is a recent technology that restricts the execution and memory model of Java in such a way that applications can be statically analysed and certified for their real-time properties and safe use of memory. Our interest is in the development of comprehensive and sound techniques for the formal specification, refinement, design, and implementation of SCJ programs, using a correct-by-construction approach. As part of this work, we present here an account of laws and patterns that are of general use for the refinement of SCJ mission specifications into designs of parallel handlers used in the SCJ programming paradigm. Our notation is a combination of languages from the Circus family, supporting state-rich reactive models with the addition of class objects and real-time properties. Our work is a first step to elicit laws of programming for SCJ and fits into a refinement strategy that we have developed previously to derive SCJ programs.
On the Decidability and Complexity of Some Fragments of Metric Temporal Logic
Venue: arXiv cs.LO 2013
Year: 2013

Metric Temporal Logic, $\mtlfull$ is amongst the most studied real-time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval constraints $I$. \oomit{The classical results of Alur and Henzinger showed that $\mtlfull$ is undecidable where as $\mitl$ which uses only non-singular intervals $NS$ is decidable. In a surprizing result, Ouaknine and Worrell showed that the satisfiability of $\mtl$ is decidable over finite pointwise models, albeit with NPR decision complexity, whereas it remains undecidable for infinite pointwise models or for continuous time.} In this paper, we sharpen the decidability results by showing that the satisfiability of $\mtlsns$ (where $NS$ denotes non-singular intervals) is also decidable over finite pointwise strictly monotonic time. We give a satisfiability preserving reduction from the logic $\mtlsns$ to decidable logic $\mtl$ of Ouaknine and Worrell using the technique of temporal projections. We also investigate the decidability of unary fragment $\mtlfullunary$ (a question posed by A. Rabinovich) and show that $\mtlfut$ over continuous time as well as $\mtlfullunary$ over finite pointwise time are both undecidable. Moreover, $\mathsf{MTL}^{pw}[\fut_I]$ over finite pointwise models already has NPR lower bound for satisfiability checking. We also compare the expressive powers of some of these fragments using the technique of EF games for $\mathsf{MTL}$.
Streamforce: outsourcing access control enforcement for stream data to the clouds
Venue: arXiv cs.DB 2013
Year: 2013

As tremendous amount of data being generated everyday from human activity and from devices equipped with sensing capabilities, cloud computing emerges as a scalable and cost-effective platform to store and manage the data. While benefits of cloud computing are numerous, security concerns arising when data and computation are outsourced to a third party still hinder the complete movement to the cloud. In this paper, we focus on the problem of data privacy on the cloud, particularly on access controls over stream data. The nature of stream data and the complexity of sharing data make access control a more challenging issue than in traditional archival databases. We present Streamforce - a system allowing data owners to securely outsource their data to the cloud. The owner specifies fine-grained policies which are enforced by the cloud. The latter performs most of the heavy computations, while learning nothing about the data. To this end, we employ a number of encryption schemes, including deterministic encryption, proxy-based attribute based encryption and sliding-window encryption. In Streamforce, access control policies are modeled as secure continuous queries, which entails minimal changes to existing stream processing engines, and allows for easy expression of a wide-range of policies. In particular, Streamforce comes with a number of secure query operators including Map, Filter, Join and Aggregate. Finally, we implement Streamforce over an open source stream processing engine (Esper) and evaluate its performance on a cloud platform. The results demonstrate practical performance for many real-world applications, and although the security overhead is visible, Streamforce is highly scalable.