Walk logic as a framework for path query languages on graph databases

Motivated by the current interest in languages for expressing path queries to graph databases, this paper proposes to investigate Walk Logic (WL): the extension of first-order logic on finite graphs with the possibility to explicitly quantify over walks. WL can serve as a unifying framework for path query languages. To support this claim, WL is compared in expressive power with various established query languages for graphs, such as first-order logic extended with reachability; the monadic second-order logic of graphs; hybrid computation tree logic; and regular path queries. WL also serves as a framework to investigate the following natural questions: Is quantifying over walks more powerful than quantifying over paths (walks without repeating nodes) only? Is quantifying over infinite walks more powerful than quantifying over finite walks only? WL model checking is decidable, but determining the precise complexity remains an open problem.

Related papers:

title: Survey of graph database models
abstract: Graph database models can be defined as those in which data structures for the schema and instances are modeled as graphs or generalizations of them, and data manipulation is expressed by graph-oriented operations and type constructors. These models took off in the eighties and early nineties alongside object-oriented models. Their influence gradually died out with the emergence of other database models, in particular geographical, spatial, semistructured, and XML. Recently, the need to manage information with graph-like nature has reestablished the relevance of this area. The main objective of this survey is to present the work that has been conducted in the area of graph database modeling, concentrating on data structures, query languages, and integrity constraints.

title: Query languages for graph databases
abstract: Query languages for graph databases started to be investigated some 25 years ago. With much current data, such as linked data on the Web and social network data, being graph-structured, there has been a recent resurgence in interest in graph query languages. We provide a brief survey of many of the graph query languages that have been proposed, focussing on the core functionality provided in these languages. We also consider issues such as expressive power and the computational complexity of query evaluation.

title: Foundations of Databases
abstract: A. ANTECHAMBER. Database Systems. The Main Principles. Functionalities. Complexity and Diversity. Past and Future. Ties with This Book. Bibliographic Notes.  Some Basics. Languages, Computability, and Complexity. Basics from Logic. The Relational Model. The Structure of the Relational Model. Named versus Unnamed Perspectives. Notation. Bibliographic Notes.   Algebra and Calculus. The Relational Algebras. Nonrecursive Datalog with Negation. The Relational Calculus. Syntactic Restrictions for Domain Independence. Aggregate Functions.  Finite Representations of Infinite Databases. Bibliographic Notes. Exercises. Static Analysis and Optimization. Issues in Practical Query Optimization. Global Optimization. Static Analysis of the Relational Calculus. Computers with Acyclic Joins. Bibliographic Notes. Exercises. Notes on Practical Languages.  The Structured Query Language. Query-by-Example and Microsoft Access. Confronting the Real World. Bibliographic Notes. Exercises. C. CONSTRAINTS. Functional and Join Dependency.   Dependency in Isolation. Finite versus Infinite Implication. Nonaxiomatizability of fd's + ind's. Restricted Kinds of Inclusion Dependency. Bibliographic Notes. Exercises. A Larger Perspective. A Unifying Framework. The Chase revisited.  An Algebraic Perspective. Bibliographic Notes. Exercises.  Universal Relation Assumption. Bibliographic Notes. Exercises. D. DATALOG AND RECURSION. Datalog. Syntax of Datalog. Model-Theoretic Semantics. Fixpoint Semantics.   Evaluation of Datalog.  Datalog with Negation. Equivalence. Recursion in Practical Language. Bibliographic Notes. Exercises. Negation in Datalog. The Basic Problem. Stratified Semantics. Well-Founded Semantics. Expressive Power. Negation as Failure of Brief. Bibliographic Notes. Exercises. E. EXPRESSIVENESS AND COMPLEXITY. Sizing up Languages. Queries. Complexity of Queries. Languages and Complexity. Bibliographic Notes. Exercises. First Order, Fixpoint and While. Complexity of First-Order Queries. Expressiveness of First-Order Queries. Fixpoint and While Queries. The Impact of Order. Bibliographic Notes. Exercises. Highly Expressive Languages. While(N)-while with Arithmetic. While(new)-while with New Values. While(uty)-An Untyped Extension of while. Bibliographic Notes. Exercises. F. FINALE. Incomplete Information. Warm-Up. Weak Representation Systems.  The Complexity of Nulls. Other Approaches. Bibliographic Notes. Exercises. Complex Values. Complex Value Databases. The Algebra. The Caculas.  Equivalence Theorems. Fixpoint and Deduction. Expressive Power and Complexity. A Practicle Query Language for Complex Values. Bibliographic Notes. Exercises. Object Databases. Informal Presentation. Formal Definition of an OODB Model. Languages for OODB Queries.  Further Issues for OODB's. Bibliographic Notes. Exercises. Dynamic Aspects. Updated Languages. Transactional Schemas. Updating Views and Deductive Databases. Active Databases. Temporal Databases and Constraints. Bibliographic Notes. Exercises. Bibliography. Symbol Index. Index.

title: Finite model theory
abstract: Finite model theory has its origins in classical model theory but owes its systematic development to research from complexity theory. The text presents the main results of descriptive complexity theory, the connection between axiomatizability of classes of finite structures and their complexity with respect to time and space bounds. The logics that are important in this context include fixed point logics, transitive closure logics and also certain infinitary languages; their model theory is studied in detail. Other topics include DATALOG languages, quantifiers and oracles, 0-1 laws, and optimization and approximation problems. The book is written in such a way that the representative parts on the model theory and descriptive complexity theory may be read independently.

title: Elements of Finite Model Theory
abstract: Emphasizes the computer science aspects of the subject. Details applications in databases, complexity theory, and formal languages, as well as other branches of computer science.

title: Reachability and connectivity queries in constraint databases
abstract: 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.
In the first part of the paper, we show that in principle there is no obstacle to getting closed languages that can express connectivity and reachability queries. In fact, we show that adding any topological property to standard languages like FO + LIN and FO+POLY results in a closed language. In the second part of the paper, we look for tractable closed languages for expressing reachability and connectivity queries. We introduce path logic, which allows one to state properties of paths with respect to given regions. We show that it is closed, has polynomial time data complexity for linear and polynomial constraints, and can express a large number of reachability properties beyond simple connectivity. Query evaluation in the logic involves obtaining a discrete abstraction of a continuous path, and model-checking of temporal formulae on the discrete structure.

title: Two-variable logic on data words
abstract: In a data word each position carries a label from a finite alphabet and a data value from some infinite domain. This model has been already considered in the realm of semistructured data, timed automata, and extended temporal logics.
 This article shows that satisfiability for the two-variable fragment FO2(∼,<,+1) of first-order logic with data equality test ∼ is decidable over finite and infinite data words. Here +1 and < are the usual successor and order predicates, respectively. The satisfiability problem is shown to be at least as hard as reachability in Petri nets. Several extensions of the logic are considered; some remain decidable while some are undecidable.

title: Automata vs. Logics on Data Words
abstract: The relationship between automata and logics has been investigated since the 1960s. In particular, it was shown how to determine, given an automaton, whether or not it is definable in first-order logic with label tests and the order relation, and for first-order logic with the successor relation. In recent years, there has been much interest in languages over an infinite alphabet. Kaminski and Francez introduced a class of automata called finite memory automata (FMA), that represent a natural analog of finite state machines. A FMA can use, in addition to its control state, a (bounded) number of registers to store and compare values from the input word. The class of data languages recognized by FMA is incomparable with the class of data languages defined by firstorder formulas with the order relation and an additional binary relation for data equality. 
 
We first compare the expressive power of several variants of FMA with several data word logics. Then we consider the corresponding decision problem: given an automaton A and a logic, can the language recognized by A be defined in the logic? We show that it is undecidable for several variants of FMA, and then investigate the issue in detail for deterministic FMA. We show the problem is decidable for first-order logic with local data comparisons - an analog of first-order logic with successor. We also show instances of the problem for richer classes of first-order logic that are decidable.

title: Principles of model checking
abstract: Our growing dependence on increasingly complex computer and software systems necessitates the development of formalisms, techniques, and tools for assessing functional properties of these systems. One such technique that has emerged in the last twenty years is model checking, which systematically (and automatically) checks whether a model of a given system satisfies a desired property such as deadlock freedom, invariants, and request-response properties. This automated technique for verification and debugging has developed into a mature and widely used approach with many applications. Principles of Model Checking offers a comprehensive introduction to model checking that is not only a text suitable for classroom use but also a valuable reference for researchers and practitioners in the field. The book begins with the basic principles for modeling concurrent and communicating systems, introduces different classes of properties (including safety and liveness), presents the notion of fairness, and provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and theoretical nature.

title: Hybrid logics: characterization, interpolation and complexity
abstract: Hybrid languages are expansions of propositional modal languages which can refer to (or even quantify over) worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work (for example [BS98, BT98a, BT99]) has focussed on a more constrained system called H(↓, @). We show in detail that (↓, @) is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations (via a restricted notion of Ehrenfeucht-Fraïssé game, and an enriched notion of bisimulation) and a syntactic characterization (in terms of bounded formulas). The key result to emerge is that (↓, @) corresponds to the fragment of first-order logic which is invariant for generated submodels. We then show that (↓, @) enjoys (strong) interpolation, provide counterexamples for its finite variable fragments, and show that weak interpolation holds for the sublanguage (@). Finally, we provide complexity results for (@) and other fragments and variants, and sharpen known undecidability results for (↓, @).

title: Branching-Time Logics Repeatedly Referring to States
abstract: While classical temporal logics lose track of a state as soon as a temporal operator is applied, several branching-time logics able to repeatedly refer to a state have been introduced in the literature. We study such logics by introducing a new formalism, hybrid branching-time logics, subsuming the other approaches and making the ability to refer to a state more explicit by assigning a name to it. We analyze the expressive power of hybrid branching-time logics and the complexity of their satisfiability problem. As main result, the satisfiability problem for the hybrid versions of several branching-time logics is proved to be 2EXPTIME-complete. To prove the upper bound, the automata-theoretic approach to branching-time logics is extended to hybrid logics. As a result of independent interest, the nonemptiness problem for alternating one-pebble Büchi tree automata is shown to be 2EXPTIME-complete. A common property of the logics studied is that they refer to only one state. This restriction is crucial: The ability to refer to more than one state causes a nonelementary blow-up in complexity. In particular, we prove that satisfiability for NCTL* has nonelementary complexity.

title: Using modal logics to express and check global graph properties
abstract: Graphs are among the most frequently used structures in Computer Science. Some of the properties that must be checked in many applications are connectivity, acyclicity and the Eulerian and Hamiltonian properties. In this work, we analyze how we can express these four properties with modal logics. This involves two issues: whether each of the modal languages under consideration has enough expressive power to describe these properties and how complex (computationally) it is to use these logics to actually test whether a given graph has some desired property. First, we show that these properties are not definable in a basic modal logic or in any bisimulation-invariant extension of it, like the modal μ-calculus. We then show that it is possible to express some of the above properties in a basic hybrid logic. Unfortunately, the Hamiltonian and Eulerian properties still cannot be efficiently checked. In a second attempt, we propose an extension of CTL∗ with nominals and show that the Hamiltonian property can be more efficiently checked in this logic than in the previous one. In a third attempt, we extend the basic hybrid logic with the ↓ operator and show that we can check the Hamiltonian property with optimal (NP) complexity in this logic. Finally, we tackle the Eulerian property in two different ways. First, we develop a generic method to express edge-related properties in hybrid logics and use it to express the Eulerian property. Second, we express a necessary and sufficient condition for the Eulerian property to hold using a graded modal logic.

title: Counter-Free Automata
abstract: A particular class of finite-state automata, christened by the authors "counter-free," is shown here to behave like a good actor: it can drape itself so thoroughly in the notational guise and embed itself so deeply in the conceptual character of several quite different approaches to automata theory that on the surface it is hard to believe that all these roles are being assumed by the same class.This is one of the reasons it has been chosen for study here. The authors write that they "became impressed with the richness of its mathematical complexity" and that "a sure sign of gold is when profound mathematical theory interacts with problems that arise independently. And indeed it is noteworthy that the class of automata we shall discuss was defined more or less explicitly by several people working from very different directions and using very different concepts. The remarkable happening was that these definitions could not be recognized as equivalent until algebraic tools of analysis were brought to the field in the works of Schutzenberger and in the works of Krohn and Rhodes."The theme of the monograph is the utility and equivalence of these different definitions of counter-free automata. Its organization follows the plan of taking up, one by one, each of a number of different conceptualizations: the historically important "nerve net" approach; the algebraic approach, in which automata are treated as semigroups; the "classical" theory based on state transition diagrams; the "linguistic" approach based on the concept of regular expressions; and the "behavioral" descriptions using symbolic logic. In each of these conceptual areas, the class of automata under study is found in a new guise. Each time it appears as yet another special case. The authors' burden is to show that all these definitions are in fact equivalent.Care has been taken so that this research monograph can be used as a self-sufficient text. Notations have been defined carefully and always in the context of the discussion. Most of the chapters end with a substantial number of exercises. It is self-contained in that all concepts are defined, and all theorems used are, with one exception, either fully proved or safely left as exercises for the student.

title: First-order definable languages
abstract: We give an essentially self-contained presentation of some princi- pal results for first-order definable languages over finite and infinite words. We introduce the notion of a counter-free Buchi automaton; and we relate counter-freeness to aperiodicity and to the notion of very weak alternation. We also show that aperiodicity of a regular 1-language can be decided in polynomial space, if the language is specified by some Buchi automaton.

title: Bounded Semantics of CTL and SAT-Based Verification
abstract: Bounded model checking has been proposed as a complementary approach to BDD based symbolic model checking for combating the state explosion problem, esp. for efficient error detection. This has led to a lot of successful work with respect to error detection in the checking of LTL, ACTL (the universal fragment of CTL) and ACTL* properties by satisfiability testing. The use of bounded model checking for verification (in contrast to error detection) of LTL and ACTL properties has later also been studied. This paper studies the potentials and limitations of bounded model checking for the verification of CTL and CTL* formulas. On the theoretical side, we first provide a framework for discussion of bounded semantics, which serves as the basis for bounded model checking, then extend the bounded semantics of ACTL to a bounded semantics of CTL, and discuss the limitation of developing such a bounded semantics for CTL*. On the practical side, a deduction of a SAT-based bounded model checking approach for ACTL properties from the bounded semantics of CTL is demonstrated, and a comparison of such an approach with BDD-based model checking is presented based on experimental results.

title: Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree
abstract: In this paper we study the expressive power of the full branching time logic CTL* (of Clarke, Emerson, Halpern and Sistla), by comparing it with fragments of monadic second-order logic over the binary tree. We show that over binary tree models the system CTL* has the same expressive power as monadic second-order logic in which set quantification is restricted to infinite paths (in particular, the full strength of first-order logic is captured here by CTL*). This generalizes Kamp's theorem on the equivalence between propositional linear time logic and first-order logic over the ordering of the natural numbers. For the proof an extension of CTL* by past operators is introduced. The transition from monadic formulas to CTL* rests on a model-theoretic decomposition lemma for trees that is justified by an application of the Ehrenfeucht-Fraisse game. The paper concludes by discussing variants of the main result, dealing for example with trees of higher branching index and the extended branching time logic ECTL*.

title: Counting on CTL*: on the expressive power of monadic path logic
abstract: Monadic second-order logic (MSOL) provides a general framework for expressing properties of reactive systems as modelled by trees. Monadic path logic (MPL) is obtained by restricting second-order quantification to paths reflecting computation sequences. In this paper we show that the expressive power of MPL over trees coincides with the usual branching time logic CTL* embellished with a simple form of counting. As a corollary, we derive an earlier result that CTL* coincides with the bisimulation-invariant properties of MPL. In order to prove the main result, we first prove a new Composition Theorem for trees.

title: Counting beyond a Yottabyte, or how SPARQL 1.1 property paths will prevent adoption of the standard
abstract: SPARQL -the standard query language for querying RDF- provides only limited navigational functionalities, although these features are of fundamental importance for graph data formats such as RDF. This has led the W3C to include the property path feature in the upcoming version of the standard, SPARQL 1.1.We tested several implementations of SPARQL 1.1 handling property path queries, and we observed that their evaluation methods for this class of queries have a poor performance even in some very simple scenarios. To formally explain this fact, we conduct a theoretical study of the computational complexity of property paths evaluation. Our results imply that the poor performance of the tested implementations is not a problem of these particular systems, but of the specification itself. In fact, we show that any implementation that adheres to the SPARQL 1.1 specification (as of November 2011) is doomed to show the same behavior, the key issue being the need for counting solutions imposed by the current specification. We provide several intractability results, that together with our empirical results, provide strong evidence against the current semantics of SPARQL 1.1 property paths. Finally, we put our results in perspective, and propose a natural alternative semantics with tractable evaluation, that we think may lead to a wide adoption of the language by practitioners, developers and theoreticians.

title: The complexity of evaluating path expressions in SPARQL
abstract: The World Wide Web Consortium (W3C) recently introduced property paths in SPARQL 1.1, a query language for RDF data. Property paths allow SPARQL queries to evaluate regular expressions over graph data. However, they differ from standard regular expressions in several notable aspects. For example, they have a limited form of negation, they have numerical occurrence indicators as syntactic sugar, and their semantics on graphs is defined in a non-standard manner. We formalize the W3C semantics of property paths and investigate various query evaluation problems on graphs. More specifically, let x and y be two nodes in an edge-labeled graph and r be an expression. We study the complexities of (1) deciding whether there exists a path from x to y that matches r and (2) counting how many paths from x to y match r. Our main results show that, compared to an alternative semantics of regular expressions on graphs, the complexity of (1) and (2) under W3C semantics is significantly higher. Whereas the alternative semantics remains in polynomial time for large fragments of expressions, the W3C semantics makes problems (1) and (2) intractable almost immediately.
 As a side-result, we prove that the membership problem for regular expressions with numerical occurrence indicators and negation is in polynomial time.

title: GraphLog: a visual formalism for real life recursion
abstract: We present a query language called GraphLog, based on a graph representation of both data and queries. Queries are graph patterns. Edges in queries represent edges or paths in the database. Regular expressions are used to qualify these paths. We characterize the expressive power of the language and show that it is equivalent to stratified linear Datalog, first order logic with transitive closure, and non-deterministic logarithmic space (assuming ordering on the domain). The fact that the latter three classes coincide was not previously known. We show how GraphLog can be extended to incorporate aggregates and path summarization, and describe briefly our current prototype implementation.

title: Reasoning on regular path queries
abstract: Current information systems are required to deal with more complex data with respect to traditional relational data. The database community has already proposed abstractions for these kinds of data, in particular in terms of semistructured data models. A semistructured model conceives a database essentially as a finite directed labeled graph whose nodes represent objects, and whose edges represent relationships between objects. In the same way as conjunctive queries form the core of any query language for the relational model, regular path queries (RPQs) and their variants are considered the basic querying mechanisms for semistructured data.Besides the basic task of query answering, i.e., evaluating a query over a database, databases should support other reasoning services related to querying. One of the most important is query containment, i.e., verifying whether for all databases the answer to a query is a subset of the answer to a second query. Another important reasoning service that has received considerable attention in the recent years is view-based query processing, which amounts to processing queries based on a set of materialized views, rather than on the raw data in the database.The goal of this paper is to describe basic results and techniques concerning query containment and view based query processing for the class of two-way regular-path queries (which extend RPQs with the inverse operator). We will demonstrate that the basic services for reasoning about two way regular path queries are decidable, thus showing that the limited form of recursion expressible by these queries does not endanger the decidability of reasoning. Besides the specific results, our methods show the power of two-way automata in reasoning on complex queries.

title: Expressive Languages for Path Queries over Graph-Structured Data
abstract: For many problems arising in the setting of graph querying (such as finding semantic associations in RDF graphs, exact and approximate pattern matching, sequence alignment, etc.), the power of standard languages such as the widely studied conjunctive regular path queries (CRPQs) is insufficient in at least two ways. First, they cannot output paths and second, more crucially, they cannot express relationships among paths.
 We thus propose a class of extended CRPQs, called ECRPQs, which add regular relations on tuples of paths, and allow path variables in the heads of queries. We provide several examples of their usefulness in querying graph structured data, and study their properties. We analyze query evaluation and representation of tuples of paths in the output by means of automata. We present a detailed analysis of data and combined complexity of queries, and consider restrictions that lower the complexity of ECRPQs to that of relational conjunctive queries. We study the containment problem, and look at further extensions with first-order features, and with nonregular relations that add arithmetic constraints on the lengths of paths and numbers of occurrences of labels.

title: Relative Expressiveness of Nested Regular Expressions
abstract: Nested regular expressions (NREs) have been proposed as a powerful formalism for querying RDFS graphs, but not too much investigation on NREs has been pursued in a more general graph database context. In this paper we study the relative expressiveness of NREs by comparing it with the language of conjunctive regular path queries (CRPQs), which is one of the most widely studied query languages for graph databases. Among other results, we show that NREs and CRPQs are incomparable in terms of expressive power, but NREs properly extend the language of acyclic CRPQs. Even more, there is a natural fragment of NREs that coincide in expressive power with the class of acyclic CRPQs. Our results, plus previous results that show that NREs can be evaluated in linear time in combined complexity, put forward NREs as a query language for graph-structured data that deserves further attention.

title: Expressiveness and Static Analysis of Extended Conjunctive Regular Path Queries
abstract: We study the expressiveness and the complexity of static analysis of extended conjunctive regular path queries (ECRPQs), introduced by Barcelo et al. (2010) . ECRPQs are an extension of conjunctive regular path queries (CRPQs), a well-studied language for querying graph structured databases. Our first main result shows that query containment and equivalence of a CRPQ in an ECRPQ are undecidable. This settles one of the main open problems posed by Barcelo et al. As a second main result, we prove a non-recursive succinctness gap between CRPQs and the CRPQ-expressible fragment of ECRPQs. Apart from this, we develop a tool for proving inexpressibility results for CRPQs and ECRPQs. In particular, this enables us to show that there exist queries definable by regular expressions with backreferencing, but not expressible by ECRPQs.

title: Languages, Automata, and Logic
abstract: The subject of this chapter is the study of formal languages (mostly languages recognizable by finite automata) in the framework of mathematical logic.

title: The complexity of decision problems in automata theory and logic.
abstract: Massachusetts Institute of Technology. Dept. of Electrical Engineering. Thesis. 1974.

title: Model theory of modal logic
abstract: Publisher Summary This chapter presents a theoretical analysis of modal logic that can be applied to many application areas. It presents the central core of contemporary insight into the mathematical structure of modal logic. Model theory is about semantics; it studies the interplay between a logical language (logic) and the models (structures) for that language. Modal logics come as members of a loosely knit family and have various links to other logics––classical first- and second-order logic as well as, temporal and process logics stemming from particular applications. The chapter introduces some key notions; in particular, the different levels of semantics, followed by a discussion of the concept of bisimulation and bisimulation respecting model constructions. The study of modal logic as logic of frames is described. This comprises advanced constructions such as ultrafilter extensions and ultraproducts, basic model theory of general frames, and a survey of classical results on frame definability and relations with second-order logic. The semantics of modal logic has two emblematic features, which have a crucial impact on its model theory––namely, modal logic is local and multi-layered.

title: Model theoretic methods for fragments of FO and special classes of (finite) structures
abstract: Some prominent fragments of first-order logic are discussed from a game-oriented and modal point of view, with an emphasis on model theoretic techniques for the non-classical context of finite model theory or of other natural non-elementary classes of structures. We stress the modularity and compositionality of the games as a key ingredient in the exploration of the expressive power of logics over specific classes of structures. The leading model theoretic theme is expressive completeness – or the characterisation of fragments of first-order logic as expressively complete over some class of (finite) structures for first-order properties with some prescribed semantic preservation behaviour. In contrast with classical expressive completeness arguments, the emphasis here is on explicit model constructions and transformations, which are guided by the game analysis of both first-order logic and of the imposed semantic constraints.  finite model theory, model theoretic games, bisimulation, modal and guarded logic, expressive completeness, preservation and characterisation theorems

title: Definable relations and first-order query languages over strings
abstract: 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 of n-ary relations for every n, 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.