OpenRaiser/Intern-Atlas huggingface dataset:
Index sets for Finite Normal Predicate Logic Programs
Venue: arXiv cs.LO 2013
Year: 2013

<Q>_e is the effective list of all finite predicate logic programs. <T_e> is the list of recursive trees. We modify constructions of Marek, Nerode, and Remmel [25] to construct recursive functions f and g such that for all indices e, (i) there is a one-to-one degree preserving correspondence between the set of stable models of Q_e and the set of infinite paths through T_{f(e)} and (ii) there is a one-to-one degree preserving correspondence between the set of infinite paths through T_e and the set of stable models of Q_{g(e)}. We use these two recursive functions to reduce the problem of finding the complexity of the index set I_P for various properties P of normal finite predicate logic programs to the problem of computing index sets for primitive recursive trees for which there is a large variety of results [6], [8], [16], [17], [18], [19]. We use our correspondences to determine the complexity of the index sets of all programs and of certain special classes of finite predicate logic programs of properties such as (i) having no stable models, (ii) having at least one stable model, (iii) having exactly c stable models for any given positive integer c, (iv) having only finitely many stable models, or (vi) having infinitely many stable models.
A Review of Dynamic NURBS Approach
Venue: arXiv cs.CG 2013
Year: 2013

Dynamic NURBS, also called D-NURBS, is a known dynamic version of the nonuniform rational B-spline (NURBS) which integrates free-form shape representation and a physically-based model in a unified framework. More recently, computer aided design (CAD) and finite element (FEM) community realized the need to unify CAD and FEM descriptions which motivates a review of D-NURBS concepts. Therefore, in this paper we describe D-NURBS theory in the context of 1D shape deformations. We start with a revision of NURBS for parametric representation of curve spaces. Then, the Lagrangian mechanics is introduced in order to complete the theoretical background. Next, the D-NURBS framework for 1D curve spaces is presented as well as some details about constraints and numerical implementations. In the experimental results, we focus on parameters choice and computational cost.
A Graphical Language for Real-Time Critical Robot Commands
Venue: arXiv cs.RO 2013
Year: 2013

Industrial robotics is characterized by sophisticated mechanical components and highly-developed real-time control algorithms. However, the efficient use of robotic systems is very much limited by existing proprietary programming methods. In the research project SoftRobot, a software architecture was developed that enables the programming of complex real-time critical robot tasks with an object-oriented general purpose language. On top of this architecture, a graphical language was developed to ease the specification of complex robot commands, which can then be used as part of robot application workflows. This paper gives an overview about the design and implementation of this graphical language and illustrates its usefulness with some examples.
A likelihood based framework for assessing network evolution models tested on real network data
Venue: arXiv cs.SI 2013
Year: 2013

This paper presents a statistically sound method for using likelihood to assess potential models of network evolution. The method is tested on data from five real networks. Data from the internet autonomous system network, from two photo sharing sites and from a co-authorship network are tested using this framework.
Forecasting Full-Path Network Congestion Using One Bit Signalling
Venue: arXiv cs.NI 2013
Year: 2013

In this paper, we propose a mechanism for packet marking called Probabilistic Congestion Notification (PCN). This scheme makes use of the 1-bit Explicit Congestion Notification (ECN) field in the Internet Protocol (IP) header. It allows the source to estimate the exact level of congestion at each intermediate queue. By knowing this, the source could take avoiding action either by adapting its sending rate or by using alternate routes. The estimation mechanism makes use of time series analysis both to improve the quality of the congestion estimation and to predict, ahead of time, the congestion level which subsequent packets will encounter. The proposed protocol is tested in ns-2 simulator using a background of real Internet traffic traces. Results show that the methods can successfully calculate the congestion at any queue along the path with low error levels.
Criticisms of modelling packet traffic using long-range dependence (extended version)
Venue: arXiv cs.NI 2013
Year: 2013

This paper criticises the notion that long-range dependence is an important contributor to the queuing behaviour of real Internet traffic. The idea is questioned in two different ways. Firstly, a class of models used to simulate Internet traffic is shown to have important theoretical flaws. It is shown that this behaviour is inconsistent with the behaviour of real traffic traces. Secondly, the notion that long-range correlations significantly affects the queuing performance of traffic is investigated by destroying those correlations in real traffic traces (by reordering). It is shown that the longer ranges of correlations are not important except in one case with an extremely high load.
Primal implication as encryption
Venue: arXiv cs.LO 2013
Year: 2013

We propose a "cryptographic" interpretation for the propositional connectives of primal infon logic introduced by Y. Gurevich and I. Neeman and prove the corresponding soundness and completeness results. Primal implication $\impφψ$ corresponds to the encryption of $ψ$ with a secret key $φ$, primal disjunction $\vpφψ$ is a group key and $\bot$ reflects some backdoor constructions such as full superuser permissions or a universal decryption key. For the logic of $\bot$ as a universal key (it was never considered before) we prove that the derivability problem has linear time complexity. We also show that the universal key can be emulated using primal disjunction.
Distributed Overlay Anycast Table using Space filling curves
Venue: arXiv cs.NI 2013
Year: 2013

In this paper we present the \emph{Distributed Overlay Anycast Table}, a structured overlay that implements application-layer anycast, allowing the discovery of the closest host that is a member of a given group. One application is in locality-aware peer-to-peer networks, where peers need to discover low-latency peers participating in the distribution of a particular file or stream. The DOAT makes use of network delay coordinates and a space filling curve to achieve locality-aware routing across the overlay, and Bloom filters to aggregate group identifiers. The solution is designed to optimise both accuracy and query time, which are essential for real-time applications. We simulated DOAT using both random and realistic node distributions. The results show that accuracy is high and query time is low.
Challenges in the capture and dissemination of measurements from high-speed networks
Venue: arXiv cs.NI 2013
Year: 2013

The production of a large-scale monitoring system for a high-speed network leads to a number of challenges. These challenges are not purely techinical but also socio-political and legal. The number of stakeholders in a such a monitoring activity is large including the network operators, the users, the equipment manufacturers and of course the monitoring researchers. The MASTS project (Measurement at All Scales in Time and Space) was created to instrument the high-speed JANET Lightpath network, and has been extended to incorporate other paths supported by JANET(UK). Challenges the project has faced have included: simple access to the network; legal issues involved in the storage and dissemination of the captured information, which may be personal; the volume of data captured and the rate at which this data appears at store. To this end the MASTS system will have established four monitoring points each capturing packets on a high speed link. Traffic header data will be continuously collected, anonymised, indexed, stored and made available to the research community. A legal framework for the capture and storage of network measurement data has been developed which allows the anonymised IP traces to be used for research pur poses.
An investigation towards wavelet based optimization of automatic image registration techniques
Venue: arXiv cs.CV 2013
Year: 2013

Image registration is the process of transforming different sets of data into one coordinate system and is required for various remote sensing applications like change detection, image fusion, and other related areas. The effect of increased relief displacement, requirement of more control points, and increased data volume are the challenges associated with the registration of high resolution image data. The objective of this research work is to study the most efficient techniques and to investigate the extent of improvement achievable by enhancing them with Wavelet transform. The SIFT feature based method uses the Eigen value for extracting thousands of key points based on scale invariant features and these feature points when further enhanced by the wavelet transform yields the best results.
Energy Efficient Cooperative Strategies for Relay-Assisted Downlink Cellular Systems, Part I: Theoretical Framework
Venue: arXiv cs.IT 2013
Year: 2013

The impact of cognition on the energy efficiency of a downlink cellular system in which multiple relays assist the transmission of the base station is considered. The problem is motivated by the practical importance of relay-assisted solutions in mobile networks, such as LTE-A, in which cooperation among relays holds the promise of greatly improving the energy efficiency of the system. We study the fundamental tradeoff between the power consumption at the base station and the level of cooperation and cognition at the relay nodes. By distributing the same message to multiple relays, the base station consumes more power but it enables cooperation among the relays, thus making the transmission between relays to destination a multiuser cognitive channel. Cooperation among the relays allows for a reduction of the power used to transmit from the relays to the end users due to interference management and the coherent combining gains. These gain are present even in the case of partial or unidirectional transmitter cooperation, which is the case in cognitive channels such as the cognitive interference channel and the interference channel with a cognitive relay. We therefore address the problem of determining the optimal level of cooperation at the relays which results in the smallest total power consumption when accounting for the power reduction due to cognition. A practical design examples and numerical simulation are presented in a companion paper (part II).
Data-Intensive Workload Consolidation on Hadoop Distributed File System
Venue: arXiv cs.DC 2013
Year: 2013

Workload consolidation, sharing physical resources among multiple workloads, is a promising technique to save cost and energy in cluster computing systems. This paper highlights a few challenges of workload consolidation for Hadoop as one of the current state-of-the-art data-intensive cluster computing system. Through a systematic step-by-step procedure, we investigate challenges for efficient server consolidation in Hadoop environments. To this end, we first investigate the inter-relationship between last level cache (LLC) contention and throughput degradation for consolidated workloads on a single physical server employing Hadoop distributed file system (HDFS). We then investigate the general case of consolidation on multiple physical servers so that their throughput never falls below a desired/predefined utilization level. We use our empirical results to model consolidation as a classic two-dimensional bin packing problem and then design a computationally efficient greedy algorithm to achieve minimum throughput degradation on multiple servers. Results are very promising and show that our greedy approach is able to achieve near optimal solution in all experimented cases.
A framework to characterize performance of LASSO algorithms
Venue: arXiv cs.IT 2013
Year: 2013

In this paper we consider solving \emph{noisy} under-determined systems of linear equations with sparse solutions. A noiseless equivalent attracted enormous attention in recent years, above all, due to work of \cite{CRT,CanRomTao06,DonohoPol} where it was shown in a statistical and large dimensional context that a sparse unknown vector (of sparsity proportional to the length of the vector) can be recovered from an under-determined system via a simple polynomial $\ell_1$-optimization algorithm. \cite{CanRomTao06} further established that even when the equations are \emph{noisy}, one can, through an SOCP noisy equivalent of $\ell_1$, obtain an approximate solution that is (in an $\ell_2$-norm sense) no further than a constant times the noise from the sparse unknown vector. In our recent works \cite{StojnicCSetam09,StojnicUpper10}, we created a powerful mechanism that helped us characterize exactly the performance of $\ell_1$ optimization in the noiseless case (as shown in \cite{StojnicEquiv10} and as it must be if the axioms of mathematics are well set, the results of \cite{StojnicCSetam09,StojnicUpper10} are in an absolute agreement with the corresponding exact ones from \cite{DonohoPol}). In this paper we design a mechanism, as powerful as those from \cite{StojnicCSetam09,StojnicUpper10}, that can handle the analysis of a LASSO type of algorithm (and many others) that can be (or typically are) used for "solving" noisy under-determined systems. Using the mechanism we then, in a statistical context, compute the exact worst-case $\ell_2$ norm distance between the unknown sparse vector and the approximate one obtained through such a LASSO. The obtained results match the corresponding exact ones obtained in \cite{BayMon10,DonMalMon10}. Moreover, as a by-product of our analysis framework we recognize existence of an SOCP type of algorithm that achieves the same performance.
Proof nets and the call-by-value lambda-calculus
Venue: arXiv cs.LO 2013
Year: 2013

This paper gives a detailed account of the relationship between (a variant of) the call-by-value lambda calculus and linear logic proof nets. The presentation is carefully tuned in order to realize a strong bisimulation between the two systems: every single rewriting step on the calculus maps to a single step on the nets, and viceversa. In this way, we obtain an algebraic reformulation of proof nets. Moreover, we provide a simple correctness criterion for our proof nets, which employ boxes in an unusual way.
Minimal lambda-theories by ultraproducts
Venue: arXiv cs.LO 2013
Year: 2013

A longstanding open problem in lambda calculus is whether there exist continuous models of the untyped lambda calculus whose theory is exactly the least lambda-theory lambda-beta or the least sensible lambda-theory H (generated by equating all the unsolvable terms). A related question is whether, given a class of lambda models, there is a minimal lambda-theory represented by it. In this paper, we give a general tool to answer positively to this question and we apply it to a wide class of webbed models: the i-models. The method then applies also to graph models, Krivine models, coherent models and filter models. In particular, we build an i-model whose theory is the set of equations satisfied in all i-models.
Non determinism through type isomorphism
Venue: arXiv cs.LO 2013
Year: 2013

We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known non-deterministic and algebraic lambda-calculi.
Formalizing the Confluence of Orthogonal Rewriting Systems
Venue: arXiv cs.LO 2013
Year: 2013

Orthogonality is a discipline of programming that in a syntactic manner guarantees determinism of functional specifications. Essentially, orthogonality avoids, on the one side, the inherent ambiguity of non determinism, prohibiting the existence of different rules that specify the same function and that may apply simultaneously (non-ambiguity), and, on the other side, it eliminates the possibility of occurrence of repetitions of variables in the left-hand side of these rules (left linearity). In the theory of term rewriting systems (TRSs) determinism is captured by the well-known property of confluence, that basically states that whenever different computations or simplifications from a term are possible, the computed answers should coincide. Although the proofs are technically elaborated, confluence is well-known to be a consequence of orthogonality. Thus, orthogonality is an important mathematical discipline intrinsic to the specification of recursive functions that is naturally applied in functional programming and specification. Starting from a formalization of the theory of TRSs in the proof assistant PVS, this work describes how confluence of orthogonal TRSs has been formalized, based on axiomatizations of properties of rules, positions and substitutions involved in parallel steps of reduction, in this proof assistant. Proofs for some similar but restricted properties such as the property of confluence of non-ambiguous and (left and right) linear TRSs have been fully formalized.
Computational Analysis of Modified Blom's Scheme
Venue: arXiv cs.CR 2013
Year: 2013

To achieve security in wireless networks, it is important to be able to encrypt and authenticate messages sent among sensor nodes. Due to resource constraints, achieving such key agreement in wireless sensor networks in nontrivial. Blom's scheme is a symmetric key exchange protocol used in cryptography. In this paper, we propose a new key pre-distribution scheme by modifying Blom's scheme which reduces the computational complexity as well as memory usage.
Meshes that trap random subspaces
Venue: arXiv cs.IT 2013
Year: 2013

In our recent work \cite{StojnicCSetam09,StojnicUpper10} we considered solving under-determined systems of linear equations with sparse solutions. In a large dimensional and statistical context we proved results related to performance of a polynomial $\ell_1$-optimization technique when used for solving such systems. As one of the tools we used a probabilistic result of Gordon \cite{Gordon88}. In this paper we revisit this classic result in its core form and show how it can be reused to in a sense prove its own optimality.
Age group and gender recognition from human facial images
Venue: arXiv cs.CV 2013
Year: 2013

This work presents an automatic human gender and age group recognition system based on human facial images. It makes an extensive experiment with row pixel intensity valued features and Discrete Cosine Transform (DCT) coefficient features with Principal Component Analysis and k-Nearest Neighbor classification to identify the best recognition approach. The final results show approaches using DCT coefficient outperform their counter parts resulting in a 99% correct gender recognition rate and 68% correct age group recognition rate (considering four distinct age groups) in unseen test images. Detailed experimental settings and obtained results are clearly presented and explained in this report.
Linear Fractional Network Coding and Representable Discrete Polymatroids
Venue: arXiv cs.IT 2013
Year: 2013

A linear Fractional Network Coding (FNC) solution over $\mathbb{F}_q$ is a linear network coding solution over $\mathbb{F}_q$ in which the message dimensions need not necessarily be the same and need not be the same as the edge vector dimension. Scalar linear network coding, vector linear network coding are special cases of linear FNC. In this paper, we establish the connection between the existence of a linear FNC solution for a network over $\mathbb{F}_q$ and the representability over $\mathbb{F}_q$ of discrete polymatroids, which are the multi-set analogue of matroids. All previously known results on the connection between the scalar and vector linear solvability of networks and representations of matroids and discrete polymatroids follow as special cases. An algorithm is provided to construct networks which admit FNC solution over $\mathbb{F}_q,$ from discrete polymatroids representable over $\mathbb{F}_q.$ Example networks constructed from discrete polymatroids using the algorithm are provided, which do not admit any scalar and vector solution, and for which FNC solutions with the message dimensions being different provide a larger throughput than FNC solutions with the message dimensions being equal.
Approximating Minimization Diagrams and Generalized Proximity Search
Venue: arXiv cs.CG 2013
Year: 2013

We investigate the classes of functions whose minimization diagrams can be approximated efficiently in \Re^d. We present a general framework and a data-structure that can be used to approximate the minimization diagram of such functions. The resulting data-structure has near linear size and can answer queries in logarithmic time. Applications include approximating the Voronoi diagram of (additively or multiplicatively) weighted points. Our technique also works for more general distance functions, such as metrics induced by convex bodies, and the nearest furthest-neighbor distance to a set of point sets. Interestingly, our framework works also for distance functions that do not comply with the triangle inequality. For many of these functions no near-linear size approximation was known before.
Equivalence for Rank-metric and Matrix Codes and Automorphism Groups of Gabidulin Codes
Venue: arXiv cs.IT 2013
Year: 2013

For a growing number of applications such as cellular, peer-to-peer, and sensor networks, efficient error-free transmission of data through a network is essential. Toward this end, Kötter and Kschischang propose the use of subspace codes to provide error correction in the network coding context. The primary construction for subspace codes is the lifting of rank-metric or matrix codes, a process that preserves the structural and distance properties of the underlying code. Thus, to characterize the structure and error-correcting capability of these subspace codes, it is valuable to perform such a characterization of the underlying rank-metric and matrix codes. This paper lays a foundation for this analysis through a framework for classifying rank-metric and matrix codes based on their structure and distance properties. To enable this classification, we extend work by Berger on equivalence for rank-metric codes to define a notion of equivalence for matrix codes, and we characterize the group structure of the collection of maps that preserve such equivalence. We then compare the notions of equivalence for these two related types of codes and show that matrix equivalence is strictly more general than rank-metric equivalence. Finally, we characterize the set of equivalence maps that fix the prominent class of rank-metric codes known as Gabidulin codes. In particular, we give a complete characterization of the rank-metric automorphism group of Gabidulin codes, correcting work by Berger, and give a partial characterization of the matrix-automorphism group of the expanded matrix codes that arise from Gabidulin codes.