Expressing combinatory reduction systems derivations in the rewriting calculus

The last few years have seen the development of the rewriting calculus (also called rho-calculus or ρ-calculus) that uniformly integrates first-order term rewriting and the λ-calculus. The combination of these two latter formalisms has been already handled either by enriching first-order rewriting with higher-order capabilities, like in the Combinatory Reduction Systems (CRS), or by adding to the λ-calculus algebraic features. The various higher-order rewriting systems and the rewriting calculus share similar concepts and have similar applications, and thus, it is important to compare these formalisms to better understand their respective strengths and differences. We show in this paper that we can express Combinatory Reduction Systems derivations in terms of rewriting calculus derivations. The approach we present is based on a translation of each possible CRS-reduction into a corresponding ρ-reduction. Since for this purpose we need to make precise the matching used when evaluating CRS, the second contribution of the paper is to present an original matching algorithm for CRS terms that uses a simple term translation and the classical matching of lambda terms.     

Approximability of Clausal Constraints

We study a family of problems, called Maximum Solution (Max Sol), where the objective is to maximise a linear goal function over the feasible integer assignments to a set of variables subject to a set of constraints. When the domain is Boolean (i.e. restricted to {0,1}), the maximum solution problem is identical to the well-studied Max Ones problem, and the complexity and approximability is completely understood for all restrictions on the underlying constraints. We continue this line of research by considering the Max Sol problem for relations defined by regular signed logic over finite subsets of the natural numbers; the complexity of the corresponding decision problem has recently been classified by Creignou et al. (Theory Comput. Syst. 42(2):239–255, 2008). We give sufficient conditions for when such problems are polynomial-time solvable and we prove that they are APX-hard otherwise. Similar dichotomies are also obtained for variants of the Max Sol problem.     

Decision problems for lower/upper bound parametric timed automata

We investigate a class of parametric timed automata, called lower bound/upper bound (L/U) automata, where each parameter occurs in the timing constraints either as a lower bound or as an upper bound. For such automata, we show that basic decision problems, such as emptiness, finiteness and universality of the set of parameter valuations for which there is a corresponding infinite accepting run of the automaton, is Pspace-complete. We extend these results by allowing the specification of constraints on parameters as a linear system. We show that the considered decision problems are still Pspace-complete, if the lower bound parameters are not compared with the upper bound parameters in the linear system, and are undecidable in general. Finally, we consider a parametric extension of MITL\mathsf{MITL} _0,∞, and prove that the related satisfiability and model checking (w.r.t. L/U automata) problems are Pspace-complete.     

Secure Hamming distance based record linkage with malicious adversaries

Record linkage aims at finding the matching records from two or multiple different databases. Many approximate string matching methods in privacy-preserving record linkage have been presented. In this paper, we study the problem of secure record linkage between two data files in the two-party computation setting. We note that two records are linked when all the Hamming distances between their attributes are smaller than some fixed thresholds. We firstly construct two efficient secure protocols for computing the powers of an encrypted value and implementing zero test on an encrypted value, then present an efficient protocol within constant rounds for computing the Hamming distance based record linkage in the presence of malicious adversaries by transferring these two protocols. We also discuss the extension of our protocol for settling the Levenshtein distance based record linkage problem.     

Model Checking with Strong Fairness

In this paper we present a coherent framework for symbolic model checking of linear-time temporal logic (ltl) properties over finite state reactive systems, taking full fairness constraints into consideration. We use the computational model of a fair discrete system (fds) which takes into account both justice (weak fairness) and compassion (strong fairness). The approach presented here reduces the model-checking problem into the question of whether a given fds is feasible (i.e. has at least one computation). The contribution of the paper is twofold: On the methodological level, it presents a direct self-contained exposition of full ltl symbolic model checking without resorting to reductions to either μ-calculus or ctl. On the technical level, it extends previous methods by dealing with compassion at the algorithmic level instead of either adding it to the specification, or transforming compassion to justice. Finally, we extend ctl^∗ with past operators, and show that the basic symbolic feasibility algorithm presented here, can be used to model check an arbitrary ctl^∗ formula over an fds with full fairness constraints. This research was supported in part by an infra-structure grant from the Israeli Ministry of Science and Art, a grant from the U.S.-Israel Binational Science Foundation, and a gift from Intel.     

DEM: Deep Entity Matching Across Heterogeneous Information Networks

Heterogeneous information networks, which consist of multi-typed vertices representing objects and multi-typed edges representing relations between objects, are ubiquitous in the real world. In this paper, we study the problem of entity matching for heterogeneous information networks based on distributed network embedding and multi-layer perceptron with a highway network, and we propose a new method named DEM short for Deep Entity Matching. In contrast to the traditional entity matching methods, DEM utilizes the multi-layer perceptron with a highway network to explore the hidden relations to improve the performance of matching. Importantly, we incorporate DEM with the network embedding methodology, enabling highly efficient computing in a vectorized manner. DEM’s generic modeling of both the network structure and the entity attributes enables it to model various heterogeneous information networks flexibly. To illustrate its functionality, we apply the DEM algorithm to two real-world entity matching applications: user linkage under the social network analysis scenario that predicts the same or matched users in different social platforms and record linkage that predicts the same or matched records in different citation networks. Extensive experiments on real-world datasets demonstrate DEM’s effectiveness and rationality.

     

Ordering and Path Constraints over Semistructured Data

Constraints are a valuable tool for managing information. Feature constraints have been used for describing records in constraint programming (Aït-Kaci and Podelski, 1993; Smolka and Treinen, 1994) and record like structures in computational linguistics (Kaplan and Bresnan, 1982; Shieber, 1986). In this paper, we consider how constraint-based technology can be used to query and reason about semistructured data. The constraint system FT (Müller et al., 1997) provides information ordering constraints interpreted over feature trees. Here, we show how a generalization of FT combined with path constraints can be used to formally represent, state constraints, and reason about semistructured data. The constraint languages we propose provide possibilities to straightforwardly capture, for example, what it means for a tree to be a subtree or subsumed by another, or what it means for two paths to be divergent. We establish a logical semantics for our constraints thanks to axiom schemes presenting our first-order theory constraint system. We propose using the constraint systems for querying semistructured data.     

Solving the Euclidean bottleneck matching problem byk-relative neighborhood graphs

Given a set of pointsV in the plane, the Euclidean bottleneck matching problem is to match each point with some other point such that the longest Euclidean distance between matched points, resulting from this matching, is minimized. To solve this problem, we definek-relative neighborhood graphs, (kRNG) which are derived from Toussaint's relative neighborhood graphs (RNG). Two points are calledk-relative neighbors if and only if there are less thank points ofV which are closer to both of the two points than the two points are to each other. AkRNG is an undirected graph (V,E _r ^k ) whereE _r ^k is the set of pairs of points ofV which arek-relative neighbors. We prove that there exists an optimal solution of the Euclidean bottleneck matching problem which is a subset ofE _r ¹⁷ . We also prove that ¦E _r ^k ¦ < 18kn wheren is the number of points in setV. Our algorithm would construct a 17RNG first. This takesO(n ²) time. We then use Gabow and Tarjan's bottleneck maximum cardinality matching algorithm for general graphs whose time-complexity isO((n logn)^0.5 m), wherem is the number of edges in the graph, to solve the bottleneck maximum cardinality matching problem in the 17RNG. This takesO(n ^1.5 log^0.5 n) time. The total time-complexity of our algorithm for the Euclidean bottleneck matching problem isO(n ² +n ^1.5 log^0.5 n).This research was partially supported by a grant from the National Science Council of the Republic of China under Grant NSC-78-0408-E-007-05.     

Checking the reliability of socket based communication software

Locating potential execution errors in software is gaining more attention due to the economical and social impact of software crashes. For this reason, many software engineers are now in need of automatic debugging tools in their development environments. Fortunately, the work on formal method technologies during the past 25 years has produced a number of techniques and tools that can make the debugging task almost automatic, using standard computer equipment and with a reasonable response time. In particular, verification techniques like model-checking that were traditionally employed for formal specifications of the software can now be directly employed for real source code. Due to the maturity of model-checking technology, its application to real software is now a promising and realistic approach to increase software quality. There are already some successful examples of tools for this purpose that mainly work with self-contained programs (programs with no system-calls). However, verifying software that uses external functionality provided by the operating system via API s is currently a challenging trend. In this paper, we propose a method for using the tool spin to verify C software systems that use services provided by the operating system thorough a given API. Our approach consists in building a model of the underlying operating system to be joined with the original C code in order to obtain the input for the model checker spin. The whole modeling process is transparent for the C programmer, because it is performed automatically and without special syntactic constraints in the input C code. Regarding verification, we consider optimization techniques suitable for this application domain, and we guarantee that the system only reports potential (non-spurious) errors. We present the applicability of our approach focusing on the verification of distributed software systems that use the API Socket and the network protocol stack TCP/IP for communications. In order to ensure correctness, we define and use a formal semantics of the API to conduct the construction of correct models.     

Partial match queries in relaxed multidimensional search trees

Partial match queries arise frequently in the context of large databases, where each record contains a distinct multidimensional key, that is, the key of each record is aK-tuple of values. The components of a key are called thecoordinates orattributes of the key. In a partial match query we specify the value ofs attributes, 0<s<K, and leave the remainingK —s attributes unspecified. The goal is to retrieve all the records in the database that match the specified attributes. In this paper we present several results about the average performance and variance of partial matches in relaxedK-dimensional trees (search trees and digital tries). These data structures are variants of the well knownK d-trees andK d-tries. In relaxed trees the sequence of attributes used to guide a query is explicitly stored at the nodes of the tree and randomly generated and, in general, will be different for different search paths. In the standard variants, the sequence of attributes that guides a query examines the attributes in a cyclic fashion, fixed and identical for all search paths. We show that the probabilistic analysis of the relaxed multidimensional trees is very similar to that of standardK d-trees andK d-tries, and also to the analysis of quadtrees. In fact, besides the average cost and variance of partial match in relaxedK d-trees andK d-tries, we also obtain the variance of partial matches in two-dimensional quadtrees. We also compute the average cost of partial matches in other relaxed multidimensional digital tries, namely, relaxedK d-Patricia and relaxedK d-digital search trees. This research was supported by Acciones Integradas Hispano-Austríacas HU1997-0016 (Austrian-Spanish Scientific Exchange Program). The first author was also supported by ESPRIT LTR 20244 (ALCOM IT), CICYT TIC97-1475-CE, DGES PB95-0787 (KOALA), and CIRIT 1997SGR-00366 (SGR). The second author was also supported by the Austrian Research Society (FWF) under Project P12599-MAT. Online publication October 13, 2000.     

Efficient top-K approximate searches against a relation with multiple attributes

In this paper, we study the problem of efficiently identifying K records that are most similar to a given query record, where the similarity is defined as: (1) for each record, we calculate the similarity score between the record and the query record over each individual attribute using a specific similarity function; (2) an aggregate function is utilized to combine these similarity scores with weights and the aggregated value is served as the similarity of the record. After similarities of all records have been computed, K records with the greatest similarities can further be identified. Under this framework, unfortunately, the computational cost will be extremely expensive when the cardinality of relation is large as computation of similarity for each record is required. As a result, in this paper, we propose two efficient algorithms, named ScanIndex and Top-Down (TD for short), to cope with this problem. With respect to ScanIndex, similarity scores that are equal to zero over individual attributes are free from computation. Based on ScanIndex, with respect to TD, similarity scores less than thresholds (rather than zero) over individual attributes are skipped, where these thresholds are improved dynamically over time. Experimental results demonstrate that, comparing with the naive approach, the performance can be improved by two orders of magnitude using ScanIndex and TD.     

Privacy preserving record linkage in the presence of missing values

The problem of record linkage is to identify records from two datasets, which refer to the same entities (e.g. patients). A particular issue of record linkage is the presence of missing values in records, which has not been fully addressed. Another issue is how privacy and confidentiality can be preserved in the process of record linkage. In this paper, we propose an approach for privacy preserving record linkage in the presence of missing values. For any missing value in a record, our approach imputes the similarity measure between the missing value and the value of the corresponding field in any of the possible matching records from another dataset. We use the k-NNs (k Nearest Neighbours in the same dataset) of the record with the missing value and their distances to the record for similarity imputation. For privacy preservation, our approach uses the Bloom filter protocol in the settings of both standard privacy preserving record linkage without missing values and privacy preserving record linkage with missing values. We have conducted an experimental evaluation using three pairs of synthetic datasets with different rates of missing values. Our experimental results show the effectiveness and efficiency of our proposed approach.     

State-based versus event-based specifications for information systems: a comparison of B and eb 3

This paper compares two formal methods, B and eb³, for specifying information systems. These two methods are chosen as examples of the state-based paradigm and the event-based paradigm, respectively. The paper considers four viewpoints: functional behavior expression, validation, verification, and evolution. Issues in expressing event ordering constraints, data integrity constraints, and modularity are thereby considered. A simple case study is used to illustrate the comparison, namely, a library management system. Two equivalent specifications are presented using each method. The paper concludes that B and eb³ are complementary. The former is better at expressing complex ordering and static data integrity constraints, whereas the latter provides a simpler, modular, explicit representation of dynamic constraints that are closer to the user’s point of view, while providing loosely coupled definitions of data attributes. The generality of these results from the state-based paradigm and the event-based paradigm perspective are discussed.     

Distributed algorithms for covering, packing and maximum weighted matching

This paper gives poly-logarithmic-round, distributed δ-approximation algorithms for covering problems with submodular cost and monotone covering constraints (Submodular-cost Covering). The approximation ratio δ is the maximum number of variables in any constraint. Special cases include Covering Mixed Integer Linear Programs (CMIP), and Weighted Vertex Cover (with δ = 2). Via duality, the paper also gives poly-logarithmic-round, distributed δ-approximation algorithms for Fractional Packing linear programs (where δ is the maximum number of constraints in which any variable occurs), and for Max Weighted c-Matching in hypergraphs (where δ is the maximum size of any of the hyperedges; for graphs δ = 2). The paper also gives parallel (RNC) 2-approximation algorithms for CMIP with two variables per constraint and Weighted Vertex Cover. The algorithms are randomized. All of the approximation ratios exactly match those of comparable centralized algorithms.     

Random Bichromatic Matchings

Given a graph with edges colored Red and Blue, we study the problem of sampling and approximately counting the number of matchings with exactly k Red edges. We solve the problem of estimating the number of perfect matchings with exactly k Red edges for dense graphs. We study a Markov chain on the space of all matchings of a graph that favors matchings with k Red edges. We show that it is rapidly mixing using non-traditional canonical paths that can backtrack. We show that this chain can be used to sample matchings in the 2-dimensional toroidal lattice of any fixed size ℓ with k Red edges, where the horizontal edges are Red and the vertical edges are Blue. An extended abstract appeared in J.R. Correa, A. Hevia and M.A. Kiwi (eds.) Proceedings of the 7th Latin American Theoretical Informatics Symposium, LNCS 3887, pp. 190–201, Springer, 2006. N. Bhatnagar’s and D. Randall’s research was supported in part by NSF grants CCR-0515105 and DMS-0505505. V.V. Vazirani’s research was supported in part by NSF grants 0311541, 0220343 and CCR-0515186. N. Bhatnagar’s and E. Vigoda’s research was supported in part by NSF grant CCR-0455666.     

A binary neural k-nearest neighbour technique

K-Nearest Neighbour (k-NN) is a widely used technique for classifying and clustering data. K-NN is effective but is often criticised for its polynomial run-time growth as k-NN calculates the distance to every other record in the data set for each record in turn. This paper evaluates a novel k-NN classifier with linear growth and faster run-time built from binary neural networks. The binary neural approach uses robust encoding to map standard ordinal, categorical and real-valued data sets onto a binary neural network. The binary neural network uses high speed pattern matching to recall the k-best matches. We compare various configurations of the binary approach to a conventional approach for memory overheads, training speed, retrieval speed and retrieval accuracy. We demonstrate the superior performance with respect to speed and memory requirements of the binary approach compared to the standard approach and we pinpoint the optimal configurations.     

基于聚类汇总的记录匹配算法

记录匹配算法在异构数据的集成和数据开采等领域应用广泛，其主要任务是找出来自不同数据源中代表同一对象实体的记录，这些记录具备相似的属性和属性值。为避免组合爆炸问题，现有的记录匹配算法不再对数据库中的记录数两两匹配，而是结合排序策略和静态聚类匹配方法实现，但这种静态方法不适应数据的动态变化。因此，本文提出基于聚类汇总的记录匹配算法，该算法可以解决静态方法导致的匹配记录丢失问题，同时能够减少计算量，提高匹配记录搜索效率。     

Attribution of divergent northern vegetation growth responses to lengthening non-frozen seasons using satellite optical-NIR and microwave remote sensing

The non-frozen (NF) season duration strongly influences the northern carbon cycle where frozen (FR) temperatures are a major constraint to biological processes. The landscape freeze-thaw (FT) signal from satellite microwave remote sensing provides a surrogate measure of FR temperature constraints to ecosystem productivity, trace gas exchange, and surface water mobility. We analysed a new global satellite data record of daily landscape FT dynamics derived from temporal classification of overlapping SMMR and SSM/I 37 GHz frequency brightness temperatures (T_b). The FT record was used to quantify regional patterns, annual variability, and trends in the NF season over northern (≥45°N) vegetated land areas. The ecological significance of these changes was evaluated against satellite normalized difference vegetation index (NDVI) anomalies, estimated moisture and temperature constraints to productivity determined from meteorological reanalysis, and atmospheric CO₂ records. The FT record shows a lengthening (2.4 days decade^?1; p < 0.005) mean annual NF season trend (1979–2010) for the high northern latitudes that is 26% larger than the Northern Hemisphere trend. The NDVI summer growth response to these changes is spatially complex and coincides with local dominance of cold temperature or moisture constraints to productivity. Longer NF seasons are predominantly enhancing productivity in cold temperature-constrained areas, whereas these effects are reduced or reversed in more moisture-constrained areas. Longer NF seasons also increase the atmospheric CO₂ seasonal amplitude by enhancing both regional carbon uptake and emissions. We find that cold temperature constraints to northern growing seasons are relaxing, whereas potential benefits for productivity and carbon sink activity are becoming more dependent on the terrestrial water balance and supply of plant-available moisture needed to meet additional water use demands under a warming climate.     

Supporting Efficient Record Linkage for Large Data Sets Using Mapping Techniques

This paper describes an efficient approach to record linkage. Given two lists of records, the record-linkage problem consists of determining all pairs that are similar to each other, where the overall similarity between two records is defined based on domain-specific similarities over individual attributes. The record-linkage problem arises naturally in the context of data cleansing that usually precedes data analysis and mining. Since the scalability issue of record linkage was addressed in [21], the repertoire of database techniques dealing with multidimensional data sets has significantly increased. Specifically, many effective and efficient approaches for distance-preserving transforms and similarity joins have been developed. Based on these advances, we explore a novel approach to record linkage. For each attribute of records, we first map values to a multidimensional Euclidean space that preserves domain-specific similarity. Many mapping algorithms can be applied, and we use the Fastmap approach [16] as an example. Given the merging rule that defines when two records are similar based on their attribute-level similarities, a set of attributes are chosen along which the merge will proceed. A multidimensional similarity join over the chosen attributes is used to find similar pairs of records. Our extensive experiments using real data sets show that our solution has very good efficiency and recall. Part of this article was published in [28]. In addition to the prior materials, this article contains more analysis, a complete proof, and more experimental results that were not included in the original paper.