title: On Verifying Complex Properties using Symbolic Shape Analysis

abstract: One of the main challenges in the verification of software systems is the analysis of unbounded data structures with dynamic memory allocation, such as linked data structures and arrays. We describe Bohne, a new analysis for verifying data structures. Bohne verifies data structure operations and shows that 1) the operations preserve data structure invariants and 2) the operations satisfy their specifications expressed in terms of changes to the set of objects stored in the data structure. During the analysis, Bohne infers loop invariants in the form of disjunctions of universally quantified Boolean combinations of formulas. To synthesize loop invariants of this form, Bohne uses a combination of decision procedures for Monadic Second-Order Logic over trees, SMT-LIB decision procedures (currently CVC Lite), and an automated reasoner within the Isabelle interactive theorem prover. This architecture shows that synthesized loop invariants can serve as a useful communication mechanism between different decision procedures. Using Bohne, we have verified operations on data structures such as linked lists with iterators and back pointers, trees with and without parent pointers, two-level skip lists, array data structures, and sorted lists. We have deployed Bohne in the Hob and Jahob data structure analysis systems, enabling us to combine Bohne with analyses of data structure clients and apply it in the context of larger programs. This report describes the Bohne algorithm as well as techniques that Bohne uses to reduce the ammount of annotations and the running time of the analysis.


title: Binomial multichannel algorithm

abstract: The binomial multichannel algorithm is proposed. Some its properties are discussed.


title: Throughput Optimal Distributed Control of Stochastic Wireless Networks

abstract: The Maximum Differential Backlog (MDB) control policy of Tassiulas and Ephremides has been shown to adaptively maximize the stable throughput of multi-hop wireless networks with random traffic arrivals and queueing. The practical implementation of the MDB policy in wireless networks with mutually interfering links, however, requires the development of distributed optimization algorithms. Within the context of CDMA-based multi-hop wireless networks, we develop a set of node-based scaled gradient projection power control algorithms which solves the MDB optimization problem in a distributed manner using low communication overhead. As these algorithms require time to converge to a neighborhood of the optimum, the optimal rates determined by the MDB policy can only be found iteratively over time. For this, we show that the iterative MDB policy with convergence time remains throughput optimal.


title: A multipurpose Hopf deformation of the Algebra of Feynman-like Diagrams

abstract: We construct a three parameter deformation of the Hopf algebra $\mathbf{LDIAG}$. This new algebra is a true Hopf deformation which reduces to $\mathbf{LDIAG}$ on one hand and to $\mathbf{MQSym}$ on the other, relating $\mathbf{LDIAG}$ to other Hopf algebras of interest in contemporary physics. Further, its product law reproduces that of the algebra of polyzeta functions.


title: Generalized Majority-Minority Operations are Tractable

abstract: Generalized majority-minority (GMM) operations are introduced as a common generalization of near unanimity operations and Mal'tsev operations on finite sets. We show that every instance of the constraint satisfaction problem (CSP), where all constraint relations are invariant under a (fixed) GMM operation, is solvable in polynomial time. This constitutes one of the largest tractable cases of the CSP.


title: The recognizability of sets of graphs is a robust property

abstract: 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.


title: Algebraic recognizability of languages

abstract: Recognizable languages of finite words are part of every computer science cursus, and they are routinely described as a cornerstone for applications and for theory. We would like to briefly explore why that is, and how this word-related notion extends to more complex models, such as those developed for modeling distributed or timed behaviors.


title: A State-Based Regression Formulation for Domains with Sensing Actions<br> and Incomplete Information

abstract: We present a state-based regression function for planning domains where an agent does not have complete information and may have sensing actions. We consider binary domains and employ a three-valued characterization of domains with sensing actions to define the regression function. We prove the soundness and completeness of our regression formulation with respect to the definition of progression. More specifically, we show that (i) a plan obtained through regression for a planning problem is indeed a progression solution of that planning problem, and that (ii) for each plan found through progression, using regression one obtains that plan or an equivalent one.


title: A Richer Understanding of the Complexity of Election Systems

abstract: We provide an overview of some recent progress on the complexity of election systems. The issues studied include the complexity of the winner, manipulation, bribery, and control problems.


title: Algebraic recognizability of regular tree languages

abstract: We propose a new algebraic framework to discuss and classify recognizable tree languages, and to characterize interesting classes of such languages. Our algebraic tool, called preclones, encompasses the classical notion of syntactic Sigma-algebra or minimal tree automaton, but adds new expressivity to it. The main result in this paper is a variety theorem \`{a} la Eilenberg, but we also discuss important examples of logically defined classes of recognizable tree languages, whose characterization and decidability was established in recent papers (by Benedikt and S\'{e}goufin, and by Bojanczyk and Walukiewicz) and can be naturally formulated in terms of pseudovarieties of preclones. Finally, this paper constitutes the foundation for another paper by the same authors, where first-order definable tree languages receive an algebraic characterization.


title: A VFRoe scheme for 1D shallow water flows : wetting and drying simulation

abstract: A finite-volume method for the one-dimensional shallow-water equations including topographic source terms is presented. Exploiting an original idea by Leroux, the system of partial-differential equations is completed by a trivial equation for the bathymetry. By applying a change of variable, the system is given a celerity-speed formulation, and linearized. As a result, an approximate Riemann solver preserving the positivity of the celerity can be constructed, permitting wetting and drying flow simulations to be performed. Finally, the simulation of numerical test cases is presented.


title: Measuring Fundamental Properties of Real-World Complex Networks

abstract: Complex networks, modeled as large graphs, received much attention during these last years. However, data on such networks is only available through intricate measurement procedures. Until recently, most studies assumed that these procedures eventually lead to samples large enough to be representative of the whole, at least concerning some key properties. This has crucial impact on network modeling and simulation, which rely on these properties. Recent contributions proved that this approach may be misleading, but no solution has been proposed. We provide here the first practical way to distinguish between cases where it is indeed misleading, and cases where the observed properties may be trusted. It consists in studying how the properties of interest evolve when the sample grows, and in particular whether they reach a steady state or not. In order to illustrate this method and to demonstrate its relevance, we apply it to data-sets on complex network measurements that are representative of the ones commonly used. The obtained results show that the method fulfills its goals very well. We moreover identify some properties which seem easier to evaluate in practice, thus opening interesting perspectives.


title: Theory and Practice of Triangle Problems in Very Large (Sparse (Power-Law)) Graphs

abstract: 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.


title: Constructing LDPC Codes by 2-Lifts

abstract: We propose a new low-density parity-check code construction scheme based on 2-lifts. The proposed codes have an advantage of admitting efficient hardware implementations. With the motivation of designing codes with low error floors, we present an analysis of the low-weight stopping set distributions of the proposed codes. Based on this analysis, we propose design criteria for designing codes with low error floors. Numerical results show that the resulting codes have low error probabilities over binary erasure channels.


title: Duality of Fix-Points for Distributive Lattices

abstract: 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.


title: Verification, Validation and Integrity of Distributed and Interchanged Rule Based Policies and Contracts in the Semantic Web

abstract: Rule-based policy and contract systems have rarely been studied in terms of their software engineering properties. This is a serious omission, because in rule-based policy or contract representation languages rules are being used as a declarative programming language to formalize real-world decision logic and create IS production systems upon. This paper adopts an SE methodology from extreme programming, namely test driven development, and discusses how it can be adapted to verification, validation and integrity testing (V&V&I) of policy and contract specifications. Since, the test-driven approach focuses on the behavioral aspects and the drawn conclusions instead of the structure of the rule base and the causes of faults, it is independent of the complexity of the rule language and the system under test and thus much easier to use and understand for the rule engineer and the user.


title: Rule-based Knowledge Representation for Service Level Agreement

abstract: Automated management and monitoring of service contracts like Service Level Agreements (SLAs) or higher-level policies is vital for efficient and reliable distributed service-oriented architectures (SOA) with high quality of ser-vice (QoS) levels. IT service provider need to manage, execute and maintain thousands of SLAs for different customers and different types of services, which needs new levels of flexibility and automation not available with the current technol-ogy. I propose a novel rule-based knowledge representation (KR) for SLA rules and a respective rule-based service level management (RBSLM) framework. My rule-based approach based on logic programming provides several advantages including automated rule chaining allowing for compact knowledge representation and high levels of automation as well as flexibility to adapt to rapidly changing business requirements. Therewith, I address an urgent need service-oriented busi-nesses do have nowadays which is to dynamically change their business and contractual logic in order to adapt to rapidly changing business environments and to overcome the restricting nature of slow change cycles.


title: Approximating Rate-Distortion Graphs of Individual Data: Experiments in Lossy Compression and Denoising

abstract: Classical rate-distortion theory requires knowledge of an elusive source distribution. Instead, we analyze rate-distortion properties of individual objects using the recently developed algorithmic rate-distortion theory. The latter is based on the noncomputable notion of Kolmogorov complexity. To apply the theory we approximate the Kolmogorov complexity by standard data compression techniques, and perform a number of experiments with lossy compression and denoising of objects from different domains. We also introduce a natural generalization to lossy compression with side information. To maintain full generality we need to address a difficult searching problem. While our solutions are therefore not time efficient, we do observe good denoising and compression performance.


title: Multi-Antenna Cooperative Wireless Systems: A Diversity-Multiplexing Tradeoff Perspective

abstract: We consider a general multiple antenna network with multiple sources, multiple destinations and multiple relays in terms of the diversity-multiplexing tradeoff (DMT). We examine several subcases of this most general problem taking into account the processing capability of the relays (half-duplex or full-duplex), and the network geometry (clustered or non-clustered). We first study the multiple antenna relay channel with a full-duplex relay to understand the effect of increased degrees of freedom in the direct link. We find DMT upper bounds and investigate the achievable performance of decode-and-forward (DF), and compress-and-forward (CF) protocols. Our results suggest that while DF is DMT optimal when all terminals have one antenna each, it may not maintain its good performance when the degrees of freedom in the direct link is increased, whereas CF continues to perform optimally. We also study the multiple antenna relay channel with a half-duplex relay. We show that the half-duplex DMT behavior can significantly be different from the full-duplex case. We find that CF is DMT optimal for half-duplex relaying as well, and is the first protocol known to achieve the half-duplex relay DMT. We next study the multiple-access relay channel (MARC) DMT. Finally, we investigate a system with a single source-destination pair and multiple relays, each node with a single antenna, and show that even under the idealistic assumption of full-duplex relays and a clustered network, this virtual multi-input multi-output (MIMO) system can never fully mimic a real MIMO DMT. For cooperative systems with multiple sources and multiple destinations the same limitation remains to be in effect.


title: Optimal Design of Multiple Description Lattice Vector Quantizers

abstract: In the design of multiple description lattice vector quantizers (MDLVQ), index assignment plays a critical role. In addition, one also needs to choose the Voronoi cell size of the central lattice v, the sublattice index N, and the number of side descriptions K to minimize the expected MDLVQ distortion, given the total entropy rate of all side descriptions Rt and description loss probability p. In this paper we propose a linear-time MDLVQ index assignment algorithm for any K >= 2 balanced descriptions in any dimensions, based on a new construction of so-called K-fraction lattice. The algorithm is greedy in nature but is proven to be asymptotically (N -> infinity) optimal for any K >= 2 balanced descriptions in any dimensions, given Rt and p. The result is stronger when K = 2: the optimality holds for finite N as well, under some mild conditions. For K > 2, a local adjustment algorithm is developed to augment the greedy index assignment, and conjectured to be optimal for finite N. Our algorithmic study also leads to better understanding of v, N and K in optimal MDLVQ design. For K = 2 we derive, for the first time, a non-asymptotical closed form expression of the expected distortion of optimal MDLVQ in p, Rt, N. For K > 2, we tighten the current asymptotic formula of the expected distortion, relating the optimal values of N and K to p and Rt more precisely.


title: The Three Gap Theorem (Steinhauss Conjecture)

abstract: We deal with the distribution of N points placed consecutively around the circle by a fixed angle of a. From the proof of Tony van Ravenstein, we propose a detailed proof of the Steinhaus conjecture whose result is the following: the N points partition the circle into gaps of at most three different lengths. We study the mathematical notions required for the proof of this theorem revealed during a formal proof carried out in Coq.


title: Problem Evolution: A new approach to problem solving systems

abstract: In this paper we present a novel tool to evaluate problem solving systems. Instead of using a system to solve a problem, we suggest using the problem to evaluate the system. By finding a numerical representation of a problem's complexity, one can implement genetic algorithm to search for the most complex problem the given system can solve. This allows a comparison between different systems that solve the same set of problems. In this paper we implement this approach on pattern recognition neural networks to try and find the most complex pattern a given configuration can solve. The complexity of the pattern is calculated using linguistic complexity. The results demonstrate the power of the problem evolution approach in ranking different neural network configurations according to their pattern recognition abilities. Future research and implementations of this technique are also discussed.


title: E-prints and Journal Articles in Astronomy: a Productive Co-existence

abstract: Are the e-prints (electronic preprints) from the arXiv repository being used instead of the journal articles? In this paper we show that the e-prints have not undermined the usage of journal papers in the astrophysics community. As soon as the journal article is published, the astronomical community prefers to read the journal article and the use of e-prints through the NASA Astrophysics Data System drops to zero. This suggests that the majority of astronomers have access to institutional subscriptions and that they choose to read the journal article when given the choice. Within the NASA Astrophysics Data System they are given this choice, because the e-print and the journal article are treated equally, since both are just one click away. In other words, the e-prints have not undermined journal use in the astrophysics community and thus currently do not pose a financial threat to the publishers. We present readership data for the arXiv category "astro-ph" and the 4 core journals in astronomy (Astrophysical Journal, Astronomical Journal, Monthly Notices of the Royal Astronomical Society and Astronomy & Astrophysics). Furthermore, we show that the half-life (the point where the use of an article drops to half the use of a newly published article) for an e-print is shorter than for a journal paper. The ADS is funded by NASA Grant NNG06GG68G. arXiv receives funding from NSF award #0404553


title: On Bus Graph Realizability

abstract: In this paper, we consider the following graph embedding problem: Given a bipartite graph G = (V1; V2;E), where the maximum degree of vertices in V2 is 4, can G be embedded on a two dimensional grid such that each vertex in V1 is drawn as a line segment along a grid line, each vertex in V2 is drawn as a point at a grid point, and each edge e = (u; v) for some u 2 V1 and v 2 V2 is drawn as a line segment connecting u and v, perpendicular to the line segment for u? We show that this problem is NP-complete, and sketch how our proof techniques can be used to show the hardness of several other related problems.


title: Max-Cut and Max-Bisection are NP-hard on unit disk graphs

abstract: We prove that the Max-Cut and Max-Bisection problems are NP-hard on unit disk graphs. We also show that $\lambda$-precision graphs are planar for $\lambda$ > 1 / \sqrt{2}$.


title: One approach to the digital visualization of hedgehogs in holomorphic dynamics

abstract: In the field of holomorphic dynamics in one complex variable, hedgehog is the local invariant set arising about a Cremer point and endowed with a very complicate shape as well as relating to very weak numerical conditions. We give a solution to the open problem of its digital visualization, featuring either a time saving approach and a far-reaching insight.


title: A Predicative Harmonization of the Time and Provable Hierarchies

abstract: A decidable transfinite hierarchy is defined by assigning ordinals to the programs of an imperative language. It singles out: the classes TIMEF(n^c) and TIMEF(n_c); the finite Grzegorczyk classes at and above the elementary level, and the \Sigma_k-IND fragments of PA. Limited operators, diagonalization, and majorization functions are not used.


title: A Fast Block Matching Algorithm for Video Motion Estimation Based on Particle Swarm Optimization and Motion Prejudgment

abstract: In this paper, we propose a fast 2-D block-based motion estimation algorithm called Particle Swarm Optimization - Zero-motion Prejudgment(PSO-ZMP) which consists of three sequential routines: 1)Zero-motion prejudgment. The routine aims at finding static macroblocks(MB) which do not need to perform remaining search thus reduces the computational cost; 2)Predictive image coding and 3)PSO matching routine. Simulation results obtained show that the proposed PSO-ZMP algorithm achieves over 10 times of computation less than Diamond Search(DS) and 5 times less than the recent proposed Adaptive Rood Pattern Searching(ARPS). Meanwhile the PSNR performances using PSO-ZMP are very close to that using DS and ARPS in some less-motioned sequences. While in some sequences containing dense and complex motion contents, the PSNR performances of PSO-ZMP are several dB lower than that using DS and ARPS but in an acceptable degree.


title: Semantic Description of Parameters in Web Service Annotations

abstract: A modification of OWL-S regarding parameter description is proposed. It is strictly based on Description Logic. In addition to class description of parameters it also allows the modelling of relations between parameters and the precise description of the size of data to be supplied to a service. In particular, it solves two major issues identified within current proposals for a Semantic Web Service annotation standard.


title: An application-oriented terminology evaluation: the case of back-of-the book indexes

abstract: This paper addresses the problem of computational terminology evaluation not per se but in a specific application context. This paper describes the evaluation procedure that has been used to assess the validity of our overall indexing approach and the quality of the IndDoc indexing tool. Even if user-oriented extended evaluation is irreplaceable, we argue that early evaluations are possible and they are useful for development guidance.


title: Using NLP to build the hypertextuel network of a back-of-the-book index

abstract: Relying on the idea that back-of-the-book indexes are traditional devices for navigation through large documents, we have developed a method to build a hypertextual network that helps the navigation in a document. Building such an hypertextual network requires selecting a list of descriptors, identifying the relevant text segments to associate with each descriptor and finally ranking the descriptors and reference segments by relevance order. We propose a specific document segmentation method and a relevance measure for information ranking. The algorithms are tested on 4 corpora (of different types and domains) without human intervention or any semantic knowledge.


title: Event-based Information Extraction for the biomedical domain: the Caderige project

abstract: This paper gives an overview of the Caderige project. This project involves teams from different areas (biology, machine learning, natural language processing) in order to develop high-level analysis tools for extracting structured information from biological bibliographical databases, especially Medline. The paper gives an overview of the approach and compares it to the state of the art.


title: The ALVIS Format for Linguistically Annotated Documents

abstract: The paper describes the ALVIS annotation format designed for the indexing of large collections of documents in topic-specific search engines. This paper is exemplified on the biological domain and on MedLine abstracts, as developing a specialized search engine for biologists is one of the ALVIS case studies. The ALVIS principle for linguistic annotations is based on existing works and standard propositions. We made the choice of stand-off annotations rather than inserted mark-up. Annotations are encoded as XML elements which form the linguistic subsection of the document record.


title: Ontologies and Information Extraction

abstract: This report argues that, even in the simplest cases, IE is an ontology-driven process. It is not a mere text filtering method based on simple pattern matching and keywords, because the extracted pieces of texts are interpreted with respect to a predefined partial domain model. This report shows that depending on the nature and the depth of the interpretation to be done for extracting the information, more or less knowledge must be involved. This report is mainly illustrated in biology, a domain in which there are critical needs for content-based exploration of the scientific literature and which becomes a major application domain for IE.


title: MDL Denoising Revisited

abstract: We refine and extend an earlier MDL denoising criterion for wavelet-based denoising. We start by showing that the denoising problem can be reformulated as a clustering problem, where the goal is to obtain separate clusters for informative and non-informative wavelet coefficients, respectively. This suggests two refinements, adding a code-length for the model index, and extending the model in order to account for subband-dependent coefficient distributions. A third refinement is derivation of soft thresholding inspired by predictive universal coding with weighted mixtures. We propose a practical method incorporating all three refinements, which is shown to achieve good performance and robustness in denoising both artificial and natural signals.


title: The Capacity of Channels with Feedback

abstract: We introduce a general framework for treating channels with memory and feedback. First, we generalize Massey's concept of directed information and use it to characterize the feedback capacity of general channels. Second, we present coding results for Markov channels. This requires determining appropriate sufficient statistics at the encoder and decoder. Third, a dynamic programming framework for computing the capacity of Markov channels is presented. Fourth, it is shown that the average cost optimality equation (ACOE) can be viewed as an implicit single-letter characterization of the capacity. Fifth, scenarios with simple sufficient statistics are described.


title: Motion Primitives for Robotic Flight Control

abstract: We introduce a simple framework for learning aggressive maneuvers in flight control of UAVs. Having inspired from biological environment, dynamic movement primitives are analyzed and extended using nonlinear contraction theory. Accordingly, primitives of an observed movement are stably combined and concatenated. We demonstrate our results experimentally on the Quanser Helicopter, in which we first imitate aggressive maneuvers and then use them as primitives to achieve new maneuvers that can fly over an obstacle.


title: Polygon Convexity: A Minimal O(n) Test

abstract: 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.


title: Modular self-organization

abstract: The aim of this paper is to provide a sound framework for addressing a difficult problem: the automatic construction of an autonomous agent's modular architecture. We combine results from two apparently uncorrelated domains: Autonomous planning through Markov Decision Processes and a General Data Clustering Approach using a kernel-like method. Our fundamental idea is that the former is a good framework for addressing autonomy whereas the latter allows to tackle self-organizing problems.


title: ECA-LP / ECA-RuleML: A Homogeneous Event-Condition-Action Logic Programming Language

abstract: Event-driven reactive functionalities are an urgent need in nowadays distributed service-oriented applications and (Semantic) Web-based environments. An important problem to be addressed is how to correctly and efficiently capture and process the event-based behavioral, reactive logic represented as ECA rules in combination with other conditional decision logic which is represented as derivation rules. In this paper we elaborate on a homogeneous integration approach which combines derivation rules, reaction rules (ECA rules) and other rule types such as integrity constraint into the general framework of logic programming. The developed ECA-LP language provides expressive features such as ID-based updates with support for external and self-updates of the intensional and extensional knowledge, transac-tions including integrity testing and an event algebra to define and process complex events and actions based on a novel interval-based Event Calculus variant.


title: The Management and Integration of Biomedical Knowledge: Application in the Health-e-Child Project (Position Paper)

abstract: The Health-e-Child project aims to develop an integrated healthcare platform for European paediatrics. In order to achieve a comprehensive view of childrens health, a complex integration of biomedical data, information, and knowledge is necessary. Ontologies will be used to formally define this domain knowledge and will form the basis for the medical knowledge management system. This paper introduces an innovative methodology for the vertical integration of biomedical knowledge. This approach will be largely clinician-centered and will enable the definition of ontology fragments, connections between them (semantic bridges) and enriched ontology fragments (views). The strategy for the specification and capture of fragments, bridges and views is outlined with preliminary examples demonstrated in the collection of biomedical information from hospital databases, biomedical ontologies, and biomedical public databases.


title: A Semidefinite Relaxation for Air Traffic Flow Scheduling

abstract: We first formulate the problem of optimally scheduling air traffic low with sector capacity constraints as a mixed integer linear program. We then use semidefinite relaxation techniques to form a convex relaxation of that problem. Finally, we present a randomization algorithm to further improve the quality of the solution. Because of the specific structure of the air traffic flow problem, the relaxation has a single semidefinite constraint of size dn where d is the maximum delay and n the number of flights.


title: A Combinatorial Family of Near Regular LDPC Codes

abstract: 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.


title: Identifying Crosscutting Concerns Using Fan-in Analysis

abstract: Aspect mining is a reverse engineering process that aims at finding crosscutting concerns in existing systems. This paper proposes an aspect mining approach based on determining methods that are called from many different places, and hence have a high fan-in, which can be seen as a symptom of crosscutting functionality. The approach is semi-automatic, and consists of three steps: metric calculation, method filtering, and call site analysis. Carrying out these steps is an interactive process supported by an Eclipse plug-in called FINT. Fan-in analysis has been applied to three open source Java systems, totaling around 200,000 lines of code. The most interesting concerns identified are discussed in detail, which includes several concerns not previously discussed in the aspect-oriented literature. The results show that a significant number of crosscutting concerns can be recognized using fan-in analysis, and each of the three steps can be supported by tools.


title: Pseudo-Codeword Performance Analysis for LDPC Convolutional Codes

abstract: Message-passing iterative decoders for low-density parity-check (LDPC) block codes are known to be subject to decoding failures due to so-called pseudo-codewords. These failures can cause the large signal-to-noise ratio performance of message-passing iterative decoding to be worse than that predicted by the maximum-likelihood decoding union bound. In this paper we address the pseudo-codeword problem from the convolutional-code perspective. In particular, we compare the performance of LDPC convolutional codes with that of their ``wrapped'' quasi-cyclic block versions and we show that the minimum pseudo-weight of an LDPC convolutional code is at least as large as the minimum pseudo-weight of an underlying quasi-cyclic code. This result, which parallels a well-known relationship between the minimum Hamming weight of convolutional codes and the minimum Hamming weight of their quasi-cyclic counterparts, is due to the fact that every pseudo-codeword in the convolutional code induces a pseudo-codeword in the block code with pseudo-weight no larger than that of the convolutional code's pseudo-codeword. This difference in the weight spectra leads to improved performance at low-to-moderate signal-to-noise ratios for the convolutional code, a conclusion supported by simulation results.


title: Dynamic Spectrum Access: Signal Processing, Networking, and Regulatory Policy

abstract: In this article, we first provide a taxonomy of dynamic spectrum access. We then focus on opportunistic spectrum access, the overlay approach under the hierarchical access model of dynamic spectrum access. we aim to provide an overview of challenges and recent developments in both technological and regulatory aspects of opportunistic spectrum access.


title: Modelling and Simulation of Scheduling Policies Implemented in Ethernet Switch by Using Coloured Petri Nets

abstract: The objective of this paper is to propose models enabling to study the behaviour of Ethernet switch for Networked Control Systems. Two scheduler policies are analyzed: the static priority and the WRR (Weighted Round Robin). The modelling work is based on Coloured Petri Nets. A temporal validation step based on the simulation of these modelling, shows that the obtained results are near to the expected behaviour of these scheduler policies.


title: Control compensation based on upper bound delay in networked control systems

abstract: 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.


title: Use of upper bound delay estimate in stability analysis and robust control compensation in networked control systems

abstract: Recent interest in networked control systems (NCS) has instigated research in various areas of both communication networks and control. The analysis of NCS has often been performed either from the network, or the control point of view and not many papers exist were the analysis of both is done in the same context. Here a simple overall analysis is presented. In the paper the procedure of obtaining the upper bound delay value in the switched Ethernet network is proposed and the obtained delay estimate is used in stability analysis of the feedback loop and in the control compensation. The upper bound delay algorithm is based on the network calculus theory, the stability analysis uses the small gain theorem, and control compensating strategy is based on Smith predictor, where however the upper bound delay is utilised in obtaining the delay estimate.


title: Mining Generalized Graph Patterns based on User Examples

abstract: There has been a lot of recent interest in mining patterns from graphs. Often, the exact structure of the patterns of interest is not known. This happens, for example, when molecular structures are mined to discover fragments useful as features in chemical compound classification task, or when web sites are mined to discover sets of web pages representing logical documents. Such patterns are often generated from a few small subgraphs (cores), according to certain generalization rules (GRs). We call such patterns "generalized patterns"(GPs). While being structurally different, GPs often perform the same function in the network. Previously proposed approaches to mining GPs either assumed that the cores and the GRs are given, or that all interesting GPs are frequent. These are strong assumptions, which often do not hold in practical applications. In this paper, we propose an approach to mining GPs that is free from the above assumptions. Given a small number of GPs selected by the user, our algorithm discovers all GPs similar to the user examples. First, a machine learning-style approach is used to find the cores. Second, generalizations of the cores in the graph are computed to identify GPs. Evaluation on synthetic data, generated using real cores and GRs from biological and web domains, demonstrates effectiveness of our approach.


title: Loop Calculus Helps to Improve Belief Propagation and Linear Programming Decodings of Low-Density-Parity-Check Codes

abstract: We illustrate the utility of the recently developed loop calculus for improving the Belief Propagation (BP) algorithm. If the algorithm that minimizes the Bethe free energy fails we modify the free energy by accounting for a critical loop in a graphical representation of the code. The log-likelihood specific critical loop is found by means of the loop calculus. The general method is tested using an example of the Linear Programming (LP) decoding, that can be viewed as a special limit of the BP decoding. Considering the (155,64,20) code that performs over Additive-White-Gaussian-Noise channel we show that the loop calculus improves the LP decoding and corrects all previously found dangerous configurations of log-likelihoods related to pseudo-codewords with low effective distance, thus reducing the code's error-floor.

categories: cs.IT cond-mat.dis-nn cond-mat.stat-mech math.IT


title: Detection of Markov Random Fields on Two-Dimensional Intersymbol Interference Channels

abstract: We present a novel iterative algorithm for detection of binary Markov random fields (MRFs) corrupted by two-dimensional (2D) intersymbol interference (ISI) and additive white Gaussian noise (AWGN). We assume a first-order binary MRF as a simple model for correlated images. We assume a 2D digital storage channel, where the MRF is interleaved before being written and then read by a 2D transducer; such channels occur in recently proposed optical disk storage systems. The detection algorithm is a concatenation of two soft-input/soft-output (SISO) detectors: an iterative row-column soft-decision feedback (IRCSDF) ISI detector, and a MRF detector. The MRF detector is a SISO version of the stochastic relaxation algorithm by Geman and Geman in IEEE Trans. Pattern Anal. and Mach. Intell., Nov. 1984. On the 2 x 2 averaging-mask ISI channel, at a bit error rate (BER) of 10^{-5}, the concatenated algorithm achieves SNR savings of between 0.5 and 2.0 dB over the IRCSDF detector alone; the savings increase as the MRFs become more correlated, or as the SNR decreases. The algorithm is also fairly robust to mismatches between the assumed and actual MRF parameters.


title: Entangled Graphs

abstract: In this paper we prove a separability criterion for mixed states in $\mathbb C^p\otimes\mathbb C^q$. We also show that the density matrix of a graph with only one entangled edge is entangled.


title: Sensor Scheduling for Optimal Observability Using Estimation Entropy

abstract: We consider sensor scheduling as the optimal observability problem for partially observable Markov decision processes (POMDP). This model fits to the cases where a Markov process is observed by a single sensor which needs to be dynamically adjusted or by a set of sensors which are selected one at a time in a way that maximizes the information acquisition from the process. Similar to conventional POMDP problems, in this model the control action is based on all past measurements; however here this action is not for the control of state process, which is autonomous, but it is for influencing the measurement of that process. This POMDP is a controlled version of the hidden Markov process, and we show that its optimal observability problem can be formulated as an average cost Markov decision process (MDP) scheduling problem. In this problem, a policy is a rule for selecting sensors or adjusting the measuring device based on the measurement history. Given a policy, we can evaluate the estimation entropy for the joint state-measurement processes which inversely measures the observability of state process for that policy. Considering estimation entropy as the cost of a policy, we show that the problem of finding optimal policy is equivalent to an average cost MDP scheduling problem where the cost function is the entropy function over the belief space. This allows the application of the policy iteration algorithm for finding the policy achieving minimum estimation entropy, thus optimum observability.


title: A Fast Image Encryption Scheme based on Chaotic Standard Map

abstract: In recent years, a variety of effective chaos-based image encryption schemes have been proposed. The typical structure of these schemes has the permutation and the diffusion stages performed alternatively. The confusion and diffusion effect is solely contributed by the permutation and the diffusion stage, respectively. As a result, more overall rounds than necessary are required to achieve a certain level of security. In this paper, we suggest to introduce certain diffusion effect in the confusion stage by simple sequential add-and-shift operations. The purpose is to reduce the workload of the time-consuming diffusion part so that fewer overall rounds and hence a shorter encryption time is needed. Simulation results show that at a similar performance level, the proposed cryptosystem needs less than one-third the encryption time of an existing cryptosystem. The effective acceleration of the encryption speed is thus achieved.


title: Duality for Several Families of Evaluation Codes

abstract: 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.


title: Redundancies of Correction-Capability-Optimized Reed-Muller Codes

abstract: This article is focused on some variations of Reed-Muller codes that yield improvements to the rate for a prescribed decoding performance under the Berlekamp-Massey-Sakata algorithm with majority voting. Explicit formulas for the redundancies of the new codes are given.


title: The Order Bound on the Minimum Distance of the One-Point Codes Associated to a Garcia-Stichtenoth Tower of Function Fields

abstract: Garcia and Stichtenoth discovered two towers of function fields that meet the Drinfeld-Vl\u{a}du\c{t} 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.


title: On Semigroups Generated by Two Consecutive Integers and Improved Hermitian Codes

abstract: Analysis of the Berlekamp-Massey-Sakata algorithm for decoding one-point codes leads to two methods for improving code rate. One method, due to Feng and Rao, removes parity checks that may be recovered by their majority voting algorithm. The second method is to design the code to correct only those error vectors of a given weight that are also geometrically generic. In this work, formulae are given for the redundancies of Hermitian codes optimized with respect to these criteria as well as the formula for the order bound on the minimum distance. The results proceed from an analysis of numerical semigroups generated by two consecutive integers. The formula for the redundancy of optimal Hermitian codes correcting a given number of errors answers an open question stated by Pellikaan and Torres in 1999.


title: Labeling Schemes with Queries

abstract: We study the question of ``how robust are the known lower bounds of labeling schemes when one increases the number of consulted labels''. Let $f$ be a function on pairs of vertices. An $f$-labeling scheme for a family of graphs $\cF$ labels the vertices of all graphs in $\cF$ such that for every graph $G\in\cF$ and every two vertices $u,v\in G$, the value $f(u,v)$ can be inferred by merely inspecting the labels of $u$ and $v$. This paper introduces a natural generalization: the notion of $f$-labeling schemes with queries, in which the value $f(u,v)$ can be inferred by inspecting not only the labels of $u$ and $v$ but possibly the labels of some additional vertices. We show that inspecting the label of a single additional vertex (one {\em query}) enables us to reduce the label size of many labeling schemes significantly.


title: Conditional Expressions for Blind Deconvolution: Multi-point form

abstract: We present conditional expression (CE) for finding blurs convolved in given images. The CE is given in terms of the zero-values of the blurs evaluated at multi-point. The CE can detect multiple blur all at once. We illustrate the multiple blur-detection by using a test image.


title: Simple method to eliminate blur based on Lane and Bates algorithm

abstract: A simple search method for finding a blur convolved in a given image is presented. The method can be easily extended to a large blur. The method has been experimentally tested with a model blurred image.


title: Private Approximate Heavy Hitters

abstract: We consider the problem of private computation of approximate Heavy Hitters. Alice and Bob each hold a vector and, in the vector sum, they want to find the B largest values along with their indices. While the exact problem requires linear communication, protocols in the literature solve this problem approximately using polynomial computation time, polylogarithmic communication, and constantly many rounds. We show how to solve the problem privately with comparable cost, in the sense that nothing is learned by Alice and Bob beyond what is implied by their input, the ideal top-B output, and goodness of approximation (equivalently, the Euclidean norm of the vector sum). We give lower bounds showing that the Euclidean norm must leak by any efficient algorithm.


title: Updates in Answer Set Programming: An Approach Based on Basic Structural Properties

abstract: We have studied the update operator defined for update sequences by Eiter et al. without tautologies and we have observed that it satisfies an interesting property This property, which we call Weak Independence of Syntax (WIS), is similar to one of the postulates proposed by Alchourron, Gardenfors, and Makinson (AGM); only that in this case it applies to nonmonotonic logic. In addition, we consider other five additional basic properties about update programs and we show that the operator of Eiter et al. satisfies them. This work continues the analysis of the AGM postulates under a refined view that considers nelson logic as a monotonic logic which allows us to expand our understanding of answer sets. Moreover, nelson logic helped us to derive an alternative definition of the operator defined by Eiter et al. avoiding the use of unnecessary extra atoms.


title: Practical Entropy-Compressed Rank/Select Dictionary

abstract: 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.


title: Conditional Expressions for Blind Deconvolution: Derivative form

abstract: We developed novel conditional expressions (CEs) for Lane and Bates' blind deconvolution. The CEs are given in term of the derivatives of the zero-values of the z-transform of given images. The CEs make it possible to automatically detect multiple blur convolved in the given images all at once without performing any analysis of the zero-sheets of the given images. We illustrate the multiple blur-detection by the CEs for a model image


title: Embedding Metrics into Ultrametrics and Graphs into Spanning Trees with Constant Average Distortion

abstract: This paper addresses the basic question of how well can a tree approximate distances of a metric space or a graph. Given a graph, the problem of constructing a spanning tree in a graph which strongly preserves distances in the graph is a fundamental problem in network design. We present scaling distortion embeddings where the distortion scales as a function of $\epsilon$, with the guarantee that for each $\epsilon$ the distortion of a fraction $1-\epsilon$ of all pairs is bounded accordingly. Such a bound implies, in particular, that the \emph{average distortion} and $\ell_q$-distortions are small. Specifically, our embeddings have \emph{constant} average distortion and $O(\sqrt{\log n})$ $\ell_2$-distortion. This follows from the following results: we prove that any metric space embeds into an ultrametric with scaling distortion $O(\sqrt{1/\epsilon})$. For the graph setting we prove that any weighted graph contains a spanning tree with scaling distortion $O(\sqrt{1/\epsilon})$. These bounds are tight even for embedding in arbitrary trees. For probabilistic embedding into spanning trees we prove a scaling distortion of $\tilde{O}(\log^2 (1/\epsilon))$, which implies \emph{constant} $\ell_q$-distortion for every fixed $q<\infty$.


title: Rapport technique du projet OGRE

abstract: This repport concerns automatic understanding of (french) iterative sentences, i.e. sentences where one single verb has to be interpreted by a more or less regular plurality of events. A linguistic analysis is proposed along an extension of Reichenbach's theory, several formal representations are considered and a corpus of 18000 newspaper extracts is described.


title: Domain Wall Displacement Detection Technology Research Report

abstract: This article introduce a new data storage method called DWDD(Domain Wall Displacement Detection) and tell you why it succeed.


title: A Typed Hybrid Description Logic Programming Language with Polymorphic Order-Sorted DL-Typed Unification for Semantic Web Type Systems

abstract: In this paper we elaborate on a specific application in the context of hybrid description logic programs (hybrid DLPs), namely description logic Semantic Web type systems (DL-types) which are used for term typing of LP rules based on a polymorphic, order-sorted, hybrid DL-typed unification as procedural semantics of hybrid DLPs. Using Semantic Web ontologies as type systems facilitates interchange of domain-independent rules over domain boundaries via dynamically typing and mapping of explicitly defined type ontologies.


title: Full Text Searching in the Astrophysics Data System

abstract: The Smithsonian/NASA Astrophysics Data System (ADS) provides a search system for the astronomy and physics scholarly literature. All major and many smaller astronomy journals that were published on paper have been scanned back to volume 1 and are available through the ADS free of charge. All scanned pages have been converted to text and can be searched through the ADS Full Text Search System. In addition, searches can be fanned out to several external search systems to include the literature published in electronic form. Results from the different search systems are combined into one results list. The ADS Full Text Search System is available at: http://adsabs.harvard.edu/fulltext_service.html


title: Connectivity in the Astronomy Digital Library

abstract: The Astrophysics Data System (ADS) provides an extensive system of links between the literature and other on-line information. Recently, the journals of the American Astronomical Society (AAS) and a group of NASA data centers have collaborated to provide more links between on-line data obtained by space missions and the on-line journals. Authors can now specify which data sets they have used in their article. This information is used by the participants to provide the links between the literature and the data. The ADS is available at: http://ads.harvard.edu


title: VPSPACE and a Transfer Theorem over the Reals

abstract: We introduce a new class VPSPACE of families of polynomials. Roughly speaking, a family of polynomials is in VPSPACE if its coefficients can be computed in polynomial space. Our main theorem is that if (uniform, constant-free) VPSPACE families can be evaluated efficiently then the class PAR of decision problems that can be solved in parallel polynomial time over the real numbers collapses to P. As a result, one must first be able to show that there are VPSPACE families which are hard to evaluate in order to separate over the reals P from NP, or even from PAR.


title: One-Pass, One-Hash n-Gram Statistics Estimation

abstract: In multimedia, text or bioinformatics databases, applications query sequences of n consecutive symbols called n-grams. Estimating the number of distinct n-grams is a view-size estimation problem. While view sizes can be estimated by sampling under statistical assumptions, we desire an unassuming algorithm with universally valid accuracy bounds. Most related work has focused on repeatedly hashing the data, which is prohibitive for large data sources. We prove that a one-pass one-hash algorithm is sufficient for accurate estimates if the hashing is sufficiently independent. To reduce costs further, we investigate recursive random hashing algorithms and show that they are sufficiently independent in practice. We compare our running times with exact counts using suffix arrays and show that, while we use hardly any storage, we are an order of magnitude faster. The approach further is extended to a one-pass/one-hash computation of n-gram entropy and iceberg counts. The experiments use a large collection of English text from the Gutenberg Project as well as synthetic data.


title: Creation and use of Citations in the ADS

abstract: 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.


title: On Shift Sequences for Interleaved Construction of Sequence Sets with Low Correlation

abstract: Construction of signal sets with low correlation property is of interest to designers of CDMA systems. One of the preferred ways of constructing such sets is the interleaved construction which uses two sequences a and b with 2-level autocorrelation and a shift sequence e. The shift sequence has to satisfy certain conditions for the resulting signal set to have low correlation properties. This article shows that the conditions reported in literature are too strong and gives a version which results in more number of shift sequences. An open problem on the existence of shift sequences for attaining an interleaved set with maximum correlation value bounded by v+2 is also taken up and solved.


title: Cooperative Processes for Scientific Workflows

abstract: The work described in this paper is a contribution to the problems of managing in data-intensive scientific applications. First, we discuss scientific workflows and motivate there use in scientific applications. Then, we introduce the concept of cooperative processes and describe their interactions and uses in a flexible cooperative workflow system called \textit{Bonita}. Finally, we propose an approach to integrate and synthesize the data exchanged by the mapping of data-intensive science into Bonita, using a binary approach, and illustrate the endeavors done to enhance the performance computations within a dynamic environment.


title: Implementing a Unification Algorithm for Protocol Analysis with XOR

abstract: In this paper, we propose a unification algorithm for the theory $E$ which combines unification algorithms for $E\_{\std}$ and $E\_{\ACUN}$ (ACUN properties, like XOR) but compared to the more general combination methods uses specific properties of the equational theories for further optimizations. Our optimizations drastically reduce the number of non-deterministic choices, in particular those for variable identification and linear orderings. This is important for reducing both the runtime of the unification algorithm and the number of unifiers in the complete set of unifiers. We emphasize that obtaining a ``small'' set of unifiers is essential for the efficiency of the constraint solving procedure within which the unification algorithm is used. The method is implemented in the CL-Atse tool for security protocol analysis.


title: Why did the accident happen? A norm-based reasoning approach

abstract: 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.


title: Norm Based Causal Reasoning in Textual Corpus

abstract: Truth based entailments are not sufficient for a good comprehension of NL. In fact, it can not deduce implicit information necessary to understand a text. On the other hand, norm based entailments are able to reach this goal. This idea was behind the development of Frames (Minsky 75) and Scripts (Schank 77, Schank 79) in the 70's. But these theories are not formalized enough and their adaptation to new situations is far from being obvious. In this paper, we present a reasoning system which uses norms in a causal reasoning process in order to find the cause of an accident from a text describing it.


title: A Quasigroup Based Cryptographic System

abstract: This paper presents a quasigroup encryptor that has very good scrambling properties. We show that the output of the encryptor maximizes the output entropy and the encrypted output for constant and random inputs is very similar. The system architecture of the quasigroup encryptor and the autocorrelation properties of the output sequences are provided.


title: Raisonnement stratifi\'{e} \`{a} base de normes pour inf\'{e}rer les causes dans un corpus textuel

abstract: To understand texts written in natural language (LN), we use our knowledge about the norms of the domain. Norms allow to infer more implicit information from the text. This kind of information can, in general, be defeasible, but it remains useful and acceptable while the text do not contradict it explicitly. In this paper we describe a non-monotonic reasoning system based on the norms of the car crash domain. The system infers the cause of an accident from its textual description. The cause of an accident is seen as the most specific norm which has been violated. The predicates and the rules of the system are stratified: organized on layers in order to obtain an efficient reasoning.


title: NectaRSS, an RSS feed ranking system that implicitly learns user preferences

abstract: In this paper a new RSS feed ranking method called NectaRSS is introduced. The system recommends information to a user based on his/her past choices. User preferences are automatically acquired, avoiding explicit feedback, and ranking is based on those preferences distilled to a user profile. NectaRSS uses the well-known vector space model for user profiles and new documents, and compares them using information-retrieval techniques, but introduces a novel method for user profile creation and adaptation from users' past choices. The efficiency of the proposed method has been tested by embedding it into an intelligent aggregator (RSS feed reader), which has been used by different and heterogeneous users. Besides, this paper proves that the ranking of newsitems yielded by NectaRSS improves its quality with user's choices, and its superiority over other algorithms that use a different information representation method.


title: XString: XML as a String

abstract: Extensible markup language (XML) is a technology that has been much hyped, so that XML has become an industry buzzword. Behind the hype is a powerful technology for data representation in a platform independent manner. As a text document, however, XML suffers from being too bloated, and requires an XML parser to access and manipulate it. XString is an encoding method for XML, in essence, a markup language's markup language. XString gives the benefit of compressing XML, and allows for easy manipulation and processing of XML source as a very long string.


title: On the Fading Paper Achievable Region of the Fading MIMO Broadcast Channel

abstract: 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.


title: Iterative Decoding of Low-Density Parity Check Codes (A Survey)

abstract: Much progress has been made on decoding algorithms for error-correcting codes in the last decade. In this article, we give an introduction to some fundamental results on iterative, message-passing algorithms for low-density parity check codes. For certain important stochastic channels, this line of work has enabled getting very close to Shannon capacity with algorithms that are extremely efficient (both in theory and practice).


title: Une exp\'{e}rience de s\'{e}mantique inf\'{e}rentielle

abstract: We develop a system which must be able to perform the same inferences that a human reader of an accident report can do and more particularly to determine the apparent causes of the accident. We describe the general framework in which we are situated, linguistic and semantic levels of the analysis and the inference rules used by the system.


title: Network calculus based FDI approach for switched Ethernet architecture

abstract: 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.


title: Low Correlation Sequences over the QAM Constellation

abstract: This paper presents the first concerted look at low correlation sequence families over QAM constellations of size M^2=4^m and their potential applicability as spreading sequences in a CDMA setting. Five constructions are presented, and it is shown how such sequence families have the ability to transport a larger amount of data as well as enable variable-rate signalling on the reverse link. Canonical family CQ has period N, normalized maximum-correlation parameter theta_max bounded above by A sqrt(N), where 'A' ranges from 1.8 in the 16-QAM case to 3.0 for large M. In a CDMA setting, each user is enabled to transfer 2m bits of data per period of the spreading sequence which can be increased to 3m bits of data by halving the size of the sequence family. The technique used to construct CQ is easily extended to produce larger sequence families and an example is provided. Selected family SQ has a lower value of theta_max but permits only (m+1)-bit data modulation. The interleaved 16-QAM sequence family IQ has theta_max <= sqrt(2) sqrt(N) and supports 3-bit data modulation. The remaining two families are over a quadrature-PAM (Q-PAM) subset of size 2M of the M^2-QAM constellation. Family P has a lower value of theta_max in comparison with Family SQ, while still permitting (m+1)-bit data modulation. Interleaved family IP, over the 8-ary Q-PAM constellation, permits 3-bit data modulation and interestingly, achieves the Welch lower bound on theta_max.


title: Covering selfish machines

abstract: We consider the machine covering problem for selfish related machines. For a constant number of machines, m, we show a monotone polynomial time approximation scheme (PTAS) with running time that is linear in the number of jobs. It uses a new technique for reducing the number of jobs while remaining close to the optimal solution. We also present an FPTAS for the classical machine covering problem (the previous best result was a PTAS) and use this to give a monotone FPTAS. Additionally, we give a monotone approximation algorithm with approximation ratio \min(m,(2+\eps)s_1/s_m) where \eps>0 can be chosen arbitrarily small and s_i is the (real) speed of machine i. Finally we give improved results for two machines. Our paper presents the first results for this problem in the context of selfish machines.


title: LTL with the Freeze Quantifier and Register Automata

abstract: A data word is a sequence of pairs of a letter from a finite alphabet and an element from an infinite set, where the latter can only be compared for equality. To reason about data words, linear temporal logic is extended by the freeze quantifier, which stores the element at the current word position into a register, for equality comparisons deeper in the formula. By translations from the logic to alternating automata with registers and then to faulty counter automata whose counters may erroneously increase at any time, and from faulty and error-free counter automata to the logic, we obtain a complete complexity table for logical fragments defined by varying the set of temporal operators and the number of registers. In particular, the logic with future-time operators and 1 register is decidable but not primitive recursive over finite data words. Adding past-time operators or 1 more register, or switching to infinite data words, cause undecidability.


title: Memory and compiler optimizations for low-power and -energy

abstract: Embedded systems become more and more widespread, especially autonomous ones, and clearly tend to be ubiquitous. In such systems, low-power and low-energy usage get ever more crucial. Furthermore, these issues also become paramount in (massively) multi-processors systems, either in one machine or more widely in a grid. The various problems faced pertain to autonomy, power supply possibilities, thermal dissipation, or even sheer energy cost. Although it has since long been studied in harware, energy optimization is more recent in software. In this paper, we thus aim at raising awareness to low-power and low-energy issues in the language and compilation community. We thus broadly but briefly survey techniques and solutions to this energy issue, focusing on a few specific aspects in the context of compiler optimizations and memory management.


title: Data in the ADS -- Understanding How to Use it Better

abstract: The Smithsonian/NASA ADS Abstract Service contains a wealth of data for astronomers and librarians alike, yet the vast majority of usage consists of rudimentary searches. Hints on how to obtain more focused search results by using more of the various capabilities of the ADS are presented, including searching by affiliation. We also discuss the classification of articles by content and by referee status. The ADS is funded by NASA Grant NNG06GG68G-16613687.


title: Paper to Screen: Processing Historical Scans in the ADS

abstract: The NASA Astrophysics Data System in conjunction with the Wolbach Library at the Harvard-Smithsonian Center for Astrophysics is working on a project to microfilm historical observatory publications. The microfilm is then scanned for inclusion in the ADS. The ADS currently contains over 700,000 scanned pages of volumes of historical literature. Many of these volumes lack clear pagination or other bibliographic data that are necessary to take advantage of the searching capabilities of the ADS. This paper will address some of the interesting challenges that needed to be resolved during the processing of the Observatory Reports included in the ADS.


title: Pathways: Augmenting interoperability across scholarly repositories

abstract: In the emerging eScience environment, repositories of papers, datasets, software, etc., should be the foundation of a global and natively-digital scholarly communications system. The current infrastructure falls far short of this goal. Cross-repository interoperability must be augmented to support the many workflows and value-chains involved in scholarly communication. This will not be achieved through the promotion of single repository architecture or content representation, but instead requires an interoperability framework to connect the many heterogeneous systems that will exist. We present a simple data model and service architecture that augments repository interoperability to enable scholarly value-chains to be implemented. We describe an experiment that demonstrates how the proposed infrastructure can be deployed to implement the workflow involved in the creation of an overlay journal over several different repository systems (Fedora, aDORe, DSpace and arXiv).


title: Pipelined Feed-Forward Cyclic Redundancy Check (CRC) Calculation

abstract: This paper discusses a method for pipelining the calculation of CRC's, such as ITU/CCITT CRC32, into a mostly feed-forward architecture. This method allows several benefits such as independent scaling of circuit frequency and data throughput. Additionally it allows calculation over packet tails (packet length not a multiple of CRC input width). Finally it offers the ability to update a CRC where a subset of data in the packet has changed.


title: A kernel for time series based on global alignments

abstract: We propose in this paper a new family of kernels to handle times series, notably speech data, within the framework of kernel methods which includes popular algorithms such as the Support Vector Machine. These kernels elaborate on the well known Dynamic Time Warping (DTW) family of distances by considering the same set of elementary operations, namely substitutions and repetitions of tokens, to map a sequence onto another. Associating to each of these operations a given score, DTW algorithms use dynamic programming techniques to compute an optimal sequence of operations with high overall score. In this paper we consider instead the score spanned by all possible alignments, take a smoothed version of their maximum and derive a kernel out of this formulation. We prove that this kernel is positive definite under favorable conditions and show how it can be tuned effectively for practical applications as we report encouraging results on a speech recognition task.


title: Postinal Determinacy of Games with Infinitely Many Priorities

abstract: We study two-player games of infinite duration that are played on finite or infinite game graphs. A winning strategy for such a game is positional if it only depends on the current position, and not on the history of the play. A game is positionally determined if, from each position, one of the two players has a positional winning strategy. The theory of such games is well studied for winning conditions that are defined in terms of a mapping that assigns to each position a priority from a finite set. Specifically, in Muller games the winner of a play is determined by the set of those priorities that have been seen infinitely often; an important special case are parity games where the least (or greatest) priority occurring infinitely often determines the winner. It is well-known that parity games are positionally determined whereas Muller games are determined via finite-memory strategies. In this paper, we extend this theory to the case of games with infinitely many priorities. Such games arise in several application areas, for instance in pushdown games with winning conditions depending on stack contents. For parity games there are several generalisations to the case of infinitely many priorities. While max-parity games over omega or min-parity games over larger ordinals than omega require strategies with infinite memory, we can prove that min-parity games with priorities in omega are positionally determined. Indeed, it turns out that the min-parity condition over omega is the only infinitary Muller condition that guarantees positional determinacy on all game graphs.


title: Positional Determinacy of Games with Infinitely Many Priorities


title: Optimization of Memory Usage in Tardos's Fingerprinting Codes

abstract: It is known that Tardos's collusion-secure probabilistic fingerprinting code (Tardos code; STOC'03) has length of theoretically minimal order with respect to the number of colluding users. However, Tardos code uses certain continuous probability distribution in codeword generation, which creates some problems for practical use, in particular, it requires large extra memory. A solution proposed so far is to use some finite probability distributions instead. In this paper, we determine the optimal finite distribution in order to decrease extra memory amount. By our result, the extra memory is reduced to 1/32 of the original, or even becomes needless, in some practical setting. Moreover, the code length is also reduced, e.g. to about 20.6% of Tardos code asymptotically. Finally, we address some other practical issues such as approximation errors which are inevitable in any real implementation.


title: The Capacity Region of a Class of Discrete Degraded Interference Channels

abstract: We provide a single-letter characterization for the capacity region of a class of discrete degraded interference channels (DDICs). The class of DDICs considered includes the discrete additive degraded interference channel (DADIC) studied by Benzel. We show that for the class of DDICs studied, encoder cooperation does not increase the capacity region, and therefore, the capacity region of the class of DDICs is the same as the capacity region of the corresponding degraded broadcast channel.


title: Church's thesis is questioned by new calculation paradigm

abstract: 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.


title: The Application of Fuzzy Logic to the Construction of the Ranking Function of Information Retrieval Systems

abstract: The quality of the ranking function is an important factor that determines the quality of the Information Retrieval system. Each document is assigned a score by the ranking function; the score indicates the likelihood of relevance of the document given a query. In the vector space model, the ranking function is defined by a mathematic expression. We propose a fuzzy logic (FL) approach to defining the ranking function. FL provides a convenient way of converting knowledge expressed in a natural language into fuzzy logic rules. The resulting ranking function could be easily viewed, extended, and verified: * if (tf is high) and (idf is high) > (relevance is high); * if (overlap is high) > (relevance is high). By using above FL rules, we are able to achieve performance approximately equal to the state of the art search engine Apache Lucene (deltaP10 +0.92%; deltaMAP -0.1%). The fuzzy logic approach allows combining the logic-based model with the vector model. The resulting model possesses simplicity and formalism of the logic based model, and the flexibility and performance of the vector model.


title: Crosstalk-free Conjugate Networks for Optical Multicast Switching

abstract: High-speed photonic switching networks can switch optical signals at the rate of several terabits per second. However, they suffer from an intrinsic crosstalk problem when two optical signals cross at the same switch element. To avoid crosstalk, active connections must be node-disjoint in the switching network. In this paper, we propose a sequence of decomposition and merge operations, called conjugate transformation, performed on each switch element to tackle this problem. The network resulting from this transformation is called conjugate network. By using the numbering-schemes of networks, we prove that if the route assignments in the original network are link-disjoint, their corresponding ones in the conjugate network would be node-disjoint. Thus, traditional nonblocking switching networks can be transformed into crosstalk-free optical switches in a routine manner. Furthermore, we show that crosstalk-free multicast switches can also be obtained from existing nonblocking multicast switches via the same conjugate transformation.


title: A Computational Model of Spatial Memory Anticipation during Visual Search

abstract: Some visual search tasks require to memorize the location of stimuli that have been previously scanned. Considerations about the eye movements raise the question of how we are able to maintain a coherent memory, despite the frequent drastically changes in the perception. In this article, we present a computational model that is able to anticipate the consequences of the eye movements on the visual perception in order to update a spatial memory


title: A Polynomial Time Algorithm for The Traveling Salesman Problem

abstract: The ATSP polytope can be expressed by asymmetric polynomial size linear program.


title: Farthest-Point Heuristic based Initialization Methods for K-Modes Clustering

abstract: The k-modes algorithm has become a popular technique in solving categorical data clustering problems in different application domains. However, the algorithm requires random selection of initial points for the clusters. Different initial points often lead to considerable distinct clustering results. In this paper we present an experimental study on applying a farthest-point heuristic based initialization method to k-modes clustering to improve its performance. Experiments show that new initialization method leads to better clustering accuracy than random selection initialization method for k-modes clustering.


title: M\'{e}canismes de Transmission Multipoint pour R\'{e}seaux Locaux Sans Fil IEEE 802.11

abstract: Le standard IEEE 802.11 est inefficace pour la transmission multim\'{e}dia en multipoint. En particulier, les paquets multipoints sont envoy\'{e}s en boucle ouverte de la m\^{e}me mani\`{e}re que les paquets broadcast. L'absence d'acquittements rend impossible la mise en oeuvre de m\'{e}canismes de contr\^{o}le de congestion, de m\'{e}canisme de fiabilisation de la transmission ainsi que d'algorithmes d'adaptation du d\'{e}bit de transmission physique. Dans ce rapport, nous proposons de nouveaux m\'{e}canismes de ransmission multipoint qui se basent sur une approche leader pour renvoyer des acquittements. Nous nous interessons \`{a} des solutions pratiques qui sont suceptibles d'\^{e}tre implant\'{e}s dans les cartes r\'{e}seaux sans fil actuelles et futures et qui restent compatibles avec les stations IEEE 802.11 standards. Nous proposons deux m\'{e}canismes pour adapter le d\'{e}bit de transmission physique des flots multipoints: un m\'{e}canisme simplifi\'{e} appel\'{e} LB-ARF et un m\'{e}canisme plus robuste appel\'{e} RRAM. Nos simulations montrent que pour des environnements statiques, un m\'{e}canisme aussi simple que LB-ARF suffit pour obtenir de bonnes performances. Le m\'{e}canisme RRAM est quant \`{a} lui aussi efficace dans des environnements statiques que lorsque les stations sont mobiles.


title: Spectra of large block matrices

abstract: In a frequency selective slow-fading channel in a MIMO system, the channel matrix is of the form of a block matrix. This paper proposes a method to calculate the limit of the eigenvalue distribution of block matrices if the size of the blocks tends to infinity. While it considers random matrices, it takes an operator-valued free probability approach to achieve this goal. Using this method, one derives a system of equations, which can be solved numerically to compute the desired eigenvalue distribution. The paper initially tackles the problem for square block matrices, then extends the solution to rectangular block matrices. Finally, it deals with Wishart type block matrices. For two special cases, the results of our approach are compared with results from simulations. The first scenario investigates the limit eigenvalue distribution of block Toeplitz matrices. The second scenario deals with the distribution of Wishart type block matrices for a frequency selective slow-fading channel in a MIMO system for two different cases of $n_R=n_T$ and $n_R=2n_T$. Using this method, one may calculate the capacity and the Signal-to-Interference-and-Noise Ratio in large MIMO systems.


title: Streaming Maximum-Minimum Filter Using No More than Three Comparisons per Element

abstract: The running maximum-minimum (max-min) filter computes the maxima and minima over running windows of size w. This filter has numerous applications in signal processing and time series analysis. We present an easy-to-implement online algorithm requiring no more than 3 comparisons per element, in the worst case. Comparatively, no algorithm is known to compute the running maximum (or minimum) filter in 1.5 comparisons per element, in the worst case. Our algorithm has reduced latency and memory usage.


title: Capacity of the Trapdoor Channel with Feedback

abstract: We establish that the feedback capacity of the trapdoor channel is the logarithm of the golden ratio and provide a simple communication scheme that achieves capacity. As part of the analysis, we formulate a class of dynamic programs that characterize capacities of unifilar finite-state channels. The trapdoor channel is an instance that admits a simple analytic solution.


title: MV3: A new word based stream cipher using rapid mixing and revolving buffers

abstract: MV3 is a new word based stream cipher for encrypting long streams of data. A direct adaptation of a byte based cipher such as RC4 into a 32- or 64-bit word version will obviously need vast amounts of memory. This scaling issue necessitates a look for new components and principles, as well as mathematical analysis to justify their use. Our approach, like RC4's, is based on rapidly mixing random walks on directed graphs (that is, walks which reach a random state quickly, from any starting point). We begin with some well understood walks, and then introduce nonlinearity in their steps in order to improve security and show long term statistical correlations are negligible. To minimize the short term correlations, as well as to deter attacks using equations involving successive outputs, we provide a method for sequencing the outputs derived from the walk using three revolving buffers. The cipher is fast -- it runs at a speed of less than 5 cycles per byte on a Pentium IV processor. A word based cipher needs to output more bits per step, which exposes more correlations for attacks. Moreover we seek simplicity of construction and transparent analysis. To meet these requirements, we use a larger state and claim security corresponding to only a fraction of it. Our design is for an adequately secure word-based cipher; our very preliminary estimate puts the security close to exhaustive search for keys of size < 256 bits.


title: Restricted Complexity, General Complexity

abstract: Why has the problematic of complexity appeared so late? And why would it be justified?


title: The Mathematical Parallels Between Packet Switching and Information Transmission

abstract: All communication networks comprise of transmission systems and switching systems, even though they are usually treated as two separate issues. Communication channels are generally disturbed by noise from various sources. In circuit switched networks, reliable communication requires the error-tolerant transmission of bits over noisy channels. In packet switched networks, however, not only can bits be corrupted with noise, but resources along connection paths are also subject to contention. Thus, quality of service (QoS) is determined by buffer delays and packet losses. The theme of this paper is to show that transmission noise and packet contention actually have similar characteristics and can be tamed by comparable means to achieve reliable communication, and a number of analogies between switching and transmission are identified. The sampling theorem of bandlimited signals provides the cornerstone of digital communication and signal processing. Recently, the Birkhoff-von Neumann decomposition of traffic matrices has been widely applied to packet switches. With respect to the complexity reduction of packet switching, we show that the decomposition of a doubly stochastic traffic matrix plays a similar role to that of the sampling theorem in digital transmission. We conclude that packet switching systems are governed by mathematical laws that are similar to those of digital transmission systems as envisioned by Shannon in his seminal 1948 paper, A Mathematical Theory of Communication.


title: Strong bi-homogeneous B\'{e}zout theorem and its use in effective real algebraic geometry

abstract: Let f1, ..., fs be a polynomial family in Q[X1,..., Xn] (with s less than n) of degree bounded by D. Suppose that f1, ..., fs generates a radical ideal, and defines a smooth algebraic variety V. Consider a projection P. We prove that the degree of the critical locus of P restricted to V is bounded by D^s(D-1)^(n-s) times binomial of n and n-s. This result is obtained in two steps. First the critical points of P restricted to V are characterized as projections of the solutions of Lagrange's system for which a bi-homogeneous structure is exhibited. Secondly we prove a bi-homogeneous B\'ezout Theorem, which bounds the sum of the degrees of the equidimensional components of the radical of an ideal generated by a bi-homogeneous polynomial family. This result is improved when f1,..., fs is a regular sequence. Moreover, we use Lagrange's system to design an algorithm computing at least one point in each connected component of a smooth real algebraic set. This algorithm generalizes, to the non equidimensional case, the one of Safey El Din and Schost. The evaluation of the output size of this algorithm gives new upper bounds on the first Betti number of a smooth real algebraic set. Finally, we estimate its arithmetic complexity and prove that in the worst cases it is polynomial in n, s, D^s(D-1)^(n-s) and the binomial of n and n-s, and the complexity of evaluation of f1,..., fs.


title: Finite-Dimensional Bounds on Zm and Binary LDPC Codes with Belief Propagation Decoders

abstract: This paper focuses on finite-dimensional upper and lower bounds on decodable thresholds of Zm and binary low-density parity-check (LDPC) codes, assuming belief propagation decoding on memoryless channels. A concrete framework is presented, admitting systematic searches for new bounds. Two noise measures are considered: the Bhattacharyya noise parameter and the soft bit value for a maximum a posteriori probability (MAP) decoder on the uncoded channel. For Zm LDPC codes, an iterative m-dimensional bound is derived for m-ary-input/symmetric-output channels, which gives a sufficient stability condition for Zm LDPC codes and is complemented by a matched necessary stability condition introduced herein. Applications to coded modulation and to codes with non-equiprobable distributed codewords are also discussed. For binary codes, two new lower bounds are provided for symmetric channels, including a two-dimensional iterative bound and a one-dimensional non-iterative bound, the latter of which is the best known bound that is tight for binary symmetric channels (BSCs), and is a strict improvement over the bound derived by the channel degradation argument. By adopting the reverse channel perspective, upper and lower bounds on the decodable Bhattacharyya noise parameter are derived for non-symmetric channels, which coincides with the existing bound for symmetric channels.


title: Towards a Bayesian framework for option pricing

abstract: In this paper, we describe a general method for constructing the posterior distribution of an option price. Our framework takes as inputs the prior distributions of the parameters of the stochastic process followed by the underlying, as well as the likelihood function implied by the observed price history for the underlying. Our work extends that of Karolyi (1993) and Darsinos and Satchell (2001), but with the crucial difference that the likelihood function we use for inference is that which is directly implied by the underlying, rather than imposed in an ad hoc manner via the introduction of a function representing "measurement error." As such, an important problem still relevant for our method is that of model risk, and we address this issue by describing how to perform a Bayesian averaging of parameter inferences based on the different models considered using our framework.


title: Enumeration Problems Related to Ground Horn Theories

abstract: We investigate the enumeration of varieties of boolean theories related to Horn clauses. We describe a number of combinatorial equivalences among different characterizations and calculate the number of different theories in $n$ variables for slightly different characterizations. The method of counting is via counting models using a satisfiability checker.


title: Extending the Calculus of Constructions with Tarski's fix-point theorem

abstract: We propose to use Tarski's least fixpoint theorem as a basis to define recursive functions in the calculus of inductive constructions. This widens the class of functions that can be modeled in type-theory based theorem proving tool to potentially non-terminating functions. This is only possible if we extend the logical framework by adding the axioms that correspond to classical logic. We claim that the extended framework makes it possible to reason about terminating and non-terminating computations and we show that common facilities of the calculus of inductive construction, like program extraction can be extended to also handle the new functions.


title: Constructing experimental indicators for Open Access documents

abstract: 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.