OpenRaiser/Intern-Atlas huggingface dataset:
(HO)RPO Revisited
Venue: arXiv cs.LO 2006
Year: 2006

The notion of computability closure has been introduced for proving the termination of the combination of higher-order rewriting and beta-reduction. It is also used for strengthening the higher-order recursive path ordering. In the present paper, we study in more details the relations between the computability closure and the (higher-order) recursive path ordering. We show that the first-order recursive path ordering is equal to an ordering naturally defined from the computability closure. In the higher-order case, we get an ordering containing the higher-order recursive path ordering whose well-foundedness relies on the correctness of the computability closure. This provides a simple way to extend the higher-order recursive path ordering to richer type systems.
Topology Control and Network Lifetime in Three-Dimensional Wireless Sensor Networks
Venue: arXiv cs.NI 2006
Year: 2006

Coverage and connectivity issues of three-dimensional (3D) networks are addressed in [2], but that work assumes that a node can be placed at any arbitrary location. In this work, we drop that assumption and rather assume that nodes are uniformly and densely deployed in a 3D space. We want to devise a mechanism that keeps some nodes active and puts other nodes into sleep so that the number of active nodes at a time is minimized (and thus network life time is maximized), while maintaining full coverage and connectivity. One simple way to do that is to partition the 3D space into cells, and only one node in each cell remains active at a time. Our results show that the number of active nodes can be minimized if the shape of each cell is a truncated octahedron. It requires the sensing range to be at least 0.542326 times the transmission radius. This value is 0.5, 0.53452 and 0.5 for cube, hexagonal prism, and rhombic dodecahedron, respectively. However, at a time the number of active nodes for cube, hexagonal prism and rhombic dodecahedron model is respectively 2.372239, 1.82615 and 1.49468 times of that of truncated octahedron model. So clearly truncated octahedron model has the highest network lifetime. We also provide a distributed topology control algorithm that can be used by each sensor node to determine its cell id using a constant number of local arithmetic operations provided that the sensor node knows its location. We also validate our results by simulation.
Automatic annotation of multilingual text collections with a conceptual thesaurus
Venue: arXiv cs.CL 2006
Year: 2006

Automatic annotation of documents with controlled vocabulary terms (descriptors) from a conceptual thesaurus is not only useful for document indexing and retrieval. The mapping of texts onto the same thesaurus furthermore allows to establish links between similar documents. This is also a substantial requirement of the Semantic Web. This paper presents an almost language-independent system that maps documents written in different languages onto the same multilingual conceptual thesaurus, EUROVOC. Conceptual thesauri differ from Natural Language Thesauri in that they consist of relatively small controlled lists of words or phrases with a rather abstract meaning. To automatically identify which thesaurus descriptors describe the contents of a document best, we developed a statistical, associative system that is trained on texts that have previously been indexed manually. In addition to describing the large number of empirically optimised parameters of the fully functional application, we present the performance of the software according to a human evaluation by professional indexers.
Extending an Information Extraction tool set to Central and Eastern European languages
Venue: arXiv cs.CL 2006
Year: 2006

In a highly multilingual and multicultural environment such as in the European Commission with soon over twenty official languages, there is an urgent need for text analysis tools that use minimal linguistic knowledge so that they can be adapted to many languages without much human effort. We are presenting two such Information Extraction tools that have already been adapted to various Western and Eastern European languages: one for the recognition of date expressions in text, and one for the detection of geographical place names and the visualisation of the results in geographical maps. An evaluation of the performance has produced very satisfying results.
k-Colorability of P5-free graphs
Venue: arXiv cs.DM 2006
Year: 2006

A polynomial time algorithm that determines for a fixed integer k whether or not a P5-free graph can be k-colored is presented in this paper. If such a coloring exists, the algorithm will produce a valid k-coloring.
Using groups for investigating rewrite systems
Venue: arXiv cs.LO 2006
Year: 2006

We describe several technical tools that prove to be efficient for investigating the rewrite systems associated with a family of algebraic laws, and might be useful for more general rewrite systems. These tools consist in introducing a monoid of partial operators, listing the monoid relations expressing the possible local confluence of the rewrite system, then introducing the group presented by these relations, and finally replacing the initial rewrite system with a internal process entirely sitting in the latter group. When the approach can be completed, one typically obtains a practical method for constructing algebras satisfying prescribed laws and for solving the associated word problem.
The recognizability of sets of graphs is a robust property
Venue: arXiv cs.LO 2006
Year: 2006

Once the set of finite graphs is equipped with an algebra structure (arising from the definition of operations that generalize the concatenation of words), one can define the notion of a recognizable set of graphs in terms of finite congruences. Applications to the construction of efficient algorithms and to the theory of context-free sets of graphs follow naturally. The class of recognizable sets depends on the signature of graph operations. We consider three signatures related respectively to Hyperedge Replacement (HR) context-free graph grammars, to Vertex Replacement (VR) context-free graph grammars, and to modular decompositions of graphs. We compare the corresponding classes of recognizable sets. We show that they are robust in the sense that many variants of each signature (where in particular operations are defined by quantifier-free formulas, a quite flexible framework) yield the same notions of recognizability. We prove that for graphs without large complete bipartite subgraphs, HR-recognizability and VR-recognizability coincide. The same combinatorial condition equates HR-context-free and VR-context-free sets of graphs. Inasmuch as possible, results are formulated in the more general framework of relational structures.
Theory and Practice of Triangle Problems in Very Large (Sparse (Power-Law)) Graphs
Venue: arXiv cs.DS 2006
Year: 2006

Finding, counting and/or listing triangles (three vertices with three edges) in large graphs are natural fundamental problems, which received recently much attention because of their importance in complex network analysis. We provide here a detailed state of the art on these problems, in a unified way. We note that, until now, authors paid surprisingly little attention to space complexity, despite its both fundamental and practical interest. We give the space complexities of known algorithms and discuss their implications. Then we propose improvements of a known algorithm, as well as a new algorithm, which are time optimal for triangle listing and beats previous algorithms concerning space complexity. They have the additional advantage of performing better on power-law graphs, which we also study. We finally show with an experimental study that these two algorithms perform very well in practice, allowing to handle cases that were previously out of reach.
Duality of Fix-Points for Distributive Lattices
Venue: arXiv cs.DS 2006
Year: 2006

We present a novel algorithm for calculating fix-points. The algorithm calculates fix-points of an endo-function f on a distributive lattice, by performing reachability computation a graph derived from the dual of f; this is in comparison to traditional algorithms that are based on iterated application of f until a fix-point is reached.
Polygon Convexity: A Minimal O(n) Test
Venue: arXiv cs.CG 2006
Year: 2006

An O(n) test for polygon convexity is stated and proved. It is also proved that the test is minimal in a certain exact sense.
A Combinatorial Family of Near Regular LDPC Codes
Venue: arXiv cs.IT 2006
Year: 2006

An elementary combinatorial Tanner graph construction for a family of near-regular low density parity check codes achieving high girth is presented. The construction allows flexibility in the choice of design parameters like rate, average degree, girth and block length of the code and yields an asymptotic family. The complexity of constructing codes in the family grows only quadratically with the block length.
Control compensation based on upper bound delay in networked control systems
Venue: arXiv cs.NI 2006
Year: 2006

Recent interest in networked control systems (NCS) has instigated research in both communication networks and control. Analysis of NCSs has usually been performed from either the network or the control point of view, but not many papers exist where the analysis of both is done in the same context. In this paper an overall analysis of the networked control system is presented. First, the procedure of obtaining the upper bound delay value for packet transmission in the switched Ethernet network is presented. Next, the obtained delay estimate is utilised in delay compensation for improving the Quality of Performance (QoP) of the control systems. The presented upper bound delay algorithm applies ideas from network calculus theory. For the improvement of QoP, two delay compensation strategies, the Smith predictor based and the robust control based delay compensation strategies, are presented and compared.
Duality for Several Families of Evaluation Codes
Venue: arXiv cs.IT 2006
Year: 2006

We consider generalizations of Reed-Muller codes, toric codes, and codes from certain plane curves, such as those defined by norm and trace functions on finite fields. In each case we are interested in codes defined by evaluating arbitrary subsets of monomials, and in identifying when the dual codes are also obtained by evaluating monomials. We then move to the context of order domain theory, in which the subsets of monomials can be chosen to optimize decoding performance using the Berlekamp-Massey-Sakata algorithm with majority voting. We show that for the codes under consideration these subsets are well-behaved and the dual codes are also defined by monomials.
The Order Bound on the Minimum Distance of the One-Point Codes Associated to a Garcia-Stichtenoth Tower of Function Fields
Venue: arXiv cs.IT 2006
Year: 2006

Garcia and Stichtenoth discovered two towers of function fields that meet the Drinfeld-Vlăduţ bound on the ratio of the number of points to the genus. For one of these towers, Garcia, Pellikaan and Torres derived a recursive description of the Weierstrass semigroups associated to a tower of points on the associated curves. In this article, a non-recursive description of the semigroups is given and from this the enumeration of each of the semigroups is derived as well as its inverse. This enables us to find an explicit formula for the order (Feng-Rao) bound on the minimum distance of the associated one-point codes.
Practical Entropy-Compressed Rank/Select Dictionary
Venue: arXiv cs.DS 2006
Year: 2006

Rank/Select dictionaries are data structures for an ordered set $S \subset \{0,1,...,n-1\}$ to compute $\rank(x,S)$ (the number of elements in $S$ which are no greater than $x$), and $\select(i,S)$ (the $i$-th smallest element in $S$), which are the fundamental components of \emph{succinct data structures} of strings, trees, graphs, etc. In those data structures, however, only asymptotic behavior has been considered and their performance for real data is not satisfactory. In this paper, we propose novel four Rank/Select dictionaries, esp, recrank, vcode and sdarray, each of which is small if the number of elements in $S$ is small, and indeed close to $nH_0(S)$ ($H_0(S) \leq 1$ is the zero-th order \textit{empirical entropy} of $S$) in practice, and its query time is superior to the previous ones. Experimental results reveal the characteristics of our data structures and also show that these data structures are superior to existing implementations in both size and query time.
Creation and use of Citations in the ADS
Venue: arXiv cs.DL 2006
Year: 2006

With over 20 million records, the ADS citation database is regularly used by researchers and librarians to measure the scientific impact of individuals, groups, and institutions. In addition to the traditional sources of citations, the ADS has recently added references extracted from the arXiv e-prints on a nightly basis. We review the procedures used to harvest and identify the reference data used in the creation of citations, the policies and procedures that we follow to avoid double-counting and to eliminate contributions which may not be scholarly in nature. Finally, we describe how users and institutions can easily obtain quantitative citation data from the ADS, both interactively and via web-based programming tools. The ADS is available at http://ads.harvard.edu.
Why did the accident happen? A norm-based reasoning approach
Venue: arXiv cs.AI 2006
Year: 2006

In this paper we describe an architecture of a system that answer the question : Why did the accident happen? from the textual description of an accident. We present briefly the different parts of the architecture and then we describe with more detail the semantic part of the system i.e. the part in which the norm-based reasoning is performed on the explicit knowlege extracted from the text.
Network calculus based FDI approach for switched Ethernet architecture
Venue: arXiv cs.NI 2006
Year: 2006

The Networked Control Systems (NCS) are complex systems which integrate information provided by several domians such as automatic control, computer science, communication network. The work presented in this paper concerns fault detection, isolation and compensation of communication network. The proposed method is based on the classical approach of Fault Detection and Isolation and Fault Tolerant Control (FDI/FTC) currently used in diagnosis. The modelling of the network to be supervised is based on both couloured petri nets and network calculus theory often used to represent and analyse the network behaviour. The goal is to implement inside network devices algorithms enabling to detect, isolate and compensate communication faults in an autonomous way.
Church's thesis is questioned by new calculation paradigm
Venue: arXiv cs.LO 2006
Year: 2006

Church's thesis claims that all effecticely calculable functions are recursive. A shortcoming of the various definitions of recursive functions lies in the fact that it is not a matter of a syntactical check to find out if an entity gives rise to a function. Eight new ideas for a precise setup of arithmetical logic and its metalanguage give the proper environment for the construction of a special computer, the ARBACUS computer. Computers do not come to a necessary halt; it is requested that calculators are constructed on the basis of computers in a way that they always come to a halt, then all calculations are effective. The ARBATOR is defined as a calculator with two-layer-computation. It allows for the calculation of all primitive recursive functions, but multi-level-arbation also allows for the calculation of other arbative functions that are not primitive recursive. The new paradigm of calculation does not have the above mentioned shortcoming. The defenders of Church's thesis are challenged to show that exotic arbative functions are recursive and to put forward a recursive function that is not arbative. A construction with three-tier-multi-level-arbation that includes a diagonalisation leads to the extravagant yet calculable Snark-function that is not arbative. As long as it is not shown that all exotic arbative functions and particularily the Snark-function are arithmetically representable Goedel's first incompleteness sentence is in limbo.
Comparing Typical Opening Move Choices Made by Humans and Chess Engines
Venue: arXiv cs.AI 2006
Year: 2006

The opening book is an important component of a chess engine, and thus computer chess programmers have been developing automated methods to improve the quality of their books. For chess, which has a very rich opening theory, large databases of high-quality games can be used as the basis of an opening book, from which statistics relating to move choices from given positions can be collected. In order to find out whether the opening books used by modern chess engines in machine versus machine competitions are ``comparable'' to those used by chess players in human versus human competitions, we carried out analysis on 26 test positions using statistics from two opening books one compiled from humans' games and the other from machines' games. Our analysis using several nonparametric measures, shows that, overall, there is a strong association between humans' and machines' choices of opening moves when using a book to guide their choices.
The Delay-Limited Capacity Region of OFDM Broadcast Channels
Venue: arXiv cs.IT 2006
Year: 2006

In this work, the delay limited capacity (DLC) of orthogonal frequency division multiplexing (OFDM) systems is investigated. The analysis is organized into two parts. In the first part, the impact of system parameters on the OFDM DLC is analyzed in a general setting. The main results are that under weak assumptions the maximum achievable single user DLC is almost independent of the distribution of the path attenuations in the low signal-to-noise (SNR) region but depends strongly on the delay spread. In the high SNR region the roles are exchanged. Here, the impact of delay spread is negligible while the impact of the distribution becomes dominant. The relevant asymptotic quantities are derived without employing simplifying assumptions on the OFDM correlation structure. Moreover, for both cases it is shown that the DLC is maximized if the total channel energy is uniformly spread, i.e. the power delay profile is uniform. It is worth pointing out that since universal bounds are obtained the results can also be used for other classes of parallel channels with block fading characteristic. The second part extends the setting to the broadcast channel and studies the corresponding OFDM DLC BC region. An algorithm for computing the OFDM BC DLC region is presented. To derive simple but smart resource allocation strategies, the principle of rate water-filling employing order statistics is introduced. This yields analytical lower bounds on the OFDM DLC region based on orthogonal frequency division multiple access (OFDMA) and ordinal channel state information (CSI). Finally, the schemes are compared to an algorithm using full CSI.
Termination and Confluence of Higher-Order Rewrite Systems
Venue: arXiv cs.LO 2006
Year: 2006

In the last twenty years, several approaches to higher-order rewriting have been proposed, among which Klop's Combinatory Rewrite Systems (CRSs), Nipkow's Higher-order Rewrite Systems (HRSs) and Jouannaud and Okada's higher-order algebraic specification languages, of which only the last one considers typed terms. The later approach has been extended by Jouannaud, Okada and the present author into Inductive Data Type Systems (IDTSs). In this paper, we extend IDTSs with the CRS higher-order pattern-matching mechanism, resulting in simply-typed CRSs. Then, we show how the termination criterion developed for IDTSs with first-order pattern-matching, called the General Schema, can be extended so as to prove the strong normalization of IDTSs with higher-order pattern-matching. Next, we compare the unified approach with HRSs. We first prove that the extended General Schema can also be applied to HRSs. Second, we show how Nipkow's higher-order critical pair analysis technique for proving local confluence can be applied to IDTSs.
MIMO Broadcast Channels with Block Diagonalization and Finite Rate Feedback
Venue: arXiv cs.IT 2006
Year: 2006

Block diagonalization is a linear precoding technique for the multiple antenna broadcast (downlink) channel that involves transmission of multiple data streams to each receiver such that no multi-user interference is experienced at any of the receivers. This low-complexity scheme operates only a few dB away from capacity but does require very accurate channel knowledge at the transmitter, which can be very difficult to obtain in fading scenarios. We consider a limited feedback system where each receiver knows its channel perfectly, but the transmitter is only provided with a finite number of channel feedback bits from each receiver. Using a random vector quantization argument, we quantify the throughput loss due to imperfect channel knowledge as a function of the feedback level. The quality of channel knowledge must improve proportional to the SNR in order to prevent interference-limitations, and we show that scaling the number of feedback bits linearly with the system SNR is sufficient to maintain a bounded rate loss. Finally, we investigate a simple scalar quantization scheme that is seen to achieve the same scaling behavior as vector quantization.
Share and Disperse: How to Resist Against Aggregator Compromises in Sensor Networks
Venue: arXiv cs.NI 2006
Year: 2006

A common approach to overcome the limited nature of sensor networks is to aggregate data at intermediate nodes. A challenging issue in this context is to guarantee end-to-end security mainly because sensor networks are extremely vulnerable to node compromises. In order to secure data aggregation, in this paper we propose three schemes that rely on multipath routing. The first one guarantees data confidentiality through secret sharing, while the second and third ones provide data availability through information dispersal. Based on qualitative analysis and implementation, we show that, by applying these schemes, a sensor network can achieve data confidentiality, authenticity, and protection against denial of service attacks even in the presence of multiple compromised nodes.
Solving planning domains with polytree causal graphs is NP-complete
Venue: arXiv cs.AI 2006
Year: 2006

We show that solving planning domains on binary variables with polytree causal graph is \NP-complete. This is in contrast to a polynomial-time algorithm of Domshlak and Brafman that solves these planning domains for polytree causal graphs of bounded indegree.
Reuse of Specification Patterns with the B Method
Venue: arXiv cs.SE 2006
Year: 2006

This paper describes an approach for reusing specification patterns. Specification patterns are design patterns that are expressed in a formal specification language. Reusing a specification pattern means instantiating it or composing it with other specification patterns. Three levels of composition are defined: juxtaposition, composition with inter-patterns links and unification. This paper shows through examples how to define specification patterns in B, how to reuse them directly in B, and also how to reuse the proofs associated with specification patterns.