OpenRaiser/Intern-Atlas huggingface dataset:
Incarnation in Ludics and maximal cliques of paths
Venue: arXiv cs.LO 2015
Year: 2015

Ludics is a reconstruction of logic with interaction as a primitive notion, in the sense that the primary logical concepts are no more formulas and proofs but cut-elimination interpreted as an interaction between objects called designs. When the interaction between two designs goes well, such two designs are said to be orthogonal. A behaviour is a set of designs closed under bi-orthogonality. Logical formulas are then denoted by behaviours. Finally proofs are interpreted as designs satisfying particular properties. In that way, designs are more general than proofs and we may notice in particular that they are not typed objects. Incarnation is introduced by Girard in Ludics as a characterization of "useful" designs in a behaviour. The incarnation of a design is defined as its subdesign that is the smallest one in the behaviour ordered by inclusion. It is useful in particular because being "incarnated" is one of the conditions for a design to denote a proof of a formula. The computation of incarnation is important also as it gives a minimal denotation for a formula, and more generally for a behaviour. We give here a constructive way to capture the incarnation of the behaviour of a set of designs, without computing the behaviour itself. The method we follow uses an alternative definition of designs: rather than defining them as sets of chronicles, we consider them as sets of paths, a concept very close to that of play in game semantics that allows an easier handling of the interaction: the unfolding of interaction is a path common to two interacting designs.
Decentralized Multi-Robot Encirclement of a 3D Target with Guaranteed Collision Avoidance
Venue: arXiv cs.SY 2015
Year: 2015

We present a control framework for achieving encirclement of a target moving in 3D using a multi-robot system. Three variations of a basic control strategy are proposed for different versions of the encirclement problem, and their effectiveness is formally established. An extension ensuring maintenance of a safe inter-robot distance is also discussed. The proposed framework is fully decentralized and only requires local communication among robots; in particular, each robot locally estimates all the relevant global quantities. We validate the proposed strategy through simulations on kinematic point robots and quadrotor UAVs, as well as experiments on differential-drive wheeled mobile robots.
Interactive Logic Programming via Choice-Disjunctive Clauses
Venue: arXiv cs.LO 2015
Year: 2015

Adding interaction to logic programming is an essential task. Expressive logics such as linear logic provide a theoretical basis for such a mechanism. Unfortunately, none of the existing linear logic languages can model interactions with the user. This is because they uses provability as the sole basis for computation. We propose to use the game semantics instead of provability as the basis for computation to allow for more active participation from the user. We illustrate our idea via muprolog, an extension of Prolog with choice-disjunctive clauses.
Approximating the Little Grothendieck Problem over the Orthogonal and Unitary Groups
Venue: arXiv cs.DS 2015
Year: 2015

The little Grothendieck problem consists of maximizing $\sum_{ij}C_{ij}x_ix_j$ over binary variables $x_i\in\{\pm1\}$, where C is a positive semidefinite matrix. In this paper we focus on a natural generalization of this problem, the little Grothendieck problem over the orthogonal group. Given C a dn x dn positive semidefinite matrix, the objective is to maximize $\sum_{ij}Tr (C_{ij}^TO_iO_j^T)$ restricting $O_i$ to take values in the group of orthogonal matrices, where $C_{ij}$ denotes the (ij)-th d x d block of C. We propose an approximation algorithm, which we refer to as Orthogonal-Cut, to solve this problem and show a constant approximation ratio. Our method is based on semidefinite programming. For a given $d\geq 1$, we show a constant approximation ratio of $α_{R}(d)^2$, where $α_{R}(d)$ is the expected average singular value of a d x d matrix with random Gaussian $N(0,1/d)$ i.i.d. entries. For d=1 we recover the known $α_{R}(1)^2=2/π$ approximation guarantee for the classical little Grothendieck problem. Our algorithm and analysis naturally extends to the complex valued case also providing a constant approximation ratio for the analogous problem over the Unitary Group. Orthogonal-Cut also serves as an approximation algorithm for several applications, including the Procrustes problem where it improves over the best previously known approximation ratio of~$\frac1{2\sqrt{2}}$. The little Grothendieck problem falls under the class of problems approximated by a recent algorithm proposed in the context of the non-commutative Grothendieck inequality. Nonetheless, our approach is simpler and it provides a more efficient algorithm with better approximation ratios and matching integrality gaps. Finally, we also provide an improved approximation algorithm for the more general little Grothendieck problem over the orthogonal (or unitary) group with rank constraints.
A Quantized Johnson Lindenstrauss Lemma: The Finding of Buffon's Needle
Venue: arXiv cs.IT 2015
Year: 2015

In 1733, Georges-Louis Leclerc, Comte de Buffon in France, set the ground of geometric probability theory by defining an enlightening problem: What is the probability that a needle thrown randomly on a ground made of equispaced parallel strips lies on two of them? In this work, we show that the solution to this problem, and its generalization to $N$ dimensions, allows us to discover a quantized form of the Johnson-Lindenstrauss (JL) Lemma, i.e., one that combines a linear dimensionality reduction procedure with a uniform quantization of precision $δ>0$. In particular, given a finite set $\mathcal S \subset \mathbb R^N$ of $S$ points and a distortion level $ε>0$, as soon as $M > M_0 = O(ε^{-2} \log S)$, we can (randomly) construct a mapping from $(\mathcal S, \ell_2)$ to $(δ\mathbb Z^M, \ell_1)$ that approximately preserves the pairwise distances between the points of $\mathcal S$. Interestingly, compared to the common JL Lemma, the mapping is quasi-isometric and we observe both an additive and a multiplicative distortions on the embedded distances. These two distortions, however, decay as $O(\sqrt{(\log S)/M})$ when $M$ increases. Moreover, for coarse quantization, i.e., for high $δ$ compared to the set radius, the distortion is mainly additive, while for small $δ$ we tend to a Lipschitz isometric embedding. Finally, we prove the existence of a "nearly" quasi-isometric embedding of $(\mathcal S, \ell_2)$ into $(δ\mathbb Z^M, \ell_2)$. This one involves a non-linear distortion of the $\ell_2$-distance in $\mathcal S$ that vanishes for distant points in this set. Noticeably, the additive distortion in this case is slower, and decays as $O(\sqrt[4]{(\log S)/M})$.
A New Method for the Analysis of Signals: The Square Wave Transform (SWT)
Venue: arXiv cs.NA 2015
Year: 2015

The results obtained by analyzing signals with the Square Wave Method (SWM) introduced previously can be presented in the frequency domain clearly and precisely by using the Square Wave Transform (SWT) described here. As an example, the SWT is used to analyze a sequence of samples (that is, of measured values) taken from an electroencephalographic recording.
Experimental Evaluation of Interference Alignment for Broadband WLAN Systems
Venue: arXiv cs.IT 2015
Year: 2015

In this paper we present an experimental study on the performance of spatial Interference Alignment (IA) in indoor wireless local area network scenarios that use Orthogonal Frequency Division Multiplexing (OFDM) according to the physical-layer specifications of the IEEE 802.11a standard. Experiments have been carried out using a wireless network testbed capable of implementing a 3-user MIMO interference channel. We have implemented IA decoding schemes that can be designed according to distinct criteria (e.g. zero-forcing or MaxSINR). The measurement methodology has been validated considering practical issues like the number of OFDM training symbols used for channel estimation or feedback time. In case of asynchronous users, a time-domain IA decoding filter is also compared to its frequency-domain counterpart. We also evaluated the performance of IA from bit error rate measurement-based results in comparison to different time-division multiple access transmission schemes. The comparison includes single- and multiple-antenna systems transmitting over the dominant mode of the MIMO channel. Our results indicate that spatial IA is suitable for practical indoor scenarios in which wireless channels often exhibit relatively large coherence times.
The Random Bit Complexity of Mobile Robots Scattering
Venue: arXiv cs.DS 2015
Year: 2015

We consider the problem of scattering $n$ robots in a two dimensional continuous space. As this problem is impossible to solve in a deterministic manner, all solutions must be probabilistic. We investigate the amount of randomness (that is, the number of random bits used by the robots) that is required to achieve scattering. We first prove that $n \log n$ random bits are necessary to scatter $n$ robots in any setting. Also, we give a sufficient condition for a scattering algorithm to be random bit optimal. As it turns out that previous solutions for scattering satisfy our condition, they are hence proved random bit optimal for the scattering problem. Then, we investigate the time complexity of scattering when strong multiplicity detection is not available. We prove that such algorithms cannot converge in constant time in the general case and in $o(\log \log n)$ rounds for random bits optimal scattering algorithms. However, we present a family of scattering algorithms that converge as fast as needed without using multiplicity detection. Also, we put forward a specific protocol of this family that is random bit optimal ($n \log n$ random bits are used) and time optimal ($\log \log n$ rounds are used). This improves the time complexity of previous results in the same setting by a $\log n$ factor. Aside from characterizing the random bit complexity of mobile robot scattering, our study also closes its time complexity gap with and without strong multiplicity detection (that is, $O(1)$ time complexity is only achievable when strong multiplicity detection is available, and it is possible to approach it as needed otherwise).
$μ$-Limit Sets of Cellular Automata from a Computational Complexity Perspective
Venue: arXiv cs.DM 2015
Year: 2015

This paper concerns $μ$-limit sets of cellular automata: sets of configurations made of words whose probability to appear does not vanish with time, starting from an initial $μ$-random configuration. More precisely, we investigate the computational complexity of these sets and of related decision problems. Main results: first, $μ$-limit sets can have a $Σ\_3^0$-hard language, second, they can contain only $α$-complex configurations, third, any non-trivial property concerning them is at least $Π\_3^0$-hard. We prove complexity upper bounds, study restrictions of these questions to particular classes of CA, and different types of (non-)convergence of the measure of a word during the evolution.
The Bethe Free Energy Allows to Compute the Conditional Entropy of Graphical Code Instances. A Proof from the Polymer Expansion
Venue: arXiv cs.IT 2015
Year: 2015

The main objective of this paper is to explore the precise relationship between the Bethe free energy (or entropy) and the Shannon conditional entropy of graphical error correcting codes. The main result shows that the Bethe free energy associated with a low-density parity-check code used over a binary symmetric channel in a large noise regime is, with high probability, asymptotically exact as the block length grows. To arrive at this result we develop new techniques for rather general graphical models based on the loop sum as a starting point and the polymer expansion from statistical mechanics. The true free energy is computed as a series expansion containing the Bethe free energy as its zero-th order term plus a series of corrections. It is easily seen that convergence criteria for such expansions are satisfied for general high-temperature models. We apply these general results to ensembles of low-density generator-matrix and parity-check codes. While the application to generator-matrix codes follows standard "high temperature" methods, the case of parity-check codes requires non-trivial new ideas because the hard constraints correspond to a zero-temperature regime. Nevertheless one can combine the polymer expansion with expander and counting arguments to show that the difference between the true and Bethe free energies vanishes with high probability in the large block
Gait Velocity Estimation using time interleaved between Consecutive Passive IR Sensor Activations
Venue: arXiv cs.OH 2015
Year: 2015

Gait velocity has been consistently shown to be an important indicator and predictor of health status, especially in older adults. It is often assessed clinically, but the assessments occur infrequently and do not allow optimal detection of key health changes when they occur. In this paper, we show that the time gap between activations of a pair of Passive Infrared (PIR) motion sensors installed in the consecutively visited room pair carry rich latent information about a person's gait velocity. We name this time gap transition time and show that despite a six second refractory period of the PIR sensors, transition time can be used to obtain an accurate representation of gait velocity. Using a Support Vector Regression (SVR) approach to model the relationship between transition time and gait velocity, we show that gait velocity can be estimated with an average error less than 2.5 cm/sec. This is demonstrated with data collected over a 5 year period from 74 older adults monitored in their own homes. This method is simple and cost effective and has advantages over competing approaches such as: obtaining 20 to 100x more gait velocity measurements per day and offering the fusion of location-specific information with time stamped gait estimates. These advantages allow stable estimates of gait parameters (maximum or average speed, variability) at shorter time scales than current approaches. This also provides a pervasive in-home method for context-aware gait velocity sensing that allows for monitoring of gait trajectories in space and time.
Towards Energy Efficiency: Forecasting Indoor Temperature via Multivariate Analysis
Venue: arXiv cs.SY 2015
Year: 2015

The small medium large system (SMLSystem) is a house built at the Universidad CEU Cardenal Herrera (CEU-UCH) for participation in the Solar Decathlon 2013 competition. Several technologies have been integrated to reduce power consumption. One of these is a forecasting system based on artificial neural networks (ANNs), which is able to predict indoor temperature in the near future using captured data by a complex monitoring system as the input. A study of the impact on forecasting performance of different covariate combinations is presented in this paper. Additionally, a comparison of ANNs with the standard statistical forecasting methods is shown. The research in this paper has been focused on forecasting the indoor temperature of a house, as it is directly related to HVAC---heating, ventilation and air conditioning---system consumption. HVAC systems at the SMLSystem house represent 53.9% of the overall power consumption. The energy used to maintain temperature was measured to be 30--38.9% of the energy needed to lower it. Hence, these forecasting measures allow the house to adapt itself to future temperature conditions by using home automation in an energy-efficient manner. Experimental results show a high forecasting accuracy and therefore, they might be used to efficiently control an HVAC system.
Approximate Message Passing-based Compressed Sensing Reconstruction with Generalized Elastic Net Prior
Venue: arXiv cs.IT 2015
Year: 2015

In this paper, we study the compressed sensing reconstruction problem with generalized elastic net prior (GENP), where a sparse signal is sampled via a noisy underdetermined linear observation system, and an additional initial estimation of the signal (the GENP) is available during the reconstruction. We first incorporate the GENP into the LASSO and the approximate message passing (AMP) frameworks, denoted by GENP-LASSO and GENP-AMP respectively. We then investigate the parameter selection, state evolution, and noise-sensitivity analysis of GENP-AMP. We show that, thanks to the GENP, there is no phase transition boundary in the proposed frameworks, i.e., the reconstruction error is bounded in the entire plane. The error is also smaller than those of the standard AMP and scalar denoising. A practical parameterless version of the GENP-AMP is also developed, which does not need to know the sparsity of the unknown signal and the variance of the GENP. Simulation results are presented to verify the efficiency of the proposed schemes.
On Probability Estimation via Relative Frequencies and Discount
Venue: arXiv cs.IT 2015
Year: 2015

Probability estimation is an elementary building block of every statistical data compression algorithm. In practice probability estimation is often based on relative letter frequencies which get scaled down, when their sum is too large. Such algorithms are attractive in terms of memory requirements, running time and practical performance. However, there still is a lack of theoretical understanding. In this work we formulate a typical probability estimation algorithm based on relative frequencies and frequency discount, Algorithm RFD. Our main contribution is its theoretical analysis. We show that the code length it requires above an arbitrary piecewise stationary model with bounded and unbounded letter probabilities is small. This theoretically confirms the recency effect of periodic frequency discount, which has often been observed empirically.
The Noisy Power Method: A Meta Algorithm with Applications
Venue: arXiv cs.DS 2015
Year: 2015

We provide a new robust convergence analysis of the well-known power method for computing the dominant singular vectors of a matrix that we call the noisy power method. Our result characterizes the convergence behavior of the algorithm when a significant amount noise is introduced after each matrix-vector multiplication. The noisy power method can be seen as a meta-algorithm that has recently found a number of important applications in a broad range of machine learning problems including alternating minimization for matrix completion, streaming principal component analysis (PCA), and privacy-preserving spectral analysis. Our general analysis subsumes several existing ad-hoc convergence bounds and resolves a number of open problems in multiple applications including streaming PCA and privacy-preserving singular vector computation.
Toward a unified theory of sparse dimensionality reduction in Euclidean space
Venue: arXiv cs.DS 2015
Year: 2015

Let $Φ\in\mathbb{R}^{m\times n}$ be a sparse Johnson-Lindenstrauss transform [KN14] with $s$ non-zeroes per column. For a subset $T$ of the unit sphere, $\varepsilon\in(0,1/2)$ given, we study settings for $m,s$ required to ensure $$ \mathop{\mathbb{E}}_Φ\sup_{x\in T} \left|\|Φx\|_2^2 - 1 \right| < \varepsilon , $$ i.e. so that $Φ$ preserves the norm of every $x\in T$ simultaneously and multiplicatively up to $1+\varepsilon$. We introduce a new complexity parameter, which depends on the geometry of $T$, and show that it suffices to choose $s$ and $m$ such that this parameter is small. Our result is a sparse analog of Gordon's theorem, which was concerned with a dense $Φ$ having i.i.d. Gaussian entries. We qualitatively unify several results related to the Johnson-Lindenstrauss lemma, subspace embeddings, and Fourier-based restricted isometries. Our work also implies new results in using the sparse Johnson-Lindenstrauss transform in numerical linear algebra, classical and model-based compressed sensing, manifold learning, and constrained least squares problems such as the Lasso.
Recent Advances in Graph Partitioning
Venue: arXiv cs.DS 2015
Year: 2015

We survey recent trends in practical algorithms for balanced graph partitioning together with applications and future research directions.
#BIS-Hardness for 2-Spin Systems on Bipartite Bounded Degree Graphs in the Tree Nonuniqueness Region
Venue: arXiv cs.CC 2015
Year: 2015

Counting independent sets on bipartite graphs (#BIS) is considered a canonical counting problem of intermediate approximation complexity. It is conjectured that #BIS neither has an FPRAS nor is as hard as #SAT to approximate. We study #BIS in the general framework of two-state spin systems on bipartite graphs. We define two notions, nearly-independent phase-correlated spins and unary symmetry breaking. We prove that it is #BIS-hard to approximate the partition function of any 2-spin system on bipartite graphs supporting these two notions. As a consequence, we classify the complexity of approximating the partition function of antiferromagnetic 2-spin systems on bounded-degree bipartite graphs.
On the Security of Key Extraction from Measuring Physical Quantities
Venue: arXiv cs.CR 2015
Year: 2015

Key extraction via measuring a physical quantity is a class of information theoretic key exchange protocols that rely on the physical characteristics of the communication channel to enable the computation of a shared key by two (or more) parties that share no prior secret information. The key is supposed to be information theoretically hidden to an eavesdropper. Despite the recent surge of research activity in the area, concrete claims about the security of the protocols typically rely on channel abstractions that are not fully experimentally substantiated. In this work, we propose a novel methodology for the {\em experimental} security analysis of these protocols. The crux of our methodology is a falsifiable channel abstraction that is accompanied by an efficient experimental approximation algorithm of the {\em conditional min-entropy} available to the two parties given the view of the eavesdropper. We focus on the signal strength between two wirelessly communicating transceivers as the measured quantity and we use an experimental setup to compute the conditional min-entropy of the channel given the view of the attacker which we find to be linearly increasing. Armed with this understanding of the channel, we showcase the methodology by providing a general protocol for key extraction in this setting that is shown to be secure for a concrete parameter selection. In this way we provide a first comprehensively analyzed wireless key extraction protocol that is demonstrably secure against passive adversaries. Our methodology uses hidden Markov models as the channel model and a dynamic programming approach to approximate conditional min-entropy but other possible instantiations of the methodology can be motivated by our work.
Spectral Efficiency of Random Time-Hopping CDMA
Venue: arXiv cs.IT 2015
Year: 2015

Traditionally paired with impulsive communications, Time-Hopping CDMA (TH-CDMA) is a multiple access technique that separates users in time by coding their transmissions into pulses occupying a subset of $N_\mathsf{s}$ chips out of the total $N$ included in a symbol period, in contrast with traditional Direct-Sequence CDMA (DS-CDMA) where $N_\mathsf{s}=N$. This work analyzes TH-CDMA with random spreading, by determining whether peculiar theoretical limits are identifiable, with both optimal and sub-optimal receiver structures, in particular in the archetypal case of sparse spreading, that is, $N_\mathsf{s}=1$. Results indicate that TH-CDMA has a fundamentally different behavior than DS-CDMA, where the crucial role played by energy concentration, typical of time-hopping, directly relates with its intrinsic "uneven" use of degrees of freedom.