We present new results on finite satisfiability of logics with counting and arithmetic. One result is a tight bound on the complexity of satisfiability of logics with so-called local Presburger quantifiers, which sum over neighbors of a node in a graph. A second contribution concerns computing a semilinear representation of the cardinalities associated with a formula in two variable logic extended with counting quantifiers. Such a representation allows you to get bounds not only on satisfiability for these logics, but for satisfiability in the presence of additional "global cardinality constraints": restrictions on cardinalities of unary formulas, expressed using arbitrary decidability logics over arithmetic. In the process, we provide simpler proofs of some key prior results on finite satisfiability and semi-linearity of the spectrum for these logics.

Graph neural networks (GNNs) are the predominant architecture for learning over graphs. As with any machine learning model, an important issue is the detection of attacks, where an adversary can change the output with a small perturbation of the input. Techniques for solving the adversarial robustness problem – determining whether an attack exists – were originally developed for image classification. In the case of graph learning, the attack model usually considers changes to the graph structure in addition to or instead of the numerical features of the input, and the state of the art techniques proceed via reduction to constraint solving, working on top of powerful solvers, e.g. for mixed integer programming. We show that it is possible to improve on the state of the art in structural robustness by replacing the use of powerful solvers by calls to efficient partial solvers, which run in polynomial time but may be incomplete. We evaluate our tool $$\textsc {RobLight} $$ on a diverse set of GNN variants and datasets.

We consider the complexity of the open-world query answering problem, where we wish to determine certain answers to conjunctive queries over incomplete datasets specified by an initial set of facts and a set of guarded TGDs. This problem has been well-studied in the literature and is decidable but with a high complexity, namely, it is 2EXPTIME complete. Further, the complexity shrinks by one exponential when the arity is fixed. We show in this paper how we can obtain better complexity bounds when considering separately the arity of the guard atom and that of the additional atoms, called the side signature. Our results make use of the technique of linearizing guarded TGDs, introduced in Gottlob, Manna, and Pieris. Specifically, we present a variant of the linearization process, making use of a restricted version of the chase that we recently introduced. Our results imply that open-world query answering with guarded TGDs can be solved in EXPTIME with arbitrary-arity guard relations if we simply bound the arity of the side signature; and that the complexity drops to NP if we fix the side signature and bound the width of the dependencies.

We present results concerning the expressiveness and decidability of a popular graph learning formalism, graph neural networks (GNNs), exploiting connections with logic. We use a family of recently-discovered decidable logics involving “Presburger quantifiers.” We show how to use these logics to measure the expressiveness of classes of GNNs, in some cases getting exact correspondences between the expressiveness of logics and GNNs. We also employ the logics, and the techniques used to analyze them, to obtain decision procedures for verification problems over GNNs. We complement this with undecidability results for static analysis problems involving the logics, as well as for GNN verification problems.

For many standard models of random structure, first-order logic sentences exhibit a convergence phenomenon on random inputs. The most well-known example is for random graphs with constant edge probability, where the probabilities of first-order sentences converge to 0 or 1. In other cases, such as certain "sparse random graph" models, the probabilities of sentences converge, although not necessarily to 0 or 1. In this work we deal with extensions of first-order logic with aggregate operators, variations of averaging. These logics will consist of real-valued terms, and we allow arbitrary Lipschitz functions to be used as "connectives". We show that some of the well-known convergence laws extend to this setting.

We present results concerning the expressiveness and decidability of a popular graph learning formalism, graph neural networks (GNNs), exploiting connections with logic. We use a family of recently-discovered decidable logics involving "Presburger quantifiers". We show how to use these logics to measure the expressiveness of classes of GNNs, in some cases getting exact correspondences between the expressiveness of logics and GNNs. We also employ the logics, and the techniques used to analyze them, to obtain decision procedures for verification problems over GNNs. We complement this with undecidability results for static analysis problems involving the logics, as well as for GNN verification problems.

We study the interaction of views, queries, and background knowledge in the form of existential rules. The motivating questions concern monotonic determinacy of a query using views w.r.t. rules, which refers to the ability to recover the query answer from the views via a monotone function. We study the decidability of monotonic determinacy, and compare with variations that require the “recovery function” to be in a well-known monotone query language, such as conjunctive queries or Datalog. Surprisingly, we find that even in the presence of basic existential rules, the borderline between well-behaved and badly-behaved answerability differs radically from the unconstrained case. In order to understand this boundary, we require new results concerning entailment problems involving views and rules.

We present a new angle on the expressive power of graph neural networks (GNNs) by studying how the predictions of real-valued GNN classifiers, such as those classifying graphs probabilistically, evolve as we apply them on larger graphs drawn from some random graph model. We show that the output converges to a constant function, which upper-bounds what these classifiers can uniformly express. This strong convergence phenomenon applies to a very wide class of GNNs, including state of the art models, with aggregates including mean and the attention-based mechanism of graph transformers. Our results apply to a broad class of random graph models, including sparse and dense variants of the Erdős-Rényi model, the stochastic block model, and the Barabási-Albert model. We empirically validate these findings, observing that the convergence phenomenon appears not only on random graphs but also on some real-world graphs.

We consider learning a probabilistic classifier from partially-labelled supervision (inputs denoted with multiple possibilities) using standard neural architectures with a softmax as the final layer. We identify a bias phenomenon that can arise from the softmax layer in even simple architectures that prevents proper exploration of alternative options, making the dynamics of gradient descent overly sensitive to initialization. We introduce a novel loss function that allows for unbiased exploration within the space of alternative outputs. We give a theoretical justification for our loss function, and provide an extensive evaluation of its impact on synthetic data, on standard partially labelled benchmarks and on a contributed novel benchmark related to an existing rule learning challenge.

Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving two distinguished sets of relational symbols. One set of relations is for the "source data" I, and the other is for the "interface data" O. Such a specification is a valid definition of O in terms of I, if any two models of the specification agreeing on I agree on O. In contrast, an explicit definition is a transformation (or "query" below) that produces O from I. Variants of Beth's theorem state that one can convert implicit definitions to explicit ones. Further, this conversion can be done effectively given a proof witnessing implicit definability in a suitable proof system. We prove the analogous implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be converted to explicit definitions in the nested relational calculus (NRC). We first provide a model-theoretic argument for this result, which makes some additional connections that may be of independent interest, between NRC queries, interpretations, a standard mechanism for defining structure-to-structure translation in logic, and between interpretations and implicit to definability "up to unique isomorphism". The latter connection uses a variation of a result of Gaifman concerning "relatively categorical" theories. We also provide a proof-theoretic result that provides an effective argument: from a proof witnessing implicit definability, we can efficiently produce an NRC definition. This will involve introducing the appropriate proof system for reasoning with nested sets, along with some auxiliary Beth-type results for this system. As a consequence, we can effectively extract rewritings of NRC queries in terms of NRC views, given a proof witnessing that the query is determined by the views.

Abstract. We consider the extension of [Formula: see text] with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence, i.e., the set of the sizes of its finite models, is definable in Presburger arithmetic. In the process we present several refinements to the “biregular graph method.” In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.

Guarded tuple-generating dependencies (GTGDs) are a natural extension of description logics and referential constraints. It has long been known that queries over GTGDs can be answered by a variant of the chase —a quintessential technique for reasoning with dependencies. However, there has been little work on concrete algorithms and even less on implementation. To address this gap, we revisit Datalog rewriting approaches to query answering, where a set of GTGDs is transformed to a Datalog program that entails the same base facts on each base instance. We show that a rewriting consists of “shortcut” rules that circumvent certain chase steps, we present several algorithms that compute a rewriting by deriving such “shortcuts” efficiently, and we discuss important implementation issues. Finally, we show empirically that our techniques can process complex GTGDs derived from synthetic and real benchmarks and are thus suitable for practical use.

We investigate expansions of Presburger arithmetic, i.e., the theory of the integers with addition and order, with additional structure related to exponentiation: either a function that takes a number to the power of $2$, or a predicate for the powers of $2$. The latter theory, denoted $\mathrm{PresPower}$, was introduced by Büchi as a first attempt at characterizing the sets of tuples of numbers that can be expressed using finite automata; Büchi's method does not give an elementary upper bound, and the complexity of this theory has been open. The former theory, denoted as $\mathrm{PresExp}$, was shown decidable by Semenov; while the decision procedure for this theory differs radically from the automata-based method proposed by Büchi, Semenov's method is also non-elementary. And in fact, the theory with the power function has a non-elementary lower bound. In this paper, we show that while Semenov's and Büchi's approaches yield non-elementary blow-ups for $\mathrm{PresPower}$, the theory is in fact decidable in triply exponential time, similarly to the best known quantifier-elimination algorithm for Presburger arithmetic. We also provide a $\mathrm{NExpTime}$ upper bound for the existential fragment of $\mathrm{PresExp}$, a step towards a finer-grained analysis of its complexity. Both these results are established by analyzing a single parameterized satisfiability algorithm for $\mathrm{PresExp}$, which can be specialized to either the setting of $\mathrm{PresPower}$ or the existential theory of $\mathrm{PresExp}$. Besides the new upper bounds for the existential theory of $\mathrm{PresExp}$ and $\mathrm{PresPower}$, we believe our algorithm provides new intuition for the decidability of these theories, and for the features that lead to non-elementary blow-ups.

We revisit evaluation of logical formulas that allow both uninterpreted relations, constrained to be finite, as well as interpreted vocabulary over an infinite domain: denoted in the past as embedded finite model theory. We extend the analysis of "collapse results": the ability to eliminate first-order quantifiers over the infinite domain in favor of quantification over the finite structure. We investigate several weakenings of collapse, one allowing higher-order quantification over the finite structure, another allowing expansion of the theory. We also provide results comparing collapse for unary signatures with general signatures, and new analyses of collapse for natural decidable theories.

Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving the source data I and the interface data O. It is a valid definition of O in terms of I, if any two models of the specification agreeing on I agree on O. In contrast, an explicit definition is a query that produces O from I. Variants of Beth's theorem state that one can convert implicit definitions to explicit ones. Further, this conversion can be done effectively given a proof witnessing implicit definability in a suitable proof system. We prove the analogous effective implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be effectively converted to explicit definitions in the nested relational calculus (NRC). As a consequence, we can effectively extract rewritings of NRC queries in terms of NRC views, given a proof witnessing that the query is determined by the views.

A query Q is monotonically determined over a set of views V if Q can be expressed as a monotonic function of the view image. In the case of relational algebra views and queries, monotonic determinacy coincides with rewritability as a union of conjunctive queries, and it is decidable in important special cases, such as for conjunctive query views and queries. We investigate the situation for views and queries in the recursive query language Datalog. We give both positive and negative results about the ability to decide monotonic determinacy, and also about the co-incidence of monotonic determinacy with Datalog rewritability.

No abstract available.

Guarded tuple-generating dependencies (GTGDs) are a natural extension of description logics and referential constraints. It has long been known that queries over GTGDs can be answered by a variant of the chase ---a quintessential technique for reasoning with dependencies. However, there has been little work on concrete algorithms and even less on implementation. To address this gap, we revisit Datalog rewriting approaches to query answering, where GTGDs are transformed to a Datalog program that entails the same base facts on each base instance. We show that the rewriting can be seen as containing "shortcut" rules that circumvent certain chase steps, we present several algorithms that compute the rewriting by simulating specific types of chase steps, and we discuss important implementation issues. Finally, we show empirically that our techniques can process complex GTGDs derived from synthetic and real benchmarks and are thus suitable for practical use.

Nested relations, built up from atomic types via product and set types, form a rich data model. Over the last decades the nested relational calculus, NRC, has emerged as a standard language for defining transformations on nested collections. NRC is a strongly-typed functional language which allows building up transformations using tupling and projections, a singleton-former, and a map operation that lifts transformations on tuples to transformations on sets. In this work we describe an alternative declarative method of describing transformations in logic. A formula with distinguished inputs and outputs gives an implicit definition if one can prove that for each input there is only one output that satisfies it. Our main result shows that one can synthesize transformations from proofs that a formula provides an implicit definition, where the proof is in an intuitionistic calculus that captures a natural style of reasoning about nested collections. Our polynomial time synthesis procedure is based on an analog of Craig's interpolation lemma, starting with a provable containment between terms representing nested collections and generating an NRC expression that interpolates between them. We further show that NRC expressions that implement an implicit definition can be found when there is a classical proof of functionality, not just when there is an intuitionistic one. That is, whenever a formula implicitly defines a transformation, there is an NRC expression that implements it.

Nested relational query languages have long been seen as an attractive tool for scenarios involving large hierarchical datasets. There has been a resurgence of interest in nested relational languages. One driver has been the affinity of these languages for large-scale processing platforms such as Spark and Flink. This demonstration gives a tour of TraNCE, a new system for processing nested data on top of distributed processing systems. The core innovation of the system is a compiler that processes nested relational queries in a series of transformations; these include variants of two prior techniques, shredding and unnesting, as well as a materialization transformation that customizes the way levels of the nested output are generated. The TraNCE platform builds on these techniques by adding components for users to create and visualize queries, as well as data exploration and notebook execution targets to facilitate the construction of large-scale data science applications. The demonstration will both showcase the system from the viewpoint of usability by data scientists and illustrate the data management techniques employed.

We provide a wide-ranging study of the scenario where a subset of the relations in a relational vocabulary is visible to a user—that is, their complete contents are known—while the remaining relations are invisible. We also have a background theory—invariants given by logical sentences—that may relate the visible relations to invisible ones, and also may constrain both the visible and invisible relations in isolation. We want to determine whether some other information, given as a positive existential formula, can be inferred using only the visible information and the background theory. This formula whose inference we are concerned with is denoted as the query . We consider whether positive information about the query can be inferred, and also whether negative information—the sentence does not hold—can be inferred. We further consider both the instance-level version of the problem, where both the query and the visible instance are given, and the schema-level version, where we want to know whether truth or falsity of the query can be inferred in some instance of the schema.

We study the design of data publishing mechanisms that allow a collection of autonomous distributed datasources to collaborate to support queries. A common mechanism for data publishing is via views: functions that expose derived data to users, usually specified as declarative queries. Our autonomy assumption is that the views must be on individual sources, but with the intention of supporting integrated queries. In deciding what data to expose to users, two considerations must be balanced. The views must be sufficiently expressive to support queries that users want to ask -- the utility of the publishing mechanism. But there may also be some expressiveness restriction. Here we consider two restrictions, a minimal information requirement, saying that the views should reveal as little as possible while supporting the utility query, and a non-disclosure requirement, formalizing the need to prevent external users from computing information that data owners do not want revealed. We investigate the problem of designing views that satisfy both an expressiveness and an inexpressiveness requirement, for views in a restricted declarative language (conjunctive queries), and for arbitrary views.

We consider the extension of FO² with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence is definable in Presburger arithmetic. In the process we present several refinements to the "biregular graph method". In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.

While large-scale distributed data processing platforms have become an attractive target for query processing, these systems are problematic for applications that deal with nested collections. Programmers are forced either to perform non-trivial translations of collection programs or to employ automated flattening procedures, both of which lead to performance problems. These challenges only worsen for nested collections with skewed cardinalities, where both handcrafted rewriting and automated flattening are unable to enforce load balancing across partitions. In this work, we propose a framework that translates a program manipulating nested collections into a set of semantically equivalent shredded queries that can be efficiently evaluated. The framework employs a combination of query compilation techniques, an efficient data representation for nested collections, and automated skew-handling. We provide an extensive experimental evaluation, demonstrating significant improvements provided by the framework in diverse scenarios for nested collection programs.

Open-world query answering is the problem of deciding, given a set of facts, conjunction of constraints, and query, whether the facts and constraints imply the query. This amounts to reasoning over all instances that include the facts and satisfy the constraints. We study finite open-world query answering (FQA), which assumes that the underlying world is finite and thus only considers the finite completions of the instance. The major known decidable cases of FQA derive from the following: the guarded fragment of first-order logic, which can express referential constraints (data in one place points to data in another) but cannot express number restrictions such as functional dependencies; and the guarded fragment with number restrictions but on a signature of arity only two. In this article, we give the first decidability results for FQA that combine both referential constraints and number restrictions for arbitrary signatures: We show that, for unary inclusion dependencies and functional dependencies, the finiteness assumption of FQA can be lifted up to taking the finite implication closure of the dependencies. Our result relies on new techniques to construct finite universal models of such constraints for any bound on the maximal query size.

We reconsider the problem of containment of monadic datalog (MDL) queries in unions of conjunctive queries (UCQs). Prior work has dealt with special cases of the problem but has left the precise complexity characterization open. In addition, the complexity of one important special case, that of containment under access patterns, was not known before. We start by revisiting the connection between MDL/UCQ containment and containment problems involving regular tree languages. We then present a general approach for getting tighter bounds on the complexity of query containment, based on analysis of the number of mappings of queries into tree-like instances. We give two applications of the machinery. We first give an important special case of the MDL/UCQ containment problem that is in EXPTIME, and we use this bound to show an EXPTIME bound on containment under access patterns. Second, we show that the same technique can be used to get a new tight upper bound for containment of tree automata in UCQs. We finally show that the new MDL/UCQ upper bounds are tight. We establish a 2EXPTIME lower bound on the MDL/UCQ containment problem, resolving an open problem from the early 1990s. This bound holds for the MDL/CQ containment problem as well. We also show that changes to the conditions given in our special cases can not be eliminated, and that in particular slight variations of the problem of containment under access patterns become 2EXPTIME-complete.

Data integration systems allow users to access data sitting in multiple sources by means of queries over a global schema, related to the sources via mappings. Datasources often contain sensitive information, and thus an analysis is needed to verify that a schema satisfies a privacy policy, given as a set of queries whose answers should not be accessible to users. Such an analysis should take into account not only knowledge that an attacker may have about the mappings, but also what they may know about the semantics of the sources.In this paper, we show that source constraints can have a dramatic impact on disclosure analysis. We study the problem of determining whether a given data integration system discloses a source query to an attacker in the presence of constraints, providing both lower and upper bounds on source-aware disclosure analysis.

We look at characterizing which formulas are expressible in rich decidable logics such as guarded fixpoint logic, unary negation fixpoint logic, and guarded negation fixpoint logic. We consider semantic characterizations of definability, as well as effective characterizations. Our algorithms revolve around a finer analysis of the tree-model property and a refinement of the method of moving back and forth between relational logics and logics over trees.

Inspired by the magic sets for Datalog, we present a novel goal-driven approach for answering queries over terminating existential rules with equality (aka TGDs and EGDs). Our technique improves the performance of query answering by pruning the consequences that are not relevant for the query. This is challenging in our setting because equalities can potentially affect all predicates in a dataset. We address this problem by combining the existing singularization technique with two new ingredients: an algorithm for identifying the rules relevant to a query and a new magic sets algorithm. We show empirically that our technique can significantly improve the performance of query answering, and that it can mean the difference between answering a query in a few seconds or not being able to process the query at all.

We consider answering queries on data available through access methods, that provide lookup access to the tuples matching a given binding. Such interfaces are common on the Web; further, they often have bounds on how many results they can return, e.g., because of pagination or rate limits. We thus study result-bounded methods, which may return only a limited number of tuples. We study how to decide if a query is answerable using result-bounded methods, i.e., how to compute a plan that returns all answers to the query using the methods, assuming that the underlying data satisfies some integrity constraints. We first show how to reduce answerability to a query containment problem with constraints. Second, we show "schema simplification" theorems describing when and how result-bounded services can be used. Finally, we use these theorems to give decidability and complexity results about answerability for common constraint classes.

The last few decades have seen vast progress in computational reasoning. This has included significant developments in theory, increasing maturity of tools both in performance and usability, and the evolution of standards and benchmarks. The purpose of this article is to reflect on the use of reasoning for rewriting and simplifying relational database queries. We undertake a review of some of the results and reasoning algorithms that have been developed with a motivation from query evaluation, and add to this a look at open problems in the area as well as a critique of prior work from the point of view of practice.

We consider entailment problems involving powerful constraint languages such as frontier-guarded existential rules in which we impose additional semantic restrictions on a set of distinguished relations. We consider restricting a relation to be transitive, restricting a relation to be the transitive closure of another relation, and restricting a relation to be a linear order. We give some natural variants of guardedness that allow inference to be decidable in each case, and isolate the complexity of the corresponding decision problems. Finally we show that slight changes in these conditions lead to undecidability.

Abstract The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this article we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics.

Ontology-based data integration systems allow users to effectively access data sitting in multiple sources by means of queries over a global schema described by an ontology. In practice, datasources often contain sensitive information that the data owners want to keep inaccessible to users. In this paper, we formalize and study the problem of determining whether a given data integration system discloses a source query to an attacker. We consider disclosure on a particular dataset, and also whether a schema admits a dataset on which disclosure occurs. We provide lower and upper bounds on disclosure analysis, in the process introducing a number of techniques for analyzing logical privacy issues in ontology-based data integration.

We look at characterizing which formulas are expressible in rich decidable logics such as guarded fixpoint logic, unary negation fixpoint logic, and guarded negation fixpoint logic. We consider semantic characterizations of definability, as well as effective characterizations. Our algorithms revolve around a finer analysis of the tree-model property and a refinement of the method of moving back-and-forth between relational logics and logics over trees.

We consider a setting where a user wants to pose a query against a dataset where background knowledge, expressed as logical sentences, is available, but only a subset of the information can be used to answer the query. We thus want to reformulate the user query against the subvocabulary, arriving at a query equivalent to the user’s query assuming the background theory, but using only the restricted vocabulary. We consider two variations of the problem, one where we want any such reformulation and another where we restrict the size. We present a classification of the complexity of the problem, then provide algorithms for solving the problems in practice and evaluate their performance.

We describe ArtForm, a tool for exploring the codebase of dynamic data-driven websites where users enter data via forms. ArtForm extends an instrumented browser, so it can directly implement user interactions, adding in symbolic and concolic execution of JavaScript. The tool supports a range of exploration modes with varying degrees of user intervention. It includes a number of adaptations of concolic execution to the setting of form-based web programs.

We introduce a generalisation of weighted automata over a field, called polynomial automata, and we analyse the complexity of the Zeroness Problem in this model, that is, whether a given automaton outputs zero on all words. While this problem is non-primitive recursive in general, we highlight a subclass of polynomial automata for which the Zeroness Problem is primitive recursive. Refining further, we identify a subclass of affine VAS for which coverability is in 2EXPSPACE. We also use polynomial automata to obtain new proofs that equivalence of streaming string transducers is decidable, and that equivalence of copyless streaming string transducers is in PSPACE.

The chase is a family of algorithms used in a number of data management tasks, such as data exchange, answering queries under dependencies, query reformulation with constraints, and data cleaning. It is well established as a theoretical tool for understanding these tasks, and in addition a number of prototype systems have been developed. While individual chase-based systems and particular optimizations of the chase have been experimentally evaluated in the past, we provide the first comprehensive and publicly available benchmark---test infrastructure and a set of test scenarios---for evaluating chase implementations across a wide range of assumptions about the dependencies and the data. We used our benchmark to compare chase-based systems on data exchange and query answering tasks with one another, as well as with systems that can solve similar tasks developed in closely related communities. Our evaluation provided us with a number of new insights concerning the factors that impact the performance of chase implementations.

Guardedness restrictions are one of the principal means to obtain decidable logics --- operators such as negation are restricted so that the free variables are contained in an atom. While guardedness has been applied fruitfully in the setting of first-order logic, the ability to add fixpoints while retaining decidability has been very limited. Here we show that one of the main restrictions imposed in the past can be lifted, getting a richer decidable logic by allowing fixpoints in which the parameters of the fixpoint can be unguarded. Using automata, we show that the resulting logics have a decidable satisfiability problem, and provide a fine study of the complexity of satisfiability. We show that similar methods apply to decide questions concerning the elimination of fixpoints within formulas of the logic.

We provide a wide-ranging study of the scenario where a subset of the relations in the schema are visible --- that is, their complete contents are known --- while the remaining relations are invisible. We also have integrity constraints (invariants given by logical sentences) which may relate the visible relations to the invisible ones. We want to determine which information about a query (a positive existential sentence) can be inferred from the visible instance and the constraints. We consider both positive and negative query information, that is, whether the query or its negation holds. We consider the instance-level version of the problem, where both the query and the visible instance are given, as well as the schema-level version, where we want to know whether truth or falsity of the query can be inferred in some instance of the schema.

Semantic Web technologies such as RDF and its query language, SPARQL, offer the possibility of opening up the use of public datasets to a great variety of ordinary users. But a key obstacle to the use of open data is the unfamiliarity of users with the structure of data or with SPARQL. To deal with these issues, we introduce a system for querying RDF data by example. At its core is a technique for reverse-engineering SPARQL queries by example. We demonstrate how reverse engineering along with other techniques, such as query relaxation, enables our system, SPARQLByE, to guide users who are unfamiliar with both the dataset and with SPARQL to the desired query and result set.

Verification of properties expressed in the two-variable fragment of first-order logic FO 2 has been investigated in a number of contexts. The satisfiability problem for FO 2 over arbitrary structures is known to be NEXPTIME-complete, with satisfiable formulas having exponential-sized models. Over words, where FO 2 is known to have the same expressiveness as unary temporal logic, satisfiability is again NEXPTIME-complete. Over finite labelled ordered trees, FO 2 has the same expressiveness as navigational XPath, a popular query language for XML documents. Prior work on XPath and FO 2 gives a 2EXPTIME bound for satisfiability of FO 2 over trees. This work contains a comprehensive analysis of the complexity of FO 2 on trees, and on the size and depth of models. We show that different techniques are required depending on the vocabulary used, whether the trees are ranked or unranked, and the encoding of labels on trees. We also look at a natural restriction of FO 2 , its guarded version, GF 2 . Our results depend on an analysis of types in models of FO 2 formulas, including techniques for controlling the number of distinct subtrees, the depth, and the size of a witness to satisfiability for FO 2 sentences over finite trees.

Desirable properties of a logic include decidability, and a model theory that inherits properties of first-order logic, such as interpolation and preservation theorems. It is known that the Guarded Fragment (GF) of first-order logic is decidable and satisfies some preservation properties from first-order model theory; however, it fails to have Craig interpolation. The Guarded Negation Fragment (GNF), a recently defined extension, is known to be decidable and to have Craig interpolation. Here we give the first results on effective interpolation for extensions of GF. We provide an interpolation procedure for GNF whose complexity matches the doubly exponential upper bound for satisfiability of GNF. We show that the same construction gives not only Craig interpolation, but Lyndon interpolation and relativized interpolation, which can be used to provide effective proofs of some preservation theorems. We provide upper bounds on the size of GNF interpolants for both GNF and GF input, and complement this with matching lower bounds.

Marx and de Rijke have shown that the navigational core of the w3c XML query language XPath is not first-order complete; that is, it cannot express every query definable in first-order logic over the navigational predicates. How can one extend XPath to get a first-order complete language? Marx has shown that Conditional XPath—an extension of XPath with an “Until” operator—is first-order complete. The completeness argument makes essential use of the presence of upward axes in Conditional XPath. We examine whether it is possible to get “forward-only” languages that are first-order complete for Boolean queries on ordered trees. It is easy to see that a variant of the temporal logic CTL * is first-order complete; the variant has path quantifiers for downward, leftward, and rightward paths, while along a path one can check arbitrary formulas of Linear Temporal Logic (LTL). This language has two major disadvantages: It requires path quantification in both horizontal directions (in particular, it requires looking backward at the prior siblings of a node), and it requires the consideration of formulas of LTL of arbitrary complexity on vertical paths. This last is in contrast with Marx’s Conditional XPath, which requires only the checking of a single Until operator on a path. We investigate whether either of these restrictions can be eliminated. Our main results are negative ones. We show that if we restrict our CTL * language by having an Until operator in only one horizontal direction, then we lose completeness. We also show that no restriction to a “small” subset of LTL along vertical paths is sufficient for first-order completeness. Smallness here means of bounded “Until Depth,” a measure of complexity of LTL formulas defined by Etessami and Wilke. In particular, it follows from our work that Conditional XPath with only forward axes is not expressively complete; this extends results proved by Rabinovich and Maoz in the context of infinite unordered trees.

We present algorithms for answering queries making use of information about source integrity constraints, access restrictions, and access costs. Our method can exploit the integrity constraints to find plans even when there is no direct access to relations appearing in the query. We look at different kinds of plans, depending on the kind of relational operators that are permitted within their commands. To each type of plan, we associate a semantic property that is necessary for having a plan of that type. The key idea of our method is to move from a search for a plan to a search for a proof of the corresponding semantic property, and then generate a plan from a proof . We provide algorithms for converting proofs to plans and show that they will find a plan of the desired type whenever such a plan exists. We show that while discovery of one proof allows us to find a single plan that answers the query, we can explore alternative proofs to find lower-cost plans.

Open-world query answering is the problem of deciding, given a set of facts, conjunction of constraints, and query, whether the facts and constraints imply the query. This amounts to reasoning over all instances that include the facts and satisfy the constraints. We study finite open-world query answering (FQA), which assumes that the underlying world is finite and thus only considers the finite completions of the instance. The major known decidable cases of FQA derive from the following: the guarded fragment of first-order logic, which can express referential constraints (data in one place points to data in another) but cannot express number restrictions such as functional dependencies, and the guarded fragment with number restrictions but on a signature of arity only two. In this paper, we give the first decidability results for FQA that combine both referential constraints and number restrictions for arbitrary signatures: we show that, for unary inclusion dependencies and functional dependencies, the finiteness assumption of FQA can be lifted up to taking the finite implication closure of the dependencies[5]. Our result relies on new techniques to construct finite universal models of such constraints, for any bound on the maximal query size.

A logic satisfies Craig interpolation if whenever one formula ?1 in the logic entails another formula ?2 in the logic, there is an intermediate formula -- one entailed by ?1 and entailing ?2 -- using only relations in the common signature of ? and ?2. Uniform interpolation strengthens this by requiring the interpolant to depend only on ?1 and the common signature. A uniform interpolant can thus be thought of as a minimal upper approximation of a formula within a sub signature. For first-order logic, interpolation holds but uniform interpolation fails. Uniform interpolation is known to hold for several modal and description logics, but little is known about uniform interpolation for fragments of predicate logic over relations with arbitrary arity. Further, little is known about ordinary Craig interpolation for logics over relations of arbitrary arity that have a recursion mechanism, such as fix point logics. In this work we take a step towards filling these gaps, proving interpolation for a decidable fragment of least fix point logic called unary negation fix point logic. We prove this by showing that for any fixed k, uniform interpolation holds for the k-variable fragment of the logic. In order to show this we develop the technique of reducing questions about logics with tree-like models to questions about modal logics, following an approach by Gradel, Hirsch, and Otto. While this technique has been applied to expressivity and satisfiability questions before, we show how to extend it to reduce interpolation questions about such logics to interpolation for the µ-calculus.

Given a formula phi(x, X) positive in X, the bounded ness problem asks whether the fix point induced by phi is reached within some uniform bound independent of the structure (i.e. Whether the fix point is spurious, and can in fact be captured by a finite unfolding of the formula). In this paper, we study the bounded ness problem when phi is in the guarded fragment or guarded negation fragment of first-order logic, or the fix point extensions of these logics. It is known that guarded logics have many desirable computational and model theoretic properties, including in some cases decidable bounded ness. We prove that bounded ness for the guarded negation fragment is decidable in elementary time, and, making use of an unpublished result of Colcombet, even 2EXPTIME-complete. Our proof extends the connection between guarded logics and automata, reducing bounded ness for guarded logics to a question about cost automata on trees, a type of automaton with counters that assigns a natural number to each input rather than just a boolean.

Traditional query processing involves a search for plans formed by applying algebraic operators on top of primitives representing access to relations in the input query. But many querying scenarios involve two interacting issues that complicate the search. On the one hand, the search space may be limited by access restrictions associated with the interfaces to datasources, which require certain parameters to be given as inputs. On the other hand, the search space may be extended through the presence of integrity constraints that relate sources to each other, allowing for plans that do not match the structure of the user query. In this paper we present the first optimization approach that attacks both these difficulties within a single framework, presenting a system in which classical cost-based join optimization is extended to support both access-restrictions and constraints. Instead of iteratively exploring subqueries of the input query, our optimizer explores a space of proofs that witness the answering of the query, where each proof has a direct correspondence with a query plan.

We study verification of systems whose transitions consist of accesses to a Web-based data source . An access is a lookup on a relation within a relational database, fixing values for a set of positions in the relation. For example, a transition can represent access to a Web form, where the user is restricted to filling in values for a particular set of fields. We look at verifying properties of a schema describing the possible accesses of such a system. We present a language where one can describe the properties of an access path and also specify additional restrictions on accesses that are enforced by the schema. Our main property language, AccessLTL, is based on a first-order extension of linear-time temporal logic, interpreting access paths as sequences of relational structures. We also present a lower-level automaton model, A-automata, into which AccessLTL specifications can compile. We show that AccessLTL and A-automata can express static analysis problems related to “querying with limited access patterns” that have been studied in the database literature in the past, such as whether an access is relevant to answering a query and whether two queries are equivalent in the accessible data they can return. We prove decidability and complexity results for several restrictions and variants of AccessLTL and explain which properties of paths can be expressed in each restriction.

We look at generating plans that answer queries over restricted interfaces, making use of information about source integrity constraints, access restrictions, and access costs. Our method can exploit the integrity constraints to find low-cost access plans even when there is no direct access to relations appearing in the query. The key idea of our method is to move from a search for a plan to a search for a proof that a query is answerable, and then \emph{generate a plan from a proof}. Discovery of one proof allows us to find a single plan that answers the query; exploration of several alternative proofs allows us to find low-cost plans. We start by overviewing a correspondence between proofs and restricted-interface plans in the context of arbitrary first-order constraints, based on interpolation. The correspondence clarifies the connection between preservation and interpolation theorems and reformulation problems, while generalizing it in several dimensions. We then provide direct plan-generation algorithms for schemas based on tuple-generating dependencies. Finally, we show how the direct plan-generation approach can be adapted to take into account the cost of plans.

The data needed to answer queries is often available through Web-based APIs. Indeed, for a given query there may be many Web-based sources which can be used to answer it, with the sources overlapping in their vocabularies, and differing in their access restrictions (required arguments) and cost. We introduce PDQ (Proof-Driven Query Answering), a system for determining a query plan in the presence of web-based sources. It is: (i) constraint-aware -- exploiting relationships between sources to rewrite an expensive query into a cheaper one, (ii) access-aware -- abiding by any access restrictions known in the sources, and (iii) cost-aware -- making use of any cost information that is available about services. PDQ takes the novel approach of generating query plans from proofs that a query is answerable. We demonstrate the use of PDQ and its effectiveness in generating low-cost plans.

We consider which queries are answerable in the presence of access restrictions and integrity constraints, and which portions of the schema are accessible in the presence of access restrictions and constraints. Unlike prior work, we focus on integrity constraint languages that subsume inclusion dependencies. We also use a semantic definition of answerability: a query is answerable if the accessible information is sufficient to determine its truth value. We show that answerability is decidable for the class of guarded dependencies, which includes all inclusion dependencies, and also for constraints given in the guarded fragment of first-order logic. We also show that answerable queries have "query plans" in a restricted language. We give corresponding results for extractability of portions of the schema. Our results relate querying with limited access patterns, determinacy-vs-rewriting, and analysis of guarded constraints.

Given two pushdown automata, the bisimilarity problem asks whether the infinite transition systems they induce are bisimilar. While this problem is known to be decidable our main result states that it is nonelementary, improving EXPTIME-hardness, which was the best previously known lower bound for this problem. Our lower bound result holds for normed pushdown automata as well.

No abstract available.

Named entity extractors can be used to enrich both text and Web documents with semantic annotations. While originally focused on a few standard entity types, the ecosystem of annotators is becoming increasingly diverse, with recognition capabilities ranging from generic to specialised entity types. Both the overlap and the diversity in annotator vocabularies motivate the need for managing and integrating semantic annotations: allowing users to see the results of multiple annotations and to merge them into a unified solution. We demonstrate ROSEANN, a system for the management of semantic annotations. ROSEANN provides users with a unified view over the opinion of multiple independent annotators both on text and Web documents. It allows users to understand and reconcile conflicts between annotations via ontology-aware aggregation. ROSEANN incorporates both supervised aggregation, appropriate when representative training data is available, and an unsupervised method based on the notion of weighted-repair.

A growing number of resources are available for enriching documents with semantic annotations. While originally focused on a few standard classes of annotations, the ecosystem of annotators is now becoming increasingly diverse. Although annotators often have very different vocabularies, with both high-level and specialist concepts, they also have many semantic interconnections. We will show that both the overlap and the diversity in annotator vocabularies motivate the need for semantic annotation integration: middleware that produces a unified annotation on top of diverse semantic annotators. On the one hand, the diversity of vocabulary allows applications to benefit from the much richer vocabulary available in an integrated vocabulary. On the other hand, we present evidence that the most widely-used annotators on the web suffer from serious accuracy deficiencies: the overlap in vocabularies from individual annotators allows an integrated annotator to boost accuracy by exploiting inter-annotator agreement and disagreement. The integration of semantic annotations leads to new challenges, both compared to usual data integration scenarios and to standard aggregation of machine learning tools. We overview an approach to these challenges that performs ontology-aware aggregation. We introduce an approach that requires no training data, making use of ideas from database repair. We experimentally compare this with a supervised approach, which adapts maximal entropy Markov models to the setting of ontology-based annotations. We further experimentally compare both these approaches with respect to ontology-unaware supervised approaches, and to individual annotators.

An increasing number of systems provide the ability to semantically annotate documents. OpenCalais [4], Evri API [2], Zemanta [6], and Alchemy API [1] are web-hosted systems that return annotated documents, i. e. documents with annotations that are overlayed on the document structure. Many of the annotations can be linked to standard ontologies, such as DBpedia and YAGO. These annotations give insight as to the meaning of documents in a variety of ways, identifying entities and relationships inside them, classifying them according to topic or theme, and giving the attitude or sentiment of a document or document fragment. In order for users (or applications) to make use of these annotations with a means to access and manipulate documents that contain them, we provide a query language for doing this and demonstrate its utility on a demo system built on top of diverse semantic annotators and external ontologies. We explain how integrating semantic annotations and utilizing external knowledge helps in increasing the quality of query answers over annotated documents by both filtering out irrelevant answers and obtaining extra answers that are not explicitly available in the annotated documents.

We study verification of systems whose transitions consist of accesses to a Web-based data-source . An access is a lookup on a relation within a relational database, fixing values for a set of positions in the relation. For example, a transition can represent access to a Web form, where the user is restricted to filling in values for a particular set of fields. We look at verifying properties of a schema describing the possible accesses of such a system. We present a language where one can describe the properties of an access path, and also specify additional restrictions on accesses that are enforced by the schema. Our main property language, AccLTL, is based on a first-order extension of linear-time temporal logic, interpreting access paths as sequences of relational structures. We also present a lower-level automaton model, A-automata, which AccLTL specifications can compile into. We show that AccLTL and A-automata can express static analysis problems related to "querying with limited access patterns" that have been studied in the database literature in the past, such as whether an access is relevant to answering a query, and whether two queries are equivalent in the accessible data they can return. We prove decidability and complexity results for several restrictions and variants of AccLTL, and explain which properties of paths can be expressed in each restriction.

While relational algebra and calculus are a well-established foundation for classical database query languages, it is less clear what the analog is for higher-order functions, such as query transformations. Here we study a natural way to add higher-order functionality to query languages, by adding database query operators to the λ-calculus as constants. This framework, which we refer to as λ-embedded query languages, was introduced in [BPV10]. That work had a restricted focus: the containment and equivalence problems for query-to-query functions, in the case where only positive relational operators are allowed as constants. In this work we take an in-depth look at the most basic issue for such languages: the evaluation problem. We give a full picture of the complexity of evaluation for λ-embedded query languages, looking at a number of variations: with negation and without; with only relational algebra operators, and also with a recursion mechanism in the form of a query iteration operator; in a strongly-typed calculus as well as a weakly-typed one. We give tight bounds on both the combined complexity and the query complexity of evaluation in all these settings, in the process explaining connections with Datalog and prior work on λ-calculus evaluation.

What do you do if a computational object (e.g. program trace) fails a specification? An obvious approach is to perform repair: modify the object minimally to get something that satisfies the constraints. In this paper we study repair of temporal constraints, given as automata or temporal logic formulas. We focus on determining the number of repairs that must be applied to a word satisfying a given input constraint in order to ensure that it satisfies a given target constraint. This number may well be unbounded; one of our main contributions is to isolate the complexity of the "bounded repair problem", based on a characterization of the pairs of regular languages that admit such a repair. We consider this in the setting where the repair strategy is unconstrained and also when the strategy is restricted to use finite memory. Although the streaming setting is quite different from the general setting, we find that there are surprising connections between streaming and non-streaming, as well as within variants of the streaming problem.

Consider the situation where a query is to be answered using Web sources that restrict the accesses that can be made on backend relational data by requiring some attributes to be given as input of the service. The accesses provide lookups on the collection of attributes values that match the binding. They can differ in whether or not they require arguments to be generated from prior accesses. Prior work has focused on the question of whether a query can be answered using a set of data sources, and in developing static access plans (e.g., Datalog programs) that implement query answering. We are interested in dynamic aspects of the query answering problem: given partial information about the data, which accesses could provide relevant data for answering a given query? We consider immediate and long-term notions of "relevant accesses", and ascertain the complexity of query relevance, for both conjunctive queries and arbitrary positive queries. In the process, we relate dynamic relevance of an access to query containment under access limitations and characterize the complexity of this problem; we produce several complexity results about containment that are of interest by themselves.

We investigate a higher-order query language that embeds operators of the positive relational algebra within the simply-typed λ-calculus. Our language allows one to succinctly define ordinary positive relational algebra queries (conjunctive queries and unions of conjunctive queries) and, in addition, second-order query functionals, which allow the transformation of CQs and UCQs in a generic (i.e., syntax-independent) way. We investigate the equivalence and containment problems for this calculus, which subsumes traditional CQ/UCQ containment. Query functionals are said to be equivalent if the output queries are equivalent, for each possible input query, and similarly for containment. These notions of containment and equivalence depend on the class of (ordinary relational algebra) queries considered. We show that containment and equivalence are decidable when query variables are restricted to positive relational algebra and we identify the precise complexity of the problem. We also identify classes of functionals where containment is tractable. Finally, we provide upper bounds to the complexity of the containment problem when functionals act over other classes.

Independence analysis is the problem of determining whether an update affects the result of a query, e.g. a constraint or materialized view. We develop a new, modular framework for static independence analysis that decomposes the problem into two orthogonal subproblems: approximating the destabilizer , that is, a finite representation of the set of updates that can change the result of the query, and testing whether the update and destabilizer overlap via an intersection analysis. Focusing on XML queries as the view language and the XQuery Update Facility as the update language, we present a syntactic query rewriting algorithm for translating queries to destabilizers, and show that intersection checking can be reduced to satisfiability problems for which efficient checkers already exist. We present an implementation based on an expressive tree satisfiability checker and a Satisfiability Modulo Order package, and give experiments confirming that the resulting analysis is both fast and effective.

Virtual views are a mechanism that facilitates re-use and makes queries easier to express. However the use of iterative view definitions makes very simple query evaluation and analysis problems more complex. In this paper we study classical containment and equivalence problems for queries built up through simple unions of conjunctive queries and view definitions. More precisely, we determine the complexity of containment and equivalence for non-recursive Datalog. We show that the problem is much harder than its classical counterpart -- complete for co-NEXPTIME. We then show that this remains true even with restrictions on the schema and queries in place. Finally, we isolate subcases that are more tractable, ranging from NP to PSPACE.

We show how Recursive Markov Chains (RMCs) and their restrictions can define probabilistic distributions over XML documents, and study tractability of querying over such models. We show that RMCs subsume several existing probabilistic XML models. In contrast to the latter, RMC models (i) capture probabilistic versions of XML schema languages such as DTDs, (ii) can be exponentially more succinct, and (iii) do not restrict the domain of probability distributions to be finite. We investigate RMC models for which tractability can be achieved, and identify several tractable fragments that subsume known tractable probabilistic XML models. We then look at the space of models between existing probabilistic XML formalisms and RMCs, giving results on the expressiveness and succinctness of RMC subclasses, both with each other and with prior formalisms.

Marx and de Rijke have shown that the navigational core of the w3c XML query language XPath is not first-order complete -- that is it cannot express every query definable in firstorder logic over the navigational predicates. How can one extend XPath to get a first-order complete language? Marx has shown that Conditional XPath -- an extension of XPath with an "Until" operator -- is first order complete. The completeness argument makes essential use of the presence of upward axes in Conditional XPath. We examine whether it is possible to get "forward-only" languages that are first-order complete for XML Boolean queries. It is easy to see that a variant of the temporal logic CTL* is first-order complete; the variant has path quantifiers for downward, leftward and rightward paths, while along a path one can check arbitrary formulas of linear temporal logic (LTL). This language has two major disadvantages: it requires path quantification in both horizontal directions (in particular, it requires looking backward at the prior siblings of a node), and it requires the consideration of formulas of LTL of arbitrary complexity on vertical paths. This last is in contrast with Marx's Conditional XPath, which requires only the checking of a single Until operator on a path. We investigate whether either of these restrictions can be eliminated. Our main results are negative ones. We show that if we restrict our CTL* language by having an until operator in only one horizontal direction, then we lose completeness. We also show that no restriction to a "small" subset of LTL along vertical paths is sufficient for first order completeness. Smallness here means of bounded "Until Depth", a measure of complexity of LTL formulas defined by Etessami and Wilke. In particular, it follows from our work that Conditional XPath with only forward axes is not expressively complete; this extends results proved by Rabinovich and Maoz in the context of infinite unordered trees.

Abstract This work deals with the expressive power of logics on finite graphs with access to an additional “arbitrary” linear order. The queries that can be expressed this way are the order-invariant queries for the logic. For the standard logics used in computer science, such as first-order logic, it is known that access to an arbitrary linear order increases the expressiveness of the logic. However, when we look at the separating examples, we find that they have satisfying models whose Gaifman Graph is complex – unbounded in valence and in treewidth. We thus explore the expressiveness of order-invariant queries over well-behaved graphs. We prove that first-order order-invariant queries over strings and trees have no additional expressiveness over first-order logic in the original signature. We also prove new upper bounds on order-invariant queries over bounded treewidth and bounded valence graphs. Our results make use of a new technique of independent interest: the application of algebraic characterizations of definability to show collapse results.

Query-update independence analysis is the problem of determining whether an update affects the results of a query. Query-update independence is useful for avoiding recomputation of materialized views and may have applications to access control and concurrency control. This paper develops static analysis techniques for query-update independence problems involving core XQuery queries and updates with a snapshot semantics (based on the W3C XQuery Update Facility proposal). Our approach takes advantage of schema information, in contrast to previous work on this problem. We formalize our approach, sketch a proof of correctness, and report on the performance and accuracy of our implementation.

We consider regular languages of labeled trees. We give an effective characterization of the regular languages over such trees that are definable in first-order logic in the language of labeled graphs. These languages are the analog on trees of the “locally threshold testable” languages on strings. We show that this characterization yields a decision procedure for determining whether a regular tree language is first-order definable: The procedure is polynomial time in the minimal automaton presenting the regular language. We also provide an algorithm for deciding whether a regular language is definable in first-order logic supplemented with modular quantifiers.

Predicate logic has long been seen as a good foundation for querying relational data. This is embodied in the correspondence between relational calculus and first-order logic, and can also be seen in mappings from fragments of the standard relational query language SQL to extensions of first-order logic (e.g. with counting). A key question is what is the analog to this correspondence for querying tree-structured data, as seen, for example, in XML documents. We formalize this as the question of the appropriate logical query language for defining transformations on tree-structured data. The predominant practitioner paradigm for defining such transformations is top-down tree building . This is embodied by the XQuery query language, which builds the output tree in parallel starting at the root, based on variable bindings and nodeset queries in the XPath language. The goal of this article is to compare the expressiveness of top-down tree-building languages based on a benchmark of predicate logic. We start by giving a formalized XQuery XQ that can serve as a representative of the top-down approach. We show that all queries in XQ with only atomic equality are equivalent to first-order interpretations, an analog to first-order logic (FO) in the setting of transformations of tree-structured data. We then consider fragments of atomic XQ . We identify a fragment that maps efficiently into first-order, a fragment that maps into existential first-order logic, and a fragment that maps into the navigationally two-variable fragment of first-order logic—an analog of two-variable logic in the setting where data values are unbounded. When XQ is considered with deep equality, we find that queries can be translated into FO with counting ( FO (Cnt)). Translations from XQ to logical languages on relations have a number of consequences. We use them to derive complexity bounds for XQ fragments, and to bound the Boolean expressiveness of XQ fragments.

As XML-based messages have become common in many client-server protocols, there is a need to protect application servers from invalid or dangerous messages. This leads to the XML stream firewalling problem; that of applying integrity constraints against a large number of simultaneous streams. We conduct the first investigation of a constraint engine optimized for the generation of XML stream firewalls. We isolate a class of DTDs and XPath constraints which support the generation of low-space filters, and provide algorithms for generating firewalls with low per-input-character time and per-stream space. We give experimental results which show that we have achieved these goals in practice.

We study the satisfiability problem associated with XPath in the presence of DTDs. This is the problem of determining, given a query p in an XPath fragment and a DTD D , whether or not there exists an XML document T such that T conforms to D and the answer of p on T is nonempty. We consider a variety of XPath fragments widely used in practice, and investigate the impact of different XPath operators on the satisfiability analysis. We first study the problem for negation-free XPath fragments with and without upward axes, recursion and data-value joins, identifying which factors lead to tractability and which to NP-completeness. We then turn to fragments with negation but without data values, establishing lower and upper bounds in the absence and in the presence of upward modalities and recursion. We show that with negation the complexity ranges from PSPACE to EXPTIME. Moreover, when both data values and negation are in place, we find that the complexity ranges from NEXPTIME to undecidable. Furthermore, we give a finer analysis of the problem for particular classes of DTDs, exploring the impact of various DTD constructs, identifying tractable cases, as well as providing the complexity in the query size alone. Finally, we investigate the problem for XPath fragments with sibling axes, exploring the impact of horizontal modalities on the satisfiability analysis.

The popularity of collaborative tagging sites presents a unique opportunity to explore keyword search in a context where query results are determined by the opinion of a network of taggers related to a seeker. In this paper, we present the first in-depth study of network-aware search. We investigate efficient top- k processing when the score of an answer is computed as its popularity among members of a seeker's network. We argue that obvious adaptations of top- k algorithms are too space-intensive, due to the dependence of scores on the seeker's network. We therefore develop algorithms based on maintaining score upper-bounds. The global upper-bound approach maintains a single score upper-bound for every pair of item and tag, over the entire collection of users. The resulting bounds are very coarse. We thus investigate clustering seekers based on similar behavior of their networks. We show that finding the optimal clustering of seekers is intractable, but we provide heuristic methods that give substantial time improvements. We then give an optimization that can benefit smaller populations of seekers based on clustering of taggers. Our results are supported by extensive experiments on del.icio.us datasets.

We study relations on trees defined by first-order constraints over a vocabulary that includes the tree extension relation T ≺ T ′ (holding if and only if every branch of T extends to a branch of T ′), unary node-tests, and a binary relation checking whether the domains of two trees are equal. We consider both ranked and unranked trees. These are trees with and without a restriction on the number of children of nodes. We adopt the model-theoretic approach to tree relations and study relations definable over the structure consisting of the set of all trees and the aforementioned predicates. We relate definability of sets and relations of trees to computability by tree automata. We show that some natural restrictions correspond to familiar logics in the more classical setting where every tree is a structure over a fixed vocabulary, and to logics studied in the context of XML pattern languages. We then look at relational calculi over collections of trees, and obtain quantifier-restriction results that give us bounds on the expressive power and complexity. As unrestricted relational calculi can express problems that are complete for each level of the polynomial hierarchy, we look at their restrictions, corresponding to the restricted logics over the family of all unranked trees, and find several calculi with low (NC 1 ) data complexity which still express properties important for database and document applications. We also give normal forms for safe queries in the calculus.

Planar spatial datasets can be modeled by closed semi-algebraic sets in the plane. We establish a characterization of the topological properties of such datasets expressible in the relational calculus with real polynomial constraints. The characterization is in the form of a query language that can only point that can only talk about points in the set and the “cones” around these points.

Most of the functionality of modern telecommunication systems has migrated to software, and much of that software consists of code for manipulating data: data describing either subscriber features or equipment configuration. The data is generally hierarchically structured but extremely complex - it consists of hundreds or even thousands of "classes" (roughly speaking, distinct labels on a tree), with the same information occurring in different formats across many classes in a hierarchy. The data is also required to satisfy a gigantic number of integrity constraints, vital to the correct routing of phone calls. The challenge is to create tools for populating this data, updating the data, and propagating these updates to derived data; all without violating these integrity constraints. The aim of this article is to give an overview of recent projects at Bell Labs that tackle this problem. Declarative languages play a key role. Indeed, we can think of a solution as consisting of languages for: the integrity constraints, the large-scale changes to the data, and the relationships between base data and derived data. In this article the author starts by explaining the languages used, and the key algorithmic ideas behind the tools. Generally these tools can all be seen as "implementations" of closure properties of definable tree and tree-structured data languages. The author then discusses briefly some of the pragmatic issues in getting these systems used in industrial projects.

We study the satisfiability problem associated with XPath in the presence of DTDs. This is the problem of determining, given a query p in an XPath fragment and a DTD D, whether or not there exists an XML document T such that T conforms to D and the answer of p on T is nonempty. We consider a variety of XPath fragments widely used in practice, and investigate the impact of different XPath operators on satisfiability analysis. We first study the problem for negation-free XPath fragments with and without upward axes, recursion and data-value joins, identifying which factors lead to tractability and which to NP-completeness. We then turn to fragments with negation but without data values, establishing lower and upper bounds in the absence and in the presence of upward modalities and recursion. We show that with negation the complexity ranges from PSPACE to EXPTIME. Moreover, when both data values and negation are in place, we find that the complexity ranges from NEXPTIME to undecidable. Finally, we give a finer analysis of the problem for particular classes of DTDs, exploring the impact of various DTD constructs, identifying tractable cases, as well as providing the complexity in the query size alone.

Recursive state machines (RSMs) enhance the power of ordinary state machines by allowing vertices to correspond either to ordinary states or to potentially recursive invocations of other state machines. RSMs can model the control flow in sequential imperative programs containing recursive procedure calls. They can be viewed as a visual notation extending Statecharts-like hierarchical state machines, where concurrency is disallowed but recursion is allowed. They are also related to various models of pushdown systems studied in the verification and program analysis communities.After introducing RSMs and comparing their expressiveness with other models, we focus on whether verification can be efficiently performed for RSMs. Our first goal is to examine the verification of linear time properties of RSMs. We begin this study by dealing with two key components for algorithmic analysis and model checking, namely, reachability (Is a target state reachable from initial states?) and cycle detection (Is there a reachable cycle containing an accepting state?). We show that both these problems can be solved in time O ( n θ 2 ) and space O ( n θ), where n is the size of the recursive machine and θ is the maximum, over all component state machines, of the minimum of the number of entries and the number of exits of each component. From this, we easily derive algorithms for linear time temporal logic model checking with the same complexity in the model. We then turn to properties in the branching time logic CTL*, and again demonstrate a bound linear in the size of the state machine, but only for the case of RSMs with a single exit node.

Closed semi-algebraic sets in the plane form a powerful model of planar spatial datasets. We establish a characterization of the topological properties of such datasets expressible in the relational calculus with real polynomial constraints. The characterization is in the form of a query language that can only talk about points in the set and the "cones" around these points.

The emerging paradigm of electronic services promises to bring to distributed computation and services the flexibility that the web has brought to the sharing of documents. An understanding of fundamental properties of e-service composition is required in order to take full advantage of the paradigm. This paper examines proposals and standards for e-services from the perspectives of XML, data management, workflow, and process models. Key areas for study are identified, including behavioral service signatures, verification and synthesis techniques for composite services, analysis of service data manipulation commands, and XML analysis applied to service specifications. We give a sample of the relevant results and techniques in each of these areas.

We propose a framework for integrating data from multiple relational sources into an XML document that both conforms to a given DTD and satisfies predefined XML constraints. The framework is based on a specification language, AIG, that extends a DTD by (1) associating element types with semantic attributes (inherited and synthesized, inspired by the corresponding notions from Attribute Grammars), (2) computing these attributes via parameterized SQL queries over multiple data sources, and (3) incorporating XML keys and inclusion constraints. The novelty of AIG consists in semantic attributes and their dependency relations for controlling context-dependent, DTD-directed construction of XML documents, as well as for checking XML constraints in parallel with document-generation. We also present cost-based optimization techniques for efficiently evaluating AIGs, including algorithms for merging queries and for scheduling queries on multiple data sources. This provides a new grammar-based approach for data integration under both syntactic and semantic constraints.

We study analogs of classical relational calculus in the context of strings. We start by studying string logics. Taking a classical model-theoretic approach, we fix a set of string operations and look at the resulting collection of definable relations. These form an algebra---a class ofn-ary relations for everyn, closed under projection and Boolean operations. We show that by choosing the string vocabulary carefully, we get string logics that have desirable properties: computable evaluation and normal forms. We identify five distinct models and study the differences in their model-theory and complexity of evaluation. We identify a subset of these models that have additional attractive properties, such as finite VC dimension and quantifier elimination.Once you have a logic, the addition of free predicate symbols gives you a string query language. The resulting languages have attractive closure properties from a database point of view: while SQL does not allow the full composition of string pattern-matching expressions with relational operators, these logics yield compositional query languages that can capture common string-matching queries while remaining tractable. For each of the logics studied in the first part of the article, we study properties of the corresponding query languages. We give bounds on the data complexity of queries, extend the normal form results from logics to queries, and show that the languages have corresponding algebras expressing safe queries.

Abstract We settle a number of questions concerning definability in first order logic with an extra predicate symbol ranging over semi-linear sets. We give new results both on the positive and negative side: we show that in first-order logic one cannot query a semi-linear set as to whether or not it contains a line, or whether or not it contains the line segment between two given points. However, we show that some of these queries become definable if one makes small restrictions on the semi-linear sets considered.

We study relations on trees defined by first-order constraints over a vocabulary that includes the tree extension relation T

We study algebras of definable string relations, classes of regular n-ary relations that arise as the definable sets within a model whose carrier is the set of all strings. We show that the largest such algebra-the collection of regular relations-has some quite undesirable computational and model-theoretic properties. In contrast, we exhibit several definable relation algebras that have much tamer behavior: for example, they admit quantifier elimination, and have finite VC dimension. We show that the properties of a definable relation algebra are not at all determined by the one-dimensional definable sets. We give models whose definable sets are all star-free, but whose binary relations are quite complex, as well as models whose definable sets include all regular sets, but which are much more restricted and tractable than the full algebra of regular relations.

We study relational calculi with support for string operations. While SQL restricts the ability to mix string pattern-matching and relational operations, prior proposals for embedding SQL in a compositional calculus were based on adding the operation of concatenation to first-order logic. These latter proposals yield compositional query languages extending SQL, but are unfortunately computationally complete. The unbounded expressive power in turn implies strong limits on the ability to perform optimization and static analysis of properties such as query safety in these languages.

It is known that standard query languages for constraint databases lack the power to express connectivity properties. Such properties are important in the context of geographical databases, where one naturally wishes to ask queries about connectivity (what are the connected components of a given set?) or reachability (is there a path from A to B that lies entirely in a given region?). No existing constraint query languages that allow closed form evaluation can express these properties.

We rework parts of the classical relational theory when the underlying domain is a structure with some interpreted operations that can be used in queries. We identify parts of the classical theory that go through 'as before' when interpreted structure is present, parts that go through only for classes of nicely behaved structures, and parts that only arise in the interpreted case. The first category include a number of results on language equivalence and expressive power characterizations for the active-domain semantics for a variety of logics. Under this semantics, quantifiers range over elements of a relational database. The main kind of results we prove here are generic collapse results: for generic queries, adding operations beyond order, does not give us extra power. The second category includes results on the natural semantics, under which quantifiers range over the entire interpreted structure. We prove, for a variety of structures, natural-active collapse results, showing that using unrestricted quantification does not give us any extra power. Moreover, for a variety of structures, including the real field, we give a set of algorithms for eliminating unbounded quantifications in favor of bounded ones. Furthermore, we extend these collapse results to a new class of higher-order logics that mix unbounded and bounded quantification. We give a set of normal forms for these logics, under special conditions on the interpreted structures. As a by-product, we obtain an elementary proof of the fact that parity test is not definable in the relational calculus with polynomial inequality constraints. We also give examples of structures with nice model-theoretic properties over which the natural-active collapse fails.

We extend some of the classical characterization theorems of relational database theory---particularly those related to query safety---to the context where database elements come with fixed interpreted structure and where formulae over elements of that structure can be used in queries. We show that the addition of common interpreted functions, such as real addition and multiplication, to the relational calculus preserves important characterization theorems of the relational calculus and also preserves certain combinatorial properties of queries. Our main result of the first kind is that there is a syntactic characterization of the collection of safe queries over the relational calculus supplemented by a wide class of interpreted functions---a class that includes addition, multiplication, and exponentiation---and that this characterization gives us an interpreted analog of the concept of range-restricted query from the uninterpreted setting. Furthermore, our range-restricted queries are particularly intuitive for the relational calculus with real arithmetic and give a natural syntax for safe queries in the presence of polynomial functions. We use these characterizations to show that safety is decidable for Boolean combinations of conjunctive queries for a large class of interpreted structures. We show a dichotomy theorem that sets a polynomial bound on the growth of the output of a query that might refer to addition, multiplication, and exponentiation. We apply the above results for finite databases to get results on constraint databases representing potentially infinite objects. We start by getting syntactic characterizations of the queries on constraint databases that preserve geometric conditions in the constraint data model. We consider classes of convex polytopes, polyhedra, and compact semilinear sets, the latter corresponding to many spatial applications. We show how to give an effective syntax to safe queries and prove that for conjunctive queries the preservation properties are decidable.

libkinQbell-

We extend bounds on the expressive power of first-order logic over finite structures and over ordered finite structures, by generalizing to the situation where the finite structures are embedded in an infinite structure M, where M satisfies some simple combinatorial properties studied in model-theoretic stability theory. We first consider first-order logic over finite structures embedded in a stable structure, and show that it has the same generic expressive power as first-order logic on unordered finite structures. It follows from this that having the additional structure of, for example, an abelian group or an equivalence relation, does not allow one to define any new generic queries. We also consider first-order logic over finite structures living within any model M that lacks the independence property and show that its expressive power is bounded by first-order logic over finite ordered structures. This latter result gives an enormous class of structures in which the expressive power of first-order logic is sharply limited; it shows that common queries such as parity and connectivity cannot be defined for finite structures living within structures from this huge class. It also gives a pure combinatorial property of an interpreted structure M that is sufficient to extend results on first-order logic on ordered structures to first-order logic on finite structures embedded in M.

We extend some of the classical characterization theorems of relational database theory | par-ticularly those related to query safety | to the context where database elements come with xed interpreted structure, and where formulae over elements of that structure can be used in queries. We show that the addition of common interpreted functions such as real addition and multiplication to the relational calculus preserves important characterization theorems of the relational calculus, and also preserves certain combinatorial properties of queries. Our main result of the rst kind is that there is a syntactic characterization of the collection of safe queries over the relational calculus supplemented by a wide class of interpreted functions | a class that includes addition, multipli-cation, and exponentiation | and that this characterization gives us an interpreted analog of the concept of range-restricted query from the uninterpreted setting. Furthermore, our range-restricted queries are particularly intuitive for the relational calculus with real arithmetic, and give a natural syntax for safe queries in the presence of polynomial functions. We use these characterizations to show that safety is decidable for Boolean combinations of conjunctive queries for a large class of interpreted structures. We show a dichotomy theorem that sets a polynomial bound on the growth of the output of a query that might refer to addition, multiplication and exponentiation. We apply the above results for nite databases to get results on constraint databases, represent-ing potentially innite objects. We start by getting syntactic characterizations of the queries on constraint databases that preserve geometric conditions in the constraint data model. We consider classes of convex polytopes, polyhedra, and compact semi-linear sets, the latter corresponding to many spatial applications. We show how to give an eective syntax to safe queries, and prove that for conjunctive queries the preservation properties are decidable. 1

The expressive power of first-order query languages with several classes of equality and inequality constraints is studied in this paper. We settle the conjecture that recursive queries such as parity test and transitive closure cannot be expressed in the relational calculus augmented with polynomial inequality constraints over the reals. Furthermore, noting that relational queries exhibit several forms of genericity, we establish a number of collapse results of the following form: The class of generic Boolean queries expressible in the relational calculus augmented with a given class of constraints coincides with the class of queries expressible in the relational calculus (with or without an order relation). We prove such results for both the natural and active-domain semantics. As a consequence, the relational calculus augmented with polynomial inequalities expresses the same classes of generic Boolean queries under both the natural and active-domain semantics. In the course of proving these results for the active-domin semantics, we establish Ramsey-type theorems saying that any query involving certain kinds of constraints coincides with a constraint-free query on databases whose elements come from a certain infinite subset of the domain. To prove the collapse results for the natural semantics, we make use of techniques from nonstandard analysis and from the model theory of ordered structures.

Abstract We study classes of ultrafilters on ω defined by a natural property of the Loeb measure in the Nonstandard Universe corresponding to the ultrafilter. This class, the Property M ultrafilters, is shown to contain all ultrafilters built up by taking iterated products over collections of pairwise nonisomorphic selective ultrafilters. Results on Property M ultrafilters are applied to the construction of extensions of probability measures, and to the study of measurable reductions between ultrafilters.

We rework parts of the classical relational theory when the underlying domain is a structure with some interpreted operations that can be used in queries.We identify parts of the classical theory that go through 'as before' when interpreted structure is present, parts that go through only for classes of nicely-behaved structures, and parts that only arise in the interpreted case.The first category includes a number of results on equivalence of query languages, as well as expressive power characterizations for the active-domain semantics for a variety of logics.The second category includes most of our results on the natural semantics, including results on cases where the natural semantics collapses to the active semantics.While these collapse results have been proved by nonconstructive means for first-order logic in previous work, we here give a set of algorithms for eliminating unbounded quantifications in favor of bounded ones.Furthermore, we show these results for a new class of higher-order logics that mix unbounded and bounded quantification.We give a set of normal forms for these lo&s, under special conditions on the interpreted structures.As a by-product, we obtain an elementary proof of the fact that parity test is not definable in the relational calculus with polynomial inequality constraints.

We study the structure of first-order and second-order queries over constraint databases. Constraint databases are formally modeled as finite relational structures embedded in some fixed infinite structure. We concentrate on problems of elimination of constraints, reducing quantification range to the active domain of the database and obtaining new complexity bounds. We show that for a large class of signatures, including real arithmetic constraints, unbounded quantification can be eliminated. That is, one can transform a sentence containing unrestricted quantification over the infinite universe to get an equivalent sentence in which quantifiers range over the finite relational structure. We use this result to get a new complexity upper bound on the evaluation of real arithmetic constraints. We also expand upon techniques for getting upper bounds on the expressiveness of constraint query languages, and apply it to a number of first-order and second-order query languages.

The expressive power of first-order query languages with several classes of equality and inequality constraints is studied in this paper. We settle the conjecture that recursive queries such as parity test and transitive closure cannot be expressed in the relational calculus augmented with polynomial inequality constraints over the reals. Furthermore, noting that relational queries exhibit several forms of genericity, we establish a number of collapse results of the following form: The class of generic Boolean queries expressible in the relational calculus augmented with a given class of constraints coincides with the class of queries expressible in the relational calculus (with or without an order relation). We prove such results for both the natural and active-domain semantics. As a consequence, the relational calculus augmented with polynomial inequalities expresses the same classes of generic Boolean queries under both the natural and active-domain semantics.In the course of proving these results for the active-domin semantics, we establish Ramsey-type theorems saying that any query involving certain kinds of constraints coincides with a constraint-free query on databases whose elements come from a certain infinite subset of the domain. To prove the collapse results for the natural semantics, we make use of techniques from nonstandard analysis and from the model theory of ordered structures.

Article Free Access Share on Verifiable properties of database transactions Authors: Michael Benedikt Bell Laboratories, 600 Mountain Avenue, Murray Hill NJ Bell Laboratories, 600 Mountain Avenue, Murray Hill NJView Profile , Timothy Griffin Bell Laboratories, 600 Mountain Avenue, Murray Hill NJ Bell Laboratories, 600 Mountain Avenue, Murray Hill NJView Profile , Leonid Libkin Bell Laboratories, 600 Mountain Avenue, Murray Hill NJ Bell Laboratories, 600 Mountain Avenue, Murray Hill NJView Profile Authors Info & Claims PODS '96: Proceedings of the fifteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of database systemsJune 1996 Pages 117–127https://doi.org/10.1145/237661.237692Published:03 June 1996Publication History 18citation320DownloadsMetricsTotal Citations18Total Downloads320Last 12 Months16Last 6 weeks1 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF