OpenRaiser/Intern-Atlas huggingface dataset:
Fast and Power Efficient Sensor Arbitration: Physical Layer Collision Recovery of Passive RFID Tags
Venue: arXiv cs.NI 2010
Year: 2010

This work concerns physical layer collision recovery for cheap sensors with allowed variations in frequency and delay of their communications. The work is presented as a generic, communication theoretic framework and demonstrated using UHF RFID tag technology. Previous work in this area has not provided recovery for more than two tags, which is shown to be possible in this work. Also presented is a novel mathematical model of the tag signal, incorporating the allowed variations in frequency and delay. The main motivation is seen in the observation that random variations in frequency and delay make the collided signals of different tags separable. The collision recovery is done by estimating the sensor specific variation in frequency and delay and using these estimates in a successive interference cancellation algorithm and a maximum likelihood sequence decoder, to iteratively reconstruct a sensor signal and remove it from the received signal. Numerical simulations show that the estimates and proposed algorithm are effective in recovering collisions. The proposed algorithm is then incorporated into a numerical simulation of the Qprotocol for UHF RFID tags and is shown to be effective in providing fast and power efficient sensor arbitration.
A Decidable Timeout based Extension of Propositional Linear Temporal Logic
Venue: arXiv cs.LO 2010
Year: 2010

We develop a timeout based extension of propositional linear temporal logic (which we call TLTL) to specify timing properties of timeout based models of real time systems. TLTL formulas explicitly refer to a running global clock together with static timing variables as well as a dynamic variable abstracting the timeout behavior. We extend LTL with the capability to express timeout constraints. From the expressiveness view point, TLTL is not comparable with important known clock based real-time logics including TPTL, XCTL, and MTL, i.e., TLTL can specify certain properties, which cannot be specified in these logics (also vice-versa). We define a corresponding timeout tableau for satisfiability checking of the TLTL formulas. Also a model checking algorithm over timeout Kripke structure is presented. Further we prove that the validity checking for such an extended logic remains PSPACE-complete even in the presence of timeout constraints and infinite state models. Under discrete time semantics, with bounded timeout increments, the model-checking problem that if a TLTL-formula holds in a timeout Kripke structure is also PSPACE complete. We further prove that when TLTL is interpreted over discrete time, it can be embedded in the monadic second order logic with time, and when TLTL is interpreted over dense time without the condition of non-zenoness, the resulting logic becomes $Σ_1^1$-complete.
The Development of Dominance Stripes and Orientation Maps in a Self-Organising Visual Cortex Network (VICON)
Venue: arXiv cs.NE 2010
Year: 2010

A self-organising neural network is presented that is based on a rigorous Bayesian analysis of the information contained in individual neural firing events. This leads to a visual cortex network (VICON) that has many of the properties emerge when a mammalian visual cortex is exposed to data arriving from two imaging sensors (i.e. the two retinae), such as dominance stripes and orientation maps.
Balanced Interval Coloring
Venue: arXiv cs.DS 2010
Year: 2010

We consider the discrepancy problem of coloring $n$ intervals with $k$ colors such that at each point on the line, the maximal difference between the number of intervals of any two colors is minimal. Somewhat surprisingly, a coloring with maximal difference at most one always exists. Furthermore, we give an algorithm with running time $O(n \log n + kn \log k)$ for its construction. This is in particular interesting because many known results for discrepancy problems are non-constructive. This problem naturally models a load balancing scenario, where $n$ tasks with given start- and endtimes have to be distributed among $k$ servers. Our results imply that this can be done ideally balanced. When generalizing to $d$-dimensional boxes (instead of intervals), a solution with difference at most one is not always possible. We show that for any $d \ge 2$ and any $k \ge 2$ it is NP-complete to decide if such a solution exists, which implies also NP-hardness of the respective minimization problem. In an online scenario, where intervals arrive over time and the color has to be decided upon arrival, the maximal difference in the size of color classes can become arbitrarily high for any online algorithm.
Improved Approximation for the Directed Spanner Problem
Venue: arXiv cs.DS 2010
Year: 2010

We prove that the size of the sparsest directed k-spanner of a graph can be approximated in polynomial time to within a factor of $\tilde{O}(\sqrt{n})$, for all k >= 3. This improves the $\tilde{O}(n^{2/3})$-approximation recently shown by Dinitz and Krauthgamer.
Self-Organising Stochastic Encoders
Venue: arXiv cs.NE 2010
Year: 2010

The processing of mega-dimensional data, such as images, scales linearly with image size only if fixed size processing windows are used. It would be very useful to be able to automate the process of sizing and interconnecting the processing windows. A stochastic encoder that is an extension of the standard Linde-Buzo-Gray vector quantiser, called a stochastic vector quantiser (SVQ), includes this required behaviour amongst its emergent properties, because it automatically splits the input space into statistically independent subspaces, which it then separately encodes. Various optimal SVQs have been obtained, both analytically and numerically. Analytic solutions which demonstrate how the input space is split into independent subspaces may be obtained when an SVQ is used to encode data that lives on a 2-torus (e.g. the superposition of a pair of uncorrelated sinusoids). Many numerical solutions have also been obtained, using both SVQs and chains of linked SVQs: (1) images of multiple independent targets (encoders for single targets emerge), (2) images of multiple correlated targets (various types of encoder for single and multiple targets emerge), (3) superpositions of various waveforms (encoders for the separate waveforms emerge - this is a type of independent component analysis (ICA)), (4) maternal and foetal ECGs (another example of ICA), (5) images of textures (orientation maps and dominance stripes emerge). Overall, SVQs exhibit a rich variety of self-organising behaviour, which effectively discovers the internal structure of the training data. This should have an immediate impact on "intelligent" computation, because it reduces the need for expert human intervention in the design of data processing algorithms.
Multicolored Dynamos on Toroidal Meshes
Venue: arXiv cs.DC 2010
Year: 2010

Detecting on a graph the presence of the minimum number of nodes (target set) that will be able to "activate" a prescribed number of vertices in the graph is called the target set selection problem (TSS) proposed by Kempe, Kleinberg, and Tardos. In TSS's settings, nodes have two possible states (active or non-active) and the threshold triggering the activation of a node is given by the number of its active neighbors. Dealing with fault tolerance in a majority based system the two possible states are used to denote faulty or non-faulty nodes, and the threshold is given by the state of the majority of neighbors. Here, the major effort was in determining the distribution of initial faults leading the entire system to a faulty behavior. Such an activation pattern, also known as dynamic monopoly (or shortly dynamo), was introduced by Peleg in 1996. In this paper we extend the TSS problem's settings by representing nodes' states with a "multicolored" set. The extended version of the problem can be described as follows: let G be a simple connected graph where every node is assigned a color from a finite ordered set C = {1, . . ., k} of colors. At each local time step, each node can recolor itself, depending on the local configurations, with the color held by the majority of its neighbors. Given G, we study the initial distributions of colors leading the system to a k monochromatic configuration in toroidal meshes, focusing on the minimum number of initial k-colored nodes. We find upper and lower bounds to the size of a dynamo, and then special classes of dynamos, outlined by means of a new approach based on recoloring patterns, are characterized.
Self-organized Emergence of Navigability on Small-World Networks
Venue: arXiv cs.SI 2010
Year: 2010

This paper mainly investigates why small-world networks are navigable and how to navigate small-world networks. We find that the navigability can naturally emerge from self-organization in the absence of prior knowledge about underlying reference frames of networks. Through a process of information exchange and accumulation on networks, a hidden metric space for navigation on networks is constructed. Navigation based on distances between vertices in the hidden metric space can efficiently deliver messages on small-world networks, in which long range connections play an important role. Numerical simulations further suggest that high cluster coefficient and low diameter are both necessary for navigability. These interesting results provide profound insights into scalable routing on the Internet due to its distributed and localized requirements.
Solving a real-life large-scale energy management problem
Venue: arXiv cs.OH 2010
Year: 2010

This paper introduces a three-phase heuristic approach for a large-scale energy management and maintenance scheduling problem. The problem is concerned with scheduling maintenance and refueling for nuclear power plants up to five years into the future, while handling a number of scenarios for future demand and prices. The goal is to minimize the expected total production costs. The first phase of the heuristic solves a simplified constraint programming model of the problem, the second performs a local search, and the third handles overproduction in a greedy fashion. This work was initiated in the context of the ROADEF/EURO Challenge 2010, a competition organized jointly by the French Operational Research and Decision Support Society, the European Operational Research Society, and the European utility company Electricite de France. In the concluding phase of the competition our team ranked second in the junior category and sixth overall. After correcting an implementation bug in the program that was submitted for evaluation, our heuristic solves all ten real-life instances, and the solutions obtained are all within 2.45% of the currently best known solutions. The results given here would have ranked first in the original competition.
Popular and/or Prestigious? Measures of Scholarly Esteem
Venue: arXiv cs.DL 2010
Year: 2010

Citation analysis does not generally take the quality of citations into account: all citations are weighted equally irrespective of source. However, a scholar may be highly cited but not highly regarded: popularity and prestige are not identical measures of esteem. In this study we define popularity as the number of times an author is cited and prestige as the number of times an author is cited by highly cited papers. Information Retrieval (IR) is the test field. We compare the 40 leading researchers in terms of their popularity and prestige over time. Some authors are ranked high on prestige but not on popularity, while others are ranked high on popularity but not on prestige. We also relate measures of popularity and prestige to date of Ph.D. award, number of key publications, organizational affiliation, receipt of prizes/honors, and gender.
Nominal Unification Revisited
Venue: arXiv cs.LO 2010
Year: 2010

Nominal unification calculates substitutions that make terms involving binders equal modulo alpha-equivalence. Although nominal unification can be seen as equivalent to Miller's higher-order pattern unification, it has properties, such as the use of first-order terms with names (as opposed to alpha-equivalence classes) and that no new names need to be generated during unification, which set it clearly apart from higher-order pattern unification. The purpose of this paper is to simplify a clunky proof from the original paper on nominal unification and to give an overview over some results about nominal unification.
A Machine Checked Model of Idempotent MGU Axioms For Lists of Equational Constraints
Venue: arXiv cs.LO 2010
Year: 2010

We present formalized proofs verifying that the first-order unification algorithm defined over lists of satisfiable constraints generates a most general unifier (MGU), which also happens to be idempotent. All of our proofs have been formalized in the Coq theorem prover. Our proofs show that finite maps produced by the unification algorithm provide a model of the axioms characterizing idempotent MGUs of lists of constraints. The axioms that serve as the basis for our verification are derived from a standard set by extending them to lists of constraints. For us, constraints are equalities between terms in the language of simple types. Substitutions are formally modeled as finite maps using the Coq library Coq.FSets.FMapInterface. Coq's method of functional induction is the main proof technique used in proving many of the axioms.
Beating the Productivity Checker Using Embedded Languages
Venue: arXiv cs.LO 2010
Year: 2010

Some total languages, like Agda and Coq, allow the use of guarded corecursion to construct infinite values and proofs. Guarded corecursion is a form of recursion in which arbitrary recursive calls are allowed, as long as they are guarded by a coinductive constructor. Guardedness ensures that programs are productive, i.e. that every finite prefix of an infinite value can be computed in finite time. However, many productive programs are not guarded, and it can be nontrivial to put them in guarded form. This paper gives a method for turning a productive program into a guarded program. The method amounts to defining a problem-specific language as a data type, writing the program in the problem-specific language, and writing a guarded interpreter for this language.
Information-Theoretic Capacity and Error Exponents of Stationary Point Processes under Random Additive Displacements
Venue: arXiv cs.IT 2010
Year: 2010

This paper studies the Shannon regime for the random displacement of stationary point processes. Let each point of some initial stationary point process in $\R^n$ give rise to one daughter point, the location of which is obtained by adding a random vector to the coordinates of the mother point, with all displacement vectors independently and identically distributed for all points. The decoding problem is then the following one: the whole mother point process is known as well as the coordinates of some daughter point; the displacements are only known through their law; can one find the mother of this daughter point? The Shannon regime is that where the dimension $n$ tends to infinity and where the logarithm of the intensity of the point process is proportional to $n$. We show that this problem exhibits a sharp threshold: if the sum of the proportionality factor and of the differential entropy rate of the noise is positive, then the probability of finding the right mother point tends to 0 with $n$ for all point processes and decoding strategies. If this sum is negative, there exist mother point processes, for instance Poisson, and decoding strategies, for instance maximum likelihood, for which the probability of finding the right mother tends to 1 with $n$. We then use large deviations theory to show that in the latter case, if the entropy spectrum of the noise satisfies a large deviation principle, then the error probability goes exponentially fast to 0 with an exponent that is given in closed form in terms of the rate function of the noise entropy spectrum. This is done for two classes of mother point processes: Poisson and Matérn. The practical interest to information theory comes from the explicit connection that we also establish between this problem and the estimation of error exponents in Shannon's additive noise channel with power constraints on the codewords.
Experience in applying remote technology in the secondary education institutions in Russia, located in rural areas (From the experience of Podolsky municipal district schools)
Venue: arXiv cs.CY 2010
Year: 2010

This article examines the experience of distance education technologies in Podolsky municipal district, Moscow region.
Jensen divergence based on Fisher's information
Venue: arXiv cs.IT 2010
Year: 2010

The measure of Jensen-Fisher divergence between probability distributions is introduced and its theoretical grounds set up. This quantity, in contrast to the remaining Jensen divergences, is very sensitive to the fluctuations of the probability distributions because it is controlled by the (local) Fisher information, which is a gradient functional of the distribution. So, it is appropriate and informative when studying the similarity of distributions, mainly for those having oscillatory character. The new Jensen-Fisher divergence shares with the Jensen-Shannon divergence the following properties: non-negativity, additivity when applied to an arbitrary number of probability densities, symmetry under exchange of these densities, vanishing if and only if all the densities are equal, and definiteness even when these densities present non-common zeros. Moreover, the Jensen-Fisher divergence is shown to be expressed in terms of the relative Fisher information as the Jensen-Shannon divergence does in terms of the Kullback-Leibler or relative Shannon entropy. Finally the Jensen-Shannon and Jensen-Fisher divergences are compared for the following three large, non-trivial and qualitatively different families of probability distributions: the sinusoidal, generalized gamma-like and Rakhmanov-Hermite distributions.
XSB: Extending Prolog with Tabled Logic Programming
Venue: arXiv cs.PL 2010
Year: 2010

The paradigm of Tabled Logic Programming (TLP) is now supported by a number of Prolog systems, including XSB, YAP Prolog, B-Prolog, Mercury, ALS, and Ciao. The reasons for this are partly theoretical: tabling ensures termination and optimal known complexity for queries to a large class of programs. However the overriding reasons are practical. TLP allows sophisticated programs to be written concisely and efficiently, especially when mechanisms such as tabled negation and call and answer subsumption are supported. As a result TLP has now been used in a variety of applications from program analysis to querying over the semantic web. This paper provides a survey of TLP and its applications as implemented in XSB Prolog, along with discussion of how XSB supports tabling with dynamically changing code, and in a multi-threaded environment.
Severe Language Effect in University Rankings: Particularly Germany and France are wronged in citation-based rankings
Venue: arXiv cs.DL 2010
Year: 2010

We applied a set of standard bibliometric indicators to monitor the scientific state-of-arte of 500 universities worldwide and constructed a ranking on the basis of these indicators (Leiden Ranking 2010). We find a dramatic and hitherto largely underestimated language effect in the bibliometric, citation-based measurement of research performance when comparing the ranking based on all Web of Science (WoS) covered publications and on only English WoS covered publications, particularly for Germany and France.
Exploring Simple Triangular and Hexagonal Grid Polygons Online
Venue: arXiv cs.CG 2010
Year: 2010

We investigate the online exploration problem (aka covering) of a short-sighted mobile robot moving in an unknown cellular environment with hexagons and triangles as types of cells. To explore a cell, the robot must enter it. Once inside, the robot knows which of the 3 or 6 adjacent cells exist and which are boundary edges. The robot's task is to visit every cell in the given environment and to return to the start. Our interest is in a short exploration tour; that is, in keeping the number of multiple cell visits small. For arbitrary environments containing no obstacles we provide a strategy producing tours of length S <= C + 1/4 E - 2.5 for hexagonal grids, and S <= C + E - 4 for triangular grids. C denotes the number of cells-the area-, E denotes the number of boundary edges-the perimeter-of the given environment. Further, we show that our strategy is 4/3-competitive in both types of grids, and we provide lower bounds of 14/13 for hexagonal grids and 7/6 for triangular grids.
Properties of Exercise Strategies
Venue: arXiv cs.CY 2010
Year: 2010

Mathematical learning environments give domain-specific and immediate feedback to students solving a mathematical exercise. Based on a language for specifying strategies, we have developed a feedback framework that automatically calculates semantically rich feedback. We offer this feedback functionality to mathematical learning environments via a set of web services. Feedback is only effective when it is precise and to the point. The tests we have performed give some confidence about the correctness of our feedback services. To increase confidence in our services, we explicitly specify the properties our feedback services should satisfy, and, if possible, prove them correct. For this, we give a formal description of the concepts used in our feedback framework services. The formalisation allows us to reason about these concepts, and to state a number of desired properties of the concepts. Our feedback services use exercise descriptions for their instances on domains such as logic, algebra, and linear algebra. We formulate requirements these domain descriptions should satisfy for the feedback services to react as expected.
Non-negative Weighted #CSPs: An Effective Complexity Dichotomy
Venue: arXiv cs.CC 2010
Year: 2010

We prove a complexity dichotomy theorem for all non-negative weighted counting Constraint Satisfaction Problems (CSP). This caps a long series of important results on counting problems including unweighted and weighted graph homomorphisms and the celebrated dichotomy theorem for unweighted #CSP. Our dichotomy theorem gives a succinct criterion for tractability. If a set F of constraint functions satisfies the criterion, then the counting CSP problem defined by F is solvable in polynomial time; if it does not satisfy the criterion, then the problem is #P-hard. We furthermore show that the question of whether F satisfies the criterion is decidable in NP. Surprisingly, our tractability criterion is simpler than the previous criteria for the more restricted classes of problems, although when specialized to those cases, they are logically equivalent. Our proof mainly uses Linear Algebra, and represents a departure from Universal Algebra, the dominant methodology in recent years.
The dependence on the initial states and the transitivity of the regular autonomous asynchronous systems
Venue: arXiv cs.OH 2010
Year: 2010

The asynchronous systems are non-deterministic real time, binary valued models of the asynchronous circuits from electronics. Autonomy means that there is no input and regularity means analogies with the (real) dynamical systems. We introduce the concepts of dependence on the initial states and of transitivity for these systems.