OpenRaiser/Intern-Atlas huggingface dataset:
Perspicuity and Granularity in Refinement
Venue: arXiv cs.SE 2011
Year: 2011

This paper reconsiders refinements which introduce actions on the concrete level which were not present at the abstract level. It draws a distinction between concrete actions which are "perspicuous" at the abstract level, and changes of granularity of actions between different levels of abstraction. The main contribution of this paper is in exploring the relation between these different methods of "action refinement", and the basic refinement relation that is used. In particular, it shows how the "refining skip" method is incompatible with failures-based refinement relations, and consequently some decisions in designing Event-B refinement are entangled.
Concurrent Scheduling of Event-B Models
Venue: arXiv cs.LO 2011
Year: 2011

Event-B is a refinement-based formal method that has been shown to be useful in developing concurrent and distributed programs. Large models can be decomposed into sub-models that can be refined semi-independently and executed in parallel. In this paper, we show how to introduce explicit control flow for the concurrent sub-models in the form of event schedules. We explore how schedules can be designed so that their application results in a correctness-preserving refinement step. For practical application, two patterns for schedule introduction are provided, together with their associated proof obligations. We demonstrate our method by applying it on the dining philosophers problem.
Parameterized Eulerian Strong Component Arc Deletion Problem on Tournaments
Venue: arXiv cs.DS 2011
Year: 2011

In the problem {\sc Min-DESC}, we are given a digraph $D$ and an integer $k$, and asked if there exists a set $A'$ of at most $k$ arcs in $D$, such that if we remove the arcs of $A'$, in the resulting digraph every strong component is Eulerian. {\sc Min-DESC} is NP-hard; Cechlárová and Schlotter (IPEC 2010) asked if the problem is fixed-parameter tractable when parameterized by $k$. We consider the subproblem of{\sc Min-DESC} when $D$ is a tournament. We show that this problem is fixed-parameter tractable with respect to $k$.
Development of mechanism for enhancing data security in quantum cryptography
Venue: arXiv cs.CR 2011
Year: 2011

Nowadays security in communication is increasingly important to the network communication because many categories of data are required restriction on authorization of access, modify, delete and insert. Quantum cryptography is one of the solutions that use property of polarization to ensure that transmitted data is not tampered. The research paper provides the mechanism that enhances the data security in quantum cryptography during exchange of information. In first phase detailed explanation of Quantum key distribution's BB84 protocol is given. BB84 protocol is used as the basis for the mechanism. In next phase the proposed mechanism is explained. The proposed mechanism combines BB84 protocol at two levels, from sender to receiver and then from receiver to sender. Moreover, a logic circuit is used to combine the bits hence to reduce the probability of eavesdropping. The key obtained can be used to exchange the information securely further it can help in encryption and decryption of crucial data. Double level BB84 mechanism will help in information reconciliation as well as privacy amplification. In future the proposed mechanism will be very beneficial where unconditional security is required during key and other secret information exchange
Fast Isomorphism Testing of Graphs with Regularly-Connected Components
Venue: arXiv cs.DS 2011
Year: 2011

The Graph Isomorphism problem has both theoretical and practical interest. In this paper we present an algorithm, called conauto-1.2, that efficiently tests whether two graphs are isomorphic, and finds an isomorphism if they are. This algorithm is an improved version of the algorithm conauto, which has been shown to be very fast for random graphs and several families of hard graphs. In this paper we establish a new theorem that allows, at very low cost, the easy discovery of many automorphisms. This result is especially suited for graphs with regularly connected components, and can be applied in any isomorphism testing and canonical labeling algorithm to drastically improve its performance. In particular, algorithm conauto-1.2 is obtained by the application of this result to conauto. The resulting algorithm preserves all the nice features of conauto, but drastically improves the testing of graphs with regularly connected components. We run extensive experiments, which show that the most popular algorithms (namely, nauty and bliss) can not compete with conauto-1.2 for these graph families.
OFDM pilot allocation for sparse channel estimation
Venue: arXiv cs.IT 2011
Year: 2011

In communication systems, efficient use of the spectrum is an indispensable concern. Recently the use of compressed sensing for the purpose of estimating Orthogonal Frequency Division Multiplexing (OFDM) sparse multipath channels has been proposed to decrease the transmitted overhead in form of the pilot subcarriers which are essential for channel estimation. In this paper, we investigate the problem of deterministic pilot allocation in OFDM systems. The method is based on minimizing the coherence of the submatrix of the unitary Discrete Fourier Transform (DFT) matrix associated with the pilot subcarriers. Unlike the usual case of equidistant pilot subcarriers, we show that non-uniform patterns based on cyclic difference sets are optimal. In cases where there are no difference sets, we perform a greedy search method for finding a suboptimal solution. We also investigate the performance of the recovery methods such as Orthogonal Matching Pursuit (OMP) and Iterative Method with Adaptive Thresholding (IMAT) for estimation of the channel taps.
The Communicative Multiagent Team Decision Problem: Analyzing Teamwork Theories and Models
Venue: arXiv cs.AI 2011
Year: 2011

Despite the significant progress in multiagent teamwork, existing research does not address the optimality of its prescriptions nor the complexity of the teamwork problem. Without a characterization of the optimality-complexity tradeoffs, it is impossible to determine whether the assumptions and approximations made by a particular theory gain enough efficiency to justify the losses in overall performance. To provide a tool for use by multiagent researchers in evaluating this tradeoff, we present a unified framework, the COMmunicative Multiagent Team Decision Problem (COM-MTDP). The COM-MTDP model combines and extends existing multiagent theories, such as decentralized partially observable Markov decision processes and economic team theory. In addition to their generality of representation, COM-MTDPs also support the analysis of both the optimality of team performance and the computational complexity of the agents' decision problem. In analyzing complexity, we present a breakdown of the computational complexity of constructing optimal teams under various classes of problem domains, along the dimensions of observability and communication cost. In analyzing optimality, we exploit the COM-MTDP's ability to encode existing teamwork theories and models to encode two instantiations of joint intentions theory taken from the literature. Furthermore, the COM-MTDP model provides a basis for the development of novel team coordination algorithms. We derive a domain-independent criterion for optimal communication and provide a comparative analysis of the two joint intentions instantiations with respect to this optimal policy. We have implemented a reusable, domain-independent software package based on COM-MTDPs to analyze teamwork coordination strategies, and we demonstrate its use by encoding and evaluating the two joint intentions strategies within an example domain.
Competitive Safety Analysis: Robust Decision-Making in Multi-Agent Systems
Venue: arXiv cs.GT 2011
Year: 2011

Much work in AI deals with the selection of proper actions in a given (known or unknown) environment. However, the way to select a proper action when facing other agents is quite unclear. Most work in AI adopts classical game-theoretic equilibrium analysis to predict agent behavior in such settings. This approach however does not provide us with any guarantee for the agent. In this paper we introduce competitive safety analysis. This approach bridges the gap between the desired normative AI approach, where a strategy should be selected in order to guarantee a desired payoff, and equilibrium analysis. We show that a safety level strategy is able to guarantee the value obtained in a Nash equilibrium, in several classical computer science settings. Then, we discuss the concept of competitive safety strategies, and illustrate its use in a decentralized load balancing setting, typical to network problems. In particular, we show that when we have many agents, it is possible to guarantee an expected payoff which is a factor of 8/9 of the payoff obtained in a Nash equilibrium. Our discussion of competitive safety analysis for decentralized load balancing is further developed to deal with many communication links and arbitrary speeds. Finally, we discuss the extension of the above concepts to Bayesian games, and illustrate their use in a basic auctions setup.
Specific-to-General Learning for Temporal Events with Application to Learning Event Definitions from Video
Venue: arXiv cs.AI 2011
Year: 2011

We develop, analyze, and evaluate a novel, supervised, specific-to-general learner for a simple temporal logic and use the resulting algorithm to learn visual event definitions from video sequences. First, we introduce a simple, propositional, temporal, event-description language called AMA that is sufficiently expressive to represent many events yet sufficiently restrictive to support learning. We then give algorithms, along with lower and upper complexity bounds, for the subsumption and generalization problems for AMA formulas. We present a positive-examples--only specific-to-general learning method based on these algorithms. We also present a polynomial-time--computable ``syntactic'' subsumption test that implies semantic subsumption without being equivalent to it. A generalization algorithm based on syntactic subsumption can be used in place of semantic generalization to improve the asymptotic complexity of the resulting learning algorithm. Finally, we apply this algorithm to the task of learning relational event definitions from video and show that it yields definitions that are competitive with hand-coded ones.
Monte Carlo Methods for Tempo Tracking and Rhythm Quantization
Venue: arXiv cs.AI 2011
Year: 2011

We present a probabilistic generative model for timing deviations in expressive music performance. The structure of the proposed model is equivalent to a switching state space model. The switch variables correspond to discrete note locations as in a musical score. The continuous hidden variables denote the tempo. We formulate two well known music recognition problems, namely tempo tracking and automatic transcription (rhythm quantization) as filtering and maximum a posteriori (MAP) state estimation tasks. Exact computation of posterior features such as the MAP state is intractable in this model class, so we introduce Monte Carlo methods for integration and optimization. We compare Markov Chain Monte Carlo (MCMC) methods (such as Gibbs sampling, simulated annealing and iterative improvement) and sequential Monte Carlo methods (particle filters). Our simulation results suggest better results with sequential methods. The methods can be applied in both online and batch scenarios such as tempo tracking and transcription and are thus potentially useful in a number of music applications such as adaptive automatic accompaniment, score typesetting and music information retrieval.
Exploiting Contextual Independence In Probabilistic Inference
Venue: arXiv cs.AI 2011
Year: 2011

Bayesian belief networks have grown to prominence because they provide compact representations for many problems for which probabilistic inference is appropriate, and there are algorithms to exploit this compactness. The next step is to allow compact representations of the conditional probabilities of a variable given its parents. In this paper we present such a representation that exploits contextual independence in terms of parent contexts; which variables act as parents may depend on the value of other variables. The internal representation is in terms of contextual factors (confactors) that is simply a pair of a context and a table. The algorithm, contextual variable elimination, is based on the standard variable elimination algorithm that eliminates the non-query variables in turn, but when eliminating a variable, the tables that need to be multiplied can depend on the context. This algorithm reduces to standard variable elimination when there is no contextual independence structure to exploit. We show how this can be much more efficient than variable elimination when there is structure to exploit. We explain why this new method can exploit more structure than previous methods for structured belief network inference and an analogous algorithm that uses trees.
Compiling Causal Theories to Successor State Axioms and STRIPS-Like Systems
Venue: arXiv cs.AI 2011
Year: 2011

We describe a system for specifying the effects of actions. Unlike those commonly used in AI planning, our system uses an action description language that allows one to specify the effects of actions using domain rules, which are state constraints that can entail new action effects from old ones. Declaratively, an action domain in our language corresponds to a nonmonotonic causal theory in the situation calculus. Procedurally, such an action domain is compiled into a set of logical theories, one for each action in the domain, from which fully instantiated successor state-like axioms and STRIPS-like systems are then generated. We expect the system to be a useful tool for knowledge engineers writing action specifications for classical AI planning systems, GOLOG systems, and other systems where formal specifications of actions are needed.
SHOP2: An HTN Planning System
Venue: arXiv cs.AI 2011
Year: 2011

The SHOP2 planning system received one of the awards for distinguished performance in the 2002 International Planning Competition. This paper describes the features of SHOP2 which enabled it to excel in the competition, especially those aspects of SHOP2 that deal with temporal and metric planning domains.
Tales of 34 iPhone Users: How they change and why they are different
Venue: arXiv cs.HC 2011
Year: 2011

We present results from a longitudinal study of 34 iPh-one 3GS users, called LiveLab. LiveLab collected unprecedented usage data through an in-device, programmable logger and several structured interviews with the participants throughout the study. We have four objectives in writing this paper: (i) share the findings with the research community; (ii) provide insights guiding the design of smartphone systems and applications; (iii) demonstrate the power of prudently designed longitudinal field studies and the power of advanced research methods; and (iv) raise important questions that the research community can help answer in a collaborative, multidisciplinary manner. We show how the smartphone usage changes over the year and why the users are different (and similar) in their usage. In particular, our findings highlight application and web usage dynamics, the influence of socioeconomic status (SES) on usage, and the shortcomings of iPhone 3GS and its ecosystem. We further show that distinct classes of usage patterns exist, and these classes are best served by different phone designs, instead of the one-size-fits-all phone Apple provides. Our findings are significant not only for understanding smartphone users but also in guiding device and application development and optimizations. While we present novel results that can only be produced by a study of this nature, we also raise new research questions to be investigated by the mobile research community.
A General Framework for Structured Sparsity via Proximal Optimization
Venue: arXiv cs.LG 2011
Year: 2011

We study a generalized framework for structured sparsity. It extends the well-known methods of Lasso and Group Lasso by incorporating additional constraints on the variables as part of a convex optimization problem. This framework provides a straightforward way of favouring prescribed sparsity patterns, such as orderings, contiguous regions and overlapping groups, among others. Existing optimization methods are limited to specific constraint sets and tend to not scale well with sample size and dimensionality. We propose a novel first order proximal method, which builds upon results on fixed points and successive approximations. The algorithm can be applied to a general class of conic and norm constraints sets and relies on a proximity operator subproblem which can be computed explicitly. Experiments on different regression problems demonstrate the efficiency of the optimization algorithm and its scalability with the size of the problem. They also demonstrate state of the art statistical performance, which improves over Lasso and StructOMP.
Structure and Complexity in Planning with Unary Operators
Venue: arXiv cs.AI 2011
Year: 2011

Unary operator domains -- i.e., domains in which operators have a single effect -- arise naturally in many control problems. In its most general form, the problem of STRIPS planning in unary operator domains is known to be as hard as the general STRIPS planning problem -- both are PSPACE-complete. However, unary operator domains induce a natural structure, called the domain's causal graph. This graph relates between the preconditions and effect of each domain operator. Causal graphs were exploited by Williams and Nayak in order to analyze plan generation for one of the controllers in NASA's Deep-Space One spacecraft. There, they utilized the fact that when this graph is acyclic, a serialization ordering over any subgoal can be obtained quickly. In this paper we conduct a comprehensive study of the relationship between the structure of a domain's causal graph and the complexity of planning in this domain. On the positive side, we show that a non-trivial polynomial time plan generation algorithm exists for domains whose causal graph induces a polytree with a constant bound on its node indegree. On the negative side, we show that even plan existence is hard when the graph is a directed-path singly connected DAG. More generally, we show that the number of paths in the causal graph is closely related to the complexity of planning in the associated domain. Finally we relate our results to the question of complexity of planning with serializable subgoals.
Set systems: order types, continuous nondeterministic deformations, and quasi-orders
Venue: arXiv cs.LO 2011
Year: 2011

By reformulating a learning process of a set system L as a game between Teacher and Learner, we define the order type of L to be the order type of the game tree, if the tree is well-founded. The features of the order type of L (dim L in symbol) are (1) We can represent any well-quasi-order (wqo for short) by the set system L of the upper-closed sets of the wqo such that the maximal order type of the wqo is equal to dim L. (2) dim L is an upper bound of the mind-change complexity of L. dim L is defined iff L has a finite elasticity (fe for short), where, according to computational learning theory, if an indexed family of recursive languages has fe then it is learnable by an algorithm from positive data. Regarding set systems as subspaces of Cantor spaces, we prove that fe of set systems is preserved by any continuous function which is monotone with respect to the set-inclusion. By it, we prove that finite elasticity is preserved by various (nondeterministic) language operators (Kleene-closure, shuffle-closure, union, product, intersection,. . ..) The monotone continuous functions represent nondeterministic computations. If a monotone continuous function has a computation tree with each node followed by at most n immediate successors and the order type of a set system L is α, then the direct image of L is a set system of order type at most n-adic diagonal Ramsey number of α. Furthermore, we provide an order-type-preserving contravariant embedding from the category of quasi-orders and finitely branching simulations between them, into the complete category of subspaces of Cantor spaces and monotone continuous functions having Girard's linearity between them. Keyword: finite elasticity, shuffle-closure
Manipulation of Nanson's and Baldwin's Rules
Venue: arXiv cs.AI 2011
Year: 2011

Nanson's and Baldwin's voting rules select a winner by successively eliminating candidates with low Borda scores. We show that these rules have a number of desirable computational properties. In particular, with unweighted votes, it is NP-hard to manipulate either rule with one manipulator, whilst with weighted votes, it is NP-hard to manipulate either rule with a small number of candidates and a coalition of manipulators. As only a couple of other voting rules are known to be NP-hard to manipulate with a single manipulator, Nanson's and Baldwin's rules appear to be particularly resistant to manipulation from a theoretical perspective. We also propose a number of approximation methods for manipulating these two rules. Experiments demonstrate that both rules are often difficult to manipulate in practice. These results suggest that elimination style voting rules deserve further study.
Online Cake Cutting (published version)
Venue: arXiv cs.AI 2011
Year: 2011

We propose an online form of the cake cutting problem. This models situations where agents arrive and depart during the process of dividing a resource. We show that well known fair division procedures like cut-and-choose and the Dubins-Spanier moving knife procedure can be adapted to apply to such online problems. We propose some fairness properties that online cake cutting procedures can possess like online forms of proportionality and envy-freeness. We also consider the impact of collusion between agents. Finally, we study theoretically and empirically the competitive ratio of these online cake cutting procedures. Based on its resistance to collusion, and its good performance in practice, our results favour the online version of the cut-and-choose procedure over the online version of the moving knife procedure.
Uncovering Social Network Sybils in the Wild
Venue: arXiv cs.SI 2011
Year: 2011

Sybil accounts are fake identities created to unfairly increase the power or resources of a single malicious user. Researchers have long known about the existence of Sybil accounts in online communities such as file-sharing systems, but have not been able to perform large scale measurements to detect them or measure their activities. In this paper, we describe our efforts to detect, characterize and understand Sybil account activity in the Renren online social network (OSN). We use ground truth provided by Renren Inc. to build measurement based Sybil account detectors, and deploy them on Renren to detect over 100,000 Sybil accounts. We study these Sybil accounts, as well as an additional 560,000 Sybil accounts caught by Renren, and analyze their link creation behavior. Most interestingly, we find that contrary to prior conjecture, Sybil accounts in OSNs do not form tight-knit communities. Instead, they integrate into the social graph just like normal users. Using link creation timestamps, we verify that the large majority of links between Sybil accounts are created accidentally, unbeknownst to the attacker. Overall, only a very small portion of Sybil accounts are connected to other Sybils with social links. Our study shows that existing Sybil defenses are unlikely to succeed in today's OSNs, and we must design new techniques to effectively detect and defend against Sybil attacks.