OpenRaiser/Intern-Atlas huggingface dataset:
Really Natural Linear Indexed Type Checking
Venue: arXiv cs.LO 2015
Year: 2015

Recent works have shown the power of linear indexed type systems for enforcing complex program properties. These systems combine linear types with a language of type-level indices, allowing more fine-grained analyses. Such systems have been fruitfully applied in diverse domains, including implicit complexity and differential privacy. A natural way to enhance the expressiveness of this approach is by allowing the indices to depend on runtime information, in the spirit of dependent types. This approach is used in DFuzz, a language for differential privacy. The DFuzz type system relies on an index language supporting real and natural number arithmetic over constants and variables. Moreover, DFuzz uses a subtyping mechanism to make types more flexible. By themselves, linearity, dependency, and subtyping each require delicate handling when performing type checking or type inference; their combination increases this challenge substantially, as the features can interact in non-trivial ways. In this paper, we study the type-checking problem for DFuzz. We show how we can reduce type checking for (a simple extension of) DFuzz to constraint solving over a first-order theory of naturals and real numbers which, although undecidable, can often be handled in practice by standard numeric solvers.
Template-based Monocular 3D Shape Recovery using Laplacian Meshes
Venue: arXiv cs.CV 2015
Year: 2015

We show that by extending the Laplacian formalism, which was first introduced in the Graphics community to regularize 3D meshes, we can turn the monocular 3D shape reconstruction of a deformable surface given correspondences with a reference image into a much better-posed problem. This allows us to quickly and reliably eliminate outliers by simply solving a linear least squares problem. This yields an initial 3D shape estimate, which is not necessarily accurate, but whose 2D projections are. The initial shape is then refined by a constrained optimization problem to output the final surface reconstruction. Our approach allows us to reduce the dimensionality of the surface reconstruction problem without sacrificing accuracy, thus allowing for real-time implementations.
Controlled Label Propagation: Preventing Over-Propagation through Gradual Expansion
Venue: arXiv cs.SI 2015
Year: 2015

Identifying communities has always been a fundamental task in analysis of complex networks. Many methods have been devised over the last decade for detection of communities. Amongst them, the label propagation algorithm brings great scalability together with high accuracy. However, it has one major flaw; when the community structure in the network is not clear enough, it will assign every node the same label, thus detecting the whole graph as one giant community. We have addressed this issue by setting a capacity for communities, starting from a small value and gradually increasing it over time. Preliminary results show that not only our extension improves the detection capability of classic label propagation algorithm when communities are not clearly detectable, but also improves the overall quality of the identified clusters in complex networks with a clear community structure.
Identification of Image Operations Based on Steganalytic Features
Venue: arXiv cs.MM 2015
Year: 2015

Image forensics have attracted wide attention during the past decade. Though many forensic methods have been proposed to identify image forgeries, most of them are targeted ones, since their proposed features are highly dependent on the image operation under investigation. The performance of the well-designed features for detecting the targeted operation usually degrades significantly for other operations. On the other hand, a wise attacker can perform anti-forensics to fool the existing forensic methods, making countering anti-forensics become an urgent need. In this paper, we try to find a universal feature to detect various image processing and anti-forensic operations. Based on our extensive experiments and analysis, we find that any image processing/anti-forensic operations would inevitably modify many image pixels. This would change some inherent statistics within original images, which is similar to the case of steganography. Therefore, we model image processing/anti-forensic operations as steganography problems, and propose a detection strategy by applying steganalytic features. With some advanced steganalytic features, we are able to detect various image operations and further identify their types. In our experiments, we have tested several steganalytic features on 11 different kinds of typical image processing operations and 4 kinds of anti-forensic operations. The experimental results have shown that the proposed strategy significantly outperforms the existing forensic methods in both effectiveness and universality.
Self-organizing Networks of Information Gathering Cognitive Agents
Venue: arXiv cs.SI 2015
Year: 2015

In many scenarios, networks emerge endogenously as cognitive agents establish links in order to exchange information. Network formation has been widely studied in economics, but only on the basis of simplistic models that assume that the value of each additional piece of information is constant. In this paper we present a first model and associated analysis for network formation under the much more realistic assumption that the value of each additional piece of information depends on the type of that piece of information and on the information already possessed: information may be complementary or redundant. We model the formation of a network as a non-cooperative game in which the actions are the formation of links and the benefit of forming a link is the value of the information exchanged minus the cost of forming the link. We characterize the topologies of the networks emerging at a Nash equilibrium (NE) of this game and compare the efficiency of equilibrium networks with the efficiency of centrally designed networks. To quantify the impact of information redundancy and linking cost on social information loss, we provide estimates for the Price of Anarchy (PoA); to quantify the impact on individual information loss we introduce and provide estimates for a measure we call Maximum Information Loss (MIL). Finally, we consider the setting in which agents are not endowed with information, but must produce it. We show that the validity of the well-known "law of the few" depends on how information aggregates; in particular, the "law of the few" fails when information displays complementarities.
A Denotational Semantics for Communicating Unstructured Code
Venue: arXiv cs.PL 2015
Year: 2015

An important property of programming language semantics is that they should be compositional. However, unstructured low-level code contains goto-like commands making it hard to define a semantics that is compositional. In this paper, we follow the ideas of Saabas and Uustalu to structure low-level code. This gives us the possibility to define a compositional denotational semantics based on least fixed points to allow for the use of inductive verification methods. We capture the semantics of communication using finite traces similar to the denotations of CSP. In addition, we examine properties of this semantics and give an example that demonstrates reasoning about communication and jumps. With this semantics, we lay the foundations for a proof calculus that captures both, the semantics of unstructured low-level code and communication.
Using Model-Checking Techniques for Component-Based Systems with Reconfigurations
Venue: arXiv cs.SE 2015
Year: 2015

Within a component-based approach allowing dynamic reconfigurations, sequences of successive reconfiguration operations are expressed by means of reconfiguration paths, possibly infinite. We show that a subclass of such paths can be modelled by finite state automata. This feature allows us to use techniques related to model-checking to prove some architectural, event, and temporal properties related to dynamic reconfiguration. Our method is proved correct w.r.t. these properties' definition.
A Formal Approach based on Fuzzy Logic for the Specification of Component-Based Interactive Systems
Venue: arXiv cs.SE 2015
Year: 2015

Formal methods are widely recognized as a powerful engineering method for the specification, simulation, development, and verification of distributed interactive systems. However, most formal methods rely on a two-valued logic, and are therefore limited to the axioms of that logic: a specification is valid or invalid, component behavior is realizable or not, safety properties hold or are violated, systems are available or unavailable. Especially when the problem domain entails uncertainty, impreciseness, and vagueness, the appliance of such methods becomes a challenging task. In order to overcome the limitations resulting from the strict modus operandi of formal methods, the main objective of this work is to relax the boolean notion of formal specifications by using fuzzy logic. The present approach is based on Focus theory, a model-based and strictly formal method for componentbased interactive systems. The contribution of this work is twofold: i) we introduce a specification technique based on fuzzy logic which can be used on top of Focus to develop formal specifications in a qualitative fashion; ii) we partially extend Focus theory to a fuzzy one which allows the specification of fuzzy components and fuzzy interactions. While the former provides a methodology for approximating I/O behaviors under imprecision, the latter enables to capture a more quantitative view of specification properties such as realizability.
Algebraic Methods in the Congested Clique
Venue: arXiv cs.DC 2015
Year: 2015

In this work, we use algebraic methods for studying distance computation and subgraph detection tasks in the congested clique model. Specifically, we adapt parallel matrix multiplication implementations to the congested clique, obtaining an $O(n^{1-2/ω})$ round matrix multiplication algorithm, where $ω< 2.3728639$ is the exponent of matrix multiplication. In conjunction with known techniques from centralised algorithmics, this gives significant improvements over previous best upper bounds in the congested clique model. The highlight results include: -- triangle and 4-cycle counting in $O(n^{0.158})$ rounds, improving upon the $O(n^{1/3})$ triangle detection algorithm of Dolev et al. [DISC 2012], -- a $(1 + o(1))$-approximation of all-pairs shortest paths in $O(n^{0.158})$ rounds, improving upon the $\tilde{O} (n^{1/2})$-round $(2 + o(1))$-approximation algorithm of Nanongkai [STOC 2014], and -- computing the girth in $O(n^{0.158})$ rounds, which is the first non-trivial solution in this model. In addition, we present a novel constant-round combinatorial algorithm for detecting 4-cycles.
The Book Thickness of 1-Planar Graphs is Constant
Venue: arXiv cs.DS 2015
Year: 2015

In a book embedding, the vertices of a graph are placed on the spine of a book and the edges are assigned to pages, so that edges on the same page do not cross. In this paper, we prove that every $1$-planar graph (that is, a graph that can be drawn on the plane such that no edge is crossed more than once) admits an embedding in a book with constant number of pages. To the best of our knowledge, the best non-trivial previous upper-bound is $O(\sqrt{n})$, where $n$ is the number of vertices of the graph.
A Rice-like theorem for primitive recursive functions
Venue: arXiv cs.LO 2015
Year: 2015

We provide an explicit characterization of the properties of primitive recursive functions that are decidable or semi-decidable, given a primitive recursive index for the function. The result is much more general as it applies to any c.e. class of total computable functions. This is an analog of Rice and Rice-Shapiro theorem, for restricted classes of total computable functions.
3D Object Class Detection in the Wild
Venue: arXiv cs.CV 2015
Year: 2015

Object class detection has been a synonym for 2D bounding box localization for the longest time, fueled by the success of powerful statistical learning techniques, combined with robust image representations. Only recently, there has been a growing interest in revisiting the promise of computer vision from the early days: to precisely delineate the contents of a visual scene, object by object, in 3D. In this paper, we draw from recent advances in object detection and 2D-3D object lifting in order to design an object class detector that is particularly tailored towards 3D object class detection. Our 3D object class detection method consists of several stages gradually enriching the object detection output with object viewpoint, keypoints and 3D shape estimates. Following careful design, in each stage it constantly improves the performance and achieves state-ofthe-art performance in simultaneous 2D bounding box and viewpoint estimation on the challenging Pascal3D+ dataset.
Combining partially independent belief functions
Venue: arXiv cs.AI 2015
Year: 2015

The theory of belief functions manages uncertainty and also proposes a set of combination rules to aggregate opinions of several sources. Some combination rules mix evidential information where sources are independent; other rules are suited to combine evidential information held by dependent sources. In this paper we have two main contributions: First we suggest a method to quantify sources' degree of independence that may guide the choice of the more appropriate set of combination rules. Second, we propose a new combination rule that takes consideration of sources' degree of independence. The proposed method is illustrated on generated mass functions.
Energy Efficient Precoder Design for MIMO-OFDM with Rate-dependent Circuit Power
Venue: arXiv cs.IT 2015
Year: 2015

This paper studies an energy efficient design of precoders for point-to-point multiple-input-multiple-output (MIMO) orthogonal frequency-division multiplexing (OFDM) systems. Differently from traditional approaches, the optimal power allocation strategy is studied by modelling the circuit power as a rate-dependent function. We show that if the circuit power is a constant plus an increasing and convex function of the transmission rate, the problem of minimizing the consumed energy per bit received can be reformulated as a convex fractional program and solved by means of a bisection algorithm. The impact of the some system parameters is investigated either analytically or by means of computational results.
Constant Composition Distribution Matching
Venue: arXiv cs.IT 2015
Year: 2015

Distribution matching transforms independent and Bernoulli(1/2) distributed input bits into a sequence of output symbols with a desired distribution. Fixed-to-fixed length, invertible, and low complexity encoders and decoders based on constant composition and arithmetic coding are presented. Asymptotically in the blocklength, the encoder achieves the maximum rate, namely the entropy of the desired distribution. Furthermore, the normalized divergence of the encoder output and the desired distribution goes to zero in the blocklength.
Least Squares Estimation-Based Synchronous Generator Parameter Estimation Using PMU Data
Venue: arXiv cs.SY 2015
Year: 2015

In this paper, least square estimation (LSE)-based dynamic generator model parameter identification is investigated. Electromechanical dynamics related parameters such as inertia constant and primary frequency control droop for a synchronous generator are estimated using Phasor Measurement Unit (PMU) data obtained at the generator terminal bus. The key idea of applying LSE for dynamic parameter estimation is to have a discrete \underline{a}uto\underline{r}egression with e\underline{x}ogenous input (ARX) model. With an ARX model, a linear estimation problem can be formulated and the parameters of the ARX model can be found. This paper gives the detailed derivation of converting a generator model with primary frequency control into an ARX model. The generator parameters will be recovered from the estimated ARX model parameters afterwards. Two types of conversion methods are presented: zero-order hold (ZOH) method and Tustin method. Numerical results are presented to illustrate the proposed LSE application in dynamic system parameter identification using PMU data.
Exploiting Directionality for Millimeter-Wave Wireless System Improvement
Venue: arXiv cs.IT 2015
Year: 2015

This paper presents directional and omnidirectional RMS delay spread statistics obtained from 28 GHz and 73 GHz ultrawideband propagation measurements carried out in New York City using a 400 Megachips per second broadband sliding correlator channel sounder and highly directional steerable horn antennas. The 28 GHz measurements did not systematically seek the optimum antenna pointing angles and resulted in 33% outage for 39 T-R separation distances within 200 m. The 73 GHz measurements systematically found the best antenna pointing angles and resulted in 14.3% outage for 35 T-R separation distances within 200 m, all for mobile height receivers. Pointing the antennas to yield the strongest received power is shown to significantly reduce RMS delay spreads in line-of-sight (LOS) environments. A new term, distance extension exponent (DEE) is defined, and used to mathematically describe the increase in coverage distance that results by combining beams from angles with the strongest received power at a given location. These results suggest that employing directionality in millimeter-wave communications systems will reduce inter-symbol interference, improve link margin at cell edges, and enhance overall system performance.
Abrupt Change Detection in Power System Fault Analysis using Adaptive Whitening Filter and Wavelet Transform
Venue: arXiv cs.CE 2015
Year: 2015

This paper describes the application of the adaptive whitening filter and the wavelet transform used to detect the abrupt changes in the signals recorded during disturbances in the electrical power network in South Africa. Main focus has been to estimate exactly the time-instants of the changes in the signal model parameters during the pre-fault condition and following events like initiation of fault, circuit-breaker opening, auto-reclosure of the circuit-breakers. The key idea is to decompose the fault signals, de-noised using the adaptive whitening filter, into effective detailed and smoothed version using the multiresolution signal decomposition technique based on discrete wavelet transform. Then we apply the threshold method on the decomposed signals to estimate the change time-instants, segmenting the fault signals into the event-specific sections for further signal processing and analysis. This paper presents application on the recorded signals in the power transmission network of South Africa.
The AWGN BC with MAC Feedback: A Reduction to Noiseless Feedback via Interaction
Venue: arXiv cs.IT 2015
Year: 2015

We consider the problem of communication over a two-user Additive White Gaussian Noise Broadcast Channel (AWGN-BC) with an AWGN Multiple Access (MAC) active feedback. We describe a constructive reduction from this setup to the well-studied setup of linear-feedback coding over the AWGN-BC with noiseless feedback (and different parameters). This reduction facilitates the design of linear-feedback coding schemes in the (passive) noiseless feedback regime, which can then be easily and constructively transformed into coding schemes in the MAC feedback regime that attain the exact same rates. Our construction introduces an element of interaction into the coding protocol, and is based on modulo-lattice operations. As an example, we apply our method to the Ozarow-Leung scheme, and demonstrate how MAC feedback can be used to increase the capacity region of the AWGN-BC.
Can we track the geography of surnames based on bibliographic data?
Venue: arXiv cs.DL 2015
Year: 2015

In this paper we explore the possibility of using bibliographic databases for tracking the geographic origin of surnames. Surnames are used as a proxy to determine the ethnic, genetic or geographic origin of individuals in many fields such as Genetics or Demography; however they could also be used for bibliometric purposes such as the analysis of scientific migration flows. Here we present two relevant methodologies for determining the most probable country to which a surname could be assigned. The first methodology assigns surnames based on the most common country that can be assigned to a surname and the Kullback-Liebler divergence measure. The second method uses the Gini Index to evaluate the assignment of surnames to countries. We test both methodologies with control groups and conclude that, despite needing further analysis on its validity; these methodologies already show promising results.
Deception by Design: Evidence-Based Signaling Games for Network Defense
Venue: arXiv cs.CR 2015
Year: 2015

Deception plays a critical role in the financial industry, online markets, national defense, and countless other areas. Understanding and harnessing deception - especially in cyberspace - is both crucial and difficult. Recent work in this area has used game theory to study the roles of incentives and rational behavior. Building upon this work, we employ a game-theoretic model for the purpose of mechanism design. Specifically, we study a defensive use of deception: implementation of honeypots for network defense. How does the design problem change when an adversary develops the ability to detect honeypots? We analyze two models: cheap-talk games and an augmented version of those games that we call cheap-talk games with evidence, in which the receiver can detect deception with some probability. Our first contribution is this new model for deceptive interactions. We show that the model includes traditional signaling games and complete information games as special cases. We also demonstrate numerically that deception detection sometimes eliminate pure-strategy equilibria. Finally, we present the surprising result that the utility of a deceptive defender can sometimes increase when an adversary develops the ability to detect deception. These results apply concretely to network defense. They are also general enough for the large and critical body of strategic interactions that involve deception.
Shared latent subspace modelling within Gaussian-Binary Restricted Boltzmann Machines for NIST i-Vector Challenge 2014
Venue: arXiv cs.LG 2015
Year: 2015

This paper presents a novel approach to speaker subspace modelling based on Gaussian-Binary Restricted Boltzmann Machines (GRBM). The proposed model is based on the idea of shared factors as in the Probabilistic Linear Discriminant Analysis (PLDA). GRBM hidden layer is divided into speaker and channel factors, herein the speaker factor is shared over all vectors of the speaker. Then Maximum Likelihood Parameter Estimation (MLE) for proposed model is introduced. Various new scoring techniques for speaker verification using GRBM are proposed. The results for NIST i-vector Challenge 2014 dataset are presented.