Search

Data words assign to each position a letter from a finite alphabet and a data value from an infinite set. Introduced as an abstraction of paths in XML documents, they recently found applications in querying graph databases as well. Those are actively studied due to applications in such diverse areas as social networks, semantic web, and biological databases. Querying formalisms for graph databases are based on specifying paths conforming to some regular conditions, which led to a study of regular expressions for data words.Previously studied regular expressions for data words were either rather limited, or had the full expressiveness of register automata, at the expense of a quite unnatural and unintuitive binding mechanism for data values. Our goal is to introduce a natural extension of regular expressions with proper bindings for data values, similar to the notion of freeze quantifiers used in connection with temporal logics over data words, and to study both language-theoretic properties of the resulting class of languages of data words, and their applications in querying graph databases.

International audience; We survey results about static analysis of pattern-based queries over XML documents. These queries are analogs of conjunctive queries, their unions and Boolean combinations, in which tree patterns play the role of atomic formulae. As in the relational case, they can be viewed as both queries and incomplete documents, and thus static analysis problems can also be viewed as finding certain answers of queries over such documents. We look at satisfiability of patterns under schemas, containment of queries for various features of XML used in queries, finding certain answers, and applications of pattern-based queries in reasoning about schema mappings for data exchange.

Data trees serve as an abstraction of XML documents: in such trees, every node comes with a label from a finite alphabet, as well as a data value from an infinite set. Incomplete data trees model XML documents with incomplete information; they may include both structural incompleteness and incompleteness of data. Here we study two basic problems for incomplete data trees under typical constraints such as keys and foreign keys. The first problem is consistency of specifications of incomplete data trees. We show that many of recently established results on consistency of constraints and schema descriptions can be transferred to the consistency of incomplete tree specifications without any increase in complexity. After that we examine query answering over incomplete data trees under constraints, and show that tractable bounds can be recovered under key constraints, but are lost under foreign keys.

In data words, each position carries not only a letter form a finite alphabet, as the usual words do, but also a data value coming from an infinite domain. There has been a renewed interest in them due to applications in querying and reasoning about data models with complex structural properties, notably XML, and more recently, graph databases. Logical formalisms designed for querying such data often require concise and easily understandable presentations of regular languages over data words. Our goal, therefore, is to define and study regular expressions for data words. As the automaton model, we take register automata, which are a natural analog of NFAs for data words. We first equip standard regular expressions with limited memory, and show that they capture the class of data words defined by register automata. The complexity of the main decision problems for these expressions (nonemptiness, membership) also turns out to be the same as for register automata. We then look at a subclass of these regular expressions that can define many properties of interest in applications of data words, and show that the main decision problems can be solved efficiently for it.

We show that problems arising in static analysis of XML specifications and transformations can be dealt with using techniques similar to those developed for static analysis of programs. Many properties of interest in the XML context are related to navigation, and can be formulated in temporal logics for trees. We choose a logic that admits a simple single-exponential translation into unranked tree automata, in the spirit of the classical LTL-to-Buchi automata translation. Automata arising from this translation have a number of additional properties; in particular, they are convenient for reasoning about unary node-selecting queries, which are important in the XML context. We give two applications of such reasoning: one deals with a classical XML problem of reasoning about navigation in the presence of schemas, and the other relates to verifying security properties of XML views.

We consider the problem of recurrent reachability over infinite systems given by regular relations on words and trees, i.e, whether a given regular set of states can be reached infinitely often from a given initial state in the given transition system. Under the condition that the transitive closure of the transition relation is regular, we show that the problem is decidable, and the set of all initial states satisfying the property is regular. Moreover, our algorithm constructs an automaton for this set in polynomial time, assuming that a transducer of the transitive closure can be computed in poly-time. We then demonstrate that transition systems generated by pushdown systems, regular ground tree rewrite systems, and the well-known process algebra PA satisfy our condition and transducers for their transitive closures can be computed in poly-time. Our result also implies that model checking EF-logic extended by recurrent reachability predicate (EGF) over such systems is decidable.

Specifications of XML documents typically consist of typing information (e.g., a DTD), and integrity constraints. Just like relational schema specifications, not all are good - some are prone to redundancies and update anomalies. In the relational world we have a well-developed theory of data design (also known as normalization). A few definitions of XML normal forms have been proposed, but the main question is why a particular design is good. In the XML world, we still lack universally accepted query languages such as relational algebra, or update languages that let us reason about storage redundancies, lossless decompositions, and update anomalies. A better approach, therefore, is to come up with notions of good design based on the intrinsic properties of the model itself. We present such an approach, based on Shannon's information theory, and show how it applies to relational normal forms as well as to XML design, for both native and relational storage.

Nested words are a restriction of the class of visibly pushdown languages that provide a natural model of runs of programs with recursive procedure calls. The usual connection between monadic second-order logic (MSO) and automata extends from words to nested words and gives us a natural notion of regular languages of nested words. In this paper we look at some well-known aspects of regular languages - their characterization via fixed points, deterministic and alternating automata for them, and synchronization for defining regular relations - and extend them to nested words. We show that mu-calculus is as expressive as MSO over finite and infinite nested words, and the equivalence holds, more generally, for mu-calculus with past modalities evaluated in arbitrary positions in a word, not only in the first position. We introduce the notion of alternating automata for nested words, show that they are as expressive as the usual automata, and also prove that Muller automata can be determinized (unlike in the case of visibly pushdown languages). Finally we look at synchronization over nested words. We show that the usual letter-to-letter synchronization is completely incompatible with nested words (in the sense that even the weakest form of it leads to an undecidable formalism) and present an alternative form of synchronization that gives us decidable notions of regular relations.

Close relationships between XML navigation and temporal logics have been discovered recently, in particular between logics LTL and CTL* and XPath navigation, and between the μ-calculus and navigation based on regular expressions. This opened up the possibility of bringing model-checking techniques into the field of XML, as documents are naturally represented as labeled transition systems. Most known results of this kind, however, are limited to Boolean or unary queries, which are not always sufficient for complex querying tasks. Here we present a technique for combining temporal logics to capture n-ary XML queries expressible in two yardstick languages: FO and MSO. We show that by adding simple terms to the language, and combining a temporal logic for words together with a temporal logic for unary tree queries, one obtains logics that select arbitrary tuples of elements, and can thus be used as building blocks in complex query languages. We present general results on the expressiveness of such temporal logics, study their model-checking properties, and relate them to some common XML querying tasks.

Specifications of XML documents typically consist of typing information (for example, a DTD), and integrity constraints (for example, keys and foreign keys). We show that combining the two may lead to seemingly reasonable specifications that are nevertheless inconsistent: there is no XML document that both conforms to the DTD and satisfies the constraints. We then survey results on the complexity of consistency checking, and show that, depending on the classes of DTDs and constraints involved, it ranges from linear time to undecidable. Furthermore, we show that for some of the most common classes of specifications checking consistency is intractable.

In this chapter, we introduce finite variable logics: a unifying tool for studying fixed point logics. These logics use infinitary connectives already seen in Chap. 8, but here we impose a different restriction: each formula can use only finitely many variables. We show that fixed point logics LFP, IFP, and PFP can be embedded in such a finite variable logic. Furthermore, the finite variable logic is easier to study: it can be characterized by games, and this gives us bounds on the expressive power of fixed point logics; in particular, we show that without a linear ordering, they fail to capture complexity classes. We then study definability and ordering of types in finite variable logics, and use these techniques to relate separating complexity classes to separating sonic fixed point logics over unordered structures.

We continue dealing with extensions of first-order logic. We have seen that the expressive power of FO on finite structures is limited in a number of ways: it cannot express counting properties, nor is it capable of expressing properties that require iterative algorithms, as those typically violate locality.

In this final chapter, we briefly outline three different application areas of finite model theory. In mathematical logic, finite models are used as a tool for proving decidability results for satisfiability of FO sentences. In the area of temporal logics and verification, one analyzes the behavior of certain logics on some special finite structures (Kripke structures). And finally, it was recently discovered that many constraint satisfaction problems can be reduced to the existence of a homomorphism between two finite structures.

The goal of this chapter is to study the complexity of queries expressible in FO. We start with the general definition of different ways of measuring the complexity of a logic over finite structures: these are data, expression, and combined complexity. We then connect FO with Boolean circuits and establish some bounds on the data complexity. We also consider the issue of uniformity for a circuit model, and study it via logical definability. We then move to the combined complexity of FO, and show that it is much higher than the data complexity. Finally, we investigate an important subclass of FO queries — conjunctive queries — which play a central role in database theory.

Most logics we have seen so far are not well suited for expressing many tractable graph properties, such as graph connectivity, reachability, and so on. The limited expressiveness of FO and counting logics is due to the fact that they lack mechanisms for expressing fixed point computations. Other logics we have seen, such as MSO, ∃SO, and ∀SO, can express intractable graph properties.

In this chapter we introduce the technique of coding Turing machines in various logics. It is precisely this technique that gave rise to numerous applications of finite model theory in computational complexity. We start by proving the earliest such result, Trakhtenbrot’s theorem, stating that finite satisfiability is not decidable. For the proof of Trakhtenbrot’s theorem, we code Turing machines with no inputs. By a refinement of this technique, we code nondeterministic polynomial time Turing machines in existential second-order logic (∃SO), proving Fagin’s theorem stating that∃SO-definable properties of finite structures are precisely those whose complexity is NP.

We start this chapter by giving a few examples of inexpressibility proofs, using the standard model-theoretic machinery (compactness, the Lowenheim-Skolern theorem). We then show that this machinery is not generally applicable in the finite model theory context, and introduce the notion of Ehrenfeucht-Fraisse games for first-order logic. We prove the EhrenfeuchtFraisse theorem, characterizing the expressive power of FO via games, and introduce the notion of types, which will be central throughout the book.

We now move to extensions of first-order logic. In this chapter we introduce second-order logic, and consider its often used fragment, monadic second-order logic,or MSO, in which one can quantify over subsets of the universe. We study the expressive power of this logic over graphs, proving that its existential fragment expresses some NP-complete problems, but at the same time cannot express graph connectivity. Then we restrict our attention to strings and trees, and show that, over them, MSO captures regular string and tree languages. We explore the connection with automata to prove further definability and complexity results.

In this chapter we show that properties expressible in many logics are almost surely true or almost surely false; that is, either they hold for almost all structures, or they fail for almost all structures. This phenomenon is known as the zero-one law. We prove it for FO, fixed point logics, and L ∞ω ω . We shall also see that the “almost everywhere” behavior of logics is drastically different from their “everywhere” behavior. For example, while satisfiability in the finite is undecidable, it is decidable if a sentence is true in almost all finite models.

In finite model theory, we deal with logics over finite structures. In embedded finite model theory, we deal with logics over finite structures embedded into infinite ones.

Data description for XML usually comes in the form of a type specification (e.g., a DTD) together with integrity constraints. XML Schema allows one to mix DTD features with semantic information, such as keys and foreign keys. It was shown recently [2,7] that the interaction of DTDs with constraints may be rather nontrivial. In particular, testing if a general specification is consistent is undecidable, but for the most common case of single-attribute constraints it is NP-complete, and linear time if no foreign keys are present.However, XML Schema design did not adopt the form of constraints prevalent in the database literature, and slightly changed the semantics of keys, foreign keys, and unique constraints. In this paper we demonstrate the very costly effect of this slight change on the feasibility of consistency checking. In particular, all the known hardness results extend to the XML Schema case, but tractability results do not. We show that even without foreign keys, and with very simple DTD features, checking consistency of XML-Schema specifications is intractable.

It is a folk result in database theory that SQL cannot express recursive queries such as reachability; in fact, a new construct was added to SQL3 to overcome this limitation. However, the evidence for this claim is usually given in the form of a reference to a proof that relational algebra cannot express such queries. SQL, on the other hand, in all its implementations has three features that fundamentally distinguish it from relational algebra: namely, grouping, arithmetic operations, and aggregation. In the past few years, most questions about the additional power provided by these features have been answered. This paper surveys those results, and presents new simple and self-contained proofs of the main results on the expressive power of SQL. Somewhat surprisingly, tiny differences in the language definition affect the results in a dramatic way: under some very natural assumptions, it can be proved that SQL cannot define recursive queries, no matter what aggregate functions and arithmetic operations are allowed. But relaxing these assumptions just a tiny bit makes the problem of proving expressivity bounds for SQL as hard as some long-standing open problems in complexity theory.

We consider IES(SQL), the incremental evaluation system over an SQL-like language with grouping, arithmetics, and aggregation. We show that every second order query is in IES(SQL) and that there are PSPACE-complete queries in IES(SQL). We further show that every PSPACE query is in IES(SQL) augmented with a deterministic transitive closure operator. Lastly, we consider ordered databases and provide a complete analysis of a hierarchy on IES(SQL) defined with respect to arity-bounded auxiliary relations.

Whenever we have data represented by constraints (such as order, linear, polynomial, etc.), running time for many constraint processing algorithms can be considerably lowered if it is known that certain variables in those constraints are independent of each other. For example, when one deals with spatial and temporal databases given by constraints, the projection operation, which corresponds to quantifier elimination, is usually the costliest. Since the behavior of many quantifier elimination algorithms becomes worse as the dimension increases, eliminating certain variables from consideration helps speed up those algorithms. While these observations have been made in the literature, it remained unknown when the problem of testing if certain variables are independent is decidable, and how to construct efficiently a new representation of a constraint-set in which those variables do not appear together in the same atomic constraints. Here we answer this question. We first consider a general condition that gives us decidability of variable independence; this condition is stated in terms of model-theoretic properties of the structures corresponding to constraint classes. We then show that this condition covers the domains most relevant to spatial and temporal applications. For some of these domains, including linear and polynomial constraints over the reals, we provide a uniform decision procedure which gives us tractability, and present a polynomial-time algorithm for producing nice constraint representations.

As we have seen in the previous chapter, usual relational databases are just a special case of the constraint model; indeed, a tuple \(\vec a = ({a_1},...,{a_n})\) can be represented as a constraint \({c_{\vec a}}({x_1},...,{x_n}) \equiv {x_1} = {a_1} \wedge ... \wedge {x_n} = {a_n}\) in free variables x 1,..., x n . A relation \(R = \left\{ {\vec a,...,{{\vec a}_m}} \right\}\) is then represented by a formula \({c_R}({x_1},...,{x_n}) \equiv {c_{\vec a}} \vee \cdots \vee {c_{{{\vec a}_m}}}\) stating that the interpretation of a tuple (x 1 ,..., x n) must be among the \({\vec a_i}S.\) Consequently, constraint query languages, over a structure \(M = \left\langle {U,\Omega } \right\rangle \), can be considered as query languages over ordinary relational databases whose elements come from the set u. For example, FO + Lin and FO + Poly, the relational calculus with linear and polynomial constraints, can be considered as query languages over ordinary relational databases that store numbers.

The power of classical query languages is linked to the fact that they express a restricted class of declarative programs. The class of semantic objects expressible through queries in the relational calculus, for example, is limited in a number of ways: They have PTIME data complexity, and their expressiveness is well understood. Although relational calculus queries may not return finite results, a natural subclass of the relational calculus does; namely the class of range-restricted queries. This class gives guarantees of finite output, and is complete in this respect, capturing all relational calculus queries whose outputs are always finite, the safe queries.

Well-known theorems of Hanf's and Gaifman's establishing locality of first-order definable properties have been used in many applications. These theorems were recently generalized to other logics, which led to new applications in descriptive complexity and database theory. However, a logical characterization of local properties that correspond to Hanf's and Gaifman's theorems, is still lacking. Such a characterization only exists for structures of bounded valence. In this paper, we give logical characterizations of local properties behind Hanf's and Gaifman's theorems. We first deal with an infinitary logic with counting terms and quantifiers, that is known to capture Hanflocality on structures of bounded valence. We show that testing isomorphism of neighborhoods can be added to it without violating Hanflocality, while increasing its expressive power. We then show that adding local second-order quantification to it captures precisely all Hanf-local properties. To capture Gaifman-locality, one must also add a (potentially infinite) case statement. We further show that the hierarchy based on the number of variants in the case statement is strict.

Aggregation operators like COUNT, SUM, and AVG form an indispensable part of database query languages for the relational data model. As constraint query languages give a natural analog of relational calculus in the geometric context, a crucial question concerns how to extend standard aggregation constructs from the relational model to the geometric setting. This question has two components.

We survey recent results on logics with counting and their local properties. We first consider game-theoretic characterizations of first-order logic and its counting extensions provided by unary generalized quantifiers. We then study Gaifman's and Hanf's locality theorems, their connection with game characterizations, and examples of their usage in proving expressivity bounds for first-order logic and its extensions. We review the abstract notions of Gaifman's and Hanf's locality, and show how they are related. We also consider a closely related bounded degree property, and demonstrate its usefulness in proving expressivity bounds. We discuss two applications. One deals with proving lower bounds for the complexity class TC0. In particular, we use logical characterization of TC0 and locality theorems for first-order with counting quantifiers to provide lower bounds. We then explain how the notions of locality are used in database theory to prove that extensions of relational calculus with aggregate functions and grouping still lack the power to express fixpoint computation.

Most of work on partial information in databases asks which operations of standard languages, like relational algebra, can still be performed correctly in the presence of nulls. In this paper a different point of view is advocated. We believe that the semantics of partiality must be clearly understood and it should give us new design principles for languages for databases with partial information.

It is a folk result that relational algebra or calculus extended with aggregate functions cannot compute the transitive closure. However, proving folk results is sometimes a nontrivial task. In this paper, we tell the story of the work on expressive power of relational languages with aggregate functions. We also prove by far the most powerful result that describes the expressiveness of such languages. There are four main features of our result that distinguish it from previous ones: 1. It does not rely on any unproven assumptions, such as separation of complexity classes. 2. It establishes a general property of queries definable with the help of aggregate functions. This property can easily be applied to prove many expressiveness bounds. 3. The class of aggregate functions is much larger than any previously considered. 4. The proof is “non-syntactic.” That is, it does not depend on a specific syntax chosen for the language with aggregates.

We examine the power of incremental evaluation systems that use an SQL-like language for maintaining recursively-defined views. We show that recursive queries such as transitive closure, and “alternating paths” can be incrementally maintained in a nested relational language, when some auxiliary relations are allowed. In the presence of aggregate functions, even more queries can be maintained, for example, the “same generation” query. In contrast, it is still an open problem whether such queries are maintainable in relational calculus. We then restrict the language so that no nested relations are involved (but we keep the aggregate functions). Such a language captures the capability of most practical relational database systems. We prove that this restriction does not reduce the incremental computational power; that is, any query that can be maintained in a nested language with aggregates, is still maintainable using only fiat relations. We also show that one does not need auxiliary relations of arity more than 2. In particular, this implies that the recursive queries maintainable in the nested language with aggregates, can be also maintained in a practical relational database systems using auxiliary tables of arity at most 2. This is again in sharp contrast to maintenance in relational calculus, which admits a strict arity-based hierarchy.

This paper studies expressivity bounds for extensions of first-order logic with counting and unary quantifiers in the presence of relations of large degree. There are several motivations for this work. First, it is known that first-order logic with counting quantifiers captures uniform TC° over ordered structures. Thus, proving expressivity bounds for first-order with counting can be seen as an attempt to show TC° ⊂ ≠ DLOG using techniques of descriptive complexity. Second, the presence of auxiliary built-in relations (e.g., order, successor) is known to make a big impact on expressivity results in finite-model theory and database theory. Our goal is to extend techniques from “pure” setting to that of auxiliary relations.

The goal of this paper is to study tractable iteration mechanisms for bags. The presence of duplicates in bags prevents iteration mechanisms developed in the context of sets to be directly applied to bags without losing tractability. We study two constructs for controlling tractability of iteration over bags. The deflationary fixpoint construct keeps removing elements from a bag until a fixpoint is reached. The bounded fixpoint construct is an inflationary iteration mechanism that never exceeds some predefined bounding bag. We study these constructs in the context of a standard (nested) bag algebra. We show that the deflationary and bounded inflationary fixpoint constructs are equally expressive and strictly more expressive than their set-based counterparts. We also show that, unlike in the set case, the bag algebra with bounded fixpoint fails to capture all PTIME queries over databases with ordered domains. We then show that adding just one construct, which can be used to assign unique tags to duplicates, captures the class of all polynomial time queries over bags when a total ordering on the domain of atomic elements is available. Finally, we compare the expressive powers of the bag algebra and the nested relational algebra with aggregate functions in the presence of these fixpoint operators.

One source of partial information in databases is the need to combine information from several databases. Even if each database is complete for some “world”, the combined databases will not be, and answers to queries against such combined databases can only be approximated. In this paper we describe various situations in which a precise answer cannot be obtained for a query asked against multiple databases. Based on an analysis of these situations, we propose a classification of constructs that can be used to model approximations.

We describe a functional database language OR-SML for handling disjunctive information in database queries, its implementation in Standard ML [10], and its interface to HOL90. The core language has the power of the nested relational algebra, and it is augmented with or-sets which are used to deal with disjunctive information. Sets, or-sets and tuples can be freely combined to create objects, which gives the language a greater flexibility. We give an example of queries over the “database” of HOL90 theories which require disjunctive information and show how to use the language to answer these queries. Since the system is running on top of Standard ML and all database objects are values in the latter, the system benefits from combining a sophisticated query language with the full power of a programming language. The language has been implemented as an HOL90-loadable library of modules in Standard ML.

We describe a functional database language OR-SML for handling disjunctive information in database queries, and its implementation on top of Standard ML [12]. The core language has the power of the nested relational algebra, augmented by or-sets which are used to deal with disjunctive information. Sets, or-sets and tuples can be freely combined to create objects, which gives the language a greater flexibility. It is configurable by user-defined base types, and can be used independently or interfaced to other systems built in ML. We give examples of queries which require disjunctive information (such as querying incomplete or independent databases) and show how to use the language to answer these queries.

The problem of decomposing domains into sensible factors is addressed and solved for the case of dI-domains. A decomposition theorem is proved which allows the represention of a large subclass of dI-domains in a product of flat domains. Direct product decompositions of Scott-domains are studied separately.

We study an approach to relational databases which treats relations not as subsets of a Cartesian product but as subsets of some domain — a partially ordered space of descriptions. This approach permits generalizations of relations that admit null values and variants. In previous work it was shown how to define the notion of a relation scheme in such a setting. Here we provide a characterization of a scheme that is more general, and show that operations analogous to projection, selection and join retain the desired properties. Schemes also allow us to develop dependency theory for such generalized relations. An extension of this model is described which admits a set constructor and is therefore useful for the study of higher-order relations and their generalizations.

In this paper we present the semilattice-theoretical approach to the investigation of the relational datamodels. It is known that the poset of closures is a model of changing databases. We show that it is in fact a lattice isomorphic to the subsemilattice-lattice of free semilattice, and the arbitrary subsemilattice-lattices can be considered as a model of restrictedly changing databases. The properties of these lattices in the context of database problems are studied. We also discuss the separation and dimension problems and establish some estimates.