OpenRaiser/Intern-Atlas huggingface dataset:
Playing Pushdown Parity Games in a Hurry
Venue: arXiv cs.GT 2012
Year: 2012

We continue the investigation of finite-duration variants of infinite-duration games by extending known results for games played on finite graphs to those played on infinite ones. In particular, we establish an equivalence between pushdown parity games and a finite-duration variant. This allows us to determine the winner of a pushdown parity game by solving a reachability game on a finite tree.
Unambiguous Tree Languages Are Topologically Harder Than Deterministic Ones
Venue: arXiv cs.FL 2012
Year: 2012

The paper gives an example of a tree language G that is recognised by an unambiguous parity automaton and is analytic-complete as a set in Cantor space. This already shows that the unambiguous languages are topologically more complex than the deterministic ones, that are all coanalytic. Using set G as a building block we construct an unambiguous language that is topologically harder than any countable boolean combination of analytic and coanalytic sets. In particular the language is harder than any set in difference hierarchy of analytic sets considered by O.Finkel and P.Simonnet in the context of nondeterministic automata.
Minimum Component Based First-Order Inverting and Non-inverting Outputs of All-Pass Filter at the Same Circuit
Venue: arXiv cs.OH 2012
Year: 2012

In this paper, a new voltage-mode first order all-pass filter using minimum active and passive components is presented. The proposed circuit employs one fully differential second generation current conveyor (FDCCII), one grounded capacitor, one resistor and offers the following advantages: the use of only grounded capacitor which is attractive for integrated circuit implementation, low active and passive sensitivities, providing inverting and non-inverting voltage-mode all-pass responses simultaneously from the single circuit and no requirement for component matching conditions. The theory is validated through PSPICE simulation using TSMC 0.35micrometer CMOS process parameters.
New Generalizations of the Bethe Approximation via Asymptotic Expansion
Venue: arXiv cs.IT 2012
Year: 2012

The Bethe approximation, discovered in statistical physics, gives an efficient algorithm called belief propagation (BP) for approximating a partition function. BP empirically gives an accurate approximation for many problems, e.g., low-density parity-check codes, compressed sensing, etc. Recently, Vontobel gives a novel characterization of the Bethe approximation using graph cover. In this paper, a new approximation based on the Bethe approximation is proposed. The new approximation is derived from Vontobel's characterization using graph cover, and expressed by using the edge zeta function, which is related with the Hessian of the Bethe free energy as shown by Watanabe and Fukumizu. On some conditions, it is proved that the new approximation is asymptotically better than the Bethe approximation.
Concrete Semantics of Programs with Non-Deterministic and Random Inputs
Venue: arXiv cs.LO 2012
Year: 2012

This document gives semantics to programs written in a C-like programming language, featuring interactions with an external environment with noisy and imprecise data.
Complete Axiomatizations of Fragments of Monadic Second-Order Logic on Finite Trees
Venue: arXiv cs.LO 2012
Year: 2012

We consider a specific class of tree structures that can represent basic structures in linguistics and computer science such as XML documents, parse trees, and treebanks, namely, finite node-labeled sibling-ordered trees. We present axiomatizations of the monadic second-order logic (MSO), monadic transitive closure logic (FO(TC1)) and monadic least fixed-point logic (FO(LFP1)) theories of this class of structures. These logics can express important properties such as reachability. Using model-theoretic techniques, we show by a uniform argument that these axiomatizations are complete, i.e., each formula that is valid on all finite trees is provable using our axioms. As a backdrop to our positive results, on arbitrary structures, the logics that we study are known to be non-recursively axiomatizable.
Optimization in Differentiable Manifolds in Order to Determine the Method of Construction of Prehistoric Wall-Paintings
Venue: arXiv cs.CV 2012
Year: 2012

In this paper a general methodology is introduced for the determination of potential prototype curves used for the drawing of prehistoric wall-paintings. The approach includes a) preprocessing of the wall-paintings contours to properly partition them, according to their curvature, b) choice of prototype curves families, c) analysis and optimization in 4-manifold for a first estimation of the form of these prototypes, d) clustering of the contour parts and the prototypes, to determine a minimal number of potential guides, e) further optimization in 4-manifold, applied to each cluster separately, in order to determine the exact functional form of the potential guides, together with the corresponding drawn contour parts. The introduced methodology simultaneously deals with two problems: a) the arbitrariness in data-points orientation and b) the determination of one proper form for a prototype curve that optimally fits the corresponding contour data. Arbitrariness in orientation has been dealt with a novel curvature based error, while the proper forms of curve prototypes have been exhaustively determined by embedding curvature deformations of the prototypes into 4-manifolds. Application of this methodology to celebrated wall-paintings excavated at Tyrins, Greece and the Greek island of Thera, manifests it is highly probable that these wall-paintings had been drawn by means of geometric guides that correspond to linear spirals and hyperbolae. These geometric forms fit the drawings' lines with an exceptionally low average error, less than 0.39mm. Hence, the approach suggests the existence of accurate realizations of complicated geometric entities, more than 1000 years before their axiomatic formulation in Classical Ages.
Inferring Species Trees from Incongruent Multi-Copy Gene Trees Using the Robinson-Foulds Distance
Venue: arXiv cs.DS 2012
Year: 2012

We present a new method for inferring species trees from multi-copy gene trees. Our method is based on a generalization of the Robinson-Foulds (RF) distance to multi-labeled trees (mul-trees), i.e., gene trees in which multiple leaves can have the same label. Unlike most previous phylogenetic methods using gene trees, this method does not assume that gene tree incongruence is caused by a single, specific biological process, such as gene duplication and loss, deep coalescence, or lateral gene transfer. We prove that it is NP-hard to compute the RF distance between two mul-trees, but it is easy to calculate the generalized RF distance between a mul-tree and a singly-labeled tree. Motivated by this observation, we formulate the RF supertree problem for mul-trees (MulRF), which takes a collection of mul-trees and constructs a species tree that minimizes the total RF distance from the input mul-trees. We present a fast heuristic algorithm for the MulRF supertree problem. Simulation experiments demonstrate that the MulRF method produces more accurate species trees than gene tree parsimony methods when incongruence is caused by gene tree error, duplications and losses, and/or lateral gene transfer. Furthermore, the MulRF heuristic runs quickly on data sets containing hundreds of trees with up to a hundred taxa.
AI in arbitrary world
Venue: arXiv cs.AI 2012
Year: 2012

In order to build AI we have to create a program which copes well in an arbitrary world. In this paper we will restrict our attention on one concrete world, which represents the game Tick-Tack-Toe. This world is a very simple one but it is sufficiently complicated for our task because most people cannot manage with it. The main difficulty in this world is that the player cannot see the entire internal state of the world so he has to build a model in order to understand the world. The model which we will offer will consist of final automata and first order formulas.
Kinects and Human Kinetics: A New Approach for Studying Crowd Behavior
Venue: arXiv cs.CV 2012
Year: 2012

Modeling crowd behavior relies on accurate data of pedestrian movements at a high level of detail. Imaging sensors such as cameras provide a good basis for capturing such detailed pedestrian motion data. However, currently available computer vision technologies, when applied to conventional video footage, still cannot automatically unveil accurate motions of groups of people or crowds from the image sequences. We present a novel data collection approach for studying crowd behavior which uses the increasingly popular low-cost sensor Microsoft Kinect. The Kinect captures both standard camera data and a three-dimensional depth map. Our human detection and tracking algorithm is based on agglomerative clustering of depth data captured from an elevated view - in contrast to the lateral view used for gesture recognition in Kinect gaming applications. Our approach transforms local Kinect 3D data to a common world coordinate system in order to stitch together human trajectories from multiple Kinects, which allows for a scalable and flexible capturing area. At a testbed with real-world pedestrian traffic we demonstrate that our approach can provide accurate trajectories from three Kinects with a Pedestrian Detection Rate of up to 94% and a Multiple Object Tracking Precision of 4 cm. Using a comprehensive dataset of 2240 captured human trajectories we calibrate three variations of the Social Force model. The results of our model validations indicate their particular ability to reproduce the observed crowd behavior in microscopic simulations.
A Proposed General Method for Parameter Estimation of Noise Corrupted Oscillator Systems
Venue: arXiv cs.SY 2012
Year: 2012

This paper provides a proposed means to estimate parameters of noise corrupted oscillator systems. An application for a submarine combat control systems (CCS) rack is described as exemplary of the method.
A call-by-value lambda-calculus with lists and control
Venue: arXiv cs.LO 2012
Year: 2012

Calculi with control operators have been studied to reason about control in programming languages and to interpret the computational content of classical proofs. To make these calculi into a real programming language, one should also include data types. As a step into that direction, this paper defines a simply typed call-by-value lambda calculus with the control operators catch and throw, a data type of lists, and an operator for primitive recursion (a la Goedel's T). We prove that our system satisfies subject reduction, progress, confluence for untyped terms, and strong normalization for well-typed terms.
Performance Analysis of Probabilistic Rebroadcasting in Grid FSR for MANET
Venue: arXiv cs.NI 2012
Year: 2012

Mobile Ad-hoc Network (MANET) is the self organizing collection of mobile nodes. The communication in MANET is done via a wireless media. Ad hoc wireless networks have massive commercial and military potential because of their mobility support. Due to demanding real time multimedia applications, Quality of Services (QoS) support in such infrastructure less networks have become essential. QoS routing in mobile Ad-Hoc networks is challenging due to rapid change in network topology. In this paper, we focused to reduce flooding performance of the Fisheye State Routing (FSR) protocol in Grid using ns-2 network simulator under different performance metrics scenario in respect to number of Nodes. For example, the connection establishment is costly in terms of time and resource where the network is mostly affected by connection request flooding. The proposed approach presents a way to reduce flooding in MANETs. Flooding is dictated by the propagation of connection-request packets from the source to its neighborhood nodes. The proposed architecture embarks on the concept of sharing neighborhood information. The proposed approach focuses on exposing its neighborhood peer to another node that is referred to as its friend-node, which had requested/forwarded connection request. If there is a high probability for the friend node to communicate through the exposed routes, this could improve the efficacy of bandwidth utilization by reducing flooding, as the routes have been acquired, without any broadcasts. Friendship between nodes is quantized based on empirical computations and heuristic algorithms. The nodes store the neighborhood information in their cache that is periodically verified for consistency. Simulation results show the performance of this proposed method.
Risks of Friendships on Social Networks
Venue: arXiv cs.SI 2012
Year: 2012

In this paper, we explore the risks of friends in social networks caused by their friendship patterns, by using real life social network data and starting from a previously defined risk model. Particularly, we observe that risks of friendships can be mined by analyzing users' attitude towards friends of friends. This allows us to give new insights into friendship and risk dynamics on social networks.
Detecting dense communities in large social and information networks with the Core & Peel algorithm
Venue: arXiv cs.SI 2012
Year: 2012

Detecting and characterizing dense subgraphs (tight communities) in social and information networks is an important exploratory tool in social network analysis. Several approaches have been proposed that either (i) partition the whole network into clusters, even in low density region, or (ii) are aimed at finding a single densest community (and need to be iterated to find the next one). As social networks grow larger both approaches (i) and (ii) result in algorithms too slow to be practical, in particular when speed in analyzing the data is required. In this paper we propose an approach that aims at balancing efficiency of computation and expressiveness and manageability of the output community representation. We define the notion of a partial dense cover (PDC) of a graph. Intuitively a PDC of a graph is a collection of sets of nodes that (a) each set forms a disjoint dense induced subgraphs and (b) its removal leaves the residual graph without dense regions. Exact computation of PDC is an NP-complete problem, thus, we propose an efficient heuristic algorithms for computing a PDC which we christen Core and Peel. Moreover we propose a novel benchmarking technique that allows us to evaluate algorithms for computing PDC using the classical IR concepts of precision and recall even without a golden standard. Tests on 25 social and technological networks from the Stanford Large Network Dataset Collection confirm that Core and Peel is efficient and attains very high precison and recall.
An optimized conflict-free replicated set
Venue: arXiv cs.DC 2012
Year: 2012

Eventual consistency of replicated data supports concurrent updates, reduces latency and improves fault tolerance, but forgoes strong consistency. Accordingly, several cloud computing platforms implement eventually-consistent data types. The set is a widespread and useful abstraction, and many replicated set designs have been proposed. We present a reasoning abstraction, permutation equivalence, that systematizes the characterization of the expected concurrency semantics of concurrent types. Under this framework we present one of the existing conflict-free replicated data types, Observed-Remove Set. Furthermore, in order to decrease the size of meta-data, we propose a new optimization to avoid tombstones. This approach that can be transposed to other data types, such as maps, graphs or sequences.
A polygon-based interpolation operator for super-resolution imaging
Venue: arXiv cs.CV 2012
Year: 2012

We outline the super-resolution reconstruction problem posed as a maximization of probability. We then introduce an interpolation method based on polygonal pixel overlap, express it as a linear operator, and use it to improve reconstruction. Polygon interpolation outperforms the simpler bilinear interpolation operator and, unlike Gaussian modeling of pixels, requires no parameter estimation. A free software implementation that reproduces the results shown is provided.
Notes on image annotation
Venue: arXiv cs.CV 2012
Year: 2012

We are under the illusion that seeing is effortless, but frequently the visual system is lazy and makes us believe that we understand something when in fact we don't. Labeling a picture forces us to become aware of the difficulties underlying scene understanding. Suddenly, the act of seeing is not effortless anymore. We have to make an effort in order to understand parts of the picture that we neglected at first glance. In this report, an expert image annotator relates her experience on segmenting and labeling tens of thousands of images. During this process, the notes she took try to highlight the difficulties encountered, the solutions adopted, and the decisions made in order to get a consistent set of annotations. Those annotations constitute the SUN database.
Microelectromechanical system cantilever-based frequency doublers
Venue: arXiv cs.OH 2012
Year: 2012

Microelectromechanical system (MEMS) based on-chip resonators offer great potential for high frequency signal processing circuits like reference oscillators and filters. This is due to their exceptional features like small size, large frequency-quality factor product, integrability with CMOS ICs, low power consumption, low cost batch fabrication etc. A capacitively transduced cantilever beam resonator is one such popular MEMS resonator topology. In this letter, the inherent square-law nonlinearity of the voltage-to-force transfer function of a cantilever resonator's capacitive transducer has been employed for the realization of frequency doubling effect. Using this concept, frequency doubling of input signals of 500 kHz to 1 MHz, and 227.5 kHz to 455 kHz has been experimentally demonstrated for two cantilever beams of length 51.75 and 76.75 micrometer respectively. The MEMS cantilevers have been fabricated with polysilicon using the PolyMUMPs surface micromachining process, and their testing has been performed using Laser Doppler Vibrometry. The test results obtained are in reasonable compliance with the analytical and CoventorWare finite-element simulation results. The high efficiency demonstrated by the cantilever frequency doubler makes it a promising choice for signal generation at high frequencies.
Multiplayer Cost Games with Simple Nash Equilibria
Venue: arXiv cs.GT 2012
Year: 2012

Multiplayer games with selfish agents naturally occur in the design of distributed and embedded systems. As the goals of selfish agents are usually neither equivalent nor antagonistic to each other, such games are non zero-sum games. We study such games and show that a large class of these games, including games where the individual objectives are mean- or discounted-payoff, or quantitative reachability, and show that they do not only have a solution, but a simple solution. We establish the existence of Nash equilibria that are composed of k memoryless strategies for each agent in a setting with k agents, one main and k-1 minor strategies. The main strategy describes what happens when all agents comply, whereas the minor strategies ensure that all other agents immediately start to co-operate against the agent who first deviates from the plan. This simplicity is important, as rational agents are an idealisation. Realistically, agents have to decide on their moves with very limited resources, and complicated strategies that require exponential--or even non-elementary--implementations cannot realistically be implemented. The existence of simple strategies that we prove in this paper therefore holds a promise of implementability.
Modelling a Decentralized Constraint Satisfaction Solver for Collision-Free Channel Access
Venue: arXiv cs.NI 2012
Year: 2012

In this paper, the problem of assigning channel slots to a number of contending stations is modeled as a Constraint Satisfaction Problem (CSP). A learning MAC protocol that uses deterministic backoffs after successful transmissions is used as a decentralized solver for the CSP. The convergence process of the solver is modeled by an absorbing Markov chain (MC), and analytical, closed-form expressions for its transition probabilities are derived. Using these, the expected number of steps required to reach a solution is found. The analysis is validated by means of simulations and the model is extended to account for the presence of channel errors. The results are applicable in various resource allocation scenarios in wireless networks.
Quick Summary
Venue: arXiv cs.CL 2012
Year: 2012

Quick Summary is an innovate implementation of an automatic document summarizer that inputs a document in the English language and evaluates each sentence. The scanner or evaluator determines criteria based on its grammatical structure and place in the paragraph. The program then asks the user to specify the number of sentences the person wishes to highlight. For example should the user ask to have three of the most important sentences, it would highlight the first and most important sentence in green. Commonly this is the sentence containing the conclusion. Then Quick Summary finds the second most important sentence usually called a satellite and highlights it in yellow. This is usually the topic sentence. Then the program finds the third most important sentence and highlights it in red. The implementations of this technology are useful in a society of information overload when a person typically receives 42 emails a day (Microsoft). The paper also is a candid look at difficulty that machine learning has in textural translating. However, it speaks on how to overcome the obstacles that historically prevented progress. This paper proposes mathematical meta-data criteria that justify the place of importance of a sentence. Just as tools for the study of relational symmetry in bio-informatics, this tool seeks to classify words with greater clarity. "Survey Finds Workers Average Only Three Productive Days per Week." Microsoft News Center. Microsoft. Web. 31 Mar. 2012.
Estimation and compensation of inter carrier interference in wimax physical layer under various channel models
Venue: arXiv cs.NI 2012
Year: 2012

WiMAX is Wireless Interoperability for Microwave Access has emerged as a promising solution for transmission of higher data rates for fixed and mobile applications. IEEE 802.16d and e are the standards proposed. To attain higher data rates the Multi Carrier System with Multiple Input and Multiple Output MIMO is incorporated in the WiMAX. And all these sub carriers are considered to be orthogonal to each other. As the number of sub carriers is increased there is no guarantee of sustained orthogonality, i.e. at some point the carriers are not independent to each other, and hence where the orthogonality can be loosed which leads to interference and also owing to the synchronization between transmitter and receiver local oscillator, it causes interference known as Inter Carrier Interference (ICI).In this scheme at the transmitter side the modulated data and a few predefined pilot symbols are mapped onto the non neighboring sub carriers with weighting coefficients of +1 and -1. With the aid of pilot symbols the frequency offset is exactly estimated by using Maximum Likelihood Estimation MLE and hence can be minimized. At demodulation stage the received signals are linearly combined along with their weighted oefficients and pilot symbols, called as Pilot Aided Self Cancellation Method PASCS. The simulations are carried out on Stanford University Interim (SUI)channels. The simulation results shows that by incorporating this method into WiMAX systems it performs better when the Line Of Sight (LOS) component is present in the transmission and also it improves the Bit Error Rate (BER) and Carrier to Interference Ratio (CIR). The CIR can be improved 20 dB. In this paper the effectiveness of PASCS scheme is compared with the Self Cancellation Method (SCM). It provides accurate estimation of frequency offset and when residual CFO is less significant the ICI can be diminished successfully.