OpenRaiser/Intern-Atlas huggingface dataset:
A Quartic Kernel for Pathwidth-One Vertex Deletion
Venue: arXiv cs.DS 2010
Year: 2010

The pathwidth of a graph is a measure of how path-like the graph is. Given a graph G and an integer k, the problem of finding whether there exist at most k vertices in G whose deletion results in a graph of pathwidth at most one is NP- complete. We initiate the study of the parameterized complexity of this problem, parameterized by k. We show that the problem has a quartic vertex-kernel: We show that, given an input instance (G = (V, E), k); |V| = n, we can construct, in polynomial time, an instance (G', k') such that (i) (G, k) is a YES instance if and only if (G', k') is a YES instance, (ii) G' has O(k^{4}) vertices, and (iii) k' \leq k. We also give a fixed parameter tractable (FPT) algorithm for the problem that runs in O(7^{k} k \cdot n^{2}) time.
Going Green: A Holistic Approach to Transform Business
Venue: arXiv cs.CY 2010
Year: 2010

In recent years environmental and energy conservation issues have taken the central theme in the global business arena. The reality of rising energy cost and their impact on international affairs coupled with the different kinds of environmental issues has shifted the social and economic consciousness of the business community. Hence, the business community is now in search of an eco-friendly business model. This paper highlights the concept of green business and their needs in the current global scenario.
Memristor Crossbar-based Hardware Implementation of Fuzzy Membership Functions
Venue: arXiv cs.NE 2010
Year: 2010

In May 1, 2008, researchers at Hewlett Packard (HP) announced the first physical realization of a fundamental circuit element called memristor that attracted so much interest worldwide. This newly found element can easily be combined with crossbar interconnect technology which this new structure has opened a new field in designing configurable or programmable electronic systems. These systems in return can have applications in signal processing and artificial intelligence. In this paper, based on the simple memristor crossbar structure, we propose new and simple circuits for hardware implementation of fuzzy membership functions. In our proposed circuits, these fuzzy membership functions can have any shapes and resolutions. In addition, these circuits can be used as a basis in the construction of evolutionary systems.
Distance Measures for Reduced Ordering Based Vector Filters
Venue: arXiv cs.CV 2010
Year: 2010

Reduced ordering based vector filters have proved successful in removing long-tailed noise from color images while preserving edges and fine image details. These filters commonly utilize variants of the Minkowski distance to order the color vectors with the aim of distinguishing between noisy and noise-free vectors. In this paper, we review various alternative distance measures and evaluate their performance on a large and diverse set of images using several effectiveness and efficiency criteria. The results demonstrate that there are in fact strong alternatives to the popular Minkowski metrics.
The General Vector Addition System Reachability Problem by Presburger Inductive Invariants
Venue: arXiv cs.LO 2010
Year: 2010

The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known to be decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition. This decomposition is used in this paper to prove that the Parikh images of languages recognized by VASs are semi-pseudo-linear; a class that extends the semi-linear sets, a.k.a. the sets definable in Presburger arithmetic. We provide an application of this result; we prove that a final configuration is not reachable from an initial one if and only if there exists a semi-linear inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Presburger formula denotes an inductive invariant, we deduce that there exist checkable certificates of non-reachability. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas.
Parameterized Complexity Results in Symmetry Breaking
Venue: arXiv cs.AI 2010
Year: 2010

Symmetry is a common feature of many combinatorial problems. Unfortunately eliminating all symmetry from a problem is often computationally intractable. This paper argues that recent parameterized complexity results provide insight into that intractability and help identify special cases in which symmetry can be dealt with more tractably
Stack-Summarizing Control-Flow Analysis of Higher-Order Programs
Venue: arXiv cs.PL 2010
Year: 2010

Two sinks drain precision from higher-order flow analyses: (1) merging of argument values upon procedure call and (2) merging of return values upon procedure return. To combat the loss of precision, these two sinks have been addressed independently. In the case of procedure calls, abstract garbage collection reduces argument merging; while in the case of procedure returns, context-free approaches eliminate return value merging. It is natural to expect a combined analysis could enjoy the mutually beneficial interaction between the two approaches. The central contribution of this work is a direct product of abstract garbage collection with context-free analysis. The central challenge to overcome is the conflict between the core constraint of a pushdown system and the needs of garbage collection: a pushdown system can only see the top of the stack, yet garbage collection needs to see the entire stack during a collection. To make the direct product computable, we develop "stack summaries," a method for tracking stack properties at each control state in a pushdown analysis of higher-order programs.
Spatially regularized compressed sensing of diffusion MRI data
Venue: arXiv cs.IT 2010
Year: 2010

The present paper introduces a method for substantial reduction of the number of diffusion encoding gradients required for reliable reconstruction of HARDI signals. The method exploits the theory of compressed sensing (CS), which establishes conditions on which a signal of interest can be recovered from its under-sampled measurements, provided that the signal admits a sparse representation in the domain of a linear transform. In the case at hand, the latter is defined to be spherical ridgelet transformation, which excels in sparsifying HARDI signals. What makes the resulting reconstruction procedure even more accurate is a combination of the sparsity constraints in the diffusion domain with additional constraints imposed on the estimated diffusion field in the spatial domain. Accordingly, the present paper describes a novel way to combine the diffusion- and spatial-domain constraints to achieve a maximal reduction in the number of diffusion measurements, while sacrificing little in terms of reconstruction accuracy. Finally, details are provided on a particularly efficient numerical scheme which can be used to solve the aforementioned reconstruction problem by means of standard and readily available estimation tools. The paper is concluded with experimental results which support the practical value of the proposed reconstruction methodology.
A Transformation-based Implementation for CLP with Qualification and Proximity
Venue: arXiv cs.LO 2010
Year: 2010

Uncertainty in logic programming has been widely investigated in the last decades, leading to multiple extensions of the classical LP paradigm. However, few of these are designed as extensions of the well-established and powerful CLP scheme for Constraint Logic Programming. In a previous work we have proposed the SQCLP (proximity-based qualified constraint logic programming) scheme as a quite expressive extension of CLP with support for qualification values and proximity relations as generalizations of uncertainty values and similarity relations, respectively. In this paper we provide a transformation technique for transforming SQCLP programs and goals into semantically equivalent CLP programs and goals, and a practical Prolog-based implementation of some particularly useful instances of the SQCLP scheme. We also illustrate, by showing some simple-and working-examples, how the prototype can be effectively used as a tool for solving problems where qualification values and proximity relations play a key role. Intended use of SQCLP includes flexible information retrieval applications.
Ontology Temporal Evolution for Multi-Entity Bayesian Networks under Exogenous and Endogenous Semantic Updating
Venue: arXiv cs.AI 2010
Year: 2010

It is a challenge for any Knowledge Base reasoning to manage ubiquitous uncertain ontology as well as uncertain updating times, while achieving acceptable service levels at minimum computational cost. This paper proposes an application-independent merging ontologies for any open interaction system. A solution that uses Multi-Entity Bayesan Networks with SWRL rules, and a Java program is presented to dynamically monitor Exogenous and Endogenous temporal evolution on updating merging ontologies on a probabilistic framework for the Semantic Web.
Clustering, Encoding and Diameter Computation Algorithms for Multidimensional Data
Venue: arXiv cs.DS 2010
Year: 2010

In this paper we present novel algorithms for several multidimensional data processing problems. We consider problems related to the computation of restricted clusters and of the diameter of a set of points using a new distance function. We also consider two string (1D data) processing problems, regarding an optimal encoding method and the computation of the number of occurrences of a substring within a string generated by a grammar. The algorithms have been thoroughly analyzed from a theoretical point of view and some of them have also been evaluated experimentally.
Gamed-based iSTART Practice: From MiBoard to Self-Explanation Showdown
Venue: arXiv cs.GT 2010
Year: 2010

MiBoard (Multiplayer Interactive Board Game) is an online, turnbased board game that was developed to assess the integration of game characteristics (point rewards, game-like interaction, and peer feedback) and how that might affect student engagement and learning efficacy. This online board game was designed to fit within the Extended Practice module of iSTART (Interactive Strategy Training for Active Reading and Thinking). Unfortunately, preliminary research shows that MiBoard actually reduces engagement and does not benefit the quality of student self-explanations when compared to the original Extended Practice module. Consequently the MiBoard framework has been revamped to create Self-Explanation Showdown, a faster-paced, less analytically oriented game that adds competition to the creation of self-explanations. Students are evaluated on the quality of their self-explanations using the same assessment algorithms from iSTART Extended Practice module (this includes both word-based and LSA-based assessments). The technical issues involved in development of MiBoard and Self- Explanation Showdown are described. The lessons learned from the MiBoard experience are also discussed in this paper.
Performance Bounds and Design Criteria for Estimating Finite Rate of Innovation Signals
Venue: arXiv cs.IT 2010
Year: 2010

In this paper, we consider the problem of estimating finite rate of innovation (FRI) signals from noisy measurements, and specifically analyze the interaction between FRI techniques and the underlying sampling methods. We first obtain a fundamental limit on the estimation accuracy attainable regardless of the sampling method. Next, we provide a bound on the performance achievable using any specific sampling approach. Essential differences between the noisy and noise-free cases arise from this analysis. In particular, we identify settings in which noise-free recovery techniques deteriorate substantially under slight noise levels, thus quantifying the numerical instability inherent in such methods. This instability, which is only present in some families of FRI signals, is shown to be related to a specific type of structure, which can be characterized by viewing the signal model as a union of subspaces. Finally, we develop a methodology for choosing the optimal sampling kernels based on a generalization of the Karhunen--Loève transform. The results are illustrated for several types of time-delay estimation problems.
Theory of processes
Venue: arXiv cs.LO 2010
Year: 2010

The book gives a detailed exposition of basic concepts and results of a theory of processes. The presentation of theoretical concepts and results is accompanied with illustrations of their application to solving various problems of verification of processes. Along with well-known results there are presented author's results related to verification of processes with message passing, and there are given examples of an application of these results.
Active Integrity Constraints and Revision Programming
Venue: arXiv cs.DB 2010
Year: 2010

We study active integrity constraints and revision programming, two formalisms designed to describe integrity constraints on databases and to specify policies on preferred ways to enforce them. Unlike other more commonly accepted approaches, these two formalisms attempt to provide a declarative solution to the problem. However, the original semantics of founded repairs for active integrity constraints and justified revisions for revision programs differ. Our main goal is to establish a comprehensive framework of semantics for active integrity constraints, to find a parallel framework for revision programs, and to relate the two. By doing so, we demonstrate that the two formalisms proposed independently of each other and based on different intuitions when viewed within a broader semantic framework turn out to be notational variants of each other. That lends support to the adequacy of the semantics we develop for each of the formalisms as the foundation for a declarative approach to the problem of database update and repair. In the paper we also study computational properties of the semantics we consider and establish results concerned with the concept of the minimality of change and the invariance under the shifting transformation.
Small Vertex Cover makes Petri Net Coverability and Boundedness Easier
Venue: arXiv cs.DS 2010
Year: 2010

The coverability and boundedness problems for Petri nets are known to be Expspace-complete. Given a Petri net, we associate a graph with it. With the vertex cover number k of this graph and the maximum arc weight W as parameters, we show that coverability and boundedness are in ParaPspace. This means that these problems can be solved in space O(ef(k,W)poly(n)), where ef(k,W) is some exponential function and poly(n) is some polynomial in the size of the input. We then extend the ParaPspace result to model checking a logic that can express some generalizations of coverability and boundedness.
Generating Bijections between HOAS and the Natural Numbers
Venue: arXiv cs.LO 2010
Year: 2010

A provably correct bijection between higher-order abstract syntax (HOAS) and the natural numbers enables one to define a "not equals" relationship between terms and also to have an adequate encoding of sets of terms, and maps from one term family to another. Sets and maps are useful in many situations and are preferably provided in a library of some sort. I have released a map and set library for use with Twelf which can be used with any type for which a bijection to the natural numbers exists. Since creating such bijections is tedious and error-prone, I have created a "bijection generator" that generates such bijections automatically together with proofs of correctness, all in the context of Twelf.
Representing Isabelle in LF
Venue: arXiv cs.LO 2010
Year: 2010

LF has been designed and successfully used as a meta-logical framework to represent and reason about object logics. Here we design a representation of the Isabelle logical framework in LF using the recently introduced module system for LF. The major novelty of our approach is that we can naturally represent the advanced Isabelle features of type classes and locales. Our representation of type classes relies on a feature so far lacking in the LF module system: morphism variables and abstraction over them. While conservative over the present system in terms of expressivity, this feature is needed for a representation of type classes that preserves the modular structure. Therefore, we also design the necessary extension of the LF module system.
What we understand is what we get: Assessment in Spreadsheets
Venue: arXiv cs.SE 2010
Year: 2010

In previous work we have studied how an explicit representation of background knowledge associated with a specific spreadsheet can be exploited to alleviate usability problems with spreadsheet-based applications. We have implemented this approach in the SACHS system to provide a semantic help system for spreadsheets applications. In this paper, we evaluate the (comprehension) coverage of SACHS on an Excel-based financial controlling system via a "Wizard-of-Oz" experiment. This shows that SACHS adds significant value, but systematically misses important classes of explanations. For judgements about the information contained in spreadsheets, we provide a first approach for an "assessment module" in SACHS.
Proposed System for data hiding using Cryptography and Steganography Proposed System for data hiding using Cryptography and Steganography
Venue: arXiv cs.CR 2010
Year: 2010

Steganography and Cryptography are two popular ways of sending vital information in a secret way. One hides the existence of the message and the other distorts the message itself. There are many cryptography techniques available; among them AES is one of the most powerful techniques. In Steganography we have various techniques in different domains like spatial domain, frequency domain etc. to hide the message. It is very difficult to detect hidden message in frequency domain and for this domain we use various transformations like DCT, FFT and Wavelets etc. In this project we are developing a system where we develop a new technique in which Cryptography and Steganography are used as integrated part along with newly developed enhanced security module. In Cryptography we are using AES algorithm to encrypt a message and a part of the message is hidden in DCT of an image; remaining part of the message is used to generate two secret keys which make this system highly secured. Keyword: Cryptography, Steganography, Stego- image, Threshold Value, DCT Coefficient
On the performance evaluation of wireless networks with broadcast and interference-limited channels
Venue: arXiv cs.NI 2010
Year: 2010

In this report we propose a MultiObjective (MO) performance evaluation framework for wireless ad hoc networks where criteria such as capacity, robustness, energy and delay are optimized concurrently. Within such a framework, we can determine both the Pareto-optimal performance bounds and the networking parameters that provide these bounds. The originality of this approach is that it accounts for the inherent broadcast properties of the transmission and finely models the interference distribution. In the proposed model, the network performance can be optimized when several flows (source- destination transmissions) exist. One benefit of our approach is that the complexity does not grow with the number of flows. The other major contribution of this paper is the new analytical formulation of the performance metrics. It relies on a matrix representation of the constraints imposed by the interference- limited and broadcast wireless channel. Because of the similarity of this matrix with a Markovian transition matrix, we can exploit classical results from Markov chains theory to derive steady state performance metrics relative to capacity, robustness, energy and delay. Another very interesting feature of these new metrics is that the Pareto-optimal solutions related to them provide a tight bound on capacity, robustness, energy and delay.
On Second-Order Monadic Monoidal and Groupoidal Quantifiers
Venue: arXiv cs.LO 2010
Year: 2010

We study logics defined in terms of second-order monadic monoidal and groupoidal quantifiers. These are generalized quantifiers defined by monoid and groupoid word-problems, equivalently, by regular and context-free languages. We give a computational classification of the expressive power of these logics over strings with varying built-in predicates. In particular, we show that ATIME(n) can be logically characterized in terms of second-order monadic monoidal quantifiers.
Informal Control code logic
Venue: arXiv cs.SE 2010
Year: 2010

General definitions as well as rules of reasoning regarding control code production, distribution, deployment, and usage are described. The role of testing, trust, confidence and risk analysis is considered. A rationale for control code testing is sought and found for the case of safety critical embedded control code.
Performance Analysis of an Improved Graded Precision Localization Algorithm for Wireless Sensor Networks
Venue: arXiv cs.NI 2010
Year: 2010

In this paper an improved version of the graded precision localization algorithm GRADELOC, called IGRADELOC is proposed. The performance of GRADELOC is dependent on the regions formed by the overlapping radio ranges of the nodes of the underlying sensor network. A different region pattern could significantly alter the nature and precision of localization. In IGRADELOC, two improvements are suggested. Firstly, modifications are proposed in the radio range of the fixed-grid nodes, keeping in mind the actual radio range of commonly available nodes, to allow for routing through them. Routing is not addressed by GRADELOC, but is of prime importance to the deployment of any adhoc network, especially sensor networks. A theoretical model expressing the radio range in terms of the cell dimensions of the grid infrastructure is proposed, to help in carrying out a deployment plan which achieves the desirable precision of coarse-grained localization. Secondly, in GRADELOC it is observed that fine-grained localization does not achieve significant performance benefits over coarse-grained localization. In IGRADELOC, this factor is addressed with the introduction of a parameter that could be used to improve and fine-tune the precision of fine-grained localization.
Sensor Scheduling for Energy-Efficient Target Tracking in Sensor Networks
Venue: arXiv cs.MA 2010
Year: 2010

In this paper we study the problem of tracking an object moving randomly through a network of wireless sensors. Our objective is to devise strategies for scheduling the sensors to optimize the tradeoff between tracking performance and energy consumption. We cast the scheduling problem as a Partially Observable Markov Decision Process (POMDP), where the control actions correspond to the set of sensors to activate at each time step. Using a bottom-up approach, we consider different sensing, motion and cost models with increasing levels of difficulty. At the first level, the sensing regions of the different sensors do not overlap and the target is only observed within the sensing range of an active sensor. Then, we consider sensors with overlapping sensing range such that the tracking error, and hence the actions of the different sensors, are tightly coupled. Finally, we consider scenarios wherein the target locations and sensors' observations assume values on continuous spaces. Exact solutions are generally intractable even for the simplest models due to the dimensionality of the information and action spaces. Hence, we devise approximate solution techniques, and in some cases derive lower bounds on the optimal tradeoff curves. The generated scheduling policies, albeit suboptimal, often provide close-to-optimal energy-tracking tradeoffs.