OpenRaiser/Intern-Atlas huggingface dataset:
A formal proof of the four color theorem
Venue: arXiv cs.DM 2009
Year: 2009

A formal proof has not been found for the four color theorem since 1852 when Francis Guthrie first conjectured the four color theorem. Why? A bad idea, we think, directed people to a rough road. Using a similar method to that for the formal proof of the five color theorem, a formal proof is proposed in this paper of the four color theorem, namely, every planar graph is four-colorable. The formal proof proposed can also be regarded as an algorithm to color a planar graph using four colors so that no two adjacent vertices receive the same color.
Multicasting in Large Wireless Networks: Bounds on the Minimum Energy per Bit
Venue: arXiv cs.IT 2009
Year: 2009

We consider scaling laws for maximal energy efficiency of communicating a message to all the nodes in a wireless network, as the number of nodes in the network becomes large. Two cases of large wireless networks are studied -- dense random networks and constant density (extended) random networks. In addition, we also study finite size regular networks in order to understand how regularity in node placement affects energy consumption. We first establish an information-theoretic lower bound on the minimum energy per bit for multicasting in arbitrary wireless networks when the channel state information is not available at the transmitters. Upper bounds are obtained by constructing a simple flooding scheme that requires no information at the receivers about the channel states or the locations and identities of the nodes. The gap between the upper and lower bounds is only a constant factor for dense random networks and regular networks, and differs by a poly-logarithmic factor for extended random networks. Furthermore, we show that the proposed upper and lower bounds for random networks hold almost surely in the node locations as the number of nodes approaches infinity.
Modeling and Verification for Timing Satisfaction of Fault-Tolerant Systems with Finiteness
Venue: arXiv cs.DC 2009
Year: 2009

The increasing use of model-based tools enables further use of formal verification techniques in the context of distributed real-time systems. To avoid state explosion, it is necessary to construct verification models that focus on the aspects under consideration. In this paper, we discuss how we construct a verification model for timing analysis in distributed real-time systems. We (1) give observations concerning restrictions of timed automata to model these systems, (2) formulate mathematical representations on how to perform model-to-model transformation to derive verification models from system models, and (3) propose some theoretical criteria how to reduce the model size. The latter is in particular important, as for the verification of complex systems, an efficient model reflecting the properties of the system under consideration is equally important to the verification algorithm itself. Finally, we present an extension of the model-based development tool FTOS, designed to develop fault-tolerant systems, to demonstrate %the benefits of our approach.
Predicate Transformers and Linear Logic, yet another denotational model
Venue: arXiv cs.LO 2009
Year: 2009

In the refinement calculus, monotonic predicate transformers are used to model specifications for (imperative) programs. Together with a natural notion of simulation, they form a category enjoying many algebraic properties. We build on this structure to make predicate transformers into a de notational model of full linear logic: all the logical constructions have a natural interpretation in terms of predicate transformers (i.e. in terms of specifications). We then interpret proofs of a formula by a safety property for the corresponding specification.
Programming interfaces and basic topology
Venue: arXiv cs.LO 2009
Year: 2009

A pattern of interaction that arises again and again in programming is a "handshake", in which two agents exchange data. The exchange is thought of as provision of a service. Each interaction is initiated by a specific agent--the client or Angel--and concluded by the other--the server or Demon. We present a category in which the objects--called interaction structures in the paper--serve as descriptions of services provided across such handshaken interfaces. The morphisms--called (general) simulations--model components that provide one such service, relying on another. The morphisms are relations between the underlying sets of the interaction structures. The proof that a relation is a simulation can serve (in principle) as an executable program, whose specification is that it provides the service described by its domain, given an implementation of the service described by its codomain. This category is then shown to coincide with the subcategory of "generated" basic topologies in Sambin's terminology, where a basic topology is given by a closure operator whose induced sup-lattice structure need not be distributive; and moreover, this operator is inductively generated from a basic cover relation. This coincidence provides topologists with a natural source of examples for non-distributive formal topology. It raises a number of questions of interest both for formal topology and programming. The extra structure needed to make such a basic topology into a real formal topology is then interpreted in the context of interaction structures.
Structural Solutions for Cross-Layer Optimization of Wireless Multimedia Transmission
Venue: arXiv cs.MM 2009
Year: 2009

In this paper, we propose a systematic solution to the problem of cross-layer optimization for delay-sensitive media transmission over time-varying wireless channels as well as investigate the structures and properties of this solution, such that it can be easily implemented in various multimedia systems and applications. Specifically, we formulate this problem as a finite-horizon Markov decision process (MDP) by explicitly considering the users' heterogeneous multimedia traffic characteristics (e.g. delay deadlines, distortion impacts and dependencies etc.), time-varying network conditions as well as, importantly, their ability to adapt their cross-layer transmission strategies in response to these dynamics. Based on the heterogeneous characteristics of the media packets, we are able to express the transmission priorities between packets as a new type of directed acyclic graph (DAG). This DAG provides the necessary structure for determining the optimal cross-layer actions in each time slot: the root packet in the DAG will always be selected for transmission since it has the highest positive marginal utility; and the complexity of the proposed cross-layer solution is demonstrated to linearly increase w.r.t. the number of disconnected packet pairs in the DAG and exponentially increase w.r.t. the number of packets on which the current packets depend on. The simulation results demonstrate that the proposed solution significantly outperforms existing state-of-the-art cross-layer solutions. Moreover, we show that our solution provides the upper bound performance for the cross-layer optimization solutions with delayed feedback such as the well-known RaDiO framework.
Iterative Decoding on Multiple Tanner Graphs Using Random Edge Local Complementation
Venue: arXiv cs.IT 2009
Year: 2009

In this paper, we propose to enhance the performance of the sum-product algorithm (SPA) by interleaving SPA iterations with a random local graph update rule. This rule is known as edge local complementation (ELC), and has the effect of modifying the Tanner graph while preserving the code. We have previously shown how the ELC operation can be used to implement an iterative permutation group decoder (SPA-PD)--one of the most successful iterative soft-decision decoding strategies at small blocklengths. In this work, we exploit the fact that ELC can also give structurally distinct parity-check matrices for the same code. Our aim is to describe a simple iterative decoder, running SPA-PD on distinct structures, based entirely on random usage of the ELC operation. This is called SPA-ELC, and we focus on small blocklength codes with strong algebraic structure. In particular, we look at the extended Golay code and two extended quadratic residue codes. Both error rate performance and average decoding complexity, measured by the average total number of messages required in the decoding, significantly outperform those of the standard SPA, and compares well with SPA-PD. However, in contrast to SPA-PD, which requires a global action on the Tanner graph, we obtain a performance improvement via local action alone. Such localized algorithms are of mathematical interest in their own right, but are also suited to parallel/distributed realizations.
Mathematical Models in Danube Water Quality
Venue: arXiv cs.OH 2009
Year: 2009

The mathematical shaping in the study of water quality has become a branch of environmental engineering. The comprehension and effective application of mathematical models in studying environmental phenomena keep up with the results in the domain of mathematics and the development of specialized software as well. Integrated software programs simulate and predict extreme events, propose solutions, analyzing and processing data in due time. This paper presents a browsing through some mathematical categories of processing the statistical data, examples and their analysis concerning the degree of water pollution downstream the river Danube.
Proposition d'une methode de qualification et de selection d'un logiciel d'analyse et de suivi du referencement dans les moteurs de recherche
Venue: arXiv cs.OH 2009
Year: 2009

In order to measure website visibility in search engines, there are softwares for analytics and referencing follow-up. They permit to quantify website's efficacity of referencing and optimize its positionning in search engines. With regard to search engines' algorithms' evolution and centralization of Key Performance Indicators for Marketing decision making, it becomes hard to find solutions to effectively lead a lot of projects for referencing. That's why we have built a methodology in order compare, evaluate and choose a software for analytics and referencing follow-up in search engines.
Indexing Research Papers in Open Access Databases
Venue: arXiv cs.DL 2009
Year: 2009

This paper synthesizes the actions performed in order to transform a classic scientific research journal - 'Annals. Computer Science Series' - available only in printed form until 2008, into a modern e-journal with free access to the full text of the articles. For achieving this goal, the research papers have been included in various article databases, portals and library catalogs which offered a high visibility to the journal.
The Effectiveness of Computer Assisted Classes for English as a Second Language
Venue: arXiv cs.OH 2009
Year: 2009

The present study aims to evaluate the efficiency of the computer assisted English classes and to emphasize the necessity of developing sound methodological strategies adjusted to the new technology. It also present the benefits of using the computer in the pre-school and elementary school classes, highlighted by a report on the comparative observation of four groups of children studying English in a computer assisted environment.
Mining Generalized Patterns from Large Databases using Ontologies
Venue: arXiv cs.AI 2009
Year: 2009

Formal Concept Analysis (FCA) is a mathematical theory based on the formalization of the notions of concept and concept hierarchies. It has been successfully applied to several Computer Science fields such as data mining,software engineering, and knowledge engineering, and in many domains like medicine, psychology, linguistics and ecology. For instance, it has been exploited for the design, mapping and refinement of ontologies. In this paper, we show how FCA can benefit from a given domain ontology by analyzing the impact of a taxonomy (on objects and/or attributes) on the resulting concept lattice. We willmainly concentrate on the usage of a taxonomy to extract generalized patterns (i.e., knowledge generated from data when elements of a given domain ontology are used) in the form of concepts and rules, and improve navigation through these patterns. To that end, we analyze three generalization cases and show their impact on the size of the generalized pattern set. Different scenarios of simultaneous generalizations on both objects and attributes are also discussed
A Survey on Cross-Site Scripting Attacks
Venue: arXiv cs.CR 2009
Year: 2009

Web applications are becoming truly pervasive in all kinds of business models and organizations. Today, most critical systems such as those related to health care, banking, or even emergency response, are relying on these applications. They must therefore include, in addition to the expected value offered to their users, reliable mechanisms to ensure their security. In this paper, we focus on the specific problem of cross-site scripting attacks against web applications. We present a study of this kind of attacks, and survey current approaches for their prevention. Applicability and limitations of each proposal are also discussed.
Computer Based Interpretation of the Students' Evaluation of the Teaching Staff
Venue: arXiv cs.HC 2009
Year: 2009

The goal of this paper is to offer a full support for universities and quality assessment committees in retrieving the feedback from their students regarding to their teaching staff. The computer based application presented before ([Cri07]) collects data from the students. Another part of the application, presented in this paper, processes this data and presents the statistical results concerning each teacher.
On the Convex Feasibility Problem
Venue: arXiv cs.NA 2009
Year: 2009

The convergence of the projection algorithm for solving the convex feasibility problem for a family of closed convex sets, is in connection with the regularity properties of the family. In the paper [18] are pointed out four cases of such a family depending of the two characteristics: the emptiness and boudedness of the intersection of the family. The case four (the interior of the intersection is empty and the intersection itself is bounded) is unsolved. In this paper we give a (partial) answer for the case four: in the case of two closed convex sets in R3 the regularity property holds.
Improved Approximation Algorithms for Segment Minimization in Intensity Modulated Radiation Therapy
Venue: arXiv cs.DS 2009
Year: 2009

he segment minimization problem consists of finding the smallest set of integer matrices that sum to a given intensity matrix, such that each summand has only one non-zero value, and the non-zeroes in each row are consecutive. This has direct applications in intensity-modulated radiation therapy, an effective form of cancer treatment. We develop three approximation algorithms for matrices with arbitrarily many rows. Our first two algorithms improve the approximation factor from the previous best of $1+\log_2 h $ to (roughly) $3/2 \cdot (1+\log_3 h)$ and $11/6\cdot(1+\log_4{h})$, respectively, where $h$ is the largest entry in the intensity matrix. We illustrate the limitations of the specific approach used to obtain these two algorithms by proving a lower bound of $\frac{(2b-2)}{b}\cdot\log_b{h} + \frac{1}{b}$ on the approximation guarantee. Our third algorithm improves the approximation factor from $2 \cdot (\log D+1)$ to $24/13 \cdot (\log D+1)$, where $D$ is (roughly) the largest difference between consecutive elements of a row of the intensity matrix. Finally, experimentation with these algorithms shows that they perform well with respect to the optimum and outperform other approximation algorithms on 77% of the 122 test cases we consider, which include both real world and synthetic data.
A Survey of Tree Convex Sets Test
Venue: arXiv cs.DS 2009
Year: 2009

Tree convex sets refer to a collection of sets such that each set in the collection is a subtree of a tree whose nodes are the elements of these sets. They extend the concept of row convex sets each of which is an interval over a total ordering of the elements of those sets. They have been applied to identify tractable Constraint Satisfaction Problems and Combinatorial Auction Problems. Recently, polynomial algorithms have been proposed to recognize tree convex sets. In this paper, we review the materials that are the key to a linear recognition algorithm.
Delay-Optimal Power and Precoder Adaptation for Multi-stream MIMO Systems
Venue: arXiv cs.IT 2009
Year: 2009

In this paper, we consider delay-optimal MIMO precoder and power allocation design for a MIMO Link in wireless fading channels. There are $L$ data streams spatially multiplexed onto the MIMO link with heterogeneous packet arrivals and delay requirements. The transmitter is assumed to have knowledge of the channel state information (CSI) as well as the joint queue state information (QSI) of the $L$ buffers. Using $L$-dimensional Markov Decision Process (MDP), we obtain optimal precoding and power allocation policies for general delay regime, which consists of an online solution and an offline solution. The online solution has negligible complexity but the offline solution has worst case complexity ${\cal O}((N+1)^L)$ where $N$ is the buffer size. Using {\em static sorting} of the $L$ eigenchannels, we decompose the MDP into $L$ independent 1-dimensional subproblems and obtained low complexity offline solution with linear complexity order ${\cal O}(NL)$ and close-to-optimal performance.
Rivisiting Token/Bucket Algorithms in New Applications
Venue: arXiv cs.DS 2009
Year: 2009

We consider a somehow peculiar Token/Bucket problem which at first sight looks confusing and difficult to solve. The winning approach to solve the problem consists in going back to the simple and traditional methods to solve computer science problems like the one taught to us by Knuth. Somehow the main trick is to be able to specify clearly what needs to be achieved, and then the solution, even if complex, appears almost by itself.
Data Distribution Optimization using Offline Algorithms and a Peer-to-Peer Small Diameter Tree Architecture with Bounded Node Degrees
Venue: arXiv cs.DC 2009
Year: 2009

Multicast data transfers occur in many distributed systems and applications (e.g. IPTV, Grids, content delivery networks). Because of this, efficient multicast data distribution optimization techniques are required. In the first part of this paper we present a small diameter, bounded degree, collaborative peer-to-peer multicast tree architecture, which supports dynamic node arrivals and departures making local decisions only. The architecture is fault tolerant and, at low arrival and departure rates, converges towards a theoretically optimal structure. In the second part of the paper we consider several offline data distribution optimization problems, for which we present novel and time-efficient algorithmic solutions.
Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators
Venue: arXiv cs.LO 2009
Year: 2009

The symmetric interaction combinators are an equally expressive variant of Lafont's interaction combinators. They are a graph-rewriting model of deterministic computation. We define two notions of observational equivalence for them, analogous to normal form and head normal form equivalence in the lambda-calculus. Then, we prove a full abstraction result for each of the two equivalences. This is obtained by interpreting nets as certain subsets of the Cantor space, called edifices, which play the same role as Boehm trees in the theory of the lambda-calculus.
Encoding models for scholarly literature
Venue: arXiv cs.CL 2009
Year: 2009

We examine the issue of digital formats for document encoding, archiving and publishing, through the specific example of "born-digital" scholarly journal articles. We will begin by looking at the traditional workflow of journal editing and publication, and how these practices have made the transition into the online domain. We will examine the range of different file formats in which electronic articles are currently stored and published. We will argue strongly that, despite the prevalence of binary and proprietary formats such as PDF and MS Word, XML is a far superior encoding choice for journal articles. Next, we look at the range of XML document structures (DTDs, Schemas) which are in common use for encoding journal articles, and consider some of their strengths and weaknesses. We will suggest that, despite the existence of specialized schemas intended specifically for journal articles (such as NLM), and more broadly-used publication-oriented schemas such as DocBook, there are strong arguments in favour of developing a subset or customization of the Text Encoding Initiative (TEI) schema for the purpose of journal-article encoding; TEI is already in use in a number of journal publication projects, and the scale and precision of the TEI tagset makes it particularly appropriate for encoding scholarly articles. We will outline the document structure of a TEI-encoded journal article, and look in detail at suggested markup patterns for specific features of journal articles.
Thinning, Entropy and the Law of Thin Numbers
Venue: arXiv cs.IT 2009
Year: 2009

Renyi's "thinning" operation on a discrete random variable is a natural discrete analog of the scaling operation for continuous random variables. The properties of thinning are investigated in an information-theoretic context, especially in connection with information-theoretic inequalities related to Poisson approximation results. The classical Binomial-to-Poisson convergence (sometimes referred to as the "law of small numbers" is seen to be a special case of a thinning limit theorem for convolutions of discrete distributions. A rate of convergence is provided for this limit, and nonasymptotic bounds are also established. This development parallels, in part, the development of Gaussian inequalities leading to the information-theoretic version of the central limit theorem. In particular, a "thinning Markov chain" is introduced, and it is shown to play a role analogous to that of the Ornstein-Uhlenbeck process in connection to the entropy power inequality.
Specific Characteristics of Applying the Paired Comparison Method for Parameterization of Consumer Wants
Venue: arXiv cs.OH 2009
Year: 2009

The article describes the main problems concerned with using expert assessment method in consumer preference researches. The author proved the expediency of using a 3-point measurement scale. The author suggested an algorithm for controlling the judgments' consistency that includes analyzing and correcting the input estimates in real-time mode.
Decision Support Systems Architectures
Venue: arXiv cs.OH 2009
Year: 2009

This paper presents the main components of the decision assisting systems. Further on three types of architectures of these systems are described, analyzed, and respectively compared, namely: the network architecture, the centralized architecture and the hierarchical architecture.
On the Challenges of Collaborative Data Processing
Venue: arXiv cs.DB 2009
Year: 2009

The last 30 years have seen the creation of a variety of electronic collaboration tools for science and business. Some of the best-known collaboration tools support text editing (e.g., wikis). Wikipedia's success shows that large-scale collaboration can produce highly valuable content. Meanwhile much structured data is being collected and made publicly available. We have never had access to more powerful databases and statistical packages. Is large-scale collaborative data analysis now possible? Using a quantitative analysis of Web 2.0 data visualization sites, we find evidence that at least moderate open collaboration occurs. We then explore some of the limiting factors of collaboration over data.