OpenRaiser/Intern-Atlas huggingface dataset:
Synthesis of Minimal Error Control Software
Venue: arXiv cs.SY 2012
Year: 2012

Software implementations of controllers for physical systems are at the core of many embedded systems. The design of controllers uses the theory of dynamical systems to construct a mathematical control law that ensures that the controlled system has certain properties, such as asymptotic convergence to an equilibrium point, while optimizing some performance criteria. However, owing to quantization errors arising from the use of fixed-point arithmetic, the implementation of this control law can only guarantee practical stability: under the actions of the implementation, the trajectories of the controlled system converge to a bounded set around the equilibrium point, and the size of the bounded set is proportional to the error in the implementation. The problem of verifying whether a controller implementation achieves practical stability for a given bounded set has been studied before. In this paper, we change the emphasis from verification to automatic synthesis. Using synthesis, the need for formal verification can be considerably reduced thereby reducing the design time as well as design cost of embedded control software. We give a methodology and a tool to synthesize embedded control software that is Pareto optimal w.r.t. both performance criteria and practical stability regions. Our technique is a combination of static analysis to estimate quantization errors for specific controller implementations and stochastic local search over the space of possible controllers using particle swarm optimization. The effectiveness of our technique is illustrated using examples of various standard control systems: in most examples, we achieve controllers with close LQR-LQG performance but with implementation errors, hence regions of practical stability, several times as small.
Adaptive Framework for Data Distribution in Wireless Sensor Networks
Venue: arXiv cs.NI 2012
Year: 2012

In recent years, the wireless sensor network (WSN) is playing a key role in sensing, collecting and disseminating information in various applications. An important feature associated with WSN is to develop an efficient data distribution and routing scheme to ensure better quality of service (QoS) that reduces the power consumption and the end-to-end data delivery time. In this work, we propose an adaptive framework to transmit data packets from a source to the sink in WSN across multiples paths with strategically distributed data packets so as to minimize the power consumption as well as the end-to-end data delivery time.
A Kuratowski-Type Theorem for Planarity of Partially Embedded Graphs
Venue: arXiv cs.DM 2012
Year: 2012

A partially embedded graph (or PEG) is a triple (G,H,\H), where G is a graph, H is a subgraph of G, and \H is a planar embedding of H. We say that a PEG (G,H,\H) is planar if the graph G has a planar embedding that extends the embedding \H. We introduce a containment relation of PEGs analogous to graph minor containment, and characterize the minimal non-planar PEGs with respect to this relation. We show that all the minimal non-planar PEGs except for finitely many belong to a single easily recognizable and explicitly described infinite family. We also describe a more complicated containment relation which only has a finite number of minimal non-planar PEGs. Furthermore, by extending an existing planarity test for PEGs, we obtain a polynomial-time algorithm which, for a given PEG, either produces a planar embedding or identifies an obstruction.
Improved Randomized Online Scheduling of Intervals and Jobs
Venue: arXiv cs.DS 2012
Year: 2012

We study the online preemptive scheduling of intervals and jobs (with restarts). Each interval or job has an arrival time, a deadline, a length and a weight. The objective is to maximize the total weight of completed intervals or jobs. While the deterministic case for intervals was settled a long time ago, the randomized case remains open. In this paper we first give a 2-competitive randomized algorithm for the case of equal length intervals. The algorithm is barely random in the sense that it randomly chooses between two deterministic algorithms at the beginning and then sticks with it thereafter. Then we extend the algorithm to cover several other cases of interval scheduling including monotone instances, C-benevolent instances and D-benevolent instances, giving the same competitive ratio. These algorithms are surprisingly simple but have the best competitive ratio against all previous (fully or barely) randomized algorithms. Next we extend the idea to give a 3-competitive algorithm for equal length jobs. Finally, we prove a lower bound of 2 on the competitive ratio of all barely random algorithms that choose between two deterministic algorithms for scheduling equal length intervals (and hence jobs).
Label-Guided Graph Exploration with Adjustable Ratio of Labels
Venue: arXiv cs.DS 2012
Year: 2012

The graph exploration problem is to visit all the nodes of a connected graph by a mobile entity, e.g., a robot. The robot has no a priori knowledge of the topology of the graph or of its size. Cohen et al. \cite{Ilcinkas08} introduced label guided graph exploration which allows the system designer to add short labels to the graph nodes in a preprocessing stage; these labels can guide the robot in the exploration of the graph. In this paper, we address the problem of adjustable 1-bit label guided graph exploration. We focus on the labeling schemes that not only enable a robot to explore the graph but also allow the system designer to adjust the ratio of the number of different labels. This flexibility is necessary when maintaining different labels may have different costs or when the ratio is pre-specified. We present 1-bit labeling (two colors, namely black and white) schemes for this problem along with a labeling algorithm for generating the required labels. Given an $n$-node graph and a rational number $ρ$, we can design a 1-bit labeling scheme such that $n/b\geq ρ$ where $b$ is the number of nodes labeled black. The robot uses $O(ρ\logΔ)$ bits of memory for exploring all graphs of maximum degree $Δ$. The exploration is completed in time $O(nΔ^{\frac{16ρ+7}{3}}/ρ+Δ^{\frac{40ρ+10}{3}})$. Moreover, our labeling scheme can work on graphs containing loops and multiple edges, while that of Cohen et al. focuses on simple graphs.
Parameterized Resolution with bounded conjunction
Venue: arXiv cs.LO 2012
Year: 2012

We provide separations between the parameterized versions of Res(1) (Resolution) and Res(2). Using a different set of parameterized contradictions, we also separate the parameterized versions of Res*(1) (tree-Resolution) and Res*(2).
STP/HAMPI and Computer Security
Venue: arXiv cs.CR 2012
Year: 2012

In the past several years I have written two SMT solvers called STP and HAMPI that have found widespread use in computer security research by leading groups in academia, industry and the government. In this brief note I summarize the features of STP/HAMPI that make them particularly suited for computer security research, and a listing of some of the more important projects that use them.
An Outer Bound for the Memoryless Two-user Interference Channel with General Cooperation
Venue: arXiv cs.IT 2012
Year: 2012

The interference channel models a wireless network where several source-destination pairs compete for the same resources. When nodes transmit simultaneously the destinations experience interference. This paper considers a 4-node network, where two nodes are sources and the other two are destinations. All nodes are full-duplex and cooperate to mitigate interference. A sum-rate outer bound is derived, which is shown to unify a number of previously derived outer bounds for special cases of cooperation. The approach is shown to extend to cooperative interference networks with more than two source-destination pairs and for any partial sum-rate. How the derived bound relates to similar bounds for channel models including cognitive nodes, i.e., nodes that have non-causal knowledge of the messages of some other node, is also discussed. Finally, the bound is evaluated for the Gaussian noise channel and used to compare different modes of cooperation.
Analyzing Nonblocking Switching Networks using Linear Programming (Duality)
Venue: arXiv cs.DM 2012
Year: 2012

The main task in analyzing a switching network design (including circuit-, multirate-, and photonic-switching) is to determine the minimum number of some switching components so that the design is non-blocking in some sense (e.g., strict- or wide-sense). We show that, in many cases, this task can be accomplished with a simple two-step strategy: (1) formulate a linear program whose optimum value is a bound for the minimum number we are seeking, and (2) specify a solution to the dual program, whose objective value by weak duality immediately yields a sufficient condition for the design to be non-blocking. We illustrate this technique through a variety of examples, ranging from circuit to multirate to photonic switching, from unicast to $f$-cast and multicast, and from strict- to wide-sense non-blocking. The switching architectures in the examples are of Clos-type and Banyan-type, which are the two most popular architectural choices for designing non-blocking switching networks. To prove the result in the multirate Clos network case, we formulate a new problem called {\sc dynamic weighted edge coloring} which generalizes the {\sc dynamic bin packing} problem. We then design an algorithm with competitive ratio 5.6355 for the problem. The algorithm is analyzed using the linear programming technique. A new upper-bound for multirate wide-sense non-blocking Clos networks follow, improving upon a decade-old bound on the same problem.
Towards Fuzzy-Hard Clustering Mapping Processes
Venue: arXiv cs.OH 2012
Year: 2012

Although the validation step can appear crucial in the case of clustering adopting fuzzy approaches, the problem of the partition validity obtained by those adopting the hard ones was not tackled. To cure this problem, we propose in this paper fuzzy-hard mapping processes of clustering while benefitting from those adopting the fuzzy case. These mapping processes concern: (1) local and global clustering evaluation measures: the first for the detection of the "worst" clusters to merging or splitting them. The second relates to the evaluation of the obtained partition for each iteration, (2) merging and splitting processes taking into account the proposed measures, and (3) automatic clustering algorithms implementing these new concepts.
Mixing Times of Self-Organizing Lists and Biased Permutations
Venue: arXiv cs.DM 2012
Year: 2012

Sampling permutations from S_n is a fundamental problem from probability theory. The nearest neighbor transposition chain \cal{M}}_{nn} is known to converge in time Θ(n^3 \log n) in the uniform case and time Θ(n^2) in the constant bias case, in which we put adjacent elements in order with probability p \neq 1/2 and out of order with probability 1-p. Here we consider the variable bias case where we put adjacent elements x<y in order with probability p{x,y} and out of order with probability 1-p_{x,y}. The problem of bounding the mixing rate of M_{nn} was posed by Fill and was motivated by the Move-Ahead-One self-organizing list update algorithm. It was conjectured that the chain would always be rapidly mixing if 1/2 \leq p_{x,y} \leq 1 for all x < y, but this was only known in the case of constant bias or when p_{x,y} is equal to 1/2 or 1, a case that corresponds to sampling linear extensions of a partial order. We prove the chain is rapidly mixing for two classes: "Choose Your Weapon," where we are given r_1,..., r_{n-1} with r_i \geq 1/2 and p_{x,y}=r_x for all x<y (so the dominant player chooses the game, thus fixing his or her probability of winning), and "League Hierarchies," where there are two leagues and players from the A-league have a fixed probability of beating players from the B-league, players within each league are similarly divided into sub-leagues with a possibly different fixed probability, and so forth recursively. Both of these classes include permutations with constant bias as a special case. Moreover, we also prove that the most general conjecture is false by constructing a counterexample where 1/2 \leq p_{x,y} \leq 1 for all x< y, but for which the nearest neighbor transposition chain requires exponential time to converge.
Computing without a computer: a new approach for solving nonlinear differential equations
Venue: arXiv cs.NA 2012
Year: 2012

The well-known Turing machine is an example of a theoretical digital computer, and it was the logical basis of constructing real electronic computers. In the present paper we propose an alternative, namely, by formalising arithmetic operations in the ordinary computing device, we attempt to go to the analytical procedure (for calculations). The method creates possibilities for solving nonlinear differential equations and systems. Our theoretical computer model requires retaining a finite number of terms to represent numbers, and utilizes digit carry procedure. The solution is represented in the form of a segment of a series in the powers of the step size of the independent variable in the finite-difference scheme. The algorithm generates a schematic representation that approximates the convergent finite-difference scheme, which, in turn, approximates the equation under consideration. The use of probabilistic methods allows us to average the recurrent calculations and exclude intermediate levels of computation. All the stages of formalizing operations of the classical computer result in "the method of the computer analogy". The proposed method leads to an explicit analytical representation of the solution. We present the general features of the algorithm which are illustrated by an example of solutions for a system of nonlinear equations.
Process algebra with conditionals in the presence of epsilon
Venue: arXiv cs.LO 2012
Year: 2012

In a previous paper, we presented several extensions of ACP with conditional expressions, including one with a retrospection operator on conditions to allow for looking back on conditions under which preceding actions have been performed. In this paper, we add a constant for a process that is only capable of terminating successfully to those extensions of ACP, which can be very useful in applications. It happens that in all cases the addition of this constant is unproblematic.
Approximation of Points on Low-Dimensional Manifolds Via Random Linear Projections
Venue: arXiv cs.IT 2012
Year: 2012

This paper considers the approximate reconstruction of points, x \in R^D, which are close to a given compact d-dimensional submanifold, M, of R^D using a small number of linear measurements of x. In particular, it is shown that a number of measurements of x which is independent of the extrinsic dimension D suffices for highly accurate reconstruction of a given x with high probability. Furthermore, it is also proven that all vectors, x, which are sufficiently close to M can be reconstructed with uniform approximation guarantees when the number of linear measurements of x depends logarithmically on D. Finally, the proofs of these facts are constructive: A practical algorithm for manifold-based signal recovery is presented in the process of proving the two main results mentioned above.
Patterns of Social Influence in a Network of Situated Cognitive Agents
Venue: arXiv cs.SI 2012
Year: 2012

This paper presents the results of computational experiments on the effects of social influence on individual and systemic behavior of situated cognitive agents in a product-consumer environment. Paired experiments were performed with identical initial conditions to compare social agents with non- social agents. Experiment results show that social agents are more productive in consuming available products, both in terms of aggregate unit consumption and aggregate utility. But this comes at a cost of individual average utility per unit consumed. In effect, social interaction achieved higher productivity by 'lowering the standards' of individual consumers. While still at an early stage of development, such an agent-based model laboratory is shown to be an effective research tool to investigate rich collective behavior in the context of demanding cognitive tasks.
Collaborative Development in Wikipedia
Venue: arXiv cs.SI 2012
Year: 2012

Using 16,068 articles in Wikipedia's Medicine Wikiproject, we study the relationship between collaboration and quality. We assess whether certain collaborative patterns are associated with information quality in terms of self-evaluated quality and article viewership. We find that the number of contributors has a curvilinear relationship to information quality, more contributors improving quality but only up to a certain point. Other articles that its collaborators work on also influences the quality of an information artifact, creating an interdependent network of artifacts and contributors. Finally, we see evidence of a recursive relationship between information quality and contributor activity, but that this recursive relationship attenuates over time.
There is No Deadline - Time Evolution of Wikipedia Discussions
Venue: arXiv cs.CY 2012
Year: 2012

Wikipedia articles are by definition never finished: at any moment their content can be edited, or discussed in the associated talk pages. In this study we analyse the evolution of these discussions to unveil patterns of collective participation along the temporal dimension, and to shed light on the process of content creation on different topics. At a micro-scale, we investigate peaks in the discussion activity and we observe a non-trivial relationship with edit activity. At a larger scale, we introduce a measure to account for how fast discussions grow in complexity, and we find speeds that span three orders of magnitude for different articles. Our analysis should help the community in tasks such as early detection of controversies and assessment of discussion maturity.
No big deal: introducing roles to reduce the size of ATL models
Venue: arXiv cs.LO 2012
Year: 2012

In the following paper we present a new semantics for the well-known strategic logic ATL. It is based on adding roles to concurrent game structures, that is at every state, each agent belongs to exactly one role, and the role specifies what actions are available to him at that state. We show advantages of the new semantics, analyze model checking complexity and prove equivalence between standard ATL semantics and our new approach.
Functional Magnetic Resonance Imaging and the Challenge of Balancing Human Security with State Security
Venue: arXiv cs.CR 2012
Year: 2012

Recent reports reveal that violent extremists are trying to obtain insider positions that may increase the impact of any attack on critical infrastructure and could potentially endanger state services, people's lives and even democracy. It is of utmost importance to be able to adopt extreme security measures in certain high-risk situations in order to secure critical infrastructure and thus lower the level of terrorist threats while preserving the rights of citizens. To counter these threats, our research is aiming for extreme measures to analyse and evaluate human threats related assessment methods for employee screening and evaluations using cognitive analysis technology, in particular functional Magnetic Resonance Imaging (fMRI). The development of fMRI has led some researchers to conclude that this technology has forensic potential and may be useful in investing personality traits, mental illness, psychopathology, racial prejudice and religious extremism. However, critics claim that this technology may present many new human rights and ethical dilemmas and could result in potentially disastrous outcomes. The main thrust of the research is to counter above concerns and harmful consequences by presenting a set of ethical and professional guidelines that will substantially reduce the risk of unethical use of this technology. The significance of this research is to ensure the limits of the state/organisation's right to peer into an individual's thought process with and without consent, to define the parameters of a person's right to ensure that fMRI scans do not pose more than an appropriate threat to cognitive liberty, and the proper use of such information in civil, forensic and security settings.
The JASMIN super-data-cluster
Venue: arXiv cs.DC 2012
Year: 2012

The JASMIN super-data-cluster is being deployed to support the data analysis requirements of the UK and European climate and earth system modelling community. Physical colocation of the core JASMIN resource with significant components of the facility for Climate and Environmental Monitoring from Space (CEMS) provides additional support for the earth observation community, as well as facilitating further comparison and evaluation of models with data. JASMIN and CEMS together centrally deploy 9.3 PB of storage - 4.6 PB of Panasas fast disk storage alongside the STFC Atlas Tape Store. Over 370 computing cores provide local computation. Remote JASMIN resources at Bristol, Leeds and Reading provide additional distributed storage and compute configured to support local workflow as a stepping stone to using the central JASMIN system. Fast network links from JASMIN provide reliable communication between the UK supercomputers MONSooN (at the Met Office) and HECToR (at the University of Edinburgh). JASMIN also supports European users via a light path to KNMI in the Netherlands. The functional components of the JASMIN infrastructure have been designed to support and integrate workflows for three main goals: (1) the efficient operation of data curation and facilitation at the STFC Centre for Environmental Data Archival; (2) efficient data analysis by the UK and European climate and earth system science communities, and; (3) flexible access for the climate impacts and earth observation communities to complex data and concomitant services.
The Wavelet Trie: Maintaining an Indexed Sequence of Strings in Compressed Space
Venue: arXiv cs.DS 2012
Year: 2012

An indexed sequence of strings is a data structure for storing a string sequence that supports random access, searching, range counting and analytics operations, both for exact matches and prefix search. String sequences lie at the core of column-oriented databases, log processing, and other storage and query tasks. In these applications each string can appear several times and the order of the strings in the sequence is relevant. The prefix structure of the strings is relevant as well: common prefixes are sought in strings to extract interesting features from the sequence. Moreover, space-efficiency is highly desirable as it translates directly into higher performance, since more data can fit in fast memory. We introduce and study the problem of compressed indexed sequence of strings, representing indexed sequences of strings in nearly-optimal compressed space, both in the static and dynamic settings, while preserving provably good performance for the supported operations. We present a new data structure for this problem, the Wavelet Trie, which combines the classical Patricia Trie with the Wavelet Tree, a succinct data structure for storing a compressed sequence. The resulting Wavelet Trie smoothly adapts to a sequence of strings that changes over time. It improves on the state-of-the-art compressed data structures by supporting a dynamic alphabet (i.e. the set of distinct strings) and prefix queries, both crucial requirements in the aforementioned applications, and on traditional indexes by reducing space occupancy to close to the entropy of the sequence.