OpenRaiser/Intern-Atlas huggingface dataset:
Algorithms for Game Metrics
Venue: arXiv cs.GT 2010
Year: 2010

Simulation and bisimulation metrics for stochastic systems provide a quantitative generalization of the classical simulation and bisimulation relations. These metrics capture the similarity of states with respect to quantitative specifications written in the quantitative μ-calculus and related probabilistic logics. We first show that the metrics provide a bound for the difference in long-run average and discounted average behavior across states, indicating that the metrics can be used both in system verification, and in performance evaluation. For turn-based games and MDPs, we provide a polynomial-time algorithm for the computation of the one-step metric distance between states. The algorithm is based on linear programming; it improves on the previous known exponential-time algorithm based on a reduction to the theory of reals. We then present PSPACE algorithms for both the decision problem and the problem of approximating the metric distance between two states, matching the best known algorithms for Markov chains. For the bisimulation kernel of the metric our algorithm works in time O(n^4) for both turn-based games and MDPs; improving the previously best known O(n^9\cdot log(n)) time algorithm for MDPs. For a concurrent game G, we show that computing the exact distance between states is at least as hard as computing the value of concurrent reachability games and the square-root-sum problem in computational geometry. We show that checking whether the metric distance is bounded by a rational r, can be done via a reduction to the theory of real closed fields, involving a formula with three quantifier alternations, yielding O(|G|^O(|G|^5)) time complexity, improving the previously known reduction, which yielded O(|G|^O(|G|^7)) time complexity. These algorithms can be iterated to approximate the metrics using binary search.
A linear time algorithm for L(2,1)-labeling of trees
Venue: arXiv cs.DS 2010
Year: 2010

An L(2,1)-labeling of a graph $G$ is an assignment $f$ from the vertex set $V(G)$ to the set of nonnegative integers such that $|f(x)-f(y)|\ge 2$ if $x$ and $y$ are adjacent and $|f(x)-f(y)|\ge 1$ if $x$ and $y$ are at distance 2, for all $x$ and $y$ in $V(G)$. A $k$-L(2,1)-labeling is an assignment $f:V(G)\to\{0,..., k\}$, and the L(2,1)-labeling problem asks the minimum $k$, which we denote by $λ(G)$, among all possible assignments. It is known that this problem is NP-hard even for graphs of treewidth 2, and tree is one of a very few classes for which the problem is polynomially solvable. The running time of the best known algorithm for trees had been $\mO(Δ^{4.5} n)$ for more than a decade, however, an $\mO(n^{1.75})$-time algorithm has been proposed recently, which substantially improved the previous one, where $Δ$ is the maximum degree of $T$ and $n=|V(T)|$. In this paper, we finally establish a linear time algorithm for L(2,1)-labeling of trees.
On finite functions with non-trivial arity gap
Venue: arXiv cs.DM 2010
Year: 2010

Given an $n$-ary $k-$valued function $f$, $gap(f)$ denotes the minimal number of essential variables in $f$ which become fictive when identifying any two distinct essential variables in $f$. We particularly solve a problem concerning the explicit determination of $n$-ary $k-$valued functions $f$ with $2\leq gap(f)\leq n\leq k$. Our methods yield new combinatorial results about the number of such functions.
Robust Network Coding in the Presence of Untrusted Nodes
Venue: arXiv cs.IT 2010
Year: 2010

While network coding can be an efficient means of information dissemination in networks, it is highly susceptible to "pollution attacks," as the injection of even a single erroneous packet has the potential to corrupt each and every packet received by a given destination. Even when suitable error-control coding is applied, an adversary can, in many interesting practical situations, overwhelm the error-correcting capability of the code. To limit the power of potential adversaries, a broadcast transformation is introduced, in which nodes are limited to just a single (broadcast) transmission per generation. Under this broadcast transformation, the multicast capacity of a network is changed (in general reduced) from the number of edge-disjoint paths between source and sink to the number of internally-disjoint paths. Exploiting this fact, we propose a family of networks whose capacity is largely unaffected by a broadcast transformation. This results in a significant achievable transmission rate for such networks, even in the presence of adversaries.
Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax
Venue: arXiv cs.LO 2010
Year: 2010

Combining higher-order abstract syntax and (co)induction in a logical framework is well known to be problematic. Previous work described the implementation of a tool called Hybrid, within Isabelle HOL, which aims to address many of these difficulties. It allows object logics to be represented using higher-order abstract syntax, and reasoned about using tactical theorem proving and principles of (co)induction. In this paper we describe how to use it in a multi-level reasoning fashion, similar in spirit to other meta-logics such as Twelf. By explicitly referencing provability in a middle layer called a specification logic, we solve the problem of reasoning by (co)induction in the presence of non-stratifiable hypothetical judgments, which allow very elegant and succinct specifications of object logic inference rules.
Concept-Oriented Model and Query Language
Venue: arXiv cs.DB 2010
Year: 2010

We describe a new approach to data modeling, called the concept-oriented model (COM), and a novel concept-oriented query language (COQL). The model is based on three principles: duality principle postulates that any element is a couple consisting of one identity and one entity, inclusion principle postulates that any element has a super-element, and order principle assumes that any element has a number of greater elements within a partially ordered set. Concept-oriented query language is based on a new data modeling construct, called concept, inclusion relation between concepts, and concept partial ordering in which greater concepts are represented by their field types. It is demonstrated how COM and COQL can be used to solve three general data modeling tasks: logical navigation, multidimensional analysis and inference. Logical navigation is based on two operations of projection and de-projection. Multidimensional analysis uses product operation for producing a cube from level concepts chosen along the chosen dimension paths. Inference is defined as a two-step procedure where input constraints are first propagated downwards using de-projection and then the constrained result is propagated upwards using projection.
Entropy Measures vs. Algorithmic Information
Venue: arXiv cs.IT 2010
Year: 2010

Algorithmic entropy and Shannon entropy are two conceptually different information measures, as the former is based on size of programs and the later in probability distributions. However, it is known that, for any recursive probability distribution, the expected value of algorithmic entropy equals its Shannon entropy, up to a constant that depends only on the distribution. We study if a similar relationship holds for Rényi and Tsallis entropies of order $α$, showing that it only holds for Rényi and Tsallis entropies of order 1 (i.e., for Shannon entropy). Regarding a time bounded analogue relationship, we show that, for distributions such that the cumulative probability distribution is computable in time $t(n)$, the expected value of time-bounded algorithmic entropy (where the alloted time is $nt(n)\log (nt(n))$) is in the same range as the unbounded version. So, for these distributions, Shannon entropy captures the notion of computationally accessible information. We prove that, for universal time-bounded distribution $\m^t(x)$, Tsallis and Rényi entropies converge if and only if $α$ is greater than 1.
Interference and Congestion Aware Gradient Broadcasting Routing for Wireless Sensor Networks
Venue: arXiv cs.NI 2010
Year: 2010

This paper addresses the problem of reliable transmission of data through a sensor network. We focus on networks rapidly deployed in harsh environments. For these networks, important design requirements are fast data transmission and rapid network setup, as well as minimized energy consumption for increased network lifetime. We propose a novel broadcasting solution that accounts for the interference impact and the congestion level of the channel, in order to improve robustness, energy consumption and delay performance, compared to a benchmark routing protocol, the GRAB algorithm. Three solutions are proposed: P-GRAB, a probabilistic routing algorithm for interference mitigation, U-GRAB, a utility-based algorithm that adjusts to real-time congestion and UP-GRAB, a combination of P-GRAB and U-GRAB. It is shown that P-GRAB provides the best performance for geometry-aware networks while the U-GRAB approach is the best option for unreliable and unstable networks.
A Self-Contained and Easily Accessible Discussion of the Method of Descente Infinie and Fermat's Only Explicitly Known Proof by Descente Infinie
Venue: arXiv cs.AI 2010
Year: 2010

We present the only proof of Pierre Fermat by descente infinie that is known to exist today. As the text of its Latin original requires active mathematical interpretation, it is more a proof sketch than a proper mathematical proof. We discuss descente infinie from the mathematical, logical, historical, linguistic, and refined logic-historical points of view. We provide the required preliminaries from number theory and develop a self-contained proof in a modern form, which nevertheless is intended to follow Fermat's ideas closely. We then annotate an English translation of Fermat's original proof with terms from the modern proof. Including all important facts, we present a concise and self-contained discussion of Fermat's proof sketch, which is easily accessible to laymen in number theory as well as to laymen in the history of mathematics, and which provides new clarification of the Method of Descente Infinie to the experts in these fields. Last but not least, this paper fills a gap regarding the easy accessibility of the subject.
Distributed Agreement in Tile Self-Assembly
Venue: arXiv cs.DC 2010
Year: 2010

Laboratory investigations have shown that a formal theory of fault-tolerance will be essential to harness nanoscale self-assembly as a medium of computation. Several researchers have voiced an intuition that self-assembly phenomena are related to the field of distributed computing. This paper formalizes some of that intuition. We construct tile assembly systems that are able to simulate the solution of the wait-free consensus problem in some distributed systems. (For potential future work, this may allow binding errors in tile assembly to be analyzed, and managed, with positive results in distributed computing, as a "blockage" in our tile assembly model is analogous to a crash failure in a distributed computing model.) We also define a strengthening of the "traditional" consensus problem, to make explicit an expectation about consensus algorithms that is often implicit in distributed computing literature. We show that solution of this strengthened consensus problem can be simulated by a two-dimensional tile assembly model only for two processes, whereas a three-dimensional tile assembly model can simulate its solution in a distributed system with any number of processes.
New Linear Codes from Matrix-Product Codes with Polynomial Units
Venue: arXiv cs.IT 2010
Year: 2010

A new construction of codes from old ones is considered, it is an extension of the matrix-product construction. Several linear codes that improve the parameters of the known ones are presented.
Multi-mode Transmission for the MIMO Broadcast Channel with Imperfect Channel State Information
Venue: arXiv cs.IT 2010
Year: 2010

This paper proposes an adaptive multi-mode transmission strategy to improve the spectral efficiency achieved in the multiple-input multiple-output (MIMO) broadcast channel with delayed and quantized channel state information. The adaptive strategy adjusts the number of active users, denoted as the transmission mode, to balance transmit array gain, spatial division multiplexing gain, and residual inter-user interference. Accurate closed-form approximations are derived for the achievable rates for different modes, which help identify the active mode that maximizes the average sum throughput for given feedback delay and channel quantization error. The proposed transmission strategy is combined with round-robin scheduling, and is shown to provide throughput gain over single-user MIMO at moderate signal-to-noise ratio. It only requires feedback of instantaneous channel state information from a small number of users. With a feedback load constraint, the proposed algorithm provides performance close to that achieved by opportunistic scheduling with instantaneous feedback from a large number of users.
On irreversible dynamic monopolies in general graphs
Venue: arXiv cs.DM 2010
Year: 2010

Consider the following coloring process in a simple directed graph $G(V,E)$ with positive indegrees. Initially, a set $S$ of vertices are white, whereas all the others are black. Thereafter, a black vertex is colored white whenever more than half of its in-neighbors are white. The coloring process ends when no additional vertices can be colored white. If all vertices end up white, we call $S$ an irreversible dynamic monopoly (or dynamo for short) under the strict-majority scenario. An irreversible dynamo under the simple-majority scenario is defined similarly except that a black vertex is colored white when at least half of its in-neighbors are white. We derive upper bounds of $(2/3)\,|\,V\,|$ and $|\,V\,|/2$ on the minimum sizes of irreversible dynamos under the strict and the simple-majority scenarios, respectively. For the special case when $G$ is an undirected connected graph, we prove the existence of an irreversible dynamo with size at most $\lceil |\,V\,|/2 \rceil$ under the strict-majority scenario. Let $ε>0$ be any constant. We also show that, unless $\text{NP}\subseteq \text{TIME}(n^{O(\ln \ln n)}),$ no polynomial-time, $((1/2-ε)\ln |\,V\,|)$-approximation algorithms exist for finding the minimum irreversible dynamo under either the strict or the simple-majority scenario. The inapproximability results hold even for bipartite graphs with diameter at most 8.
Bounded Linear Logic, Revisited
Venue: arXiv cs.LO 2010
Year: 2010

We present QBAL, an extension of Girard, Scedrov and Scott's bounded linear logic. The main novelty of the system is the possibility of quantifying over resource variables. This generalization makes bounded linear logic considerably more flexible, while preserving soundness and completeness for polynomial time. In particular, we provide compositional embeddings of Leivant's RRW and Hofmann's LFPL into QBAL.
Toggling operators in computability logic
Venue: arXiv cs.LO 2010
Year: 2010

Computability logic (CL) (see http://www.cis.upenn.edu/~giorgi/cl.html ) is a research program for redeveloping logic as a formal theory of computability, as opposed to the formal theory of truth which it has more traditionally been. Formulas in CL stand for interactive computational problems, seen as games between a machine and its environment; logical operators represent operations on such entities; and "truth" is understood as existence of an effective solution. The formalism of CL is open-ended, and may undergo series of extensions as the studies of the subject advance. So far three -- parallel, sequential and choice -- sorts of conjunction and disjunction have been studied. The present paper adds one more natural kind to this collection, termed toggling. The toggling operations can be characterized as lenient versions of choice operations where choices are retractable, being allowed to be reconsidered any finite number of times. This way, they model trial-and-error style decision steps in interactive computation. The main technical result of this paper is constructing a sound and complete axiomatization for the propositional fragment of computability logic whose vocabulary, together with negation, includes all four -- parallel, toggling, sequential and choice -- kinds of conjunction and disjunction. Along with toggling conjunction and disjunction, the paper also introduces the toggling versions of quantifiers and recurrence operations.
Dictionary Identification - Sparse Matrix-Factorisation via $\ell_1$-Minimisation
Venue: arXiv cs.IT 2010
Year: 2010

This article treats the problem of learning a dictionary providing sparse representations for a given signal class, via $\ell_1$-minimisation. The problem can also be seen as factorising a $\ddim \times \nsig$ matrix $Y=(y_1 >... y_\nsig), y_n\in \R^\ddim$ of training signals into a $\ddim \times \natoms$ dictionary matrix $\dico$ and a $\natoms \times \nsig$ coefficient matrix $\X=(x_1... x_\nsig), x_n \in \R^\natoms$, which is sparse. The exact question studied here is when a dictionary coefficient pair $(\dico,\X)$ can be recovered as local minimum of a (nonconvex) $\ell_1$-criterion with input $Y=\dico \X$. First, for general dictionaries and coefficient matrices, algebraic conditions ensuring local identifiability are derived, which are then specialised to the case when the dictionary is a basis. Finally, assuming a random Bernoulli-Gaussian sparse model on the coefficient matrix, it is shown that sufficiently incoherent bases are locally identifiable with high probability. The perhaps surprising result is that the typically sufficient number of training samples $\nsig$ grows up to a logarithmic factor only linearly with the signal dimension, i.e. $\nsig \approx C \natoms \log \natoms$, in contrast to previous approaches requiring combinatorially many samples.
Phoenix Cloud: Consolidating Different Computing Loads on Shared Cluster System for Large Organization
Venue: arXiv cs.DC 2010
Year: 2010

Different departments of a large organization often run dedicated cluster systems for different computing loads, like HPC (high performance computing) jobs or Web service applications. In this paper, we have designed and implemented a cloud management system software Phoenix Cloud to consolidate heterogeneous workloads from different departments affiliated to the same organization on the shared cluster system. We have also proposed cooperative resource provisioning and management policies for a large organization and its affiliated departments, running HPC jobs and Web service applications, to share the consolidated cluster system. The experiments show that in comparison with the case that each department operates its dedicated cluster system, Phoenix Cloud significantly decreases the scale of the required cluster system for a large organization, improves the benefit of the scientific computing department, and at the same time provisions enough resources to the other department running Web services with varying loads.
Classical Predicative Logic-Enriched Type Theories
Venue: arXiv cs.LO 2010
Year: 2010

A logic-enriched type theory (LTT) is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named LTTO and LTTO*, which we claim correspond closely to the classical predicative systems of second order arithmetic ACAO and ACA. We justify this claim by translating each second-order system into the corresponding LTT, and proving that these translations are conservative. This is part of an ongoing research project to investigate how LTTs may be used to formalise different approaches to the foundations of mathematics. The two LTTs we construct are subsystems of the logic-enriched type theory LTTW, which is intended to formalise the classical predicative foundation presented by Herman Weyl in his monograph Das Kontinuum. The system ACAO has also been claimed to correspond to Weyl's foundation. By casting ACAO and ACA as LTTs, we are able to compare them with LTTW. It is a consequence of the work in this paper that LTTW is strictly stronger than ACAO. The conservativity proof makes use of a novel technique for proving one LTT conservative over another, involving defining an interpretation of the stronger system out of the expressions of the weaker. This technique should be applicable in a wide variety of different cases outside the present work.
Approximate Characterizations for the Gaussian Source Broadcast Distortion Region
Venue: arXiv cs.IT 2010
Year: 2010

We consider the joint source-channel coding problem of sending a Gaussian source on a K-user Gaussian broadcast channel with bandwidth mismatch. A new outer bound to the achievable distortion region is derived using the technique of introducing more than one additional auxiliary random variable, which was previously used to derive sum-rate lower bound for the symmetric Gaussian multiple description problem. By combining this outer bound with the achievability result based on source-channel separation, we provide approximate characterizations of the achievable distortion region within constant multiplicative factors. Furthermore, we show that the results can be extended to general broadcast channels, and the performance of the source-channel separation based approach is also within the same constant multiplicative factors of the optimum.
On the Algorithmic Nature of the World
Venue: arXiv cs.CC 2010
Year: 2010

We propose a test based on the theory of algorithmic complexity and an experimental evaluation of Levin's universal distribution to identify evidence in support of or in contravention of the claim that the world is algorithmic in nature. To this end we have undertaken a statistical comparison of the frequency distributions of data from physical sources on the one hand--repositories of information such as images, data stored in a hard drive, computer programs and DNA sequences--and the frequency distributions generated by purely algorithmic means on the other--by running abstract computing devices such as Turing machines, cellular automata and Post Tag systems. Statistical correlations were found and their significance measured.
Large deviations sum-queue optimality of a radial sum-rate monotone opportunistic scheduler
Venue: arXiv cs.IT 2010
Year: 2010

A centralized wireless system is considered that is serving a fixed set of users with time varying channel capacities. An opportunistic scheduling rule in this context selects a user (or users) to serve based on the current channel state and user queues. Unless the user traffic is symmetric and/or the underlying capacity region a polymatroid, little is known concerning how performance optimal schedulers should tradeoff "maximizing current service rate" (being opportunistic) versus "balancing unequal queues" (enhancing user-diversity to enable future high service rate opportunities). By contrast with currently proposed opportunistic schedulers, e.g., MaxWeight and Exp Rule, a radial sum-rate monotone (RSM) scheduler de-emphasizes queue-balancing in favor of greedily maximizing the system service rate as the queue-lengths are scaled up linearly. In this paper it is shown that an RSM opportunistic scheduler, p-Log Rule, is not only throughput-optimal, but also maximizes the asymptotic exponential decay rate of the sum-queue distribution for a two-queue system. The result complements existing optimality results for opportunistic scheduling and point to RSM schedulers as a good design choice given the need for robustness in wireless systems with both heterogeneity and high degree of uncertainty.