OpenRaiser/Intern-Atlas huggingface dataset:
Achievable Rates and Outer Bound for the Half-Duplex MAC with Generalized Feedback
Venue: arXiv cs.IT 2011
Year: 2011

This paper provides comprehensive coding and outer bound for the half-duplex multiple access channel with generalized feedback (MAC-GF). Two users communicate with one destination over a discrete memoryless channel using time division. Each transmission block is divided into 3 time slots with variable durations: the destination is always in receive mode, while each user alternatively transmits and receives during the first 2 time slots, then both cooperate to send information during the last one. The paper proposes two decode-forward based coding schemes, analyzes their rate regions, and also derives two outer bounds with rate constraints similar to the achievable regions. Both schemes requires no block Makovity, allowing the destination to decode at the end of each block without any delay. In the first scheme, the codewords in the third time slot are superimposed on the codewords of the first two, whereas in the second scheme, these codewords are independent. While the second scheme is simpler, the first scheme helps emphasize the importance of joint decoding over separate decoding among multiple time slots at the destination. For the Gaussian channel, the two schemes with joint decoding are equivalent, as are the two outer bounds. For physically degraded Gaussian channels, the proposed schemes achieve the capacity. Extension to the m-user half-duplex MAC-GF are provided. Numerical results for the Gaussian channel shows significant rate region improvement over the classical MAC and that the outer bound becomes increasingly tight as the inter-user link quality increases
On the Throughput-Delay Trade-off in Georouting Networks
Venue: arXiv cs.IT 2011
Year: 2011

We study the scaling properties of a georouting scheme in a wireless multi-hop network of $n$ mobile nodes. Our aim is to increase the network capacity quasi linearly with $n$ while keeping the average delay bounded. In our model, mobile nodes move according to an i.i.d. random walk with velocity $v$ and transmit packets to randomly chosen destinations. The average packet delivery delay of our scheme is of order $1/v$ and it achieves the network capacity of order $\frac{n}{\log n\log\log n}$. This shows a practical throughput-delay trade-off, in particular when compared with the seminal result of Gupta and Kumar which shows network capacity of order $\sqrt{n/\log n}$ and negligible delay and the groundbreaking result of Grossglausser and Tse which achieves network capacity of order $n$ but with an average delay of order $\sqrt{n}/v$. We confirm the generality of our analytical results using simulations under various interference models.
Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving
Venue: arXiv cs.AI 2011
Year: 2011

OWL 2 has been standardized by the World Wide Web Consortium (W3C) as a family of ontology languages for the Semantic Web. The most expressive of these languages is OWL 2 Full, but to date no reasoner has been implemented for this language. Consistency and entailment checking are known to be undecidable for OWL 2 Full. We have translated a large fragment of the OWL 2 Full semantics into first-order logic, and used automated theorem proving systems to do reasoning based on this theory. The results are promising, and indicate that this approach can be applied in practice for effective OWL reasoning, beyond the capabilities of current Semantic Web reasoners. This is an extended version of a paper with the same title that has been published at CADE 2011, LNAI 6803, pp. 446-460. The extended version provides appendices with additional resources that were used in the reported evaluation.
Optimization of Lyapunov Invariants in Verification of Software Systems
Venue: arXiv cs.SY 2011
Year: 2011

The paper proposes a control-theoretic framework for verification of numerical software systems, and puts forward software verification as an important application of control and systems theory. The idea is to transfer Lyapunov functions and the associated computational techniques from control systems analysis and convex optimization to verification of various software safety and performance specifications. These include but are not limited to absence of overflow, absence of division-by-zero, termination in finite time, presence of dead-code, and certain user-specified assertions. Central to this framework are Lyapunov invariants. These are properly constructed functions of the program variables, and satisfy certain properties-resembling those of Lyapunov functions-along the execution trace. The search for the invariants can be formulated as a convex optimization problem. If the associated optimization problem is feasible, the result is a certificate for the specification.
Optimal Utilization of a Cognitive Shared Channel with a Rechargeable Primary Source Node
Venue: arXiv cs.IT 2011
Year: 2011

This paper considers the scenario in which a set of nodes share a common channel. Some nodes have a rechargeable battery and the others are plugged to a reliable power supply and, thus, have no energy limitations. We consider two source-destination pairs and apply the concept of cognitive radio communication in sharing the common channel. Specifically, we give high-priority to the energy-constrained source-destination pair, i.e., primary pair, and low-priority to the pair which is free from such constraint, i.e., secondary pair. In contrast to the traditional notion of cognitive radio, in which the secondary transmitter is required to relinquish the channel as soon as the primary is detected, the secondary transmitter not only utilizes the idle slots of primary pair but also transmits along with the primary transmitter with probability $p$. This is possible because we consider the general multi-packet reception model. Given the requirement on the primary pair's throughput, the probability $p$ is chosen to maximize the secondary pair's throughput. To this end, we obtain two-dimensional maximum stable throughput region which describes the theoretical limit on rates that we can push into the network while maintaining the queues in the network to be stable. The result is obtained for both cases in which the capacity of the battery at the primary node is infinite and also finite.
Predicting global usages of resources endowed with local policies
Venue: arXiv cs.DC 2011
Year: 2011

The effective usages of computational resources are a primary concern of up-to-date distributed applications. In this paper, we present a methodology to reason about resource usages (acquisition, release, revision, ...), and therefore the proposed approach enables to predict bad usages of resources. Keeping in mind the interplay between local and global information occurring in the application-resource interactions, we model resources as entities with local policies and global properties governing the overall interactions. Formally, our model takes the shape of an extension of pi-calculus with primitives to manage resources. We develop a Control Flow Analysis computing a static approximation of process behaviour and therefore of the resource usages.
Decoupled execution of synchronous coordination models via behavioural automata
Venue: arXiv cs.FL 2011
Year: 2011

Synchronous coordination systems allow the exchange of data by logically indivisible actions involving all coordinated entities. This paper introduces behavioural automata, a logically synchronous coordination model based on the Reo coordination language, which focuses on relevant aspects for the concurrent evolution of these systems. We show how our automata model encodes the Reo and Linda coordination models and how it introduces an explicit predicate that captures the concurrent evolution, distinguishing local from global actions, and lifting the need of most synchronous models to involve all entities at each coordination step, paving the way to more scalable implementations.
On Detecting Pollution Attacks in Inter-Session Network Coding
Venue: arXiv cs.NI 2011
Year: 2011

Dealing with pollution attacks in inter-session network coding is challenging due to the fact that sources, in addition to intermediate nodes, can be malicious. In this work, we precisely define corrupted packets in inter-session pollution based on the commitment of the source packets. We then propose three detection schemes: one hash-based and two MAC-based schemes: InterMacCPK and SpaceMacPM. InterMacCPK is the first multi-source homomorphic MAC scheme that supports multiple keys. Both MAC schemes can replace traditional MACs, e.g., HMAC, in networks that employ inter-session coding. All three schemes provide in-network detection, are collusion-resistant, and have very low online bandwidth and computation overhead.
Diffusive Logistic Model Towards Predicting Information Diffusion in Online Social Networks
Venue: arXiv cs.SI 2011
Year: 2011

Online social networks have recently become an effective and innovative channel for spreading information and influence among hundreds of millions of end users. Many prior work have carried out empirical studies and proposed diffusion models to understand the information diffusion process in online social networks. However, most of these studies focus on the information diffusion in temporal dimension, that is, how the information propagates over time. Little attempt has been given on understanding information diffusion over both temporal and spatial dimensions. In this paper, we propose a Partial Differential Equation (PDE), specifically, a Diffusive Logistic (DL) equation to model the temporal and spatial characteristics of information diffusion in online social networks. To be more specific, we develop a PDE-based theoretical framework to measure and predict the density of influenced users at a given distance from the original information source after a time period. The density of influenced users over time and distance provides valuable insight on the actual information diffusion process. We present the temporal and spatial patterns in a real dataset collected from Digg social news site, and validate the proposed DL equation in terms of predicting the information diffusion process. Our experiment results show that the DL model is indeed able to characterize and predict the process of information propagation in online social networks. For example, for the most popular news with 24,099 votes in Digg, the average prediction accuracy of DL model over all distances during the first 6 hours is 92.08%. To the best of our knowledge, this paper is the first attempt to use PDE-based model to study the information diffusion process in both temporal and spatial dimensions in online social networks.
Innocent strategies as presheaves and interactive equivalences for CCS
Venue: arXiv cs.LO 2011
Year: 2011

Seeking a general framework for reasoning about and comparing programming languages, we derive a new view of Milner's CCS. We construct a category E of plays, and a subcategory V of views. We argue that presheaves on V adequately represent innocent strategies, in the sense of game semantics. We then equip innocent strategies with a simple notion of interaction. This results in an interpretation of CCS. Based on this, we propose a notion of interactive equivalence for innocent strategies, which is close in spirit to Beffara's interpretation of testing equivalences in concurrency theory. In this framework we prove that the analogues of fair and must testing equivalences coincide, while they differ in the standard setting.
Interaction and observation, categorically
Venue: arXiv cs.PL 2011
Year: 2011

This paper proposes to use dialgebras to specify the semantics of interactive systems in a natural way. Dialgebras are a conservative extension of coalgebras. In this categorical model, from the point of view that we provide, the notions of observation and interaction are separate features. This is useful, for example, in the specification of process equivalences, which are obtained as kernels of the homomorphisms of dialgebras. As an example we present the asynchronous semantics of the CCS.
Correlating Formal Semantic Models of Reo Connectors: Connector Coloring and Constraint Automata
Venue: arXiv cs.PL 2011
Year: 2011

Over the past decades, coordination languages have emerged for the specification and implementation of interaction protocols for communicating software components. This class of languages includes Reo, a platform for compositional construction of connectors. In recent years, various formalisms for describing the behavior of Reo connectors have come to existence, each of them serving its own purpose. Naturally, questions about how these models relate to each other arise. From a theoretical point of view, answers to these questions provide us with better insight into the fundamentals of Reo, while from a more practical perspective, these answers broaden the applicability of Reo's development tools. In this paper, we address one of these questions: we investigate the equivalence between coloring models and constraint automata, the two most dominant and practically relevant semantic models of Reo. More specifically, we define operators that transform one model to the other (and vice versa), prove their correctness, and show that they distribute over composition. To ensure that the transformation operators map one-to-one (instead of many-to-one), we extend coloring models with data constraints. Though primarily a theoretical contribution, we sketch some potential applications of our results: the broadening of the applicability of existing tools for connector verification and animation.
Proposal for improvement in the transfer and execution of multiple instances of a virtual image
Venue: arXiv cs.DC 2011
Year: 2011

Virtualization technology allows currently any application run any application complex and expensive computational (the scientific applications are a good example) on heterogeneous distributed systems, which make regular use of Grid and Cloud technologies, enabling significant savings in computing time. This model is particularly interesting for the mass execution of scientific simulations and calculations, allowing parallel execution of applications using the same execution environment (unchanged) used by the scientist as usual. However, the use and distribution of large virtual images can be a problem (up to tens of GBytes), which is aggravated when attempting a mass mailing on a large number of distributed computers. This work has as main objective to present an analysis of how implementation and a proposal for the improvement (reduction in size) of the virtual images pretending reduce distribution time in distributed systems. This analysis is done very specific requirements that need an operating system (guest OS) on some aspects of its execution.
Evader Interdiction and Collateral Damage
Venue: arXiv cs.SI 2011
Year: 2011

In network interdiction problems, evaders (e.g., hostile agents or data packets) may be moving through a network towards targets and we wish to choose locations for sensors in order to intercept the evaders before they reach their destinations. The evaders might follow deterministic routes or Markov chains, or they may be reactive}, i.e., able to change their routes in order to avoid sensors placed to detect them. The challenge in such problems is to choose sensor locations economically, balancing security gains with costs, including the inconvenience sensors inflict upon innocent travelers. We study the objectives of 1) maximizing the number of evaders captured when limited by a budget on sensing cost and 2) capturing all evaders as cheaply as possible. We give optimal sensor placement algorithms for several classes of special graphs and hardness and approximation results for general graphs, including for deterministic or Markov chain-based and reactive or oblivious evaders. In a similar-sounding but fundamentally different problem setting posed by Rubinstein and Glazer where both evaders and innocent travelers are reactive, we again give optimal algorithms for special cases and hardness and approximation results on general graphs.
On the performance of high-order finite elements with respect to maximum principles and the non-negative constraint for diffusion-type equations
Venue: arXiv cs.NA 2011
Year: 2011

The main aim of this paper is to document the performance of $p$-refinement with respect to maximum principles and the non-negative constraint. The model problem is (steady-state) anisotropic diffusion with decay (which is a second-order elliptic partial differential equation). We considered the standard single-field formulation (which is based on the Galerkin formalism) and two least-squares-based mixed formulations. We have employed non-uniform Lagrange polynomials for altering the polynomial order in each element, and we have used $p = 1, ..., 10$. It will be shown that the violation of the non-negative constraint will not vanish with $p$-refinement for anisotropic diffusion. We shall illustrate the performance of $p$-refinement using several representative problems. The intended outcome of the paper is twofold. Firstly, this study will caution the users of high-order approximations about its performance with respect to maximum principles and the non-negative constraint. Secondly, this study will help researchers to develop new methodologies for enforcing maximum principles and the non-negative constraint under high-order approximations.
Network Localization on Unit Disk Graphs
Venue: arXiv cs.DC 2011
Year: 2011

We study the problem of cooperative localization of a large network of nodes in integer-coordinated unit disk graphs, a simplified but useful version of general random graph. Exploiting the property that the radius $r$ sets clear cut on the connectivity of two nodes, we propose an essential philosophy that "no connectivity is also useful information just like the information being connected" in unit disk graphs. Exercising this philosophy, we show that the conventional network localization problem can be re-formulated to significantly reduce the search space, and that global rigidity, a necessary and sufficient condition for the existence of unique solution in general graphs, is no longer necessary. While the problem is still NP-hard, we show that a (depth-first) tree-search algorithm with memory O(N) ($N$ is the network size) can be developed, and for practical setups, the search complexity and speed is very manageable, and is magnitudes less than the conventional problem, especially when the graph is sparse or when only very limited anchor nodes are available.
Onset of coherent attitude layers in a population of sports fans
Venue: arXiv cs.SI 2011
Year: 2011

The aim of this paper was to empirically investigate the behavior of fans, globally coupled to a common environmental source of information. The environmental stimuli were given in a form of referee's decisions list. The sample of fans had to respond on each stimulus by associating points signifying his/her own opinion, emotion and action that referee's decisions provoke. Data were fitted by the Brillouin function which was a solution of an adapted model of quantum statistical physics to social phenomena. Correlation and a principal component analysis were performed in order to detect any collective behavior of the social ensemble of fans. Results showed that fans behaved as a system subject to a phase transition where the neutral state in the opinion, emotional and action space has been destabilized and a new stable state of coherent attitudes was formed. The enhancement of fluctuations and the increase of social susceptibility (responsiveness) to referee's decisions were connected to the first few decisions. The subsequent reduction of values in these parameters signified the onset of coherent layering within the attitude space of the social ensemble of fans. In the space of opinions fan coherence was maximal as only one layer of coherence emerged. In the emotional and action spaces the number of coherent levels was 2 and 4 respectively. The principal component analysis revealed a strong collective behavior and a high degree of integration within and between the opinion, emotional and action spaces of the sample of fans. These results point to one possible way of how different proto-groups, violent and moderate, may be formed as a consequence of global coupling to a common source of information.
Stateful Testing: Finding More Errors in Code and Contracts
Venue: arXiv cs.SE 2011
Year: 2011

Automated random testing has shown to be an effective approach to finding faults but still faces a major unsolved issue: how to generate test inputs diverse enough to find many faults and find them quickly. Stateful testing, the automated testing technique introduced in this article, generates new test cases that improve an existing test suite. The generated test cases are designed to violate the dynamically inferred contracts (invariants) characterizing the existing test suite. As a consequence, they are in a good position to detect new errors, and also to improve the accuracy of the inferred contracts by discovering those that are unsound. Experiments on 13 data structure classes totalling over 28,000 lines of code demonstrate the effectiveness of stateful testing in improving over the results of long sessions of random testing: stateful testing found 68.4% new errors and improved the accuracy of automatically inferred contracts to over 99%, with just a 7% time overhead.
Analysis, Dimensioning and Robust Control of Shunt Active Filter for Harmonic Currents Compensation in Electrical Mains
Venue: arXiv cs.SY 2011
Year: 2011

In this chapter some results related to Shunt Active Filters (SAFs) and obtained by the authors and some coauthors are reported. SAFs are complex power electronics equipments adopted to compensate for cur-rent harmonic pollution in electric mains, due to nonlinear loads. By using a proper "floating" capacitor as energy reservoir, the SAF purpose is to inject in the line grid currents canceling the polluting har-monics. Control algorithms play a key role for such devices and, in general, in many power electronics applications. Moreover, systems theory is crucial, since it is the mathematical tool that enables a deep understanding of the involved dynamics of such systems, allowing a correct dimensioning, beside an effective control. As a matter of facts, current injection objective can be straightforwardly formulated as an output tracking control problem. In this fashion, the structural and insidious marginally-stable internal/zero dynamics of SAFs can be immediately highlighted and characterized in terms of sizing and control issues. For what concerns the control design strictly, time-scale separation among output and internal dynamics can be effectively exploited to split the control design in different stages that can be later aggregated, by using singular perturbation analysis. In addition, for robust asymptotic output tracking the Internal Model Principle is adopted.
Leveraging Billions of Faces to Overcome Performance Barriers in Unconstrained Face Recognition
Venue: arXiv cs.CV 2011
Year: 2011

We employ the face recognition technology developed in house at face.com to a well accepted benchmark and show that without any tuning we are able to considerably surpass state of the art results. Much of the improvement is concentrated in the high-valued performance point of zero false positive matches, where the obtained recall rate almost doubles the best reported result to date. We discuss the various components and innovations of our system that enable this significant performance gap. These components include extensive utilization of an accurate 3D reconstructed shape model dealing with challenges arising from pose and illumination. In addition, discriminative models based on billions of faces are used in order to overcome aging and facial expression as well as low light and overexposure. Finally, we identify a challenging set of identification queries that might provide useful focus for future research.