OpenRaiser/Intern-Atlas huggingface dataset:
Independence and concurrent separation logic
Venue: arXiv cs.LO 2008
Year: 2008

A compositional Petri net-based semantics is given to a simple language allowing pointer manipulation and parallelism. The model is then applied to give a notion of validity to the judgements made by concurrent separation logic that emphasizes the process-environment duality inherent in such rely-guarantee reasoning. Soundness of the rules of concurrent separation logic with respect to this definition of validity is shown. The independence information retained by the Petri net model is then exploited to characterize the independence of parallel processes enforced by the logic. This is shown to permit a refinement operation capable of changing the granularity of atomic actions.
Doubly-Generalized LDPC Codes: Stability Bound over the BEC
Venue: arXiv cs.IT 2008
Year: 2008

The iterative decoding threshold of low-density parity-check (LDPC) codes over the binary erasure channel (BEC) fulfills an upper bound depending only on the variable and check nodes with minimum distance 2. This bound is a consequence of the stability condition, and is here referred to as stability bound. In this paper, a stability bound over the BEC is developed for doubly-generalized LDPC codes, where the variable and the check nodes can be generic linear block codes, assuming maximum a posteriori erasure correction at each node. It is proved that in this generalized context as well the bound depends only on the variable and check component codes with minimum distance 2. A condition is also developed, namely the derivative matching condition, under which the bound is achieved with equality.
Distributed Double Spending Prevention
Venue: arXiv cs.CR 2008
Year: 2008

We study the problem of preventing double spending in electronic payment schemes in a distributed fashion. This problem occurs, for instance, when the spending of electronic coins needs to be controlled by a large collection of nodes (eg. in a peer-to-peer (P2P) system) instead of one central bank. Contrary to the commonly held belief that this is fundamentally impossible, we propose several solutions that do achieve a reasonable level of double spending prevention, and analyse their efficiency under varying assumptions.
Bit-Optimal Lempel-Ziv compression
Venue: arXiv cs.DS 2008
Year: 2008

One of the most famous and investigated lossless data-compression scheme is the one introduced by Lempel and Ziv about 40 years ago. This compression scheme is known as "dictionary-based compression" and consists of squeezing an input string by replacing some of its substrings with (shorter) codewords which are actually pointers to a dictionary of phrases built as the string is processed. Surprisingly enough, although many fundamental results are nowadays known about upper bounds on the speed and effectiveness of this compression process and references therein), ``we are not aware of any parsing scheme that achieves optimality when the LZ77-dictionary is in use under any constraint on the codewords other than being of equal length'' [N. Rajpoot and C. Sahinalp. Handbook of Lossless Data Compression, chapter Dictionary-based data compression. Academic Press, 2002. pag. 159]. Here optimality means to achieve the minimum number of bits in compressing each individual input string, without any assumption on its generating source. In this paper we provide the first LZ-based compressor which computes the bit-optimal parsing of any input string in efficient time and optimal space, for a general class of variable-length codeword encodings which encompasses most of the ones typically used in data compression and in the design of search engines and compressed indexes.
Snap-Stabilization in Message-Passing Systems
Venue: arXiv cs.DC 2008
Year: 2008

In this paper, we tackle the open problem of snap-stabilization in message-passing systems. Snap-stabilization is a nice approach to design protocols that withstand transient faults. Compared to the well-known self-stabilizing approach, snap-stabilization guarantees that the effect of faults is contained immediately after faults cease to occur. Our contribution is twofold: we show that (1) snap-stabilization is impossible for a wide class of problems if we consider networks with finite yet unbounded channel capacity; (2) snap-stabilization becomes possible in the same setting if we assume bounded-capacity channels. We propose three snap-stabilizing protocols working in fully-connected networks. Our work opens exciting new research perspectives, as it enables the snap-stabilizing paradigm to be implemented in actual networks.
Minimum Entropy Orientations
Venue: arXiv cs.DS 2008
Year: 2008

We study graph orientations that minimize the entropy of the in-degree sequence. The problem of finding such an orientation is an interesting special case of the minimum entropy set cover problem previously studied by Halperin and Karp [Theoret. Comput. Sci., 2005] and by the current authors [Algorithmica, to appear]. We prove that the minimum entropy orientation problem is NP-hard even if the graph is planar, and that there exists a simple linear-time algorithm that returns an approximate solution with an additive error guarantee of 1 bit. This improves on the only previously known algorithm which has an additive error guarantee of log_2 e bits (approx. 1.4427 bits).
Network as a computer: ranking paths to find flows
Venue: arXiv cs.IR 2008
Year: 2008

We explore a simple mathematical model of network computation, based on Markov chains. Similar models apply to a broad range of computational phenomena, arising in networks of computers, as well as in genetic, and neural nets, in social networks, and so on. The main problem of interaction with such spontaneously evolving computational systems is that the data are not uniformly structured. An interesting approach is to try to extract the semantical content of the data from their distribution among the nodes. A concept is then identified by finding the community of nodes that share it. The task of data structuring is thus reduced to the task of finding the network communities, as groups of nodes that together perform some non-local data processing. Towards this goal, we extend the ranking methods from nodes to paths. This allows us to extract some information about the likely flow biases from the available static information about the network.
Structure and Optimality of Myopic Policy in Opportunistic Access with Noisy Observations
Venue: arXiv cs.NI 2008
Year: 2008

A restless multi-armed bandit problem that arises in multichannel opportunistic communications is considered, where channels are modeled as independent and identical Gilbert-Elliot channels and channel state observations are subject to errors. A simple structure of the myopic policy is established under a certain condition on the false alarm probability of the channel state detector. It is shown that the myopic policy has a semi-universal structure that reduces channel selection to a simple round-robin procedure and obviates the need to know the underlying Markov transition probabilities. The optimality of the myopic policy is proved for the case of two channels and conjectured for the general case based on numerical examples.
Universal Coding for Lossless and Lossy Complementary Delivery Problems
Venue: arXiv cs.IT 2008
Year: 2008

This paper deals with a coding problem called complementary delivery, where messages from two correlated sources are jointly encoded and each decoder reproduces one of two messages using the other message as the side information. Both lossless and lossy universal complementary delivery coding schemes are investigated. In the lossless case, it is demonstrated that a universal complementary delivery code can be constructed by only combining two Slepian-Wolf codes. Especially, it is shown that a universal lossless complementary delivery code, for which error probability is exponentially tight, can be constructed from two linear Slepian-Wolf codes. In the lossy case, a universal complementary delivery coding scheme based on Wyner-Ziv codes is proposed. While the proposed scheme cannot attain the optimal rate-distortion trade-off in general, the rate-loss is upper bounded by a universal constant under some mild conditions. The proposed schemes allows us to apply any Slepian-Wolf and Wyner-Ziv codes to complementary delivery coding.
On the Complexity of Nash Equilibria of Action-Graph Games
Venue: arXiv cs.GT 2008
Year: 2008

We consider the problem of computing Nash Equilibria of action-graph games (AGGs). AGGs, introduced by Bhat and Leyton-Brown, is a succinct representation of games that encapsulates both "local" dependencies as in graphical games, and partial indifference to other agents' identities as in anonymous games, which occur in many natural settings. This is achieved by specifying a graph on the set of actions, so that the payoff of an agent for selecting a strategy depends only on the number of agents playing each of the neighboring strategies in the action graph. We present a Polynomial Time Approximation Scheme for computing mixed Nash equilibria of AGGs with constant treewidth and a constant number of agent types (and an arbitrary number of strategies), together with hardness results for the cases when either the treewidth or the number of agent types is unconstrained. In particular, we show that even if the action graph is a tree, but the number of agent-types is unconstrained, it is NP-complete to decide the existence of a pure-strategy Nash equilibrium and PPAD-complete to compute a mixed Nash equilibrium (even an approximate one); similarly for symmetric AGGs (all agents belong to a single type), if we allow arbitrary treewidth. These hardness results suggest that, in some sense, our PTAS is as strong of a positive result as one can expect.
Characterising through Erasing: A Theoretical Framework for Representing Documents Inspired by Quantum Theory
Venue: arXiv cs.IR 2008
Year: 2008

The problem of representing text documents within an Information Retrieval system is formulated as an analogy to the problem of representing the quantum states of a physical system. Lexical measurements of text are proposed as a way of representing documents which are akin to physical measurements on quantum states. Consequently, the representation of the text is only known after measurements have been made, and because the process of measuring may destroy parts of the text, the document is characterised through erasure. The mathematical foundations of such a quantum representation of text are provided in this position paper as a starting point for indexing and retrieval within a ``quantum like'' Information Retrieval system.
Multiple Access Outerbounds and the Inseparability of Parallel Interference Channels
Venue: arXiv cs.IT 2008
Year: 2008

It is known that the capacity of parallel (multi-carrier) Gaussian point-to-point, multiple access and broadcast channels can be achieved by separate encoding for each subchannel (carrier) subject to a power allocation across carriers. In this paper we show that such a separation does not apply to parallel Gaussian interference channels in general. A counter-example is provided in the form of a 3 user interference channel where separate encoding can only achieve a sum capacity of $\log({SNR})+o(\log({SNR}))$ per carrier while the actual capacity, achieved only by joint-encoding across carriers, is $3/2\log({SNR}))+o(\log({SNR}))$ per carrier. As a byproduct of our analysis, we propose a class of multiple-access-outerbounds on the capacity of the 3 user interference channel.
New Implementation Framework for Saturation-Based Reasoning
Venue: arXiv cs.AI 2008
Year: 2008

The saturation-based reasoning methods are among the most theoretically developed ones and are used by most of the state-of-the-art first-order logic reasoners. In the last decade there was a sharp increase in performance of such systems, which I attribute to the use of advanced calculi and the intensified research in implementation techniques. However, nowadays we are witnessing a slowdown in performance progress, which may be considered as a sign that the saturation-based technology is reaching its inherent limits. The position I am trying to put forward in this paper is that such scepticism is premature and a sharp improvement in performance may potentially be reached by adopting new architectural principles for saturation. The top-level algorithms and corresponding designs used in the state-of-the-art saturation-based theorem provers have (at least) two inherent drawbacks: the insufficient flexibility of the used inference selection mechanisms and the lack of means for intelligent prioritising of search directions. In this position paper I analyse these drawbacks and present two ideas on how they could be overcome. In particular, I propose a flexible low-cost high-precision mechanism for inference selection, intended to overcome problems associated with the currently used instances of clause selection-based procedures. I also outline a method for intelligent prioritising of search directions, based on probing the search space by exploring generalised search directions. I discuss some technical issues related to implementation of the proposed architectural principles and outline possible solutions.
A Distributed Merge and Split Algorithm for Fair Cooperation in Wireless Networks
Venue: arXiv cs.IT 2008
Year: 2008

This paper introduces a novel concept from coalitional game theory which allows the dynamic formation of coalitions among wireless nodes. A simple and distributed merge and split algorithm for coalition formation is constructed. This algorithm is applied to study the gains resulting from the cooperation among single antenna transmitters for virtual MIMO formation. The aim is to find an ultimate transmitters coalition structure that allows cooperating users to maximize their utilities while accounting for the cost of coalition formation. Through this novel game theoretical framework, the wireless network transmitters are able to self-organize and form a structured network composed of disjoint stable coalitions. Simulation results show that the proposed algorithm can improve the average individual user utility by 26.4% as well as cope with the mobility of the distributed users.
Algebraic geometry codes from higher dimensional varieties
Venue: arXiv cs.IT 2008
Year: 2008

This paper is a general survey of literature on Goppa-type codes from higher dimensional algebraic varieties. The construction and several techniques for estimating the minimum distance are described first. Codes from various classes of varieties, including Hermitian hypersurfaces, Grassmannians, flag varieties, ruled surfaces over curves, and Deligne-Lusztig varieties are considered. Connections with the theories of toric codes and order domains are also briefly indicated.
Multiclass Approaches for Support Vector Machine Based Land Cover Classification
Venue: arXiv cs.NE 2008
Year: 2008

SVMs were initially developed to perform binary classification; though, applications of binary classification are very limited. Most of the practical applications involve multiclass classification, especially in remote sensing land cover classification. A number of methods have been proposed to implement SVMs to produce multiclass classification. A number of methods to generate multiclass SVMs from binary SVMs have been proposed by researchers and is still a continuing research topic. This paper compares the performance of six multi-class approaches to solve classification problem with remote sensing data in term of classification accuracy and computational cost. One vs. one, one vs. rest, Directed Acyclic Graph (DAG), and Error Corrected Output Coding (ECOC) based multiclass approaches creates many binary classifiers and combines their results to determine the class label of a test pixel. Another catogery of multi class approach modify the binary class objective function and allows simultaneous computation of multiclass classification by solving a single optimisation problem. Results from this study conclude the usefulness of One vs. One multi class approach in term of accuracy and computational cost over other multi class approaches.
The minimal set of Ingleton inequalities
Venue: arXiv cs.IT 2008
Year: 2008

The Ingleton-LP bound is an outer bound for the multicast capacity region, assuming the use of linear network codes. Computation of the bound is performed on a polyhedral cone obtained by taking the intersection of half-spaces induced by the basic (Shannon-type) inequalities and Ingleton inequalities. This paper simplifies the characterization of this cone, by obtaining the unique minimal set of Ingleton inequalities. As a result, the effort required for computation of the Ingleton-LP bound can be greatly reduced.
The complexity of planar graph choosability
Venue: arXiv cs.DM 2008
Year: 2008

A graph $G$ is {\em $k$-choosable} if for every assignment of a set $S(v)$ of $k$ colors to every vertex $v$ of $G$, there is a proper coloring of $G$ that assigns to each vertex $v$ a color from $S(v)$. We consider the complexity of deciding whether a given graph is $k$-choosable for some constant $k$. In particular, it is shown that deciding whether a given planar graph is 4-choosable is NP-hard, and so is the problem of deciding whether a given planar triangle-free graph is 3-choosable. We also obtain simple constructions of a planar graph which is not 4-choosable and a planar triangle-free graph which is not 3-choosable.
Covering Directed Graphs by In-trees
Venue: arXiv cs.DM 2008
Year: 2008

Given a directed graph $D=(V,A)$ with a set of $d$ specified vertices $S=\{s_1,...,s_d\}\subseteq V$ and a function $f\colon S \to \mathbb{Z}_+$ where $\mathbb{Z}_+$ denotes the set of non-negative integers, we consider the problem which asks whether there exist $\sum_{i=1}^d f(s_i)$ in-trees denoted by $T_{i,1},T_{i,2},..., T_{i,f(s_i)}$ for every $i=1,...,d$ such that $T_{i,1},...,T_{i,f(s_i)}$ are rooted at $s_i$, each $T_{i,j}$ spans vertices from which $s_i$ is reachable and the union of all arc sets of $T_{i,j}$ for $i=1,...,d$ and $j=1,...,f(s_i)$ covers $A$. In this paper, we prove that such set of in-trees covering $A$ can be found by using an algorithm for the weighted matroid intersection problem in time bounded by a polynomial in $\sum_{i=1}^df(s_i)$ and the size of $D$. Furthermore, for the case where $D$ is acyclic, we present another characterization of the existence of in-trees covering $A$, and then we prove that in-trees covering $A$ can be computed more efficiently than the general case by finding maximum matchings in a series of bipartite graphs.
Factoring Polynomials over Finite Fields using Balance Test
Venue: arXiv cs.DS 2008
Year: 2008

We study the problem of factoring univariate polynomials over finite fields. Under the assumption of the Extended Riemann Hypothesis (ERH), (Gao, 2001) designed a polynomial time algorithm that fails to factor only if the input polynomial satisfies a strong symmetry property, namely square balance. In this paper, we propose an extension of Gao's algorithm that fails only under an even stronger symmetry property. We also show that our property can be used to improve the time complexity of best deterministic algorithms on most input polynomials. The property also yields a new randomized polynomial time algorithm.
On Termination for Faulty Channel Machines
Venue: arXiv cs.IT 2008
Year: 2008

A channel machine consists of a finite controller together with several fifo channels; the controller can read messages from the head of a channel and write messages to the tail of a channel. In this paper, we focus on channel machines with insertion errors, i.e., machines in whose channels messages can spontaneously appear. Such devices have been previously introduced in the study of Metric Temporal Logic. We consider the termination problem: are all the computations of a given insertion channel machine finite? We show that this problem has non-elementary, yet primitive recursive complexity.
Analytic aspects of the shuffle product
Venue: arXiv cs.IT 2008
Year: 2008

There exist very lucid explanations of the combinatorial origins of rational and algebraic functions, in particular with respect to regular and context free languages. In the search to understand how to extend these natural correspondences, we find that the shuffle product models many key aspects of D-finite generating functions, a class which contains algebraic. We consider several different takes on the shuffle product, shuffle closure, and shuffle grammars, and give explicit generating function consequences. In the process, we define a grammar class that models D-finite generating functions.
Tight Bounds for Blind Search on the Integers
Venue: arXiv cs.DS 2008
Year: 2008

We analyze a simple random process in which a token is moved in the interval $A=\{0,...,n\$: Fix a probability distribution $μ$ over $\{1,...,n\$. Initially, the token is placed in a random position in $A$. In round $t$, a random value $d$ is chosen according to $μ$. If the token is in position $a\geq d$, then it is moved to position $a-d$. Otherwise it stays put. Let $T$ be the number of rounds until the token reaches position 0. We show tight bounds for the expectation of $T$ for the optimal distribution $μ$. More precisely, we show that $\min_μ\{E_μ(T)\=Θ((\log n)^2)$. For the proof, a novel potential function argument is introduced. The research is motivated by the problem of approximating the minimum of a continuous function over $[0,1]$ with a ``blind'' optimization strategy.
Discrete Jordan Curve Theorem: A proof formalized in Coq with hypermaps
Venue: arXiv cs.LO 2008
Year: 2008

This paper presents a formalized proof of a discrete form of the Jordan Curve Theorem. It is based on a hypermap model of planar subdivisions, formal specifications and proofs assisted by the Coq system. Fundamental properties are proven by structural or noetherian induction: Genus Theorem, Euler's Formula, constructive planarity criteria. A notion of ring of faces is inductively defined and a Jordan Curve Theorem is stated and proven for any planar hypermap.
Compatibility of Shelah and Stupp's and Muchnik's iteration with fragments of monadic second order logic
Venue: arXiv cs.LO 2008
Year: 2008

We investigate the relation between the theory of the iterations in the sense of Shelah-Stupp and of Muchnik, resp., and the theory of the base structure for several logics. These logics are obtained from the restriction of set quantification in monadic second order logic to certain subsets like, e.g., finite sets, chains, and finite unions of chains. We show that these theories of the Shelah-Stupp iteration can be reduced to corresponding theories of the base structure. This fails for Muchnik's iteration.
Efficient Algorithms for Membership in Boolean Hierarchies of Regular Languages
Venue: arXiv cs.CC 2008
Year: 2008

The purpose of this paper is to provide efficient algorithms that decide membership for classes of several Boolean hierarchies for which efficiency (or even decidability) were previously not known. We develop new forbidden-chain characterizations for the single levels of these hierarchies and obtain the following results: - The classes of the Boolean hierarchy over level $Σ_1$ of the dot-depth hierarchy are decidable in $NL$ (previously only the decidability was known). The same remains true if predicates mod $d$ for fixed $d$ are allowed. - If modular predicates for arbitrary $d$ are allowed, then the classes of the Boolean hierarchy over level $Σ_1$ are decidable. - For the restricted case of a two-letter alphabet, the classes of the Boolean hierarchy over level $Σ_2$ of the Straubing-Thérien hierarchy are decidable in $NL$. This is the first decidability result for this hierarchy. - The membership problems for all mentioned Boolean-hierarchy classes are logspace many-one hard for $NL$. - The membership problems for quasi-aperiodic languages and for $d$-quasi-aperiodic languages are logspace many-one complete for $PSPACE$.