OpenRaiser/Intern-Atlas huggingface dataset:
Termination Casts: A Flexible Approach to Termination with General Recursion
Venue: arXiv cs.PL 2010
Year: 2010

This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The central idea is to include a primitive type-form "Terminates t", expressing that term t is terminating; and then allow terms t to be coerced from possibly diverging to total, using a proof of Terminates t. We call such coercions termination casts, and show how to implement terminating recursion using them. For the meta-theory of the system, we describe a translation from Teqt to a logical theory of termination for general recursive, simply typed functions. Every typing judgment of Teqt is translated to a theorem expressing the appropriate termination property of the computational part of the Teqt term.
Public Announcements in Strategic Games with Arbitrary Strategy Sets
Venue: arXiv cs.GT 2010
Year: 2010

In [Van Benthem 2007] the concept of a public announcement is used to study the effect of the iterated elimination of strictly dominated strategies. We offer a simple generalisation of this approach to cover arbitrary strategic games and many optimality notions. We distinguish between announcements of optimality and announcements of rationality.
SNEED: Enhancing Network Security Services Using Network Coding and Joint Capacity
Venue: arXiv cs.NI 2010
Year: 2010

Traditional network security protocols depend mainly on developing cryptographic schemes and on using biometric methods. These have led to several network security protocols that are unbreakable based on difficulty of solving untractable mathematical problems such as factoring large integers. In this paper, Security of Networks Employing Encoding and Decoding (SNEED) is developed to mitigate single and multiple link attacks. Network coding and shared capacity among the working paths are used to provide data protection and data integrity against network attackers and eavesdroppers. SNEED can be incorporated into various applications in on-demand TV, satellite communications and multimedia security. Finally, It is shown that SNEED can be implemented easily where there are k edge disjoint paths between two core nodes (routers or switches) in an enterprize network.
Texture feature extraction in the spatial-frequency domain for content-based image retrieval
Venue: arXiv cs.CV 2010
Year: 2010

The advent of large scale multimedia databases has led to great challenges in content-based image retrieval (CBIR). Even though CBIR is considered an emerging field of research, however it constitutes a strong background for new methodologies and systems implementations. Therefore, many research contributions are focusing on techniques enabling higher image retrieval accuracy while preserving low level of computational complexity. Image retrieval based on texture features is receiving special attention because of the omnipresence of this visual feature in most real-world images. This paper highlights the state-of-the-art and current progress relevant to texture-based image retrieval and spatial-frequency image representations. In particular, it gives an overview of statistical methodologies and techniques employed for texture feature extraction using most popular spatial-frequency image transforms, namely discrete wavelets, Gabor wavelets, dual-tree complex wavelet and contourlets. Indications are also given about used similarity measurement functions and most important achieved results.
Generalized Linear Weights for Sharing Credits Among Multiple Authors
Venue: arXiv cs.DL 2010
Year: 2010

Assignment of weights to multiple authors of a paper is a challenging task due to its dependence on the conventions that may be different among different fields of research and research groups. In this paper, we describe a scheme for assignment of weights to multiple authors of a paper. In our scheme, weights are assigned in a linearly decreasing/increasing fashion depending upon the weight decrement/increment parameter. We call our scheme Arithmetic: Type-2 scheme as the weights follow an arithmetic series. We analyze the proposed weight assignment scheme and compare it with the existing schemes such as equal, arithmetic, geometric, and harmonic. We argue that the a positional weight assignment scheme, called arithmetic scheme, which we refer to Arithmetic: Type-1 in this paper, and the equal weight assignment scheme can be treated as special cases of the proposed Arithmetic: Type-2 scheme.
Loops under Strategies ... Continued
Venue: arXiv cs.LO 2010
Year: 2010

While there are many approaches for automatically proving termination of term rewrite systems, up to now there exist only few techniques to disprove their termination automatically. Almost all of these techniques try to find loops, where the existence of a loop implies non-termination of the rewrite system. However, most programming languages use specific evaluation strategies, whereas loop detection techniques usually do not take strategies into account. So even if a rewrite system has a loop, it may still be terminating under certain strategies. Therefore, our goal is to develop decision procedures which can determine whether a given loop is also a loop under the respective evaluation strategy. In earlier work, such procedures were presented for the strategies of innermost, outermost, and context-sensitive evaluation. In the current paper, we build upon this work and develop such decision procedures for important strategies like leftmost-innermost, leftmost-outermost, (max-)parallel-innermost, (max-)parallel-outermost, and forbidden patterns (which generalize innermost, outermost, and context-sensitive strategies). In this way, we obtain the first approach to disprove termination under these strategies automatically.
Image Sterilization to Prevent LSB-based Steganographic Transmission
Venue: arXiv cs.MM 2010
Year: 2010

Sterilization is a very popular word used in biomedical testing (like removal of all microorganisms on surface of an article or in fluid using appropriate chemical products). Motivated by this biological analogy, we, for the first time, introduce the concept of sterilization of an image, i.e., removing any steganographic information embedded in the image. Experimental results show that our technique succeeded in sterilizing around 76% to 91% of stego pixels in an image on average, where data is embedded using LSB-based steganography.
Free and Open-Source Software is not an Emerging Property but Rather the Result of Studied Design
Venue: arXiv cs.CY 2010
Year: 2010

Free and open source software (FOSS) is considered by many, along with Wikipedia, the proof of an ongoing paradigm shift from hierarchically-managed and market-driven production of knowledge to heterarchical, collaborative and commons-based production styles. In such perspective, it has become common place to refer to FOSS as a manifestation of collective intelligence where deliverables and artefacts emerge by virtue of mere cooperation, with no need for supervising leadership. The paper argues that this assumption is based on limited understanding of the software development process, and may lead to wrong conclusions as to the potential of peer production. The development of a less than trivial piece of software, irrespective of whether it be FOSS or proprietary, is a complex cooperative effort requiring the participation of many (often thousands of) individuals. A subset of the participants always play the role of leading system and subsystem designers, determining architecture and functionality; the rest of the people work "underneath" them in a logical, functional sense. While new and powerful forces, including FOSS, are clearly at work in the post-industrial, networked econ-omy, the currently ingenuous stage of research in the field of collective intelligence and networked cooperation must give way to a deeper level of consciousness, which requires an understanding of the software development process.
Multiple-Source Multiple-Sink Maximum Flow in Directed Planar Graphs in $O(n^{1.5} \log n)$ Time
Venue: arXiv cs.DM 2010
Year: 2010

We give an $O(n^{1.5} \log n)$ algorithm that, given a directed planar graph with arc capacities, a set of source nodes and a set of sink nodes, finds a maximum flow from the sources to the sinks.
Affine-invariant diffusion geometry for the analysis of deformable 3D shapes
Venue: arXiv cs.CV 2010
Year: 2010

We introduce an (equi-)affine invariant diffusion geometry by which surfaces that go through squeeze and shear transformations can still be properly analyzed. The definition of an affine invariant metric enables us to construct an invariant Laplacian from which local and global geometric structures are extracted. Applications of the proposed framework demonstrate its power in generalizing and enriching the existing set of tools for shape analysis.
Affine-invariant geodesic geometry of deformable 3D shapes
Venue: arXiv cs.CV 2010
Year: 2010

Natural objects can be subject to various transformations yet still preserve properties that we refer to as invariants. Here, we use definitions of affine invariant arclength for surfaces in R^3 in order to extend the set of existing non-rigid shape analysis tools. In fact, we show that by re-defining the surface metric as its equi-affine version, the surface with its modified metric tensor can be treated as a canonical Euclidean object on which most classical Euclidean processing and analysis tools can be applied. The new definition of a metric is used to extend the fast marching method technique for computing geodesic distances on surfaces, where now, the distances are defined with respect to an affine invariant arclength. Applications of the proposed framework demonstrate its invariance, efficiency, and accuracy in shape analysis.
Parallel sparse matrix-vector multiplication as a test case for hybrid MPI+OpenMP programming
Venue: arXiv cs.PF 2010
Year: 2010

We evaluate optimized parallel sparse matrix-vector operations for two representative application areas on widespread multicore-based cluster configurations. First the single-socket baseline performance is analyzed and modeled with respect to basic architectural properties of standard multicore chips. Going beyond the single node, parallel sparse matrix-vector operations often suffer from an unfavorable communication to computation ratio. Starting from the observation that nonblocking MPI is not able to hide communication cost using standard MPI implementations, we demonstrate that explicit overlap of communication and computation can be achieved by using a dedicated communication thread, which may run on a virtual core. We compare our approach to pure MPI and the widely used "vector-like" hybrid programming strategy.
First-order Fragments with Successor over Infinite Words
Venue: arXiv cs.FL 2010
Year: 2010

We consider fragments of first-order logic and as models we allow finite and infinite words simultaneously. The only binary relations apart from equality are order comparison < and the successor predicate +1. We give characterizations of the fragments Sigma2 = Sigma2[<,+1] and FO2 = FO2[<,+1] in terms of algebraic and topological properties. To this end we introduce the factor topology over infinite words. It turns out that a language L is in the intersection of FO2 and Sigma2 if and only if L is the interior of an FO2 language. Symmetrically, a language is in the intersection of FO2 and Pi2 if and only if it is the topological closure of an FO2 language. The fragment Delta2, which by definition is the intersection of Sigma2 and Pi2 contains exactly the clopen languages in FO2. In particular, over infinite words Delta2 is a strict subclass of FO2. Our characterizations yield decidability of the membership problem for all these fragments over finite and infinite words; and as a corollary we also obtain decidability for infinite words. Moreover, we give a new decidable algebraic characterization of dot-depth 3/2 over finite words. Decidability of dot-depth 3/2 over finite words was first shown by Glaßer and Schmitz in STACS 2000, and decidability of the membership problem for FO2 over infinite words was shown 1998 by Wilke in his habilitation thesis whereas decidability of Sigma2 over infinite words was not known before.
Across Browsers SVG Implementation
Venue: arXiv cs.GR 2010
Year: 2010

In this work SVG will be translated into VML or HTML by using Javascript based on Backbase Client Framework. The target of this project is to implement SVG to be viewed in Internet Explorer without any plug-in and work together with other Backbase Client Framework languages. The result of this project will be added as an extension to the current Backbase Client Framework.
Belief-Propagation for Weighted b-Matchings on Arbitrary Graphs and its Relation to Linear Programs with Integer Solutions
Venue: arXiv cs.IT 2011
Year: 2011

We consider the general problem of finding the minimum weight $\bm$-matching on arbitrary graphs. We prove that, whenever the linear programming (LP) relaxation of the problem has no fractional solutions, then the belief propagation (BP) algorithm converges to the correct solution. We also show that when the LP relaxation has a fractional solution then the BP algorithm can be used to solve the LP relaxation. Our proof is based on the notion of graph covers and extends the analysis of (Bayati-Shah-Sharma 2005 and Huang-Jebara 2007}. These results are notable in the following regards: (1) It is one of a very small number of proofs showing correctness of BP without any constraint on the graph structure. (2) Variants of the proof work for both synchronous and asynchronous BP; it is the first proof of convergence and correctness of an asynchronous BP algorithm for a combinatorial optimization problem.
On Approximating Multi-Criteria TSP
Venue: arXiv cs.DS 2011
Year: 2011

We present approximation algorithms for almost all variants of the multi-criteria traveling salesman problem (TSP). First, we devise randomized approximation algorithms for multi-criteria maximum traveling salesman problems (Max-TSP). For multi-criteria Max-STSP, where the edge weights have to be symmetric, we devise an algorithm with an approximation ratio of 2/3 - eps. For multi-criteria Max-ATSP, where the edge weights may be asymmetric, we present an algorithm with a ratio of 1/2 - eps. Our algorithms work for any fixed number k of objectives. Furthermore, we present a deterministic algorithm for bi-criteria Max-STSP that achieves an approximation ratio of 7/27. Finally, we present a randomized approximation algorithm for the asymmetric multi-criteria minimum TSP with triangle inequality Min-ATSP. This algorithm achieves a ratio of log n + eps.
A language for mathematical knowledge management
Venue: arXiv cs.LO 2011
Year: 2011

We argue that the language of Zermelo Fraenkel set theory with definitions and partial functions provides the most promising bedrock semantics for communicating and sharing mathematical knowledge. We then describe a syntactic sugaring of that language that provides a way of writing remarkably readable assertions without straying far from the set-theoretic semantics. We illustrate with some examples of formalized textbook definitions from elementary set theory and point-set topology. We also present statistics concerning the complexity of these definitions, under various complexity measures.
Principal Graphs and Manifolds
Venue: arXiv cs.LG 2011
Year: 2011

In many physical, statistical, biological and other investigations it is desirable to approximate a system of points by objects of lower dimension and/or complexity. For this purpose, Karl Pearson invented principal component analysis in 1901 and found 'lines and planes of closest fit to system of points'. The famous k-means algorithm solves the approximation problem too, but by finite sets instead of lines and planes. This chapter gives a brief practical introduction into the methods of construction of general principal objects, i.e. objects embedded in the 'middle' of the multidimensional data set. As a basis, the unifying framework of mean squared distance approximation of finite datasets is selected. Principal graphs and manifolds are constructed as generalisations of principal components and k-means principal points. For this purpose, the family of expectation/maximisation algorithms with nearest generalisations is presented. Construction of principal graphs with controlled complexity is based on the graph grammar approach.
Constructing Perfect Steganographic Systems
Venue: arXiv cs.CR 2011
Year: 2011

We propose steganographic systems for the case when covertexts (containers) are generated by a finite-memory source with possibly unknown statistics. The probability distributions of covertexts with and without hidden information are the same; this means that the proposed stegosystems are perfectly secure, i.e. an observer cannot determine whether hidden information is being transmitted. The speed of transmission of hidden information can be made arbitrary close to the theoretical limit - the Shannon entropy of the source of covertexts. An interesting feature of the suggested stegosystems is that they do not require any (secret or public) key. At the same time, we outline some principled computational limitations on steganography. We show that there are such sources of covertexts, that any stegosystem that has linear (in the length of the covertext) speed of transmission of hidden text must have an exponential Kolmogorov complexity. This shows, in particular, that some assumptions on the sources of covertext are necessary.
Split decomposition and graph-labelled trees: characterizations and fully-dynamic algorithms for totally decomposable graphs
Venue: arXiv cs.DM 2011
Year: 2011

In this paper, we revisit the split decomposition of graphs and give new combinatorial and algorithmic results for the class of totally decomposable graphs, also known as the distance hereditary graphs, and for two non-trivial subclasses, namely the cographs and the 3-leaf power graphs. Precisely, we give strutural and incremental characterizations, leading to optimal fully-dynamic recognition algorithms for vertex and edge modifications, for each of these classes. These results rely on a new framework to represent the split decomposition, namely the graph-labelled trees, which also captures the modular decomposition of graphs and thereby unify these two decompositions techniques. The point of the paper is to use bijections between these graph classes and trees whose nodes are labelled by cliques and stars. Doing so, we are also able to derive an intersection model for distance hereditary graphs, which answers an open problem.
First-Order and Temporal Logics for Nested Words
Venue: arXiv cs.LO 2011
Year: 2011

Nested words are a structured model of execution paths in procedural programs, reflecting their call and return nesting structure. Finite nested words also capture the structure of parse trees and other tree-structured data, such as XML. We provide new temporal logics for finite and infinite nested words, which are natural extensions of LTL, and prove that these logics are first-order expressively-complete. One of them is based on adding a "within" modality, evaluating a formula on a subword, to a logic CaRet previously studied in the context of verifying properties of recursive state machines (RSMs). The other logic, NWTL, is based on the notion of a summary path that uses both the linear and nesting structures. For NWTL we show that satisfiability is EXPTIME-complete, and that model-checking can be done in time polynomial in the size of the RSM model and exponential in the size of the NWTL formula (and is also EXPTIME-complete). Finally, we prove that first-order logic over nested words has the three-variable property, and we present a temporal logic for nested words which is complete for the two-variable fragment of first-order.
Completion Time Minimization and Robust Power Control in Wireless Packet Networks
Venue: arXiv cs.IT 2011
Year: 2011

A wireless packet network is considered in which each user transmits a stream of packets to its destination. The transmit power of each user interferes with the transmission of all other users. A convex cost function of the completion times of the user packets is minimized by optimally allocating the users' transmission power subject to their respective power constraints. At all ranges of SINR, completion time minimization can be formulated as a convex optimization problem and hence can be efficiently solved. In particular, although the feasible rate region of the wireless network is non-convex, its corresponding completion time region is shown to be convex. When channel knowledge is imperfect, robust power control is considered based on the channel fading distribution subject to outage probability constraints. The problem is shown to be convex when the fading distribution is log-concave in exponentiated channel power gains; e.g., when each user is under independent Rayleigh, Nakagami, or log-normal fading. Applying the optimization frameworks in a wireless cellular network, the average completion time is significantly reduced as compared to full power transmission.
Contextual hypotheses and semantics of logic programs
Venue: arXiv cs.LO 2011
Year: 2011

Logic programming has developed as a rich field, built over a logical substratum whose main constituent is a nonclassical form of negation, sometimes coexisting with classical negation. The field has seen the advent of a number of alternative semantics, with Kripke-Kleene semantics, the well-founded semantics, the stable model semantics, and the answer-set semantics standing out as the most successful. We show that all aforementioned semantics are particular cases of a generic semantics, in a framework where classical negation is the unique form of negation and where the literals in the bodies of the rules can be `marked' to indicate that they can be the targets of hypotheses. A particular semantics then amounts to choosing a particular marking scheme and choosing a particular set of hypotheses. When a literal belongs to the chosen set of hypotheses, all marked occurrences of that literal in the body of a rule are assumed to be true, whereas the occurrences of that literal that have not been marked in the body of the rule are to be derived in order to contribute to the firing of the rule. Hence the notion of hypothetical reasoning that is presented in this framework is not based on making global assumptions, but more subtly on making local, contextual assumptions, taking effect as indicated by the chosen marking scheme on the basis of the chosen set of hypotheses. Our approach offers a unified view on the various semantics proposed in logic programming, classical in that only classical negation is used, and links the semantics of logic programs to mechanisms that endow rule-based systems with the power to harness hypothetical reasoning.
On the Complexity of Deciding Call-by-Need
Venue: arXiv cs.LO 2011
Year: 2011

In a recent paper we introduced a new framework for the study of call by need computations to normal form and root-stable form in term rewriting. Using elementary tree automata techniques and ground tree transducers we obtained simple decidability proofs for classes of rewrite systems that are much larger than earlier classes defined using the complicated sequentiality concept. In this paper we show that we can do without ground tree transducers in order to arrive at decidability proofs that are phrased in direct tree automata constructions. This allows us to derive better complexity bounds.