OpenRaiser/Intern-Atlas huggingface dataset:
Conditional Model Checking
Venue: arXiv cs.SE 2011
Year: 2011

Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition P ---usually a state predicate--- such that the program satisfies the specification under the condition P ---that is, as long as the program does not leave states in which P is satisfied. We are of course interested in model checkers that return conditions P that are as weak as possible. Instead of outcome (1), the model checker will return P = true; instead of (2), the condition P will return the part of the state space that satisfies the specification; and in case (3), the condition P can summarize the work that has been performed by the model checker before space-out, time-out, or giving up. If complete verification is necessary, then a different verification method or tool may be used to focus on the states that violate the condition. We give such conditions as input to a conditional model checker, such that the verification problem is restricted to the part of the state space that satisfies the condition. Our experiments show that repeated application of conditional model checkers, using different conditions, can significantly improve the verification results, state-space coverage, and performance.
How the Landscape of Random Job Shop Scheduling Instances Depends on the Ratio of Jobs to Machines
Venue: arXiv cs.AI 2011
Year: 2011

We characterize the search landscape of random instances of the job shop scheduling problem (JSP). Specifically, we investigate how the expected values of (1) backbone size, (2) distance between near-optimal schedules, and (3) makespan of random schedules vary as a function of the job to machine ratio (N/M). For the limiting cases N/M approaches 0 and N/M approaches infinity we provide analytical results, while for intermediate values of N/M we perform experiments. We prove that as N/M approaches 0, backbone size approaches 100%, while as N/M approaches infinity the backbone vanishes. In the process we show that as N/M approaches 0 (resp. N/M approaches infinity), simple priority rules almost surely generate an optimal schedule, providing theoretical evidence of an "easy-hard-easy" pattern of typical-case instance difficulty in job shop scheduling. We also draw connections between our theoretical results and the "big valley" picture of JSP landscapes.
Solving Factored MDPs with Hybrid State and Action Variables
Venue: arXiv cs.AI 2011
Year: 2011

Efficient representations and solutions for large decision problems with continuous and discrete variables are among the most important challenges faced by the designers of automated decision support systems. In this paper, we describe a novel hybrid factored Markov decision process (MDP) model that allows for a compact representation of these problems, and a new hybrid approximate linear programming (HALP) framework that permits their efficient solutions. The central idea of HALP is to approximate the optimal value function by a linear combination of basis functions and optimize its weights by linear programming. We analyze both theoretical and computational aspects of this approach, and demonstrate its scale-up potential on several hybrid optimization problems.
Learning image transformations without training examples
Venue: arXiv cs.LG 2011
Year: 2011

The use of image transformations is essential for efficient modeling and learning of visual data. But the class of relevant transformations is large: affine transformations, projective transformations, elastic deformations, ... the list goes on. Therefore, learning these transformations, rather than hand coding them, is of great conceptual interest. To the best of our knowledge, all the related work so far has been concerned with either supervised or weakly supervised learning (from correlated sequences, video streams, or image-transform pairs). In this paper, on the contrary, we present a simple method for learning affine and elastic transformations when no examples of these transformations are explicitly given, and no prior knowledge of space (such as ordering of pixels) is included either. The system has only access to a moderately large database of natural images arranged in no particular order.
Hamming Compressed Sensing
Venue: arXiv cs.IT 2011
Year: 2011

Compressed sensing (CS) and 1-bit CS cannot directly recover quantized signals and require time consuming recovery. In this paper, we introduce \textit{Hamming compressed sensing} (HCS) that directly recovers a k-bit quantized signal of dimensional $n$ from its 1-bit measurements via invoking $n$ times of Kullback-Leibler divergence based nearest neighbor search. Compared with CS and 1-bit CS, HCS allows the signal to be dense, takes considerably less (linear) recovery time and requires substantially less measurements ($\mathcal O(\log n)$). Moreover, HCS recovery can accelerate the subsequent 1-bit CS dequantizer. We study a quantized recovery error bound of HCS for general signals and "HCS+dequantizer" recovery error bound for sparse signals. Extensive numerical simulations verify the appealing accuracy, robustness, efficiency and consistency of HCS.
NP is not AL and P is not NC is not NL is not L
Venue: arXiv cs.CC 2011
Year: 2011

This paper talk about that NP is not AL and P, P is not NC, NC is not NL, and NL is not L. The point about this paper is the depend relation of the problem that need other problem's result to compute it. I show the structure of depend relation that could divide each complexity classes.
A Behavioral Distance for Fuzzy-Transition Systems
Venue: arXiv cs.AI 2011
Year: 2011

In contrast to the existing approaches to bisimulation for fuzzy systems, we introduce a behavioral distance to measure the behavioral similarity of states in a nondeterministic fuzzy-transition system. This behavioral distance is defined as the greatest fixed point of a suitable monotonic function and provides a quantitative analogue of bisimilarity. The behavioral distance has the important property that two states are at zero distance if and only if they are bisimilar. Moreover, for any given threshold, we find that states with behavioral distances bounded by the threshold are equivalent. In addition, we show that two system combinators---parallel composition and product---are non-expansive with respect to our behavioral distance, which makes compositional verification possible.
A Taxonomy of Daemons in Self-stabilization
Venue: arXiv cs.DC 2011
Year: 2011

We survey existing scheduling hypotheses made in the literature in self-stabilization, commonly referred to under the notion of daemon. We show that four main characteristics (distribution, fairness, boundedness, and enabledness) are enough to encapsulate the various differences presented in existing work. Our naming scheme makes it easy to compare daemons of particular classes, and to extend existing possibility or impossibility results to new daemons. We further examine existing daemon transformer schemes and provide the exact transformed characteristics of those transformers in our taxonomy.
Distributed Evolutionary Graph Partitioning
Venue: arXiv cs.NE 2011
Year: 2011

We present a novel distributed evolutionary algorithm, KaFFPaE, to solve the Graph Partitioning Problem, which makes use of KaFFPa (Karlsruhe Fast Flow Partitioner). The use of our multilevel graph partitioner KaFFPa provides new effective crossover and mutation operators. By combining these with a scalable communication protocol we obtain a system that is able to improve the best known partitioning results for many inputs in a very short amount of time. For example, in Walshaw's well known benchmark tables we are able to improve or recompute 76% of entries for the tables with 1%, 3% and 5% imbalance.
Interference Alignment and Neutralization in a Cognitive 3-User MAC-Interference Channel: Degrees of Freedom
Venue: arXiv cs.IT 2011
Year: 2011

A network consisting of a point-to-point (P2P) link and a multiple access channel (MAC) sharing the same medium is considered. The resulting interference network, with three transmitters and two receivers is studied from degrees of freedom (DoF) perspective, with and without cognition. Several cognition variants are examined. Namely, the setup is studied with (1) no cognitive transmitters, (2) a cognitive P2P transmitter, (3) one cognitive MAC transmitter, and (4) with two cognitive MAC transmitters. It is shown that having a cognitive P2P transmitter does not bring any DoF gain to the network. This is obtained by showing that the DoF of the two former cases (1) and (2) is 1. However, it is shown that a cognitive MAC transmitter is more beneficial since the latter two cases (3) and (4) have 3/2 DoF. The achievability of 3/2 DoF is guaranteed by using a combination of interference neutralization and interference alignment.
The Complexity of Rooted Phylogeny Problems
Venue: arXiv cs.CC 2011
Year: 2011

Several computational problems in phylogenetic reconstruction can be formulated as restrictions of the following general problem: given a formula in conjunctive normal form where the literals are rooted triples, is there a rooted binary tree that satisfies the formula? If the formulas do not contain disjunctions, the problem becomes the famous rooted triple consistency problem, which can be solved in polynomial time by an algorithm of Aho, Sagiv, Szymanski, and Ullman. If the clauses in the formulas are restricted to disjunctions of negated triples, Ng, Steel, and Wormald showed that the problem remains NP-complete. We systematically study the computational complexity of the problem for all such restrictions of the clauses in the input formula. For certain restricted disjunctions of triples we present an algorithm that has sub-quadratic running time and is asymptotically as fast as the fastest known algorithm for the rooted triple consistency problem. We also show that any restriction of the general rooted phylogeny problem that does not fall into our tractable class is NP-complete, using known results about the complexity of Boolean constraint satisfaction problems. Finally, we present a pebble game argument that shows that the rooted triple consistency problem (and also all generalizations studied in this paper) cannot be solved by Datalog.
Hierarchical Composable Optimization of Web Pages
Venue: arXiv cs.IR 2011
Year: 2011

The process of creating modern Web media experiences is challenged by the need to adapt the content and presentation choices to dynamic real-time fluctuations of user interest across multiple audiences. We introduce FAME - a Framework for Agile Media Experiences - which addresses this scalability problem. FAME allows media creators to define abstract page models that are subsequently transformed into real experiences through algorithmic experimentation. FAME's page models are hierarchically composed of simple building blocks, mirroring the structure of most Web pages. They are resolved into concrete page instances by pluggable algorithms which optimize the pages for specific business goals. Our framework allows retrieving dynamic content from multiple sources, defining the experimentation's degrees of freedom, and constraining the algorithmic choices. It offers an effective separation of concerns in the media creation process, enabling multiple stakeholders with profoundly different skills to apply their crafts and perform their duties independently, composing and reusing each other's work in modular ways.
A Survey of Distributed Data Aggregation Algorithms
Venue: arXiv cs.DC 2011
Year: 2011

Distributed data aggregation is an important task, allowing the decentralized determination of meaningful global properties, that can then be used to direct the execution of other applications. The resulting values result from the distributed computation of functions like COUNT, SUM and AVERAGE. Some application examples can found to determine the network size, total storage capacity, average load, majorities and many others. In the last decade, many different approaches have been proposed, with different trade-offs in terms of accuracy, reliability, message and time complexity. Due to the considerable amount and variety of aggregation algorithms, it can be difficult and time consuming to determine which techniques will be more appropriate to use in specific settings, justifying the existence of a survey to aid in this task. This work reviews the state of the art on distributed data aggregation algorithms, providing three main contributions. First, it formally defines the concept of aggregation, characterizing the different types of aggregation functions. Second, it succinctly describes the main aggregation techniques, organizing them in a taxonomy. Finally, it provides some guidelines toward the selection and use of the most relevant techniques, summarizing their principal characteristics.
Non-Gaussian Scale Space Filtering with 2 by 2 Matrix of Linear Filters
Venue: arXiv cs.CV 2011
Year: 2011

Construction of a scale space with a convolution filter has been studied extensively in the past. It has been proven that the only convolution kernel that satisfies the scale space requirements is a Gaussian type. In this paper, we consider a matrix of convolution filters introduced in [1] as a building kernel for a scale space, and shows that we can construct a non-Gaussian scale space with a $2\times 2$ matrix of filters. The paper derives sufficient conditions for the matrix of filters for being a scale space kernel, and present some numerical demonstrations.
Dictionary Learning for Deblurring and Digital Zoom
Venue: arXiv cs.LG 2011
Year: 2011

This paper proposes a novel approach to image deblurring and digital zooming using sparse local models of image appearance. These models, where small image patches are represented as linear combinations of a few elements drawn from some large set (dictionary) of candidates, have proven well adapted to several image restoration tasks. A key to their success has been to learn dictionaries adapted to the reconstruction of small image patches. In contrast, recent works have proposed instead to learn dictionaries which are not only adapted to data reconstruction, but also tuned for a specific task. We introduce here such an approach to deblurring and digital zoom, using pairs of blurry/sharp (or low-/high-resolution) images for training, as well as an effective stochastic gradient algorithm for solving the corresponding optimization task. Although this learning problem is not convex, once the dictionaries have been learned, the sharp/high-resolution image can be recovered via convex optimization at test time. Experiments with synthetic and real data demonstrate the effectiveness of the proposed approach, leading to state-of-the-art performance for non-blind image deblurring and digital zoom.
Using Genetic Algorithm in the Evolutionary Design of Sequential Logic Circuits
Venue: arXiv cs.NE 2011
Year: 2011

Evolvable hardware (EHW) is a set of techniques that are based on the idea of combining reconfiguration hardware systems with evolutionary algorithms. In other word, EHW has two sections; the reconfigurable hardware and evolutionary algorithm where the configurations are under the control of an evolutionary algorithm. This paper, suggests a method to design and optimize the synchronous sequential circuits. Genetic algorithm (GA) was applied as evolutionary algorithm. In this approach, for building input combinational logic circuit of each DFF, and also output combinational logic circuit, the cell arrays have been used. The obtained results show that our method can reduce the average number of generations by limitation the search space.
Spider Solitaire is NP-Complete
Venue: arXiv cs.CC 2011
Year: 2011

This project investigates the potential of computers to solve complex tasks such as games. The paper proves that the complexity of a generalized version of spider solitaire is NP-Complete and uses much of structure of the proof that FreeCell is NP-Hard in the paper Helmert, M. "Complexity Results for Standard Benchmark Domains in Planning." Artificial Intelligence 143.2 (2003): 219-62. Print. A given decision problem falls in to the class NP-Complete if it is proven to be both in NP and in NP-Hard. To prove that this is the case the paper shows that, not only do the kinds of possible moves that can be reversed prove this, but it is also shown that no spider solitaire game of size n will take more than a polynomial number of moves to complete if such a completion is possible. The paper reduces 3-SAT to SpiderSolitaire (the name used throughout the proof when referring to the generalized version of popular solitaire variant "Spider Solitaire") by showing that any 3-SAT instance can be replicated using an appropriately arranged initial tableau. The example provided reinforces the proof of NP-Hardness and helps to make the proof easier to understand, but the definitive proof lies in the equations providing instruction on how to set up any 3-SAT instance of clause size C as a instance of SpiderSolitaire.
Active Learning with Multiple Views
Venue: arXiv cs.LG 2011
Year: 2011

Active learners alleviate the burden of labeling large amounts of data by detecting and asking the user to label only the most informative examples in the domain. We focus here on active learning for multi-view domains, in which there are several disjoint subsets of features (views), each of which is sufficient to learn the target concept. In this paper we make several contributions. First, we introduce Co-Testing, which is the first approach to multi-view active learning. Second, we extend the multi-view learning framework by also exploiting weak views, which are adequate only for learning a concept that is more general/specific than the target concept. Finally, we empirically show that Co-Testing outperforms existing active learners on a variety of real world domains such as wrapper induction, Web page classification, advertisement removal, and discourse tree parsing.
Fixed point theory and semidefinite programming for computable performance analysis of block-sparsity recovery
Venue: arXiv cs.IT 2011
Year: 2011

In this paper, we employ fixed point theory and semidefinite programming to compute the performance bounds on convex block-sparsity recovery algorithms. As a prerequisite for optimal sensing matrix design, a computable performance bound would open doors for wide applications in sensor arrays, radar, DNA microarrays, and many other areas where block-sparsity arises naturally. We define a family of goodness measures for arbitrary sensing matrices as the optimal values of certain optimization problems. The reconstruction errors of convex recovery algorithms are bounded in terms of these goodness measures. We demonstrate that as long as the number of measurements is relatively large, these goodness measures are bounded away from zero for a large class of random sensing matrices, a result parallel to the probabilistic analysis of the block restricted isometry property. As the primary contribution of this work, we associate the goodness measures with the fixed points of functions defined by a series of semidefinite programs. This relation with fixed point theory yields efficient algorithms with global convergence guarantees to compute the goodness measures.
Free Deterministic Equivalents, Rectangular Random Matrix Models, and Operator-Valued Free Probability Theory
Venue: arXiv cs.IT 2011
Year: 2011

Motivated by the asymptotic collective behavior of random and deterministic matrices, we propose an approximation (called "free deterministic equivalent") to quite general random matrix models, by replacing the matrices with operators satisfying certain freeness relations. We comment on the relation between our free deterministic equivalent and deterministic equivalents considered in the engineering literature. We do not only consider the case of square matrices, but also show how rectangular matrices can be treated. Furthermore, we emphasize how operator-valued free probability techniques can be used to solve our free deterministic equivalents. As an illustration of our methods we consider a random matrix model studied first by R. Couillet, J. Hoydis, and M. Debbah. We show how its free deterministic equivalent can be treated and we thus recover in a conceptual way their result. On a technical level, we generalize a result from scalar valued free probability, by showing that randomly rotated deterministic matrices of different sizes are asymptotically free from deterministic rectangular matrices, with amalgamation over a certain algebra of projections. In the Appendix, we show how estimates for differences between Cauchy transforms can be extended from a neighborhood of infinity to a region close to the real axis. This is of some relevance if one wants to compare the original random matrix problem with its free deterministic equivalent.
Performance improvement of the software development project using the Value Management approach
Venue: arXiv cs.SE 2011
Year: 2011

Improving performance and delivering value for customers have become a central theme in business. The software industry has become an increasingly important sector for the economy growth in Tunisia. This study aims to show how using Value Management in the Tunisian software industry for project analysis gives new insight about true project value and performance. This new approach is considered as an appropriate tool for guiding the process of making decisions. It offers tools in order to analyze the service value from the customer and organization perspectives. The results showed that the VM allows to have better performance in the software development project by linking customer satisfaction and cost analysis. The present case shows to service managers how they can benchmark project function to reduce their costs and improve resource allocation taking into consideration what customers consider important during their overall service experience. It can identify best professional practices, orient decisions to improve service value
On spanning tree congestion of Hamming graphs
Venue: arXiv cs.DM 2011
Year: 2011

We present a tight lower bound for the spanning tree congestion of Hamming graphs.
Sources of Inter-package Conflicts in Debian
Venue: arXiv cs.SE 2011
Year: 2011

Inter-package conflicts require the presence of two or more packages in a particular configuration, and thus tend to be harder to detect and localize than conventional (intra-package) defects. Hundreds of such inter-package conflicts go undetected by the normal testing and distribution process until they are later reported by a user. The reason for this is that current meta-data is not fine-grained and accurate enough to cover all common types of conflicts. A case study of inter-package conflicts in Debian has shown that with more detailed package meta-data, at least one third of all package conflicts could be prevented relatively easily, while another one third could be found by targeted testing of packages that share common resources or characteristics. This paper reports the case study and proposes ideas to detect inter-package conflicts in the future.