OpenRaiser/Intern-Atlas huggingface dataset:
On the meaning of logical completeness
Venue: arXiv cs.LO 2010
Year: 2010

Goedel's completeness theorem is concerned with provability, while Girard's theorem in ludics (as well as full completeness theorems in game semantics) are concerned with proofs. Our purpose is to look for a connection between these two disciplines. Following a previous work [3], we consider an extension of the original ludics with contraction and universal nondeterminism, which play dual roles, in order to capture a polarized fragment of linear logic and thus a constructive variant of classical propositional logic. We then prove a completeness theorem for proofs in this extended setting: for any behaviour (formula) A and any design (proof attempt) P, either P is a proof of A or there is a model M of the orthogonal of A which defeats P. Compared with proofs of full completeness in game semantics, ours exhibits a striking similarity with proofs of Goedel's completeness, in that it explicitly constructs a countermodel essentially using Koenig's lemma, proceeds by induction on formulas, and implies an analogue of Loewenheim-Skolem theorem.
Use of Data Mining in Scheduler Optimization
Venue: arXiv cs.OS 2010
Year: 2010

The operating system's role in a computer system is to manage the various resources. One of these resources is the Central Processing Unit. It is managed by a component of the operating system called the CPU scheduler. Schedulers are optimized for typical workloads expected to run on the platform. However, a single scheduler may not be appropriate for all workloads. That is, a scheduler may schedule a workload such that the completion time is minimized, but when another type of workload is run on the platform, scheduling and therefore completion time will not be optimal; a different scheduling algorithm, or a different set of parameters, may work better. Several approaches to solving this problem have been proposed. The objective of this survey is to summarize the approaches based on data mining, which are available in the literature. In addition to solutions that can be directly utilized for solving this problem, we are interested in data mining research in related areas that have potential for use in operating system scheduling. We also explain general technical issues involved in scheduling in modern computers, including parallel scheduling issues related to multi-core CPUs. We propose a taxonomy that classifies the scheduling approaches we discuss into different categories.
Regulating Response Time in an Autonomic Computing System: A Comparision of Proportional Control and Fuzzy Control Approaches
Venue: arXiv cs.SY 2010
Year: 2010

Ecommerce is an area where an Autonomic Computing system could be very effectively deployed. Ecommerce has created demand for high quality information technology services and businesses are seeking quality of service guarantees from their service providers. These guarantees are expressed as part of service level agreements. Properly adjusting tuning parameters for enforcement of the service level agreement is time-consuming and skills-intensive. Moreover, in case of changes to the workload, the setting of the parameters may no longer be optimum. In an ecommerce system, where the workload changes frequently, there is a need to update the parameters at regular intervals. This paper describes two approaches, one, using a proportional controller and two, using a fuzzy controller, to automate the tuning of MaxClients parameter of Apache web server based on the required response time and the current workload. This is an illustration of the self-optimizing characteristic of an autonomic computing system.
Excerpt from the book World of Movable Objects
Venue: arXiv cs.HC 2010
Year: 2010

This book is about the transformation of screen objects into movable and resizable and about the design of applications entirely on the basis of such elements. The screen objects have a wide variety of shapes; they can be either graphical objects or controls; there are solitary objects and very complex objects parts of which are involved in individual, synchronous, and related movements. Objects can be involved in forward movements and rotation; they can be resized and reconfigured; all these movements and situations are considered. On the basis of total movability, the new type of programs - user-driven applications - are designed. These applications continue to work according to their main purposes, but the whole control of WHAT, WHEN, and HOW must appear on the screen is passed from designers to users.
Matching with Couples Revisited
Venue: arXiv cs.GT 2010
Year: 2010

It is well known that a stable matching in a many-to-one matching market with couples need not exist. We introduce a new matching algorithm for such markets and show that for a general class of large random markets the algorithm will find a stable matching with high probability. In particular we allow the number of couples to grow at a near-linear rate. Furthermore, truth-telling is an approximated equilibrium in the game induced by the new matching algorithm. Our results are tight: for markets in which the number of couples grows at a linear rate, we show that with constant probability no stable matching exists.
On the Dynamics of IP Address Allocation and Availability of End-Hosts
Venue: arXiv cs.NI 2010
Year: 2010

The availability of end-hosts and their assigned routable IP addresses has impact on the ability to fight spammers and attackers, and on peer-to-peer application performance. Previous works study the availability of hosts mostly by using either active pinging or by studying access to a mail service, both approaches suffer from inherent inaccuracies. We take a different approach by measuring the IP addresses periodically reported by a uniquely identified group of the hosts running the DIMES agent. This fresh approach provides a chance to measure the true availability of end-hosts and the dynamics of their assigned routable IP addresses. Using a two month study of 1804 hosts, we find that over 60% of the hosts have a fixed IP address and 90% median availability, while some of the remaining hosts have more than 30 different IPs. For those that have periodically changing IP addresses, we find that the median average period per AS is roughly 24 hours, with a strong relation between the offline time and the probability of altering IP address.
Usability Meets Instant Gratification on the Semantic Web
Venue: arXiv cs.OH 2010
Year: 2010

This paper presents a semantic wiki prototype application named SHAWN [later WikSAR] that allows structuring concepts within a wiki environment. To entice the use of Semantic Web technologies applications need to offer both high usability and instant gratification. Concept creation is exceptionally easy in SHAWN since metadata as well as plain text is entered within a single edit box on each wiki page in a self-explaining fashion. The entered data is immediately used for rendering sophisticated navigational means on the wiki. By editing simple wiki pages ontologies emerge.
Optimal Auctions with Correlated Bidders are Easy
Venue: arXiv cs.GT 2010
Year: 2010

We consider the problem of designing a revenue-maximizing auction for a single item, when the values of the bidders are drawn from a correlated distribution. We observe that there exists an algorithm that finds the optimal randomized mechanism that runs in time polynomial in the size of the support. We leverage this result to show that in the oracle model introduced by Ronen and Saberi [FOCS'02], there exists a polynomial time truthful in expectation mechanism that provides a $(\frac 3 2+ε)$-approximation to the revenue achievable by an optimal truthful-in-expectation mechanism, and a polynomial time deterministic truthful mechanism that guarantees $\frac 5 3$ approximation to the revenue achievable by an optimal deterministic truthful mechanism. We show that the $\frac 5 3$-approximation mechanism provides the same approximation ratio also with respect to the optimal truthful-in-expectation mechanism. This shows that the performance gap between truthful-in-expectation and deterministic mechanisms is relatively small. En route, we solve an open question of Mehta and Vazirani [EC'04]. Finally, we extend some of our results to the multi-item case, and show how to compute the optimal truthful-in-expectation mechanisms for bidders with more complex valuations.
Spin-the-bottle Sort and Annealing Sort: Oblivious Sorting via Round-robin Random Comparisons
Venue: arXiv cs.DS 2010
Year: 2010

We study sorting algorithms based on randomized round-robin comparisons. Specifically, we study Spin-the-bottle sort, where comparisons are unrestricted, and Annealing sort, where comparisons are restricted to a distance bounded by a \emph{temperature} parameter. Both algorithms are simple, randomized, data-oblivious sorting algorithms, which are useful in privacy-preserving computations, but, as we show, Annealing sort is much more efficient. We show that there is an input permutation that causes Spin-the-bottle sort to require $Ω(n^2\log n)$ expected time in order to succeed, and that in $O(n^2\log n)$ time this algorithm succeeds with high probability for any input. We also show there is an implementation of Annealing sort that runs in $O(n\log n)$ time and succeeds with very high probability.
Existence of Stable Exclusive Bilateral Exchanges in Networks
Venue: arXiv cs.GT 2010
Year: 2010

In this paper we show that when individuals in a bipartite network exclusively choose partners and exchange valued goods with their partners, then there exists a set of exchanges that are pair-wise stable. Pair-wise stability implies that no individual breaks her partnership and no two neighbors in the network can form a new partnership while breaking other partnerships if any so that at least one of them improves her payoff and the other one does at least as good. We consider a general class of continuous, strictly convex and strongly monotone preferences over bundles of goods for individuals. Thus, this work extends the general equilibrium framework from markets to networks with exclusive exchanges. We present the complete existence proof using the existence of a generalized stable matching in \cite{Generalized-Stable-Matching}. The existence proof can be extended to problems in social games as in \cite{Matching-Equilibrium} and \cite{Social-Games}.
Verifying Safety Properties With the TLA+ Proof System
Venue: arXiv cs.LO 2010
Year: 2010

TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and non-linear proof construction and verification, and it is independent of any verification tool or strategy. A Proof Manager uses backend verifiers such as theorem provers, proof assistants, SMT solvers, and decision procedures to check TLA+ proofs. This paper documents the first public release of TLAPS, distributed with a BSD-like license. It handles almost all the non-temporal part of TLA+ as well as the temporal reasoning needed to prove standard safety properties, in particular invariance and step simulation, but not liveness properties.
Do AES encryptions act randomly?
Venue: arXiv cs.IT 2010
Year: 2010

The Advanced Encryption Standard (AES) is widely recognized as the most important block cipher in common use nowadays. This high assurance in AES is given by its resistance to ten years of extensive cryptanalysis, that has shown no weakness, not even any deviation from the statistical behaviour expected from a random permutation. Only reduced versions of the ciphers have been broken, but they are not usually implemented. In this paper we build a distinguishing attack on the AES, exploiting the properties of a novel cipher embedding. With our attack we give some statistical evidence that the set of AES-$128$ encryptions acts on the message space in a way significantly different than that of the set of random permutations acting on the same space. While we feel that more computational experiments by independent third parties are needed in order to validate our statistical results, we show that the non-random behaviour is the same as we would predict using the property of our embedding. Indeed, the embedding lowers the nonlinearity of the AES rounds and therefore the AES encryptions tend, on average, to keep low the rank of low-rank matrices constructed in the large space. Our attack needs $2^{23}$ plaintext-ciphertext pairs and costs the equivalent of $2^{48}$ encryptions. We expect our attack to work also for AES-$192$ and AES-$256$, as confirmed by preliminary experiments.
Decidability Classes for Mobile Agents Computing
Venue: arXiv cs.DC 2010
Year: 2010

We establish a classification of decision problems that are to be solved by mobile agents operating in unlabeled graphs, using a deterministic protocol. The classification is with respect to the ability of a team of agents to solve the problem, possibly with the aid of additional information. In particular, our focus is on studying differences between the decidability of a decision problem by agents and its verifiability when a certificate for a positive answer is provided to the agents. We show that the class MAV of mobile agents verifiable problems is much wider than the class MAD of mobile agents decidable problems. Our main result shows that there exist natural MAV-complete problems: the most difficult problems in this class, to which all problems in MAV are reducible. Our construction of a MAV-complete problem involves two main ingredients in mobile agents computability: the topology of the quotient graph and the number of operating agents. Beyond the class MAV we show that, for a single agent, three natural oracles yield a strictly increasing chain of relative decidability classes.
Deterministic Compressed Sensing Matrices from Multiplicative Character Sequences
Venue: arXiv cs.IT 2010
Year: 2010

Compressed sensing is a novel technique where one can recover sparse signals from the undersampled measurements. In this paper, a $K \times N$ measurement matrix for compressed sensing is deterministically constructed via multiplicative character sequences. Precisely, a constant multiple of a cyclic shift of an $M$-ary power residue or Sidelnikov sequence is arranged as a column vector of the matrix, through modulating a primitive $M$-th root of unity. The Weil bound is then used to show that the matrix has asymptotically optimal coherence for large $K$ and $M$, and to present a sufficient condition on the sparsity level for unique sparse solution. Also, the restricted isometry property (RIP) is statistically studied for the deterministic matrix. Numerical results show that the deterministic compressed sensing matrix guarantees reliable matching pursuit recovery performance for both noiseless and noisy measurements.
Compensating Interpolation Distortion by New Optimized Modular Method
Venue: arXiv cs.MM 2010
Year: 2010

A modular method was suggested before to recover a band limited signal from the sample and hold and linearly interpolated (or, in general, an nth-order-hold) version of the regular samples. In this paper a novel approach for compensating the distortion of any interpolation based on modular method has been proposed. In this method the performance of the modular method is optimized by adding only some simply calculated coefficients. This approach causes drastic improvement in terms of SNRs with fewer modules compared to the classical modular method. Simulation results clearly confirm the improvement of the proposed method and also its superior robustness against additive noise.
Bounded Multivariate Surfaces On Monovariate Internal Functions
Venue: arXiv cs.CV 2010
Year: 2010

Combining the properties of monovariate internal functions as proposed in Kolmogorov superimposition theorem, in tandem with the bounds wielded by the multivariate formulation of Chebyshev inequality, a hybrid model is presented, that decomposes images into homogeneous probabilistically bounded multivariate surfaces. Given an image, the model shows a novel way of working on reduced image representation while processing and capturing the interaction among the multidimensional information that describes the content of the same. Further, it tackles the practical issues of preventing leakage by bounding the growth of surface and reducing the problem sample size. The model if used, also sheds light on how the Chebyshev parameter relates to the number of pixels and the dimensionality of the feature space that associates with a pixel. Initial segmentation results on the Berkeley image segmentation benchmark indicate the effectiveness of the proposed decomposition algorithm.
Design and Implementation of a Wireless Sensor Network for Smart Homes
Venue: arXiv cs.NI 2010
Year: 2010

Wireless sensor networks (WSNs) have become indispensable to the realization of smart homes. The objective of this paper is to develop such a WSN that can be used to construct smart home systems. The focus is on the design and implementation of the wireless sensor node and the coordinator based on ZigBee technology. A monitoring system is built by taking advantage of the GPRS network. To support multi-hop communications, an improved routing algorithm based on the Dijkstra algorithm is presented. Preliminary simulations have been conducted to evaluate the performance of the algorithm.
A Clustering-based Location Privacy Protection Scheme for Pervasive Computing
Venue: arXiv cs.CR 2010
Year: 2010

In pervasive computing environments, Location- Based Services (LBSs) are becoming increasingly important due to continuous advances in mobile networks and positioning technologies. Nevertheless, the wide deployment of LBSs can jeopardize the location privacy of mobile users. Consequently, providing safeguards for location privacy of mobile users against being attacked is an important research issue. In this paper a new scheme for safeguarding location privacy is proposed. Our approach supports location K-anonymity for a wide range of mobile users with their own desired anonymity levels by clustering. The whole area of all users is divided into clusters recursively in order to get the Minimum Bounding Rectangle (MBR). The exact location information of a user is replaced by his MBR. Privacy analysis shows that our approach can achieve high resilience to location privacy threats and provide more privacy than users expect. Complexity analysis shows clusters can be adjusted in real time as mobile users join or leave. Moreover, the clustering algorithms possess strong robustness.
E-net models for distribution, access and use of resources in security information systems
Venue: arXiv cs.CR 2010
Year: 2010

This paper presents solutions for distribution, access and use of resources in information security systems. The solutions comprise the authors' experience in development and implementation of systems for information security in the Automated Information Systems. The models, the methods and the modus operandi are being explained.
Slightly smaller splitter networks
Venue: arXiv cs.DC 2010
Year: 2010

The classic renaming protocol of Moir and Anderson (1995) uses a network of Theta(n^2) splitters to assign unique names to n processes with unbounded initial names. We show how to reduce this bound to Theta(n^{3/2}) splitters.
Integration of Agile Ontology Mapping towards NLP Search in I-SOAS
Venue: arXiv cs.CL 2010
Year: 2010

In this research paper we address the importance of Product Data Management (PDM) with respect to its contributions in industry. Moreover we also present some currently available major challenges to PDM communities and targeting some of these challenges we present an approach i.e. I-SOAS, and briefly discuss how this approach can be helpful in solving the PDM community's faced problems. Furthermore, limiting the scope of this research to one challenge, we focus on the implementation of a semantic based search mechanism in PDM Systems. Going into the details, at first we describe the respective field i.e. Language Technology (LT), contributing towards natural language processing, to take advantage in implementing a search engine capable of understanding the semantic out of natural language based search queries. Then we discuss how can we practically take advantage of LT by implementing its concepts in the form of software application with the use of semantic web technology i.e. Ontology. Later, in the end of this research paper, we briefly present a prototype application developed with the use of concepts of LT towards semantic based search.
Commutative-like Encryption: A New Characterization of ElGamal
Venue: arXiv cs.CR 2010
Year: 2010

Commutative encryption is a useful but rather strict notion in cryptography. In this paper, we deny a loose variation of commutative encryption-commutative-like encryption and give an example: the generalization of ElGamal scheme. The application of the new variation is also discussed.
Algebraic Watchdog: Mitigating Misbehavior in Wireless Network Coding
Venue: arXiv cs.CR 2010
Year: 2010

We propose a secure scheme for wireless network coding, called the algebraic watchdog. By enabling nodes to detect malicious behaviors probabilistically and use overheard messages to police their downstream neighbors locally, the algebraic watchdog delivers a secure global self-checking network. Unlike traditional Byzantine detection protocols which are receiver-based, this protocol gives the senders an active role in checking the node downstream. The key idea is inspired by Marti et al.'s watchdog-pathrater, which attempts to detect and mitigate the effects of routing misbehavior. As an initial building block of a such system, we first focus on a two-hop network. We present a graphical model to understand the inference process nodes execute to police their downstream neighbors; as well as to compute, analyze, and approximate the probabilities of misdetection and false detection. In addition, we present an algebraic analysis of the performance using an hypothesis testing framework that provides exact formulae for probabilities of false detection and misdetection. We then extend the algebraic watchdog to a more general network setting, and propose a protocol in which we can establish trust in coded systems in a distributed manner. We develop a graphical model to detect the presence of an adversarial node downstream within a general multi-hop network. The structure of the graphical model (a trellis) lends itself to well-known algorithms, such as the Viterbi algorithm, which can compute the probabilities of misdetection and false detection. We show analytically that as long as the min-cut is not dominated by the Byzantine adversaries, upstream nodes can monitor downstream neighbors and allow reliable communication with certain probability. Finally, we present simulation results that support our analysis.
Modeling Image Structure with Factorized Phase-Coupled Boltzmann Machines
Venue: arXiv cs.CV 2010
Year: 2010

We describe a model for capturing the statistical structure of local amplitude and local spatial phase in natural images. The model is based on a recently developed, factorized third-order Boltzmann machine that was shown to be effective at capturing higher-order structure in images by modeling dependencies among squared filter outputs (Ranzato and Hinton, 2010). Here, we extend this model to $L_p$-spherically symmetric subspaces. In order to model local amplitude and phase structure in images, we focus on the case of two dimensional subspaces, and the $L_2$-norm. When trained on natural images the model learns subspaces resembling quadrature-pair Gabor filters. We then introduce an additional set of hidden units that model the dependencies among subspace phases. These hidden units form a combinatorial mixture of phase coupling distributions, concentrated in the sum and difference of phase pairs. When adapted to natural images, these distributions capture local spatial phase structure in natural images.