OpenRaiser/Intern-Atlas huggingface dataset:
Constructing experimental indicators for Open Access documents
Venue: arXiv cs.DL 2006
Year: 2006

The ongoing paradigm change in the scholarly publication system ('science is turning to e-science') makes it necessary to construct alternative evaluation criteria/metrics which appropriately take into account the unique characteristics of electronic publications and other research output in digital formats. Today, major parts of scholarly Open Access (OA) publications and the self-archiving area are not well covered in the traditional citation and indexing databases. The growing share and importance of freely accessible research output demands new approaches/metrics for measuring and for evaluating of these new types of scientific publications. In this paper we propose a simple quantitative method which establishes indicators by measuring the access/download pattern of OA documents and other web entities of a single web server. The experimental indicators (search engine, backlink and direct access indicator) are constructed based on standard local web usage data. This new type of web-based indicator is developed to model the specific demand for better study/evaluation of the accessibility, visibility and interlinking of open accessible documents. We conclude that e-science will need new stable e-indicators.
Definitions by rewriting in the Calculus of Constructions
Venue: arXiv cs.LO 2006
Year: 2006

This paper presents general syntactic conditions ensuring the strong normalization and the logical consistency of the Calculus of Algebraic Constructions, an extension of the Calculus of Constructions with functions and predicates defined by higher-order rewrite rules. On the one hand, the Calculus of Constructions is a powerful type system in which one can formalize the propositions and natural deduction proofs of higher-order logic. On the other hand, rewriting is a simple and powerful computation paradigm. The combination of both allows, among other things, to develop formal proofs with a reduced size and more automation compared with more traditional proof assistants. The main novelty is to consider a general form of rewriting at the predicate-level which generalizes the strong elimination of the Calculus of Inductive Constructions.
Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like Languages
Venue: arXiv cs.LO 2006
Year: 2006

We show how to give a coherent semantics to programs that are well-specified in a version of separation logic for a language with higher types: idealized algol extended with heaps (but with immutable stack variables). In particular, we provide simple sound rules for deriving higher-order frame rules, allowing for local reasoning.
Symbolic Simulation-Checking of Dense-Time Systems
Venue: arXiv cs.LO 2006
Year: 2006

Intuitively, an (implementation) automata is simulated by a (specification) automata if every externally observable transition by the implementation automata can also be made by the specification automata. In this work, we present a symbolic algorithm for the simulation-checking of timed automatas. We first present a simulation-checking procedure that operates on state spaces, representable with convex polyhedra, of timed automatas. We then present techniques to represent those intermediate result convex polyhedra with zones and make the procedure an algorithm. We then discuss how to handle Zeno states in the implementation automata. Finally, we have endeavored to realize the algorithm and report the performance of our algorithm in the experiment.
Entropy generation in a model of reversible computation
Venue: arXiv cs.CC 2006
Year: 2006

We present a model in which, due to the quantum nature of the signals controlling the implementation time of successive unitary computational steps, \emph{physical} irreversibility appears in the execution of a \emph{logically} reversible computation.
Applying Part-of-Seech Enhanced LSA to Automatic Essay Grading
Venue: arXiv cs.IR 2006
Year: 2006

Latent Semantic Analysis (LSA) is a widely used Information Retrieval method based on "bag-of-words" assumption. However, according to general conception, syntax plays a role in representing meaning of sentences. Thus, enhancing LSA with part-of-speech (POS) information to capture the context of word occurrences appears to be theoretically feasible extension. The approach is tested empirically on a automatic essay grading system using LSA for document similarity comparisons. A comparison on several POS-enhanced LSA models is reported. Our findings show that the addition of contextual information in the form of POS tags can raise the accuracy of the LSA-based scoring models up to 10.77 per cent.
Report on article: P=NP Linear programming formulation of the Traveling Salesman Problem
Venue: arXiv cs.CC 2006
Year: 2006

This article presents counter examples for three articles claiming that P=NP. Articles for which it applies are: Moustapha Diaby "P = NP: Linear programming formulation of the traveling salesman problem" and "Equality of complexity classes P and NP: Linear programming formulation of the quadratic assignment problem", and also Sergey Gubin "A Polynomial Time Algorithm for The Traveling Salesman Problem"
The intersection and the union of the asynchronous systems
Venue: arXiv cs.GL 2006
Year: 2006

The asynchronous systems $f$ are the models of the asynchronous circuits from digital electrical engineering. They are multi-valued functions that associate to each input $u:\mathbf{R}\to \{0,1\}^{m}$ a set of states $x\in f(u),$ where $x:\mathbf{R}\to \{0,1\}^{n}.$ The intersection of the systems allows adding supplementary conditions in modeling and the union of the systems allows considering the validity of one of two systems in modeling, for example when testing the asynchronous circuits and the circuit is supposed to be 'good' or 'bad'. The purpose of the paper is that of analyzing the intersection and the union against the initial/final states, initial/final time, initial/final state functions, subsystems, dual systems, inverse systems, Cartesian product of systems, parallel connection and serial connection of systems.
On Bounds for $E$-capacity of DMC
Venue: arXiv cs.IT 2006
Year: 2006

Random coding, expurgated and sphere packing bounds are derived by method of types and method of graph decomposition for $E$-capacity of discrete memoryless channel (DMC). Three decoding rules are considered, the random coding bound is attainable by each of the three rules, but the expurgated bound is achievable only by maximum-likelihood decoding. Sphere packing bound is obtained by very simple combinatorial reasonings of the method of types. The paper joins and reviews the results of previous hard achievable publications.
A Concurrent Calculus with Atomic Transactions
Venue: arXiv cs.LO 2006
Year: 2006

The Software Transactional Memory (STM) model is an original approach for controlling concurrent accesses to ressources without the need for explicit lock-based synchronization mechanisms. A key feature of STM is to provide a way to group sequences of read and write actions inside atomic blocks, similar to database transactions, whose whole effect should occur atomically. In this paper, we investigate STM from a process algebra perspective and define an extension of asynchronous CCS with atomic blocks of actions. Our goal is not only to set a formal ground for reasoning on STM implementations but also to understand how this model fits with other concurrency control mechanisms. We also view this calculus as a test bed for extending process calculi with atomic transactions. This is an interesting direction for investigation since, for the most part, actual works that mix transactions with process calculi consider compensating transactions, a model that lacks all the well-known ACID properties. We show that the addition of atomic transactions results in a very expressive calculus, enough to easily encode other concurrent primitives such as guarded choice and multiset-synchronization (à la join-calculus). The correctness of our encodings is proved using a suitable notion of bisimulation equivalence. The equivalence is then applied to prove interesting ``laws of transactions'' and to obtain a simple normal form for transactions.
Grooming of Dynamic Traffic in WDM Star and Tree Networks Using Genetic Algorithm
Venue: arXiv cs.NI 2006
Year: 2006

The advances in WDM technology lead to the great interest in traffic grooming problems. As traffic often changes from time to time, the problem of grooming dynamic traffic is of great practical value. In this paper, we discuss dynamic grooming of traffic in star and tree networks. A genetic algorithm (GA) based approach is proposed to support arbitrary dynamic traffic patterns, which minimizes the number of ADM's and wavelengths. To evaluate the algorithm, tighter bounds are derived. Computer simulation results show that our algorithm is efficient in reducing both the numbers of ADM's and wavelengths in tree and star networks.
Anytime coding on the infinite bandwidth AWGN channel: A sequential semi-orthogonal optimal code
Venue: arXiv cs.IT 2006
Year: 2006

It is well known that orthogonal coding can be used to approach the Shannon capacity of the power-constrained AWGN channel without a bandwidth constraint. This correspondence describes a semi-orthogonal variation of pulse position modulation that is sequential in nature -- bits can be ``streamed across'' without having to buffer up blocks of bits at the transmitter. ML decoding results in an exponentially small probability of error as a function of tolerated receiver delay and thus eventually a zero probability of error on every transmitted bit. In the high-rate regime, a matching upper bound is given on the delay error exponent. We close with some comments on the case with feedback and the connections to the capacity per unit cost problem.
Complexity of Data Flow Analysis for Non-Separable Frameworks
Venue: arXiv cs.PL 2006
Year: 2006

The complexity of round robin method of intraprocedural data flow analysis is measured in number of iterations over the control flow graph. Existing complexity bounds realistically explain the complexity of only Bit-vector frameworks which are separable. In this paper we define the complexity bounds for non-separable frameworks by quantifying the interdependences among the data flow information of program entities using an Entity Dependence Graph.
Presentation Theorems for Coded Character Sets
Venue: arXiv cs.DM 2006
Year: 2006

The notion of 'presentation', as used in combinatorial group theory, is applied to coded character sets(CCSs) - sets which facilitate the interchange of messages in a digital computer network(DCN) . By grouping each element of the set into two portions and using the idea of group presentation(whereby a group is specified by its set of generators and its set of relators), the presentation of a CCS is described. This is illustrated using the Extended Binary Coded Decimal Interchange Code(EBCDIC) which is one of the most popular CCSs in DCNs. Key words: Group presentation, coded character set, digital computer network
On Degree-Based Decentralized Search in Complex Networks
Venue: arXiv cs.PF 2006
Year: 2006

Decentralized search aims to find the target node in a large network by using only local information. The applications of it include peer-to-peer file sharing, web search and anything else that requires locating a specific target in a complex system. In this paper, we examine the degree-based decentralized search method. Specifically, we evaluate the efficiency of the method in different cases with different amounts of available local information. In addition, we propose a simple refinement algorithm for significantly shortening the length of the route that has been found. Some insights useful for the future developments of efficient decentralized search schemes have been achieved.
Linear Abadi and Plotkin Logic
Venue: arXiv cs.LO 2006
Year: 2006

We present a formalization of a version of Abadi and Plotkin's logic for parametricity for a polymorphic dual intuitionistic/linear type theory with fixed points, and show, following Plotkin's suggestions, that it can be used to define a wide collection of types, including existential types, inductive types, coinductive types and general recursive types. We show that the recursive types satisfy a universal property called dinaturality, and we develop reasoning principles for the constructed types. In the case of recursive types, the reasoning principle is a mixed induction/coinduction principle, with the curious property that coinduction holds for general relations, but induction only for a limited collection of ``admissible'' relations. A similar property was observed in Pitts' 1995 analysis of recursive types in domain theory. In a future paper we will develop a category theoretic notion of models of the logic presented here, and show how the results developed in the logic can be transferred to the models.
Evolving controllers for simulated car racing
Venue: arXiv cs.NE 2006
Year: 2006

This paper describes the evolution of controllers for racing a simulated radio-controlled car around a track, modelled on a real physical track. Five different controller architectures were compared, based on neural networks, force fields and action sequences. The controllers use either egocentric (first person), Newtonian (third person) or no information about the state of the car (open-loop controller). The only controller that was able to evolve good racing behaviour was based on a neural network acting on egocentric inputs.
Logic Column 17: A Rendezvous of Logic, Complexity, and Algebra
Venue: arXiv cs.LO 2006
Year: 2006

This article surveys recent advances in applying algebraic techniques to constraint satisfaction problems.
Linear Encodings of Bounded LTL Model Checking
Venue: arXiv cs.LO 2006
Year: 2006

We consider the problem of bounded model checking (BMC) for linear temporal logic (LTL). We present several efficient encodings that have size linear in the bound. Furthermore, we show how the encodings can be extended to LTL with past operators (PLTL). The generalised encoding is still of linear size, but cannot detect minimal length counterexamples. By using the virtual unrolling technique minimal length counterexamples can be captured, however, the size of the encoding is quadratic in the specification. We also extend virtual unrolling to Buchi automata, enabling them to accept minimal length counterexamples. Our BMC encodings can be made incremental in order to benefit from incremental SAT technology. With fairly small modifications the incremental encoding can be further enhanced with a termination check, allowing us to prove properties with BMC. Experiments clearly show that our new encodings improve performance of BMC considerably, particularly in the case of the incremental encoding, and that they are very competitive for finding bugs. An analysis of the liveness-to-safety transformation reveals many similarities to the BMC encodings in this paper. Using the liveness-to-safety translation with BDD-based invariant checking results in an efficient method to find shortest counterexamples that complements the BMC-based approach.
Numerical Simulation guided Lazy Abstraction Refinement for Nonlinear Hybrid Automata
Venue: arXiv cs.LO 2006
Year: 2006

This draft suggests a new counterexample guided abstraction refinement (CEGAR) framework that uses the combination of numerical simulation for nonlinear differential equations with linear programming for linear hybrid automata (LHA) to perform reachability analysis on nonlinear hybrid automata. A notion of $ε-$ structural robustness is also introduced which allows the algorithm to validate counterexamples using numerical simulations. Keywords: verification, model checking, hybrid systems, hybrid automata, robustness, robust hybrid systems, numerical simulation, cegar, abstraction refinement.
A Low-Footprint Class Loading Mechanism for Embedded Java Virtual Machines
Venue: arXiv cs.OS 2006
Year: 2006

This paper shows that it is possible to dramatically reduce the memory consumption of classes loaded in an embedded Java virtual machine without reducing its functionalities. We describe how to pack the constant pool by deleting entries which are only used during the class loading process. We present some benchmarks which demonstrate the efficiency of this mechanism. We finally suggest some additional optimizations which can be applied if some restrictions to the functionalities of the virtual machine can be tolerated.
Large Scale In Silico Screening on Grid Infrastructures
Venue: arXiv cs.DC 2006
Year: 2006

Large-scale grid infrastructures for in silico drug discovery open opportunities of particular interest to neglected and emerging diseases. In 2005 and 2006, we have been able to deploy large scale in silico docking within the framework of the WISDOM initiative against Malaria and Avian Flu requiring about 105 years of CPU on the EGEE, Auvergrid and TWGrid infrastructures. These achievements demonstrated the relevance of large-scale grid infrastructures for the virtual screening by molecular docking. This also allowed evaluating the performances of the grid infrastructures and to identify specific issues raised by large-scale deployment.
Model Theory of Ultrafinitism I: Fuzzy Initial Segments of Arithmetics
Venue: arXiv cs.LO 2006
Year: 2006

This article is the first of an intended series of works on the model theory of Ultrafinitism. It is roughly divided into two parts. The first one addresses some of the issues related to ultrafinitistic programs, as well as some of the core ideas proposed thus far. The second part of the paper presents a model of ultrafinitistic arithmetics based on the notion of fuzzy initial segments of the standard natural numbers series. We also introduce a proof theory and a semantics for ultrafinitism through which feasibly consistent theories can be treated on the same footing as their classically consistent counterparts. We conclude with a brief sketch of a foundational program, that aims at reproducing the transfinite within the finite realm.
Wireless Information-Theoretic Security - Part II: Practical Implementation
Venue: arXiv cs.IT 2006
Year: 2006

In Part I of this two-part paper on confidential communication over wireless channels, we studied the fundamental security limits of quasi-static fading channels from the point of view of outage secrecy capacity with perfect and imperfect channel state information. In Part II, we develop a practical secret key agreement protocol for Gaussian and quasi-static fading wiretap channels. The protocol uses a four-step procedure to secure communications: establish common randomness via an opportunistic transmission, perform message reconciliation, establish a common key via privacy amplification, and use of the key. We introduce a new reconciliation procedure that uses multilevel coding and optimized low density parity check codes which in some cases comes close to achieving the secrecy capacity limits established in Part I. Finally, we develop new metrics for assessing average secure key generation rates and show that our protocol is effective in secure key renewal.
Bounding the Bias of Tree-Like Sampling in IP Topologies
Venue: arXiv cs.NI 2006
Year: 2006

It is widely believed that the Internet's AS-graph degree distribution obeys a power-law form. Most of the evidence showing the power-law distribution is based on BGP data. However, it was recently argued that since BGP collects data in a tree-like fashion, it only produces a sample of the degree distribution, and this sample may be biased. This argument was backed by simulation data and mathematical analysis, which demonstrated that under certain conditions a tree sampling procedure can produce an artificail power-law in the degree distribution. Thus, although the observed degree distribution of the AS-graph follows a power-law, this phenomenon may be an artifact of the sampling process. In this work we provide some evidence to the contrary. We show, by analysis and simulation, that when the underlying graph degree distribution obeys a power-law with an exponent larger than 2, a tree-like sampling process produces a negligible bias in the sampled degree distribution. Furthermore, recent data collected from the DIMES project, which is not based on BGP sampling, indicates that the underlying AS-graph indeed obeys a power-law degree distribution with an exponent larger than 2. By combining this empirical data with our analysis, we conclude that the bias in the degree distribution calculated from BGP data is negligible.
Partially ordered distributed computations on asynchronous point-to-point networks
Venue: arXiv cs.DC 2006
Year: 2006

Asynchronous executions of a distributed algorithm differ from each other due to the nondeterminism in the order in which the messages exchanged are handled. In many situations of interest, the asynchronous executions induced by restricting nondeterminism are more efficient, in an application-specific sense, than the others. In this work, we define partially ordered executions of a distributed algorithm as the executions satisfying some restricted orders of their actions in two different frameworks, those of the so-called event- and pulse-driven computations. The aim of these restrictions is to characterize asynchronous executions that are likely to be more efficient for some important classes of applications. Also, an asynchronous algorithm that ensures the occurrence of partially ordered executions is given for each case. Two of the applications that we believe may benefit from the restricted nondeterminism are backtrack search, in the event-driven case, and iterative algorithms for systems of linear equations, in the pulse-driven case.
Reuse of designs: Desperately seeking an interdisciplinary cognitive approach
Venue: arXiv cs.HC 2006
Year: 2006

This text analyses the papers accepted for the workshop "Reuse of designs: an interdisciplinary cognitive approach". Several dimensions and questions considered as important (by the authors and/or by us) are addressed: What about the "interdisciplinary cognitive" character of the approaches adopted by the authors? Is design indeed a domain where the use of CBR is particularly suitable? Are there important distinctions between CBR and other approaches? Which types of knowledge -other than cases- is being, or might be, used in CBR systems? With respect to cases: are there different "types" of case and different types of case use? which formats are adopted for their representation? do cases have "components"? how are cases organised in the case memory? Concerning their retrieval: which types of index are used? on which types of relation is retrieval based? how does one retrieve only a selected number of cases, i.e., how does one retrieve only the "best" cases? which processes and strategies are used, by the system and by its user? Finally, some important aspects of CBR system development are shortly discussed: should CBR systems be assistance or autonomous systems? how can case knowledge be "acquired"? what about the empirical evaluation of CBR systems? The conclusion points out some lacking points: not much attention is paid to the user, and few papers have indeed adopted an interdisciplinary cognitive approach.
Going Stupid with EcoLab
Venue: arXiv cs.MA 2006
Year: 2006

In 2005, Railsback et al. proposed a very simple model ({\em Stupid Model}) that could be implemented within a couple of hours, and later extended to demonstrate the use of common ABM platform functionality. They provided implementations of the model in several agent based modelling platforms, and compared the platforms for ease of implementation of this simple model, and performance. In this paper, I implement Railsback et al's Stupid Model in the EcoLab simulation platform, a C++ based modelling platform, demonstrating that it is a feasible platform for these sorts of models, and compare the performance of the implementation with Repast, Mason and Swarm versions.