OpenRaiser/Intern-Atlas huggingface dataset:
Simulation technique for available bandwidth estimation
Venue: arXiv cs.NI 2010
Year: 2010

The paper proposes a method for measuring available bandwidth, based on testing network packets of various sizes (Variable Packet Size method, VPS). The boundaries of applicability of the model have been found, which are based on the accuracy of measurements of packet delays, also we have derived a formula of measuring the upper limit of bandwidth. The computer simulation has been performed and relationship between the measurement error of available bandwidth and the number of measurements has been found. Experimental verification with the use of RIPE Test Box measuring system has shown that the suggested method has advantages over existing measurement techniques. Pathload utility has been chosen as an alternative technique of measurement, and to ensure reliable results statistics by SNMP agent has been withdrawn directly from the router.
Searching in Dynamic Catalogs on a Tree
Venue: arXiv cs.DS 2010
Year: 2010

In this paper we consider the following modification of the iterative search problem. We are given a tree $T$, so that a dynamic catalog $C(v)$ is associated with every tree node $v$. For any $x$ and for any node-to-root path $π$ in $T$, we must find the predecessor of $x$ in $\cup_{v\in π} C(v)$. We present a linear space dynamic data structure that supports such queries in $O(t(n)+|π|)$ time, where $t(n)$ is the time needed to search in one catalog and $|π|$ denotes the number of nodes on path $π$. We also consider the reporting variant of this problem, in which for any $x_1$, $x_2$ and for any path $π'$ all elements of $\cup_{v\in π'} (C(v)\cap [x_1,x_2])$ must be reported; here $π'$ denotes a path between an arbitrary node $v_0$ and its ancestor $v_1$. We show that such queries can be answered in $O(t(n)+|π'|+ k)$ time, where $k$ is the number of elements in the answer. To illustrate applications of our technique, we describe the first dynamic data structures for the stabbing-max problem, the horizontal point location problem, and the orthogonal line-segment intersection problem with optimal $O(\log n/\log \log n)$ query time and poly-logarithmic update time.
Manifold Elastic Net: A Unified Framework for Sparse Dimension Reduction
Venue: arXiv cs.LG 2010
Year: 2010

It is difficult to find the optimal sparse solution of a manifold learning based dimensionality reduction algorithm. The lasso or the elastic net penalized manifold learning based dimensionality reduction is not directly a lasso penalized least square problem and thus the least angle regression (LARS) (Efron et al. \cite{LARS}), one of the most popular algorithms in sparse learning, cannot be applied. Therefore, most current approaches take indirect ways or have strict settings, which can be inconvenient for applications. In this paper, we proposed the manifold elastic net or MEN for short. MEN incorporates the merits of both the manifold learning based dimensionality reduction and the sparse learning based dimensionality reduction. By using a series of equivalent transformations, we show MEN is equivalent to the lasso penalized least square problem and thus LARS is adopted to obtain the optimal sparse solution of MEN. In particular, MEN has the following advantages for subsequent classification: 1) the local geometry of samples is well preserved for low dimensional data representation, 2) both the margin maximization and the classification error minimization are considered for sparse projection calculation, 3) the projection matrix of MEN improves the parsimony in computation, 4) the elastic net penalty reduces the over-fitting problem, and 5) the projection matrix of MEN can be interpreted psychologically and physiologically. Experimental evidence on face recognition over various popular datasets suggests that MEN is superior to top level dimensionality reduction algorithms.
On the Cooperation of Independent Registries
Venue: arXiv cs.SE 2010
Year: 2010

Registries play a key role in service-oriented applications. Originally, they were neutral players between service providers and clients. The UDDI Business Registry (UBR) was meant to foster these concepts and provide a common reference for companies interested in Web services. The more Web services were used, the more companies started create their own local registries: more efficient discovery processes, better control over the quality of published information, and also more sophisticated publication policies motivated the creation of private repositories. The number and heterogeneity of the different registries - besides the decision to close the UBR are pushing for new and sophisticated means to make different registries cooperate. This paper proposes DIRE (DIstributed REgistry), a novel approach based on a publish and subscribe (P/S) infrastructure to federate different heterogeneous registries and make them exchange information about published services. The paper discusses the main motivations for the P/S-based infrastructure, proposes an integrated service model, introduces the main components of the framework, and exemplifies them on a simple case study.
Formal Verification of Self-Assembling Systems
Venue: arXiv cs.LO 2010
Year: 2010

This paper introduces the theory and practice of formal verification of self-assembling systems. We interpret a well-studied abstraction of nanomolecular self assembly, the Abstract Tile Assembly Model (aTAM), into Computation Tree Logic (CTL), a temporal logic often used in model checking. We then consider the class of "rectilinear" tile assembly systems. This class includes most aTAM systems studied in the theoretical literature, and all (algorithmic) DNA tile self-assembling systems that have been realized in laboratories to date. We present a polynomial-time algorithm that, given a tile assembly system T as input, either provides a counterexample to T's rectilinearity or verifies whether T has a unique terminal assembly. Using partial order reductions, the verification search space for this algorithm is reduced from exponential size to O(n^2), where n x n is the size of the assembly surface. That reduction is asymptotically the best possible. We report on experimental results obtained by translating tile assembly simulator files into a Petri net format manipulable by the SMART model checking engines devised by Ciardo et al. The model checker runs in O(|T| x n^4) time, where |T| is the number of tile types in tile assembly system T, and n x n is the surface size. Atypical for a model checking problem -- in which the practical limit usually is insufficient memory to store the state space -- the limit in this case was the amount of memory required to represent the rules of the model. (Storage of the state space and of the reachability graph were small by comparison.) We discuss how to overcome this obstacle by means of a front end tailored to the characteristics of self-assembly.
Video Event Recognition for Surveillance Applications (VERSA)
Venue: arXiv cs.CV 2010
Year: 2010

VERSA provides a general-purpose framework for defining and recognizing events in live or recorded surveillance video streams. The approach for event recognition in VERSA is using a declarative logic language to define the spatial and temporal relationships that characterize a given event or activity. Doing so requires the definition of certain fundamental spatial and temporal relationships and a high-level syntax for specifying frame templates and query parameters. Although the handling of uncertainty in the current VERSA implementation is simplistic, the language and architecture is amenable to extending using Fuzzy Logic or similar approaches. VERSA's high-level architecture is designed to work in XML-based, services- oriented environments. VERSA can be thought of as subscribing to the XML annotations streamed by a lower-level video analytics service that provides basic entity detection, labeling, and tracking. One or many VERSA Event Monitors could thus analyze video streams and provide alerts when certain events are detected.
Characterization of Graph-cover Pseudocodewords of Codes over $F_3$
Venue: arXiv cs.IT 2010
Year: 2010

Linear-programming pseudocodewords play a pivotal role in our understanding of the linear-programming decoding algorithms. These pseudocodewords are known to be equivalent to the graph-cover pseudocodewords. The latter pseudocodewords, when viewed as points in the multidimensional Euclidean space, lie inside a fundamental cone. This fundamental cone depends on the choice of a parity-check matrix of a code, rather than on the choice of the code itself. The cone does not depend on the channel, over which the code is employed. The knowledge of the boundaries of the fundamental cone could help in studying various properties of the pseudocodewords, such as their minimum pseudoweight, pseudoredundancy of the codes, etc. For the binary codes, the full characterization of the fundamental cone was derived by Koetter et al. However, if the underlying alphabet is large, such characterization becom is more involved. In this work, a characterization of the fundamental cone for codes over $F_3$ is discussed.
Applying Prolog to Develop Distributed Systems
Venue: arXiv cs.PL 2010
Year: 2010

Development of distributed systems is a difficult task. Declarative programming techniques hold a promising potential for effectively supporting programmer in this challenge. While Datalog-based languages have been actively explored for programming distributed systems, Prolog received relatively little attention in this application area so far. In this paper we present a Prolog-based programming system, called DAHL, for the declarative development of distributed systems. DAHL extends Prolog with an event-driven control mechanism and built-in networking procedures. Our experimental evaluation using a distributed hash-table data structure, a protocol for achieving Byzantine fault tolerance, and a distributed software model checker - all implemented in DAHL - indicates the viability of the approach.
A state of a dynamic computational structure distributed in an environment: a model and its corollaries
Venue: arXiv cs.FL 2010
Year: 2010

Currently there is great interest in computational models consisting of underlying regular computational environments, and built on them distributed computational structures. Examples of such models are cellular automata, spatial computation and space-time crystallography. For any computational model it is natural to define a functional equivalence of different but related computational structures. In the finite automata theory an example of such equivalence is automata homomorphism and, in particular, automata isomorphism. If we continue to stick to the finite automata theory, a fundamental question arise, what a state of a distributed computational structure is. This work is devoted to particular solution of the issue.
Continuum Percolation in the Intrinsically Secure Communications Graph
Venue: arXiv cs.IT 2010
Year: 2010

The intrinsically secure communications graph (iS-graph) is a random graph which captures the connections that can be securely established over a large-scale network, in the presence of eavesdroppers. It is based on principles of information-theoretic security, widely accepted as the strictest notion of security. In this paper, we are interested in characterizing the global properties of the iS-graph in terms of percolation on the infinite plane. We prove the existence of a phase transition in the Poisson iS-graph, whereby an unbounded component of securely connected nodes suddenly arises as we increase the density of legitimate nodes. Our work shows that long-range communication in a wireless network is still possible when a secrecy constraint is present.
A Translational Approach to Constraint Answer Set Solving
Venue: arXiv cs.LO 2010
Year: 2010

We present a new approach to enhancing Answer Set Programming (ASP) with Constraint Processing techniques which allows for solving interesting Constraint Satisfaction Problems in ASP. We show how constraints on finite domains can be decomposed into logic programs such that unit-propagation achieves arc, bound or range consistency. Experiments with our encodings demonstrate their computational impact.
Initial Algebra Semantics for Cyclic Sharing Tree Structures
Venue: arXiv cs.LO 2010
Year: 2010

Terms are a concise representation of tree structures. Since they can be naturally defined by an inductive type, they offer data structures in functional programming and mechanised reasoning with useful principles such as structural induction and structural recursion. However, for graphs or "tree-like" structures - trees involving cycles and sharing - it remains unclear what kind of inductive structures exists and how we can faithfully assign a term representation of them. In this paper we propose a simple term syntax for cyclic sharing structures that admits structural induction and recursion principles. We show that the obtained syntax is directly usable in the functional language Haskell and the proof assistant Agda, as well as ordinary data structures such as lists and trees. To achieve this goal, we use a categorical approach to initial algebra semantics in a presheaf category. That approach follows the line of Fiore, Plotkin and Turi's models of abstract syntax with variable binding.
Embedding Spatial Software Visualization in the IDE: an Exploratory Study
Venue: arXiv cs.SE 2010
Year: 2010

Software visualization can be of great use for understanding and exploring a software system in an intuitive manner. Spatial representation of software is a promising approach of increasing interest. However, little is known about how developers interact with spatial visualizations that are embedded in the IDE. In this paper, we present a pilot study that explores the use of Software Cartography for program comprehension of an unknown system. We investigated whether developers establish a spatial memory of the system, whether clustering by topic offers a sound base layout, and how developers interact with maps. We report our results in the form of observations, hypotheses, and implications. Key findings are a) that developers made good use of the map to inspect search results and call graphs, and b) that developers found the base layout surprising and often confusing. We conclude with concrete advice for the design of embedded software maps.
Decidability properties for fragments of CHR
Venue: arXiv cs.LO 2010
Year: 2010

We study the decidability of termination for two CHR dialects which, similarly to the Datalog like languages, are defined by using a signature which does not allow function symbols (of arity >0). Both languages allow the use of the = built-in in the body of rules, thus are built on a host language that supports unification. However each imposes one further restriction. The first CHR dialect allows only range-restricted rules, that is, it does not allow the use of variables in the body or in the guard of a rule if they do not appear in the head. We show that the existence of an infinite computation is decidable for this dialect. The second dialect instead limits the number of atoms in the head of rules to one. We prove that in this case, the existence of a terminating computation is decidable. These results show that both dialects are strictly less expressive than Turing Machines. It is worth noting that the language (without function symbols) without these restrictions is as expressive as Turing Machines.
Broadcast Approach and Oblivious Cooperative Strategies for the Wireless Relay Channel - Part I: Sequential Decode-and-Forward (SDF)
Venue: arXiv cs.IT 2010
Year: 2010

In this two part paper we consider a wireless network in which a source terminal communicates with a destination and a relay terminal is occasionally present in close proximity to the source without source's knowledge, suggesting oblivious protocols. The source-relay channel is assumed to be a fixed gain AWGN due to the proximity while the source-destination and the relay-destination channels are subject to a block flat Rayleigh fading. A perfect CSI at the respective receivers only is assumed. With the average throughput as a performance measure, we incorporate a two-layer broadcast approach into two cooperative strategies based on the decode-and-forward scheme - Sequential Decoded-and Forward (SDF) in part I and the Block-Markov (BM) in part II. The broadcast approach splits the transmitted rate into superimposed layers corresponding to a "bad" and a "good" channel states, allowing better adaptation to the actual channel conditions In part I, the achievable rate expressions for the SDF strategy are derived under the broadcast approach for multiple settings including single user, MISO and the general relay setting using successive decoding technique, both numerically and analytically. Continuous broadcasting lower bounds are derived for the MISO and an oblivious cooperation scenarios.
Concavity of Mutual Information Rate for Input-Restricted Finite-State Memoryless Channels at High SNR
Venue: arXiv cs.IT 2010
Year: 2010

We consider a finite-state memoryless channel with i.i.d. channel state and the input Markov process supported on a mixing finite-type constraint. We discuss the asymptotic behavior of entropy rate of the output hidden Markov chain and deduce that the mutual information rate of such a channel is concave with respect to the parameters of the input Markov processes at high signal-to-noise ratio. In principle, the concavity result enables good numerical approximation of the maximum mutual information rate and capacity of such a channel.
Propositional Dynamic Logic for Message-Passing Systems
Venue: arXiv cs.LO 2010
Year: 2010

We examine a bidirectional propositional dynamic logic (PDL) for finite and infinite message sequence charts (MSCs) extending LTL and TLC-. By this kind of multi-modal logic we can express properties both in the entire future and in the past of an event. Path expressions strengthen the classical until operator of temporal logic. For every formula defining an MSC language, we construct a communicating finite-state machine (CFM) accepting the same language. The CFM obtained has size exponential in the size of the formula. This synthesis problem is solved in full generality, i.e., also for MSCs with unbounded channels. The model checking problem for CFMs and HMSCs turns out to be in PSPACE for existentially bounded MSCs. Finally, we show that, for PDL with intersection, the semantics of a formula cannot be captured by a CFM anymore.
Short Note on Complexity of Multi-Value Byzantine Agreement
Venue: arXiv cs.DC 2010
Year: 2010

Randomized algorithm that achieves multi-valued Byzantine agreement with high probability, and achieves optimal complexity.
PowerTracer: Tracing requests in multi-tier services to save cluster power consumption
Venue: arXiv cs.DC 2010
Year: 2010

As energy proportional computing gradually extends the success of DVFS (Dynamic voltage and frequency scaling) to the entire system, DVFS control algorithms will play a key role in reducing server clusters' power consumption. The focus of this paper is to provide accurate cluster-level DVFS control for power saving in a server cluster. To achieve this goal, we propose a request tracing approach that online classifies the major causal path patterns of a multi-tier service and monitors their performance data as a guide for accurate DVFS control. The request tracing approach significantly decreases the time cost of performance profiling experiments that aim to establish the empirical performance model. Moreover, it decreases the controller complexity so that we can introduce a much simpler feedback controller, which only relies on the single-node DVFS modulation at a time as opposed to varying multiple CPU frequencies simultaneously. Based on the request tracing approach, we present a hybrid DVFS control system that combines an empirical performance model for fast modulation at different load levels and a simpler feedback controller for adaption. We implement a prototype of the proposed system, called PowerTracer, and conduct extensive experiments on a 3-tier platform. Our experimental results show that PowerTracer outperforms its peer in terms of power saving and system performance.
Self-Recovering Sensor-Actor Networks
Venue: arXiv cs.DC 2010
Year: 2010

Wireless sensor-actor networks are a recent development of wireless networks where both ordinary sensor nodes and more sophisticated and powerful nodes, called actors, are present. In this paper we formalize a recently introduced algorithm that recovers failed actor communication links via the existing sensor infrastructure. We prove via refinement that the recovery is terminating in a finite number of steps and is distributed, thus self-performed by the actors. Most importantly, we prove that the recovery can be done at different levels, via different types of links, such as direct actor links or indirect links between the actors, in the latter case reusing the wireless infrastructure of sensors. This leads to identifying coordination classes, e.g., for delegating the most security sensitive coordination to the direct actor-actor coordination links, the least real-time constrained coordination to indirect links, and the safety critical coordination to both direct actor links and indirect sensor paths between actors. Our formalization is done using the theorem prover in the RODIN platform.
Towards Performance Measurement And Metrics Based Analysis of PLA Applications
Venue: arXiv cs.SE 2010
Year: 2010

This article is about a measurement analysis based approach to help software practitioners in managing the additional level complexities and variabilities in software product line applications. The architecture of the proposed approach i.e. ZAC is designed and implemented to perform preprocessesed source code analysis, calculate traditional and product line metrics and visualize results in two and three dimensional diagrams. Experiments using real time data sets are performed which concluded with the results that the ZAC can be very helpful for the software practitioners in understanding the overall structure and complexity of product line applications. Moreover the obtained results prove strong positive correlation between calculated traditional and product line measures.
Test Case Generation for Object-Oriented Imperative Languages in CLP
Venue: arXiv cs.PL 2010
Year: 2010

Testing is a vital part of the software development process. Test Case Generation (TCG) is the process of automatically generating a collection of test cases which are applied to a system under test. White-box TCG is usually performed by means of symbolic execution, i.e., instead of executing the program on normal values (e.g., numbers), the program is executed on symbolic values representing arbitrary values. When dealing with an object-oriented (OO) imperative language, symbolic execution becomes challenging as, among other things, it must be able to backtrack, complex heap-allocated data structures should be created during the TCG process and features like inheritance, virtual invocations and exceptions have to be taken into account. Due to its inherent symbolic execution mechanism, we pursue in this paper that Constraint Logic Programming (CLP) has a promising unexploited application field in TCG. We will support our claim by developing a fully CLP-based framework to TCG of an OO imperative language, and by assessing it on a corresponding implementation on a set of challenging Java programs. A unique characteristic of our approach is that it handles all language features using only CLP and without the need of developing specific constraint operators (e.g., to model the heap).