OpenRaiser/Intern-Atlas huggingface dataset:
An introspective algorithm for the integer determinant
Venue: arXiv cs.SC 2007
Year: 2007

We present an algorithm computing the determinant of an integer matrix A. The algorithm is introspective in the sense that it uses several distinct algorithms that run in a concurrent manner. During the course of the algorithm partial results coming from distinct methods can be combined. Then, depending on the current running time of each method, the algorithm can emphasize a particular variant. With the use of very fast modular routines for linear algebra, our implementation is an order of magnitude faster than other existing implementations. Moreover, we prove that the expected complexity of our algorithm is only O(n^3 log^{2.5}(n ||A||)) bit operations in the dense case and O(Omega n^{1.5} log^2(n ||A||) + n^{2.5}log^3(n||A||)) in the sparse case, where ||A|| is the largest entry in absolute value of the matrix and Omega is the cost of matrix-vector multiplication in the case of a sparse matrix.
An Efficient Pseudo-Codeword Search Algorithm for Linear Programming Decoding of LDPC Codes
Venue: arXiv cs.IT 2007
Year: 2007

In Linear Programming (LP) decoding of a Low-Density-Parity-Check (LDPC) code one minimizes a linear functional, with coefficients related to log-likelihood ratios, over a relaxation of the polytope spanned by the codewords \cite{03FWK}. In order to quantify LP decoding, and thus to describe performance of the error-correction scheme at moderate and large Signal-to-Noise-Ratios (SNR), it is important to study the relaxed polytope to understand better its vertexes, so-called pseudo-codewords, especially those which are neighbors of the zero codeword. In this manuscript we propose a technique to heuristically create a list of these neighbors and their distances. Our pseudo-codeword-search algorithm starts by randomly choosing the initial configuration of the noise. The configuration is modified through a discrete number of steps. Each step consists of two sub-steps. Firstly, one applies an LP decoder to the noise-configuration deriving a pseudo-codeword. Secondly, one finds configuration of the noise equidistant from the pseudo codeword and the zero codeword. The resulting noise configuration is used as an entry for the next step. The iterations converge rapidly to a pseudo-codeword neighboring the zero codeword. Repeated many times, this procedure is characterized by the distribution function (frequency spectrum) of the pseudo-codeword effective distance. The effective distance of the coding scheme is approximated by the shortest distance pseudo-codeword in the spectrum. The efficiency of the procedure is demonstrated on examples of the Tanner $[155,64,20]$ code and Margulis $p=7$ and $p=11$ codes (672 and 2640 bits long respectively) operating over an Additive-White-Gaussian-Noise (AWGN) channel.
A Multi-Relational Network to Support the Scholarly Communication Process
Venue: arXiv cs.DL 2007
Year: 2007

The general pupose of the scholarly communication process is to support the creation and dissemination of ideas within the scientific community. At a finer granularity, there exists multiple stages which, when confronted by a member of the community, have different requirements and therefore different solutions. In order to take a researcher's idea from an initial inspiration to a community resource, the scholarly communication infrastructure may be required to 1) provide a scientist initial seed ideas; 2) form a team of well suited collaborators; 3) located the most appropriate venue to publish the formalized idea; 4) determine the most appropriate peers to review the manuscript; and 5) disseminate the end product to the most interested members of the community. Through the various delinieations of this process, the requirements of each stage are tied soley to the multi-functional resources of the community: its researchers, its journals, and its manuscritps. It is within the collection of these resources and their inherent relationships that the solutions to scholarly communication are to be found. This paper describes an associative network composed of multiple scholarly artifacts that can be used as a medium for supporting the scholarly communication process.
Open Answer Set Programming with Guarded Programs
Venue: arXiv cs.AI 2007
Year: 2007

Open answer set programming (OASP) is an extension of answer set programming where one may ground a program with an arbitrary superset of the program's constants. We define a fixed point logic (FPL) extension of Clark's completion such that open answer sets correspond to models of FPL formulas and identify a syntactic subclass of programs, called (loosely) guarded programs. Whereas reasoning with general programs in OASP is undecidable, the FPL translation of (loosely) guarded programs falls in the decidable (loosely) guarded fixed point logic (mu(L)GF). Moreover, we reduce normal closed ASP to loosely guarded OASP, enabling for the first time, a characterization of an answer set semantics by muLGF formulas. We further extend the open answer set semantics for programs with generalized literals. Such generalized programs (gPs) have interesting properties, e.g., the ability to express infinity axioms. We restrict the syntax of gPs such that both rules and generalized literals are guarded. Via a translation to guarded fixed point logic, we deduce 2-exptime-completeness of satisfiability checking in such guarded gPs (GgPs). Bound GgPs are restricted GgPs with exptime-complete satisfiability checking, but still sufficiently expressive to optimally simulate computation tree logic (CTL). We translate Datalog lite programs to GgPs, establishing equivalence of GgPs under an open answer set semantics, alternation-free muGF, and Datalog lite.
Unifying two Graph Decompositions with Modular Decomposition
Venue: arXiv cs.DS 2007
Year: 2007

We introduces the umodules, a generalisation of the notion of graph module. The theory we develop captures among others undirected graphs, tournaments, digraphs, and $2-$structures. We show that, under some axioms, a unique decomposition tree exists for umodules. Polynomial-time algorithms are provided for: non-trivial umodule test, maximal umodule computation, and decomposition tree computation when the tree exists. Our results unify many known decomposition like modular and bi-join decomposition of graphs, and a new decomposition of tournaments.
Patterns of i.i.d. Sequences and Their Entropy - Part I: General Bounds
Venue: arXiv cs.IT 2007
Year: 2007

Tight bounds on the block entropy of patterns of sequences generated by independent and identically distributed (i.i.d.) sources are derived. A pattern of a sequence is a sequence of integer indices with each index representing the order of first occurrence of the respective symbol in the original sequence. Since a pattern is the result of data processing on the original sequence, its entropy cannot be larger. Bounds derived here describe the pattern entropy as function of the original i.i.d. source entropy, the alphabet size, the symbol probabilities, and their arrangement in the probability space. Matching upper and lower bounds derived provide a useful tool for very accurate approximations of pattern block entropies for various distributions, and for assessing the decrease of the pattern entropy from that of the original i.i.d. sequence.
A Better Alternative to Piecewise Linear Time Series Segmentation
Venue: arXiv cs.DB 2007
Year: 2007

Time series are difficult to monitor, summarize and predict. Segmentation organizes time series into few intervals having uniform characteristics (flatness, linearity, modality, monotonicity and so on). For scalability, we require fast linear time algorithms. The popular piecewise linear model can determine where the data goes up or down and at what rate. Unfortunately, when the data does not follow a linear model, the computation of the local slope creates overfitting. We propose an adaptive time series model where the polynomial degree of each interval vary (constant, linear and so on). Given a number of regressors, the cost of each interval is its polynomial degree: constant intervals cost 1 regressor, linear intervals cost 2 regressors, and so on. Our goal is to minimize the Euclidean (l_2) error for a given model complexity. Experimentally, we investigate the model where intervals can be either constant or linear. Over synthetic random walks, historical stock market prices, and electrocardiograms, the adaptive model provides a more accurate segmentation than the piecewise linear model without increasing the cross-validation error or the running time, while providing a richer vocabulary to applications. Implementation issues, such as numerical stability and real-world performance, are discussed.
Imagination as Holographic Processor for Text Animation
Venue: arXiv cs.AI 2007
Year: 2007

Imagination is the critical point in developing of realistic artificial intelligence (AI) systems. One way to approach imagination would be simulation of its properties and operations. We developed two models: AI-Brain Network Hierarchy of Languages and Semantical Holographic Calculus as well as simulation system ScriptWriter that emulate the process of imagination through an automatic animation of English texts. The purpose of this paper is to demonstrate the model and to present ScriptWriter system http://nvo.sdsc.edu/NVO/JCSG/get_SRB_mime_file2.cgi//home/tamara.sdsc/test/demo.zip?F=/home/tamara.sdsc/test/demo.zip&M=application/x-gtar for simulation of the imagination.
Combinatorial laplacians and positivity under partial transpose
Venue: arXiv cs.CC 2007
Year: 2007

Density matrices of graphs are combinatorial laplacians normalized to have trace one (Braunstein \emph{et al.} \emph{Phys. Rev. A,} \textbf{73}:1, 012320 (2006)). If the vertices of a graph are arranged as an array, then its density matrix carries a block structure with respect to which properties such as separability can be considered. We prove that the so-called degree-criterion, which was conjectured to be necessary and sufficient for separability of density matrices of graphs, is equivalent to the PPT-criterion. As such it is not sufficient for testing the separability of density matrices of graphs (we provide an explicit example). Nonetheless, we prove the sufficiency when one of the array dimensions has length two (for an alternative proof see Wu, \emph{Phys. Lett. A}\textbf{351} (2006), no. 1-2, 18--22). Finally we derive a rational upper bound on the concurrence of density matrices of graphs and show that this bound is exact for graphs on four vertices.
On entropy for mixtures of discrete and continuous variables
Venue: arXiv cs.IT 2007
Year: 2007

Let $X$ be a discrete random variable with support $S$ and $f : S \to S^\prime$ be a bijection. Then it is well-known that the entropy of $X$ is the same as the entropy of $f(X)$. This entropy preservation property has been well-utilized to establish non-trivial properties of discrete stochastic processes, e.g. queuing process \cite{prg03}. Entropy as well as entropy preservation is well-defined only in the context of purely discrete or continuous random variables. However for a mixture of discrete and continuous random variables, which arise in many interesting situations, the notions of entropy and entropy preservation have not been well understood. In this paper, we extend the notion of entropy in a natural manner for a mixed-pair random variable, a pair of random variables with one discrete and the other continuous. Our extensions are consistent with the existing definitions of entropy in the sense that there exist natural injections from discrete or continuous random variables into mixed-pair random variables such that their entropy remains the same. This extension of entropy allows us to obtain sufficient conditions for entropy preservation in mixtures of discrete and continuous random variables under bijections. The extended definition of entropy leads to an entropy rate for continuous time Markov chains. As an application, we recover a known probabilistic result related to Poisson process. We strongly believe that the frame-work developed in this paper can be useful in establishing probabilistic properties of complex processes, such as load balancing systems, queuing network, caching algorithms.
Satisfying KBO Constraints
Venue: arXiv cs.SC 2007
Year: 2007

This paper presents two new approaches to prove termination of rewrite systems with the Knuth-Bendix order efficiently. The constraints for the weight function and for the precedence are encoded in (pseudo-)propositional logic and the resulting formula is tested for satisfiability. Any satisfying assignment represents a weight function and a precedence such that the induced Knuth-Bendix order orients the rules of the encoded rewrite system from left to right.
Modules over Monads and Linearity
Venue: arXiv cs.LO 2007
Year: 2007

Inspired by the classical theory of modules over a monoid, we give a first account of the natural notion of module over a monad. The associated notion of morphism of left modules ("Linear" natural transformations) captures an important property of compatibility with substitution, in the heterogeneous case where "terms" and variables therein could be of different types as well as in the homogeneous case. In this paper, we present basic constructions of modules and we show examples concerning in particular abstract syntax and lambda-calculus.
Heap Reference Analysis Using Access Graphs
Venue: arXiv cs.PL 2007
Year: 2007

Despite significant progress in the theory and practice of program analysis, analysing properties of heap data has not reached the same level of maturity as the analysis of static and stack data. The spatial and temporal structure of stack and static data is well understood while that of heap data seems arbitrary and is unbounded. We devise bounded representations which summarize properties of the heap data. This summarization is based on the structure of the program which manipulates the heap. The resulting summary representations are certain kinds of graphs called access graphs. The boundedness of these representations and the monotonicity of the operations to manipulate them make it possible to compute them through data flow analysis. An important application which benefits from heap reference analysis is garbage collection, where currently liveness is conservatively approximated by reachability from program variables. As a consequence, current garbage collectors leave a lot of garbage uncollected, a fact which has been confirmed by several empirical studies. We propose the first ever end-to-end static analysis to distinguish live objects from reachable objects. We use this information to make dead objects unreachable by modifying the program. This application is interesting because it requires discovering data flow information representing complex semantics. In particular, we discover four properties of heap data: liveness, aliasing, availability, and anticipability. Together, they cover all combinations of directions of analysis (i.e. forward and backward) and confluence of information (i.e. union and intersection). Our analysis can also be used for plugging memory leaks in C/C++ languages.
Nominal Logic Programming
Venue: arXiv cs.PL 2007
Year: 2007

Nominal logic is an extension of first-order logic which provides a simple foundation for formalizing and reasoning about abstract syntax modulo consistent renaming of bound names (that is, alpha-equivalence). This article investigates logic programming based on nominal logic. We describe some typical nominal logic programs, and develop the model-theoretic, proof-theoretic, and operational semantics of such programs. Besides being of interest for ensuring the correct behavior of implementations, these results provide a rigorous foundation for techniques for analysis and reasoning about nominal logic programs, as we illustrate via examples.
On the Fading Paper Achievable Region of the Fading MIMO Broadcast Channel
Venue: arXiv cs.IT 2007
Year: 2007

We consider transmission over the ergodic fading multi-antenna broadcast (MIMO-BC) channel with partial channel state information at the transmitter and full information at the receiver. Over the equivalent {\it non}-fading channel, capacity has recently been shown to be achievable using transmission schemes that were designed for the ``dirty paper'' channel. We focus on a similar ``fading paper'' model. The evaluation of the fading paper capacity is difficult to obtain. We confine ourselves to the {\it linear-assignment} capacity, which we define, and use convex analysis methods to prove that its maximizing distribution is Gaussian. We compare our fading-paper transmission to an application of dirty paper coding that ignores the partial state information and assumes the channel is fixed at the average fade. We show that a gain is easily achieved by appropriately exploiting the information. We also consider a cooperative upper bound on the sum-rate capacity as suggested by Sato. We present a numeric example that indicates that our scheme is capable of realizing much of this upper bound.
Type theory and rewriting
Venue: arXiv cs.LO 2007
Year: 2007

We study the properties, in particular termination, of dependent types systems for lambda calculus and rewriting.
P2P IPTV Measurement: A Comparison Study
Venue: arXiv cs.NI 2007
Year: 2007

With the success of P2P file sharing, new emerging P2P applications arise on the Internet for streaming content like voice (VoIP) or live video (IPTV). Nowadays, there are lots of works measuring P2P file sharing or P2P telephony systems, but there is still no comprehensive study about P2P IPTV, whereas it should be massively used in the future. During the last FIFA world cup, we measured network traffic generated by P2P IPTV applications like PPlive, PPstream, TVants and Sopcast. In this paper we analyze some of our results during the same games for the applications. We focus on traffic statistics and churn of peers within these P2P networks. Our objectives are threefold: we point out the traffic generated to understand the impact they will have on the network, we try to infer the mechanisms of such applications and highlight differences, and we give some insights about the users' behavior.
An unbreakable cryptosystem for common people
Venue: arXiv cs.CR 2007
Year: 2007

It has been found that an algorithm can generate true random numbers on classical computer. The algorithm can be used to generate unbreakable message PIN (personal identification number) and password.
Most Programs Stop Quickly or Never Halt
Venue: arXiv cs.IT 2007
Year: 2007

Since many real-world problems arising in the fields of compiler optimisation, automated software engineering, formal proof systems, and so forth are equivalent to the Halting Problem--the most notorious undecidable problem--there is a growing interest, not only academically, in understanding the problem better and in providing alternative solutions. Halting computations can be recognised by simply running them; the main difficulty is to detect non-halting programs. Our approach is to have the probability space extend over both space and time and to consider the probability that a random $N$-bit program has halted by a random time. We postulate an a priori computable probability distribution on all possible runtimes and we prove that given an integer k>0, we can effectively compute a time bound T such that the probability that an N-bit program will eventually halt given that it has not halted by T is smaller than 2^{-k}. We also show that the set of halting programs (which is computably enumerable, but not computable) can be written as a disjoint union of a computable set and a set of effectively vanishing probability. Finally, we show that ``long'' runtimes are effectively rare. More formally, the set of times at which an N-bit program can stop after the time 2^{N+constant} has effectively zero density.
A framework for compositional verification of security protocols
Venue: arXiv cs.CR 2007
Year: 2007

Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation. To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMax consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.
On the security of new key exchange protocols based on the triple decomposition problem
Venue: arXiv cs.CR 2007
Year: 2007

We show that two new key exchange protocols with security based on the triple DP may have security based on the MSCSP.
Managing network congestion with a Kohonen-based RED queue
Venue: arXiv cs.NI 2007
Year: 2007

The behaviour of the TCP AIMD algorithm is known to cause queue length oscillations when congestion occurs at a router output link. Indeed, due to these queueing variations, end-to-end applications experience large delay jitter. Many studies have proposed efficient Active Queue Management (AQM) mechanisms in order to reduce queue oscillations and stabilize the queue length. These AQM are mostly improvements of the Random Early Detection (RED) model. Unfortunately, these enhancements do not react in a similar manner for various network conditions and are strongly sensitive to their initial setting parameters. Although this paper proposes a solution to overcome the difficulties of setting these parameters by using a Kohonen neural network model, another goal of this study is to investigate whether cognitive intelligence could be placed in the core network to solve such stability problem. In our context, we use results from the neural network area to demonstrate that our proposal, named Kohonen-RED (KRED), enables a stable queue length without complex parameters setting and passive measurements.
The Implications of Network-Centric Software Systems on Software Architecture: A Critical Evaluation
Venue: arXiv cs.SE 2007
Year: 2007

The purpose of this paper is to evaluate the impact of emerging network-centric software systems on the field of software architecture. We first develop an insight concerning the term "network-centric" by presenting its origin and its implications within the context of software architecture. On the basis of this insight, we present our definition of a network-centric framework and its distinguishing characteristics. We then enumerate the challenges that face the field of software architecture as software development shifts from a platform-centric to a network-centric model. In order to face these challenges, we propose a formal approach embodied in a new architectural style that supports overcoming these challenges at the architectural level. Finally, we conclude by presenting an illustrative example to demonstrate the usefulness of the concepts of network centricity, summarizing our contributions, and linking our approach to future work that needs to be done in this area.