Michael Benedikt

A Analysis of Schemas With Access Restrictions

Keywords: H.3.5 [Information Systems]: Online Information Services-Webbased services, F.4.1 [Mathematical logic and formal languages]: Mathematical logic-Temporal logic Theory, Verification, Languages Access methods, optimization, Hidden Web

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.

INTRODUCTION

Many data sources do not expose either a bulk export facility or a query-based interface, enforcing instead many restrictions on the way data is accessed. For example, access to data may only be possible through Web forms, which require bindings for particular fields in the relation [START_REF] Li | Answering queries with useful bindings[END_REF][START_REF] Calì | Dynamic query optimization under access limitations and dependencies[END_REF]. Querying with limited access patterns also arises in other middleware contexts (e.g. federated access to data in Web services) as well as in construction of query interfaces on top of predetermined indexed accesses [START_REF] Ullman | Principles of Database and Knowledge-Base Systems[END_REF]]. For example, a Web telephone directory might allow several Web forms that serve as access methods to the underlying data. It may have an access method AcM 1 accessing a relation Mobile# (name, postcode, street, phoneno),

where AcM 1 allows one to enter a mobile phone customer's name (the underlined field) and access the corresponding set of tuples containing a postal code, mobile phone number and street name. The same site might have an access method AcM 2 on relation Address (street, postcode, name, houseno) allowing the user to enter a street name and postcode, returning all corresponding resident names and housenumbers. Formally an access method consists of a relation and a collection of input positions: for AcM 1 , position 1 is the sole input position, while for AcM 2 the first two positions are input. An access consists of an access method plus a binding for the input positions -for example putting "Smith" into method AcM 1 is an access. The response to an access is a collection of tuples for the relation that agree with the binding given in the access. A schema of this sort defines a collection of access paths: sequences consisting of accesses and their responses.

A:2

The impact of "limited access patterns" has thus been the subject of much study in the past decade. It is known that in the presence of limited access patterns, there may be no access path that completely answers the query, and there may also be many quite distinct paths. For example, the query Address(X, Y, "Jones", Z) asking for the address of Jones is not answerable using the access methods AcM 1 and AcM 2 above. There are certainly many ways to obtain the maximal answers: one could begin by obtaining all the street names and postcodes associated with Jones in the Mobile# table, entering these into the Address table to see if they match Jones, then taking all the new resident names we have discovered and repeating the process, until a fixedpoint is reached. If, however, Jones does not occur as a name in Mobile#, then this process will not yield Jones' tuple in Address. In general it is known [START_REF] Li | Computing complete answers to queries in the presence of limited access patterns[END_REF]] that for any conjunctive query one can construct (in linear time) a Datalog program that produces the maximal answers to a query under access patterns: the program simply tries all possible valid accesses on the database, as in the brute-force algorithm above.

In the absence of a complete plan, how can we determine which strategy for making accesses is best? Recent works [START_REF] Calì | Dynamic query optimization under access limitations and dependencies[END_REF][START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF]] have proposed optimizing recursive plans, using access pattern analysis to determine that certain kinds of accesses can not extend to a useful path. An example is the work in [START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF]] which proposes limiting the number of accesses to be explored by determining that some accesses are not "relevant" to a query. An access is long term relevant if there is an access path that begins with the access and uncovers a new query result, where the removal of the access results in the new result not being discovered. [START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF] gives the complexity of determining relevance for a number of query languages.

Long term relevance is only one property that can be used to measure the value of making a particular access -for example we may want to know whether there is an access that reveals several values in the query result. Furthermore, "limited access patterns" represent only one possible restriction that limits the possible access paths through a web interface. Many other restrictions may be enforced, e.g: -Restrictions that follow from integrity constraints on the data: e.g. a mobile phone customer name will not (arguably) overlap with a street name. Thus in an iterative process for answering the query given above, we should not bother to make accesses to the Mobile# table using street names we have acquired earlier in the process. It is also easy to see that key constraints, and more generally functional dependencies, can play a crucial role in determining whether an access is relevant. -Access order restrictions: e.g. before making any access to Mobile#, the interface may require a web user to have made at least one access to Address. -Dataflow restrictions; before performing an access to Mobile# on a name, the web user must have received that name as a response to a call to Address.

Ideally, a query processor should be able to inspect an access and determine whether it is a good candidate for use, where the assumptions on the paths as well as the notion of "good candidate" could be specified on a per-application basis. In this paper we look for a general solution to specifying and determining which accesses are promising: a language for querying the access paths that can occur in a schema. We show that every schema can be associated with a labelled transition system (LTS), with transitions for each access and nodes for each "revealed instance" (information known after a set of accesses). A fragment of the LTS for the schema with access methods AcM 1 and AcM 2 is given in Figure 1. Paths through the LTS represent possible access/response sequences of the Web-based datasource. There are infinitely many paths -in fact every access could have many possible responses. But the access restrictions in the schema place limitations on what paths one can find in the LTS. We can then identify a "query on access paths" with a query over this transition system. This work will provide a lan-Fig. 1. Tree of possible paths associated with a schema guage that allows the user to ask whether a given kind of path through instances of the schema is possible: e.g. is there a path that leads to an instance where a given conjunctive query holds, but where the path never uses access AcM 1 ? Is there a path that satisfies a given set of additional dataflow, access order restrictions, or data integrity constraints?

Paths are often queried with temporal logic [START_REF] Emerson | Temporal and modal logic[END_REF]]. We will look at natural variations of First-Order Linear Temporal Logic (FOLTL) for querying access paths. We look at a family of languages denoted AccLTL(L) ("Access LTL"), parameterized by a fragment L of relational calculus. It has a two-tiered structure: at the top level are temporal operators ("eventually", "until") that describe navigation between transitions in a path. The second tier looks at a particular transition, where we have first-order (i.e. relational calculus) queries that can ask whether the transitions satisfy a given property described in L. The relational vocabulary we consider for the "lower tier" will allow us to describe transitions given by accesses; it allows us to refer to the bindings of the access, the access method used, and the pre-and post-access versions of each schema relation. Consider the following AccLTL sentence:

(¬∃n ∃p ∃s ∃ph Mobile# pre (n, p, s, ph)) U (∃n IsBind AcM1 (n) ∧ ∃s ∃p ∃h Address pre (s, p, n, h))

The relational query prior to the "until" symbol U states that there are no entries in Mobile# pre -the Mobile# table prior to the access. The query after the until symbol U states that an access was done with method AcM 1 and binding n, where value n appeared in the Address table prior to the access. Hence this "meta query" returns the set of access paths which have no entries revealed in relation Mobile# until an access AC is performed, where AC has method AcM 1 and uses a name that already exists in the Address table. In this work we will not be interested in returning all paths satisfying a query (there are generally infinitely many). We will check whether there is a path satisfying a given specification. This is a question of satisfiability for our path query language. We may also want to check that every path through the system is of a certain form; this is the validity problem for the language -bounds for validity will follow from our results on satisfiability.

We denote the logic containing the above sentence by AccLTL(FO ∃+ Acc ), where FO ∃+ Acc is the collection of positive existential queries over a signature consisting of: the access methods, bindings, and the pre-and post-access version of each relation used in a transition. AccLTL(FO ∃+ Acc ) can express a wide variety of properties. Unfortunately we show that satisfiability for the logic is undecidable. However, we show that a rich sub-language of AccLTL(FO ∃+ Acc ), denoted AccLTL + , has a decidable satisfiability problem. In AccLTL + the formulas involving the bindings only occur positively. We give bounds on the complexity of this fragment, using a novel technique of reduction to containment problems for Datalog. We then look at the exact complexity of smaller language fragments, and show that the complexity can go much lower -e.g. within the polynomial hierarchy. The main thing we give up in these languages is the ability to express dataflow restrictions. We also study the complexity and expressiveness of extensions of the languages with inequalities and with branching time operators. In summary, our contributions are: -We present the first query language for reasoning about the possible paths of accesses and responses that may appear in a Web form or other limited-access datasource. -We show that combining a natural decidable logic for temporal data (LTL) with conjunctive queries gives an undecidable path query language. -We show that by restricting to queries that are "binding positive", we get a decidable path query language. In the process we introduce a new automaton model that corresponds to a process repeatedly querying a Web data source. We show that analysis of these "access automata" can be performed via reduction to Datalog containment problems, and we in turn show that these Datalog containment problems are decidable. The automaton and logic specification languages are powerful enough to express a rich set of data integrity constraints, access order restrictions, and data flow restrictions. -We show that the complexity of the logic can be decreased drastically by restricting the ability to express properties of the bindings that occur in accesses. The resulting language can still express important access order and data integrity restrictions, but no dataflow restrictions. -We determine the impact of adding inequalities to the relational query language, and of adding branching operators, both in terms of expressing critical properties of accesses and on complexity of verification. Organization: Section 2 gives the basic definitions related to access patterns, along with our family of languages AccLTL(L). Section 3 gives our results about the full language AccLTL(FO ∃+ Acc ). The longest section of the paper, Section 4, deals with the restricted language AccLTL + . On the way to showing decidability of AccLTL + , this section defines the related automaton model, explains the connection with certain Datalog containment problems, and provides new decidability results for Datalog containment. Section 6 discusses extensions of AccLTL + . Section 7 gives conclusions and overviews related work.

An electronic appendix, available via the Digital Library, contains additional material filling in details of a few proofs, particularly the main decidability proof of Section 4.

DEFINITIONS

Schemas and paths through a schema. Let Types be some fixed set of datatypes, including at least the integers and booleans. Our schemas extend traditional relational schemas under the "unnamed perspective" [START_REF] Abiteboul | Foundations of Databases[END_REF]. A schema Sch includes a set of relations {S 1 . . . S n }, with each S i associated with a function from {1 . . . n i }, where n i is the arity of S i , to Types. We refer to the set {1 . . . n i } as the positions of S i and the output of the function on j as the domain of the j th position. An instance I for the schema consists of a finite collection I(S i ) of tuples for each relation S i , where a tuple is a function from the positions of S i to the corresponding domains. For two tuples t and t′ , we denote by t ⋅ t′ , the concatenation of the two tuples.

A schema will also have a collection of access methods, where each method AcM is associated with a relation S i and a collection of input positions Inp(AcM). Informally, each access method allows one to input a tuple of values for Inp(AcM) and get as a result a set of matching tuples.

An access consists of an access method and a binding -a mapping taking the input positions of the method to their domains. A boolean access is one where the access method has as inputs every position of the relation -it is thus a membership test. We will use an intuitive notation for accesses, often omitting the access method. Mobile#("Jones", ?, ?, ?) is an access to relation Mobile# asking for all phone number information for people named "Jones". A boolean access is Mobile#("Jones", "OX13QD", "Parks Rd", 23)?, where we add the ? to make clear it is an access.

Given an access (AcM, b), a well-formed output for AcM (on instance I) is any set r of tuples in I in the relation of AcM that is compatible with b on the input positions. We also refer to this as a well-formed response. Note that we consider a general model where distinct executions of an access can return different responses, thus allowing non-determinism.

A sequence ((AcM 1 , b1 ), r 1 ), . . . , ((AcM n , bn ), r n ) of accesses and well-formed responses for some instance I is an access path for the instance I. Notice that if we have an access path as above, it will always be the case that each r i consists of tuples for the relation of AcM i , and its projection onto the input positions of AcM i will consist of exactly bi . Any sequence with this property will be referred to as an access path (without reference to any instance). Note that every such sequence is an access path for some instance -the instance containing all returned tuples. Given an access path p the configuration returned by p on I 0 , is the instance where relation S i contains with all tuples returned by any access to S i in p. If we take an access path and look at the sequence of configurations, returned by longer and longer prefixes, we will see that the relations grow monotonically, since we only add tuples during accesses. We will generally use the word "configuration" to emphasize that this is a database instance containing information made visible by the access, as opposed to the full information in the hidden instance. In some situations, it is useful to deal with the case where there is some initial instance Conf 0 representing information known in advance (e.g. some well-known facts). Given such a Conf 0 and a path p, we can then talk about the configuration returned by p on Conf 0 , which appends to each relation Conf 0 the responses to the accesses in p.

As mentioned in the introduction, one is not interested in arbitrary paths, but those satisfying additional "sanity properties". We allow our schemas to prescribe some common additional properties of access methods, while additional restrictions can be expressed in the logics. The weakest property we consider here is called idempotence: an access path is idempotent if whenever the path repeats the same access, it obtains the same results. This corresponds to the requirement that accesses are deterministic. A stronger property is that accesses are exact: an access path is exact on an instance I if for every access (AcM, b), the corresponding response R contains exactly the tuples in the relation of AcM which agree with b on the input positions. An access path is exact if it is exact for some input instance. Put another way, an exact access path is one that contains sound and complete views of the input data for all accesses made. Most web sources are not expected to be exact -an online music site will generally not contain information about all online music. However, some forms may be known to have canonical information -e.g. a web form accessing data from a trusted government agency. We allow situations which mix exact and non-exact accesses. In general, a schema may say that some access methods are exact, some are idempotent, and some are neither. Given a set of access methods S, we say that an access path is S-exact if there is an A:6 instance I such that the path is exact for all accesses with methods in S, and similarly talk about S-idempotence.

Finally, we often do not want paths in which values for access method inputs are "guessed", but are only interested in paths where the input to an access method is a value already known. Given an instance I 0 (representing the "initially known information") an access path p = a 1 , r 1 . . . is grounded in I 0 if every value in a binding a i occurs either in I 0 or in a response from some a j with j < i. Groundedness is a special kind of dataflow restriction -our largest logics will be able to specify groundedness, along with more specialized dataflow restrictions, but we allow them also to be imposed in the schema.

A labelled transition system (LTS) is of the from (No, L, T) where No is a collection of nodes, L is a collection of edge labels, and T is a collection of transitions -elements of No × L × No. With any schema we can associate a labelled transition system where the nodes are all the instances the labels are all the accesses, and there is a transition (I, AC, I ′ ) whenever there is some response r to AC such that the configuration resulting from the access AC and response r is I ′ . We can also consider the restricted LTS where we only allow paths with transitions (I, AC, I ′ ) in which the access AC is grounded at I, only paths that are idempotent, or only paths that are exact for a given subset of the access methods.

Logics for querying access paths. To query paths it is natural to use Linear Temporal Logic (LTL) [START_REF] Emerson | Temporal and modal logic[END_REF]]. LTL formulas define positions within a path. In Propositional LTL, the positions within paths are associated with a propositional model over some set of propositions, and one can then build up formulas from the propositions using the modal operators, S (since) , U (until), X -1 (previously), X (next), and F (eventually). For example F(Q ∧ XP ) holds on positions i in a path p that come before some position j such that proposition Q holds at j and proposition P holds on position j + 1. We want to extend LTL to deal with access paths, which are not just a sequence of propositional structures. Each position in an access path consists of an access and its response; the corresponding path through the LTS defined above consists of transitions t 1 . . . t n , where a transition t i is of the form (I i , (AcM i , bi ), I i+1 ). There is obviously a one-to-one correspondence between access paths and LTS paths as above, and we will often identify them. Since the positions carry with them a relational structure, we will use a variant of First Order Linear Temporal Logic (FOLTL) [START_REF] Emerson | Temporal and modal logic[END_REF]], which allows the use of first-order quantifiers and variables along with modal ones. We will deal here with a variant of FOLTL in which first-order sentences describing properties of positions can be nested inside temporal operators, but not vice versa. The investigation of a language which allows arbitrary nesting is left for future work.

For a given vocabulary Sch, we will consider formulas over the relational vocabulary Sch Acc consisting of two copies R pre , R post of each schema relation R ∈ Sch, and also predicates IsBind AcM for each access method AcM in Sch. The arity of IsBind AcM is the number of input positions of AcM. An LTS path t 1 . . . t n is associated with a sequence of Sch Acc structures, where the i th structure M (t i ), corresponding to t i = (I i , (AcM i , bi ), I i+1 ) interprets each predicate R pre using the interpretation of R in I i , each predicate R post as the interpretation of R in I i+1 . The predicate IsBind AcMi holds of exactly the tuple bi while all other predicates IsBind AcM are empty. When we deal with computational problems in our logics, we will always be restricting the interpretation of the predicates in the way described above. For example the statement in our logic that whenever R post (x) holds in one transition then R pre (x) holds in the next transition will be valid whenever our logic, when it is clearly not valid over arbitrary interpretations of R post and R pre .

Notice that in the paragraph above we have alluded to a version of FOLTL in which one can only describe sentences about each individual first-order structure, nesting temporal operators on top of them. When such a logic can range over arbitrary sequences of first-order structures, they are known to have very restricted expressiveness, as well as more attractive decidability properties [START_REF] Hodkinson | Decidable fragments of first-order temporal logics[END_REF]]. In contrast, we are restricting our sequences to be of a special form, with consecutive structures being related by an access. More importantly, via the formula IsBind we can express some information about the "dynamics" between consecutive structures. As shown above, it is the addition of IsBind and its relationship with the pre-and post-versions of the relations, enforced in our semantics, that will allow us to express many natural properties of access sequences, such as time-invariance. But it is also this feature that will make decidability more problematic.

We now introduce Access Linear Temporal Logic (AccLTL for short), our main specification formalism.

Definition 2.1. Let L be a subset of first-order logic over Sch Acc . The logic AccLTL(L) has as atomic formulas every sentence of L, and is built up by the usual LTL constructors:

¬ϕ ϕ ∨ ϕ ϕ ∧ ϕ X ϕ ϕ U ϕ
In analyzing accesses to data, the paths we are interested in will be the finite ones, We will thus use a semantics for the logic via positions within finite paths. The distinction from the standard semantics of LTL will only be in the interpretation of the next operator, which is interpreted as false at the end of paths. The restriction to finite paths will also allow us to use a simpler kind of automaton to analyze the logic, avoiding the acceptance conditions needed in automata for infinite objects. The semantics of AccLTL(L) is given by the relation (p, i) ⊧ ϕ, where p = t 1 . . . t n is an LTS path and i ≤ n. It combines the standard semantics of L formulas with the usual rules for the constructors of LTL: (1) (p, i) ⊧ ϕ iff ϕ ∈ L and M (t i ) satisfies ϕ in the usual sense of first-order logic. ( 2

) (p, i) ⊧ ¬ϕ iff (p, i) ⊭ ϕ. (3) (p, i) ⊧ X ϕ iff (p, i + 1) ⊧ ϕ. (4) (p, i) ⊧ ϕ U ψ iff there exists j ≥ i such that (p, j) ⊧ ψ and ∀i ≤ k < j, (p, k) ⊧ ϕ. (5) (p, i) ⊧ ϕ ∨ ψ iff (p, i) ⊧ ϕ or (p, i) ⊧ ψ and similarly (p, i) ⊧ ϕ ∧ ψ iff (p, i) ⊧ ϕ and (p, i) ⊧ ψ
In the rest of the paper, we make use of the temporal operators G ("globally") and F ("eventually"). These operators can be expressed using X and U as usual in LTL. The language of a formula ϕ is the set of paths p such that (p, 1) ⊧ ϕ.

Definition 2.2. FO ∃+

Acc consists of all positive existential FO sentences over the signature Sch Acc .

Our main language of interest is AccLTL(FO ∃+ Acc ).

Example 2.3. [START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF][START_REF] Calì | Conjunctive query containment under access limitations[END_REF]] study query containment under (in our terminology, grounded) access patterns. Boolean query Q 1 is contained in Boolean query Q 2 relative to a schema with access patterns means that for every grounded access path p, if the configuration resulting from p satisfies Q 1 , then it also satisfies Q 2 . Informally, the facts about Q 1 that we can determine given the schema restrictions are contained in the facts we can determine about Q 2 . Using a containment algorithm, one can perform query minimization in the presence of access restrictions.

In [START_REF] Calì | Conjunctive query containment under access limitations[END_REF] containment under access restrictions is shown to be decidable for conjunctive queries, while [START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF]] studies the complexity of the problem. One can see that Q 1 is contained in Q 2 under grounded access patterns iff the following AccLTL(FO ∃+ Acc ) formula is a validity (over grounded paths):

G ¬ Q pre 1 ∧ ¬Q pre 2
Here Q pre i is obtained from Q i by replacing each schema predicate S by S pre (one could as easily use S post ). We will show that containment under grounded access patterns can be expressed in a restricted fragment of AccLTL(FO ∃+ Acc ), as well as in an automatonbased specification formalism where validity relative to grounded access paths is decidable in 2EXPTIME. Our results will thus give tight bounds for containment under grounded access patterns.

Example 2.4. A boolean access AC 1 is said to be long term relevant [START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF] (LTR) for a boolean query Q on an initial instance I 0 if there is an access path p = AC 1 , r 1 AC 2 , r 2 . . . such that the configuration I resulting from applying p to I 0 satisfies Q, and the configuration resulting from the path with AC 1 dropped (i.e. AC 2 , r 2 . . .) leads to a configuration where Q does not hold. In the terminology of [START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF] we say it is LTR under grounded accesses if there is a grounded access path satisfying the above.

This property can be expressed in AccLTL(FO ∃+ Acc ) in the following sense: for each I 0 , AC 1 = (AcM 1 , b1 ), and Q there is an AccLTL(FO ∃+ Acc ) formula ϕ which is satisfiable iff AC 1 is LTR. Below we give the formula for I 0 being the empty instance:

F ¬Q pre ∧ IsBind AcM1 ( b1 ) ∧ Q post
The formula checks that there is a path p and a response r 1 to AC 1 , such that Q holds after p but not after p, AC 1 , r 1 . But for a boolean access AC 1 , the instance after p, AC 1 , r 1 is the same as the one after AC 1 , r 1 , p.

As mentioned in the introduction, we often want additional data integrity restrictions to hold on the path. In AccLTL(FO ∃+ Acc ), we can add on many data integrity restrictions, such as the disjointness of names from streets, which would be expressed by a conjunction of several formulas, including: G(¬∃n ∃p ∃s ∃ph ∃hn ∃n ′ ∃pc Mobile# pre (n, p, s, ph) ∧ Address pre (n, pc, n ′ , hn))

Similarly we can add access order restrictions and dataflow restrictions. For example, the following would restrict to paths in which names input to Mobile# must have appeared previously in Address:

G((∃n IsBind AcM1 (n)) → ∃n ∃s ∃hn ∃pc IsBind AcM1 (n) ∧ Address pre (s, pc, n, hn))

Example 2.5. (Data integrity restrictions, continued) Let Sch be a schema that includes, in addition to the access methods, a set of functional dependencies (FDs) d i = R i ∶ pos i → a i , where pos i are positions of R i and a i is a position of R i . A database instance satisfies an FD above if any two tuples s, t in R i if s j = t j for all j ∈ pos i , then s ai = t ai . We say that an access AcM is long-term relevant for Q under Sch if there is an instance I ⊇ I 0 satisfying all the FDs and an access path that reveals Q to be true, as in Example 2.4, but where each response returns only tuples in I.

This can be expressed in AccLTL(L ≠ ∃ ), where L ≠ ∃ is the set of conjunctive queries with inequalities.

F ¬Q pre ∧ IsBind AcM ( b1 ) ∧ Q post ∧ ⋀ i ¬F ∃ y y ′ R i pre ( y) ∧ R i pre ( y ′ ) ∧ ⋀ k ∈ pos i y k = y ′ k ∧ y ai ≠ y ′ ai
where Q pre and Q post are defined as in the previous example. We will look at languages with inequalities in Section 6.

Basic Computational Problems. The basic problem we consider is satisfiability of a sentence ϕ, which by default means that there is some access path p such that (p, 1) ⊧ ϕ. We will also consider satisfiability over grounded, idempotent, and (S-) exact paths. We emphasize again that we will be considering that satisfiability of formulas not arbitrary sequences of transitions, but only access paths. In such paths the instances change in a certain way: in a transition with an access on relation R, R pre and R post will change only on tuples consistent with the binding, while the other relations will not change at all. We will also consider satisfiability over grounded and exact paths, which impose restrictions which must be considered in any decision procedure for satisfaction or validity.

AN EXPRESSIVE LANGUAGE FOR ACCESS RESTRICTIONS

Since satisfiability for first-order logic is undecidable, it is clear that AccLTL(FO) has an undecidable satisfiability problem. Our first main result is that the same holds even when first-order formulas are restricted to be existential. THEOREM 3.1. Satisfiability of AccLTL(FO ∃+ Acc ) is undecidable. This is surprising, as AccLTL(FO ∃+ Acc ) formulas are very restricted: they deal with a fixed set of existential sentences on the configuration, and as a path progresses these queries can only move from false to true as more tuples are exposed by accesses. The only data that can be referenced across different configurations are the values in the binding, and the facts containing these values of these can only be related within consecutive configurations.

PROOF OF THEOREM 3.1. We first give an intuition over the proof of Theorem 3.1. The proof is a reduction from the problem of determining whether a collection Γ of functional dependencies and inclusion dependencies (IDs) implies another functional dependency σ. Functional dependencies are defined in Example 2.5 (see also [START_REF] Abiteboul | Foundations of Databases[END_REF]). An inclusion dependency is given by a relation symbol R and sequence of positions r 1 . . . r k in R (that is, integers bounded by arity(R), and a relation symbol S with positions s 1 . . . s k . It holds in a database instance if for every tuple t ∈ R there is a tuple t ′ ∈ S such that t ri = t ′ si for all i ≤ k. Since this problem is known to be undecidable [START_REF] Chandra | The implication problem for functional and inclusion dependencies is undecidable[END_REF], it suffices to reduce it to unsatisfiability of an AccLTL(FO ∃+ Acc ) formula. The difficulty here is that functional dependencies seem to require negation inside a universal quantification, while inclusion dependencies require quantifier alternation -in AccLTL(FO ∃+ Acc ) we have only boolean combinations of positive sentences. We now explain the main idea involved in bridging this gap, which will also be used in later undecidability arguments (Theorem 6.2). The schema for our accesses includes a successor relation of a total order over the tuples of each relation mentioned in Γ ∪ {σ}. The successor relation is "created" via accesses -that is, we perform accesses that reveal associations between a tuple and its successor. For each relation R mentioned in Γ ∪ {σ} we also have relations Beg(R) and End(R). Our formula will enforce that these contain the first and the last tuples in the total order, respectively, by asserting the existence of additional accesses to these relations that reveal the first and last tuple. After all the relations are filled, the satisfaction of the different FD's and ID's in Γ and the failure of σ are verified. The satisfaction of the dependencies makes use of the successor relation, and we explain the idea for FDs. We verify a dependency for one tuple at a time, iterating on the tuples according to the order. We will use a new predicate Chk FD (R) whose arity is twice the arity of R. This predicate will have a boolean access. Chk FD (R)( t, t ′ ) holding at some instance indicates that t, t ′ is in accordance with the FDs on R. This will be done in a "nested loop" (a pair of nested "untils" in the logic) in which we iterate first over tuples t, then over tuples t ′ , accessing them progressively within Chk FD (R). At every access, we check whether the FD is satisfied, and if it is we continue the iteration. We now give the formal proof.

We assume that we are given a schema consisting of functional and inclusion dependencies Γ and a distinguished functional dependency σ. We can also assume all positions carry the same type. The undecidability of implication for IDs and FDs holds in the untyped setting [START_REF] Abiteboul | Foundations of Databases[END_REF]. We will also verify the reduction over instances where all relations are of size at least two, allowing us to avoid certain corner cases.

We first give the schema produced by the reduction, which extends the relational schema Sch for the dependencies. For each relation R we have a relation Succ(R) of arity 2k: informally, Succ(R) will be the successor relation referred to above. There are two relations Beg(R) (with boolean access IsBind Beg(R) ) and End(R) (having boolean access IsBind End(R) ) with the same arity as R; these will store the minimal and the maximal tuples for the ordering generated by Succ(R). In addition there is a relation CheckIncDep(R) with the same arity as R, having boolean accesses IsBind CheckIncDep(R) . These are used to check the inclusions dependencies for R. Similarly we will have predicate Chk FD (R) with arity twice that of R.

Components of the sentence. We now build a sentence ψ as a conjunction of smaller sentences. For each relation R we have a subformula that describes a subpath that makes visible tuples in relations Beg(R), Succ(R), End(R) -one can also think of them as "building" these relations in the visible instance. The following sentence ϕ next(R) describes a transition revealing a tuple ( t 1 , t 2 ) in Succ(R) such that (i) t 1 has a predecessor in the current instance but does not have a successor in the current instance and (ii) t 2 does not appear in the successor relation at all.

(∃ t 1 t 2 t 3 IsBind Succ(R) ( t 1 , t 2 ) ∧ Succ(R) pre ( t 3 , t 1 )) ∧ Succ(R) post ( t 1 , t 2 )) ∧ ¬(∃ t 1 t 2 t 3 IsBind Succ(R) ( t 1 , t 2 ) ∧ Succ(R) pre ( t 1 , t 3 )) ∧ ¬(∃ t 1 t 2 t 3 IsBind Succ(R) ( t 1 , t 2 ) ∧ (Succ(R) pre ( t 2 , t 3 ) ∨ Succ(R) pre ( t 3 , t 2 )))
We will need to ensure the correctness of the reduction that for each LTrans path ρ satisfying the formula ψ the initial instance of ρ is empty. This can be ensured by the following sentence

ϕ ∅ = ⋀ R∈Sch ¬(∃x R pre (x))
The first sentence checks the first part of (i), the second ensures the second part of (i) and the third sentence checks (ii). The correctness of this relies on the fact that there is only one tuple in IsBind Succ(R) .

There are also two sentences ϕ Beg(R) and ϕ End(R) that mark the start and end of the exposure of the successor relation. ϕ Beg(R) is defined as:

∃ t 1 IsBind Beg(R) ( t 1 ) ∧ Beg(R) post ( t 1 )∧ X ∃ t 1 t 2 IsBind Succ(R) ( t 1 , t 2 ) ∧ Beg(R) pre ( t 1 ) ∧ Succ(R) post ( t 1 , t 2 )∧ ¬(∃ t 1 t 2 IsBind Succ(R) ( t 1 , t 2 ) ∧ Beg(R) pre ( t 2 )
where ϕ End(R) is defined as:

∃ t 1 IsBind End(R) ( t 1 ) ∧ ∃ t 3 Succ(R) pre ( t 3 , t 1 ) ∧ End(R) post ( t 1 ) ∧ ¬(∃ t 1 t 2 IsBind End(R) ( t 1 ) ∧ Succ(R) pre ( t 1 , t 2 ))
The sentence ψ we ultimately create will be the conjunction of ϕ ∅ defined above with a set of sentences asserting that the path consists of subpaths satisfying

ϕ Beg(R) ∧ X(ϕ next(R) U ϕ End(R) )
followed by a subpath satisfying ϕ verify , where ϕ verify , defined later, checks the constraints on each relation R.

ϕ verify will not add tuples to the relations Succ(R) and End(R). Thus in any path that satisfies a sentence of the form above the visible instance associated to the position satisfying ϕ verify must interpret Succ(R) as the successor relation of a linear order on a collection of tuples whose arity agrees with R, with first element the sole tuple in Beg(R) and last element the sole tuple in End(R). ϕ verify will not reveal any more tuples in those relations, but instead will iterate over all pairs of tuples in the order given by Succ(R), performing additional accesses that will check that these tuples satisfy the dependencies in Γ and fail the distinguished dependency σ.

Invariant. Before giving additional detail on the conjunct ϕ verify , we now state the correctness property of the sentence ψ.

Given an access path p for this signature with final instance J(p), we let I(p) be the instance for the database schema containing only the relation R, with the interpretation of R having for each tuple t 1 , t 2 in J(p)(Succ(R)), the tuple t 1 and also all tuples in J(p)(End(R)).

Our first invariant will be: when this sentence is satisfiable by a path p, the structure I(p) witnesses the failure of the implication of σ by Γ.

Conversely let I be a witness of the failure of the implication of σ by Γ. Let < I be a total order over the tuples of I(R). We describe a path p(I) of accesses and responses, from which we can infer a subinstance of the underlying instance. The path is built such that in the final instance of the path, the relation J(p(I))(Succ(R)) represents the successor relation of < I . To satisfy ϕ, p does an access first on the minimal tuple t of < I on the relation Beg(R), which will return true. Then starting from t and following the order < I , the pairs ( t 1 , t 2 ) such that t 2 is the successor of t 1 are exposed one by one by accesses to the relation Succ(R). The maximal tuple for < I is then exposed as being in End(R). Then the tuples of the relation J(p(I))(CheckIncDep), which contains the same tuples as I(R), are exposed one at a time following < I . Finally the tuples of J(p(I))(Chk FD ), which are those in the cross product of I(R) with itself, are exposed by accesses one by one.

Then our second invariant will be: for every counterexample I to the implication of σ by Γ, the path p(I) satisfies the sentence.

Subformula performing the verification. ϕ verify will be of the form

ϕ CheckFds ∧ X(ϕ CheckIds ∧ Xϕ CheckFdFailure )
where ϕ CheckFds checks that all functional dependencies in Γ hold, ϕ CheckIds checks the inclusion dependencies, and ϕ CheckFdFailure the failure of σ. We will focus on ϕ CheckFds next, focusing on a single relation R.

Check of the functional dependencies. Recall that in the schema we have relations Chk FD (R) with arity twice that of R. These are used to check if every pair ( t 1 , t 2 ) satisfies all FDs in Γ pertaining to R. At the end of the check, the FD is satisfied iff Chk FD (R) contains all tuples from the part of the instance generated by Succ(R).

Let the functional dependencies on R in Γ be f d 1 . . . f d j . For each f d i ∈ Γ of the form A → B we present a sentence ϕ fd i -tuple which checks that the current binding is a pair

( t 1 , t 2 ) which is not a counterexample to f d i : ∃ t 1 t 2 IsBind Chk FD (R) ( t 1 , t 2 ) ∧ ¬(∃ t 1 t 2 IsBind Chk FD (R) ( t 1 , t 2 ) ∧ Π A ( t 1 ) = Π A ( t 2 )) ∨ ∃ t 1 t 2 IsBind Chk FD (R) ( t 1 , t 2 ) ∧ Π B ( t 1 ) = Π B ( t 2 )
We now let ϕ allfd-tuple be ϕ fd1-tuple ∧ X(ϕ fd2-tuple ∧ . . . Xϕ fd j -tuple )

We now consider an iterator ϕ checknext that checks all pairs. The sentence ϕ FD-init begins the check for the first pair in R:

∃ t 1 IsBind Chk FD (R) ( t 1 , t 1 ) ∧ Chk FD (R) post ( t 1 , t 1 )∧ ∃ t 1 IsBind Chk FD (R) ( t 1 , t 1 ) ∧ Beg(R) pre ( t 1 )
This holds at a position iff it has an access on a pair ( t 1 , t 1 ) where t 1 is the first tuple in the ordering, and the access is successful. Note that there is no need to check the FD on such a tuple.

The sentence ϕ F D-next performs the iteration:

∃ t 1 t 2 IsBind Chk FD (R) ( t 1 , t 2 ) ∧ Chk FD (R) post ( t 1 , t 2 ) ∧ ¬(∃ t 1 t 2 IsBind Chk FD (R) ( t 1 , t 2 ) ∧ Chk FD (R) pre ( t 1 , t 2 )) ∧ (ϕ 1 ∨ ϕ 2 ) ∧ ϕ allfd-tuple
where ϕ 1 is

∃ t 1 t 2 t 3 IsBind Chk FD (R)) ( t 1 , t 2 ) ∧ Chk FD (R) pre ( t 1 , t 3 ) ∧ Succ(R) pre ( t 3 , t 2 )
and ϕ 2 is

∃ t 1 t 2 t 3 t 4 IsBind Chk FD (R)) ( t 1 , t 2 ) ∧ Beg(R) pre ( t 2 ) ∧ Chk FD (R) pre ( t 3 , t 4 ) Succ(R) pre ( t 3 , t 1 ) ∧ End(R) pre ( t 4 )
The sentence states that the current position has an access to a pair ( t 1 , t 2 ) that has not been checked before and such that: the access passes the test, and P red( t 1 , t 2 ) has been checked, where this denotes the predecessor in the lexicographic ordering: either t 1 paired with the predecessor of t 2 (as in ϕ 1 ) or the predecessor of t 1 and the final tuple (as in ϕ 2 ).

The sentence ϕ FD-end ends the check:

∃ t 1 t 2 IsBind Chk FD (R) ( t 1 , t 2 ) ∧ End pre ( t 2 ) ∧ ϕ allfd-tuple
We now construct the sentence ϕ CheckFds as ϕ FD-init ∧ Xϕ FD-next U ϕ FD-end thus will hold at a position iff there is a sequence of accesses after it verifying the FD for every pair ( t 1 , t 2 ).

The sentence ϕ CheckFdFailure , checking that the distinguished functional dependency σ = A ′ → B ′ fails, is simpler, since no iteration is needed:

∃ t 1 t 2 IsBind Chk FD (R) ( t 1 , t 2 ) ∧ Π A ′ ( t 1 ) = Π A ( t 2 )) ∧ ¬(∃ t 1 t 2 IsBind Chk FD (R) ( t 1 , t 2 ) ∧ Π B ( t 1 ) = Π B ( t 2 ))
The formula ϕ CheckIds checking that an inclusion dependency, e.g. mapping positions 1 . . . k of an R-tuple to positions m 1 . . . m k , is similar. The formula requires that the access path p make a single iteration over all individual tuples that have been revealed in the successor ordering, and for each such tuple u encountered, p must make some access (e.g. to a new relation) with some tuple v, also appearing in Succ(R), such that ⋀ i u i = v mi . Further details are spelled out in the proof of Theorem 6.2.

It is easy to check that the two invariants described earlier hold for this sentence.

VERIFIABLE SPECIFICATIONS: THE POSITIVE TRANSITION SUBLANGUAGE

The undecidability proof of AccLTL(FO ∃+ Acc ) makes use of the ability of the logic to enforce that an access is made to a binding that does not satisfy a certain relation. We now consider a restriction of AccLTL(FO ∃+ Acc ) which adds an additional monotonicity condition. A AccLTL(FO ∃+ Acc ) formula ϕ is binding-positive if every atom of the form IsBind( w) occurs only positively in ϕ -that is, under an even number of negations.

Definition 4.1. The logic AccLTL + is the set of binding-positive formulas in AccLTL(FO ∃+ Acc ). Note that in AccLTL + we can describe the most basic dataflow constraint, the property of an access path being grounded: an access is grounded iff for every transition in a path, for every value that occurs in a binding, it occurs in some relation in the instance prior to the access:

G ∃ x IsBind AcM (x 1 . . . x m ) ∧ ⋀ i ≤ m ⋁ R ∈ Sch ∃ y R(y 1 . . . y n ) ∧ ⋁ j ≤ n y j = x i
Thus we can reduce satisfiability over grounded instances to satisfiability over all instances. Furthermore all the examples in the introduction are expressible in this fragment; we can express relevance of an access to a query as well as containment of queries under access patterns, restricting the paths to satisfy many data integrity, dataflow, and access ordering restrictions.

Our next main result is that this restriction suffices to give decidability: THEOREM 4.2. Satisfiability of AccLTL + is decidable in 3EXPTIME. The same is true for satisfiability over grounded instances and satisfiability over idempotent and exact accesses.

Access Automata, their analysis, and connection with AccLTL +

We will show Theorem 4.2 by going through another specification formalism of interest in its own right, a natural automaton model for access paths. These are Accessautomata (A-automata for short), which run over access paths, using a finite set of control states. At each transition (I, (AcM, b), I ′ ) of an access path the evolution function of the automaton specifies what new states (if any) it can move to at the next position. The evolution function is a relational query that makes use of the binding, pre-and post-condition of the transition.

Definition 4.3 (A-Automaton).

Let Sch be a schema, Sch Acc the corresponding schema with accesses (as defined in Section 2), and C a set of constants. An Accessautomaton (A-automaton for short) over (Sch, C) is a tuple (S, s 0 , F, δ) where -S is a finite set of states, s 0 ∈ S is an initial state, F ⊆ S is a set of accepting states δ is a finite set of tuples of the form (s, ψ -∧ψ + , s ′ ) where s, s ′ are states, ψ + is a FO ∃+ Acc sentence, while ψ -is a positive boolean combination of negated FO ∃+ Acc sentences that cannot mention the predicate IsBind; all these formulas can use constants in the given set C. Figure 2 shows an A-automaton. The automaton will stay in its initial state until an access is done using access method AcM 1 using a binding x such that R(x, x) holds, at which point it will transition to a new state. After that the access path must consist of a sequence of accesses to AcM 1 , terminating in an access on method AcM 2 with binding x, which must lead to a final configuration in which S(x) holds.

Let A = (S, s 0 , F, δ) be an A-automaton and let p be a path t 1 , . . . , t n through the LTS associated with Sch, where t i = (I i , (AcM i , bi ), I i+1 ). A run of A on p assigns to every t i a tuple δ i of the form (s i , ϕ i , s i+1 ) in δ so that the relational structure M (t i ) associated with t i satisfies ϕ i . A run of A is further said to be accepting iff its first state is initial and its last state is accepting. The language L(A) accepted by an A-automaton A is the set of access paths for which there is an accepting run. Note that an automaton only accepts access paths, which by definition must satisfy at least the property that for each i, I i+1 extends I i solely by adding tuples to the relation of AcM i , and all tuples added are consistent with the binding on the input positions of AcM i . The definition of L(A) can be further qualified to account for other sanity conditions (e.g. exactness).

A-automata are powerful enough to directly express relevance of an access in the presence of dataflow restrictions as well as disjointness constraints: PROPOSITION 4.4. Let Q and Q ′ be two positive queries, ACS a set of access methods, and Σ a set of disjointness constraints. One can efficiently produce an A-automaton A such that Q is contained in Q ′ under limited access patterns with disjointness constraints iff the language recognized by A is empty. A similar statement holds for longterm relevance of an access to Q under disjointness constraints.

PROOF. We denote by Q post and Q ′ post the queries derived from Q and Q ′ by replacing any atom R(x) in them by R post (x). Let A be an A-automaton with two states s 0 and s 1 . The initial state is s 0 and the accepting state is s 1 . For any disjointness constraint σ between R and S, let ϕ σ be the following conjunctive query, which states that the disjointness constraint is violated.

ϕ σ = ∃x, y R post (x) ∧ S post (y).
Then the transitions are

δ(s 0 , s 0 ) = ⋀ σ∈Σ ¬ϕ σ ∧ ¬Q ′ post δ(s 0 , s 1 ) = ⋀ σ∈Σ ¬ϕ σ ∧ ¬Q ′ post ∧ Q post
It is easy to see that each instance I resulting from an access (AcM, b) to I ′ satisfies Σ iff (I ′ , (AcM, b), I) satisfies ⋀ σ∈Σ ¬ϕ σ . The last instance resulting from a sequence of accesses ρ satisfies Q and ¬Q ′ iff the transition of ρ satisfies ¬Q ′ post ∧ Q post .

The proposition above can be extended to a general result stating that high-level logical specifications can be compiled into A-automata. We say that an A-automaton A is equivalent to an AccLTL sentence ϕ if the language of ϕ is the same as the language of A. The following result shows that each AccLTL + formula can be converted into an A-automaton. LEMMA 4.5. For each AccLTL + formula ϕ there is an equivalent A-automaton of size exponential in the size of ϕ.

The proof relies on a conversion of propositional LTL formulas over finite words to finite state automata, plugging in the appropriate formulas for propositions.

PROOF. Let an AccLTL + formula ϕ be given. We will translate ϕ into an Aautomaton in several steps. In the first step we translate ϕ into an LTL formula (without embedded first order formulas). Let Φ be the set of maximal FO ∃+ Acc subformulas of ϕ and let P be a set of propositions that contains a proposition P χ for every χ ∈ Φ. We denote by φ the LTL formula that is obtained from ϕ by replacing each subformula χ ∈ Φ by P χ . Note that φ accepts words over the alphabet 2 P . We also transform an access path p = (I 1 , AC 1 , I ′ 1 ), . . . , (I n , AC n , I ′ n ) into a word p = S 1 , . . . , S n over the finite alphabet 2 P in which S i is the set of all predicates P χ such that χ holds on (I i , AC i , I ′ i ), i ≤ n. With these definitions, the following proposition is obvious: PROPOSITION 4.6. For every AccLTL + formula ϕ and every access path p, ϕ holds on p iff φ holds on p.

We will call a propositional symbol P χ even in φ if each occurrence of P χ in φ is under an even number of negations. We will later exploit that, by definition of AccLTL + , every atom IsBind AcM must occur under an even number of negations in ϕ. Hence if χ contains IsBind AcM then P χ is even in φ. We next show that φ has a certain monotonicity property with respect to even symbols.

Given a word w = S 1 , . . . , S n , a position i ≤ n and a proposition P ∈ P, we define w P,i = S 1 , . . . , S i-1 , S i ∪ {P }, S i+1 , . . . , S n . PROPOSITION 4.7. Let ϕ be an LTL formula and let P be an even propositional symbol in ϕ. Then for all words w over 2 P and positions i ≤ n, if w is a model of ϕ then w P,i is a model of ϕ.

PROOF. We show for all words w and positions i, j in w, that if (w, j) is a model of ϕ then (w P,i , j) is a model of ϕ. We show this statement by induction on ϕ. Fix some word w = S 1 . . . S n , some i, j ≤ n, and assume that w, j ⊧ ϕ. If ϕ is a propositional symbol P that occurs in S i then the statement is clearly true. If P does not occur in S i then i must be distinct from j and the statement is trivial. The case that ϕ is of the form ¬P is not possible because otherwise P would not be even. The cases where ϕ is of the form Xψ, Fψ of ψU ψ ′ follow from the induction hypothesis.

Combining the previous proposition with a standard construction taking propositional temporal logic (see the online appendix), we get that φ can be converted to a finite automaton: PROPOSITION 4.8. φ is equivalent (or all words over 2 P ) to a non-deterministic automaton M of size at most exponential in φ. In addition, M can be taken to have the property: if (p, S, q) is a transition in M and if P is even in φ, then (q, S ∪ {P }, q) is a transition in M .

In the next step we modify M by simply replacing the propositional formulas by the first order formulas they represented, reversing the abstraction process used to go from ϕ to φ. This process will produce a mild variation of our prior automata model for access paths that we define next, which we refer to these as FO-automata; these are simply a generalization of A-automata that do not have restrictions concerning formulas containing the predicate IsBind AcM . Formally, an FO-automaton consists of a finite set of states Q, an initial state q 0 ∈ Q, a set F ⊆ Q of accepting states, and a set δ of transitions of the form (p, ϕ, q) where p, q ∈ Q and ϕ is a boolean combination of FO ∃+ Acc sentences. The notions of (accepting) runs and accepted language are exactly as those for A-automata.

We create an FO automaton F from M as follows: F has the same states as M , and the initial and accepting states are also the same. The transitions of F are obtained from the transitions of M by replacing each set S on a transition by the formula ψ -∧ψ + where

ψ -= ⋀ Pχ ∉ S ¬χ ψ + = ⋀ Pχ ∈ S χ
From the definition of φ, on can se that for every access path p, ϕ holds on p iff M accepts p.

In general F will contain transitions that are labelled by subformulas ψ ∧ ¬ψ ′ where ψ ′ ∈ Φ is an FO ∃+ Acc formula that contains the predicate IsBind AcM . Recall that by definition of an A-automaton the predicate IsBind AcM can only occur under an even number of negations. Hence, F is not an A-automaton in general. However, we now show that F is equivalent to an A-automaton A. Let (p, ψ ∧ ¬ψ ′ , q) be a transition of F for which ψ ′ ∈ Φ is an FO ∃+ Acc formula that contains the predicate IsBind AcM . Recall that we argued previously that in this case P ψ ′ must be even. Hence, it follows from Proposition 4.8 and from the way that F is obtained from M that F also contains the transition (p, ψ ∧ψ ′ , q). Thus if we replace the transition (p, ψ ∧¬ψ ′ , q) by (p, ψ, q) we do not change the accepted language. Repeating this transformation, we obtain an A-automaton A equivalent to F .

We still need to verify that A has size at most exponential in ϕ. This is the case because the only blow-up in the above construction occurs in Proposition 4.8.

We will show that emptiness of A-automata is decidable. Note that this decidability result together with Lemma 4.5 completes the proof of Theorem 4.2. THEOREM 4.9. Emptiness of A-automata is decidable in 2EXPTIME. The same holds if accesses are restricted to be exact or idempotent.

Notice that from Theorem 4.9 and Proposition 4.4 we get a 2EXPTIME upper bound for containment and long-term relevance. This improves on the prior known bounds [START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF][START_REF] Calì | Conjunctive query containment under access limitations[END_REF].

In the body of the paper, we give the proof only for general paths. The discussion of how to extend to exact and idempotent accesses is left to the online appendix. The proof uses a tight connection between A-automata and the containment problem for Datalog queries within positive first-order queries. This connection can also be exploited to give a corresponding lower bound: THEOREM 4.10. Emptiness of A-automata and satisfiability of AccLTL + are both 2EXPTIME-hard.

These results are the most involved in the paper, and will be developed over the next few subsections.

We reduce the emptiness problem for A-automata to the problem of whether a Datalog program is contained within a positive first-order query. The reduction to this problem in turn involves several stages, and the first step goes through a syntactic subclass of A-automata, called "linear A-automata", defined below. We will show that the problem of testing emptiness of A-automata can be reduced to checking the emptiness of a bounded number of linear A-automata. We will prove that the emptiness of a linear A-automaton can be reduced to the containment of a datalog program into a positive sentence.

First step: Reduction to A-Automata of a special form

We now present the reduction of non-emptiness test for A-automata to a simpler automaton model called linear A-automaton. The binding-positive restriction plays a role in the reduction of the emptiness of an A-automaton to the emptiness of linear A-Automata. This restriction also helps in the reduction of the nonemptiness problem for linear A-automaton to the containment problem for a Datalog program in a positive sentence.

Before giving the definitions, we need to present some notation. Let ϕ be a formula over a schema Sch. Then by post(ϕ) we denote the formula obtained from ϕ by subscripting the relations of ϕ by post.

Let ψ be a sentence over a schema Sch such that ψ is a conjunction of a positive sentence and a positive Boolean combination of negated positive sentences. We denote by (i) ψ + the positive sentence in the conjunction ψ, (ii) ψ -the positive Boolean combination of negated positive sentences in the conjunction ψ. The same notation is used for sentences in FO ∃+ Acc . Let θ be the conjunction of a positive Boolean combination of negated positive sentences in FO ∃+ Acc which have no predicates IsBind AcM and of a positive sentence in FO ∃+ Acc . We denote by Sch(θ) the formula over Sch obtained by replacing any relation name R pre or R post by the relation name R and by replacing the atom IsBind AcM (x) by True. We can observe that Sch(θ) is a conjunction of a positive sentence and a positive Boolean combination of negated positive sentences; furthermore, Sch(θ

+ ) = Sch(θ) + and Sch(θ -) = Sch(θ) -.
Let LTrans be the LTS associated with Sch. Let ψ and ϕ be two sentences in FO ∃+ Acc . ψ implies ϕ over LTrans iff for each LTrans transition t, if t satisfies ψ then t satisfies ϕ. The main difference from ordinary implication is that we consider only LTrans transitions (I, (AcM, b), I ′ ). For valid transitions we always have I is included in I ′ . For example the formula ψ = ∃xR pre (x) ∧ S post (x) does imply the formula ϕ = ∃xR post (x) ∧ S post (x) over LTrans; however, ψ does not imply ψ over general instances over Sch Acc . Definition 4.11 (Linear A-automaton). An A-automaton A is linear iff the following conditions hold:

(Singleton). Every strongly connected component (SCC) of A consists of only one state.

(Deterministic-Access-Method). For any transition (s, ϕ, s ′ ) ∈ δ, ϕ + is a formula of the form ∃x IsBind AcM (x) ∧ ψ(x) where ψ(x) is a formula of FO ∃+ Acc without any atom of the form IsBind AcM ′ (ȳ). (Deterministic-Transition).

-The states of A are linearly ordered by the reachability relation. That is, they can be ordered as s 1 , . . . , s h , such that for each i < h, there is exactly one transition from the state s i to s i+1 . -Note that from requirement (Deterministic Access Method), the formula ϕ + is of the form ∃x IsBind AcM (x) ∧ ψ(x) such that ψ is a positive formula of FO ∃+ Acc which does not have any atom of the form IsBind AcM ′ (ȳ). We further require that for each transition (s i , ψ, s i+1 ) of A, there exists a vector of constants c and a sentence ϕ such that ψ(x) = (x = c) ∧ ϕ.

A:18

Therefore, ϕ + is equivalent to the formula IsBind AcM (c) ∧ ϕ. We recall that ϕ is a FO ∃+ Acc formula having no predicates IsBind AcM ′ . (Negative-Invariant). For each state s, there exists a positive Boolean combination of negated positive sentences over Sch, denoted by Ω(s), such that for each transition (s ′ , ψ, s) of A, ψ -implies post(Ω(s)) over LTrans. If s ′ = s, then we also require that post(Ω(s)) implies ψ -over LTrans. (Initial-Final-State). The initial state is the state s 1 and the accepting state is s h .

The number h is called the height of A and is denoted by height(A).

The first few requirements state that the automaton consists of a line of states with self-loops, with the transitions that change states using constants symbols, and each transition fixing an access method. Condition (Negative Invariant) imposes that the negative properties in transition formulas, which a priori mention the pre-and postversion of the transition, can be reduced to enforcing that some negative properties hold invariantly on all instances visible while in the state. Restating it slightly, it states that each state s of a linear A-automaton A is associated with a positive Boolean combination of negated positive sentences, Ω(s), such that: (NegativeInv +) If (s, ψ, s) is a transition of A and instance I satisfies Ω(s), then for any LTrans transition t = (I ′ , (AcM, b),

I ′′ ), if I ′ ⊆ I ′′ ⊆ I then t satisfies ψ -. (NegativeInv †) If (s, ψ, s ′ ) is a transition of A and an LTrans transition (I, (AcM, b), I ′ )
satisfies ψ then I ′ satisfies Ω(s).

The following lemma shows that an A-automaton corresponds, up to emptiness, to unions of linear A-automata. LEMMA 4.12. Let A be an A-automaton. Then, there exists a set {A i } 1≤i≤n of linear A-automata such that for each

1 ≤ i ≤ n, A i has size polynomial in the size of A, n is exponential in A and L(A) is empty iff L(A 1 ) ∪ . . . ∪ L(A n ) is empty.
The statement hold both for the general path semantics and for restricted (exact/idempotent) paths. The proof is presented in the online appendix. Note that Condition (Deterministic-Access-Method) can be assured by simply breaking up a single transition into multiple transitions, each of which commits to a single access.

From Emptiness of linear A-automata to Containment of Datalog in Positive Queries: statement of main results

We now proceed to show that emptiness of a linear A-automata is decidable. Together with Lemma 4.12, this implies the decidability of emptiness for (general) A-automata. This will involve reducing the emptiness of a linear A-automaton to the problem of whether a Datalog program is contained in a positive first order logic sentence.

Recall that a Datalog program is defined with respect to two database schemas, called the extensional schema, denoted by Sch ext and the intentional schema, denoted by Sch int . A Datalog program P is a finite set of rules of the form "head ∶-body" where head is an atomic formula R(x) with a relation symbol R in the intentional schema, and where body is a conjunctive query that can use relation symbols from the intentional and the extensional schema. Each Datalog program P contains a distinguished goal predicate. We use the standard notions of the least fixed point of a Datalog program P on a database D (see [START_REF] Abiteboul | Foundations of Databases[END_REF]), and we denote this fixed point by P f ull (D). We say that a Datalog program P accepts a database D if the goal predicate of P is not empty in P f ull (D).

LEMMA 4.13. Let A be a linear A-automaton. Then there exists a Datalog program P A and a positive first order logic sentence P ′ A such that L(A) is not empty iff P A is not contained in P ′ A . One can construct these in polynomial time in the size of A.

The proof of this lemma is complex, and will take up the bulk of the remainder of the section.

Let A = (S, s 1 , {s h }, δ) be a linear A-automaton, with the set of states S = {s 1 , . . . , s h }, where the indexing representing a linear-order of the single-state components.

The basic idea of this proof is that P A enforces the positive constraints of A while P ′ A enforces the negative constraints. Recall that in a linear automaton, a run always proceeds through the same sequence of states. Let ρ be an LTrans path and r be an accepting run on ρ. The extensional database D will have predicates BackgroundR i representing the part of relation R that becomes visible when doing a transition from the i th state to itself and predicates IntBackgroundR i representing the data that becomes visible when crossing from the i th state to the (i + 1) st state. The important intentional predicates ViewR i will represent intermediate stages of the predicates BackgroundR i within the evolution of each state. The Datalog program P A will have rules corresponding to the evolution of ViewR i by adding tuples from BackgroundR i and IntBackgroundR i-1 . To ensure that the tuples in ViewR i correspond to some valid binding, P A will have rules guaranteeing that only tuples that satisfy the appropriate formulas can be added to ViewR i . We can do this with a Datalog program by adding appropriate intermediate relations, exploiting the fact that the constraints on the guards are positive, and hence represented in non-recursive Datalog.

The role of the positive query P ′ A is to enforce the negated conjunctive queries in the transitions -in particular, P ′ A will contain constraints on the relations BackgroundR i and IntBackgroundR i that enforce that these only contain tuples that satisfy these negated constraints. We give the formal definition of P A and P ′ A in Subsection 4.4 below.

In the proof that our construction is correct, we show that the Datalog program P A can be decomposed into subprograms P 1 , . . . , P h that correspond to the states s 1 , . . . , s h of A in the following sense: Whenever an A-automaton has a run that ends in state s i , i ≤ h then the subprogram P 1 ∪ . . . ∪ P i of P adds tuples to the intentional database that correspond in a certain way to the tuples that A has obtained using accesses while arriving at s i . The formal proof is in Subsection 4.5 below.

The reduction from A-automata non-emptiness to query containment: Construction of the Datalog Program and the Positive Query

We give the construction of the Datalog program P A and the positive query P ′ A required by Lemma 4.13. 4.4.1. The Program P A . We define a Datalog program P A over the extensional schema Sch ext that contains for each R ∈ Sch and 1 ≤ i ≤ height(A), a relation BackgroundR i , and for each R ∈ Sch and 0 ≤ i ≤ height(A) -1 a relation IntBackgroundR i ; the arity of both relations is equal to the arity of R. Finally, Sch ext contains for each access method AcM, a relation Bind AcM of arity equal to the size of Inp(AcM).

The intentional schema Sch int of P A contains: -for each R ∈ Sch and 1 ≤ i ≤ height(A), the predicate ViewR i whose arity is the arity of R; -for every 1 ≤ i ≤ height(A), a predicate ReachC i of arity of 0; -for each R ∈ Sch, 1 ≤ i ≤ height(A), for each access method AcM such that Rel(AcM) = R, a predicate Answer(AcM) i with arity equal to the sum of the arity of R and the size of Inp(AcM); and also a predicate IntAnswer(AcM) i-1 with arity equal to the sum of the arity of R and the size of Inp(AcM). -for each access method AcM ∈ Sch and 1 ≤ i height(A), a predicate Done-Access i AcM and a predicate IDone-Access i AcM both of arity equal to the size of Inp(AcM)

The goal predicate of P A is ReachC h where h = height(A).

Recall that an access path of a linear Automaton of height h will break up into h -1 transitions which correspond to changing components, plus h subpaths representing looping within a component. The Datalog program conjoined with negation of the UCQ will accept databases that code such paths.

-Any relation R in the background database that the A-automaton A accesses will be equal to the union of the relations BackgroundR 1 , . . . , BackgroundR h , h = height(A), along with the relations IntBackgroundR 0 , . . . In this Datalog program, we allow the use of "extended rules" where the body ϕ( x) is a positive query. We require that the extended rules use in their body a guarded safe positive formula; a formula ϕ(x) that is the conjunction of a positive formula ϕ 2 (x) with a conjunctive query ϕ 1 (x) such that every free variable of ϕ 2 (x) is included in some relational atom of ϕ 1 (x). We allow a vacuous case consisting of a positive formula with no free variables. The extension of the semantics of Datalog to this case is obvious. One can also see that this class of formulas is closed under conjunction.

Rules for predicates ViewR i . We now define the rule for the predicates ViewR i . For i > 0, for each relation R ∈ Sch, for each access method AcM such that Rel(AcM) = R,

ViewR i (z) ∶-Done-Access i AcM (x), Answer(AcM) i (x, z) ViewR i (z) ∶-IDone-Access i AcM (x), IntAnswer(AcM) i (x, z) For each relation R ∈ Sch, ViewR 0 (x) ∶-IntBackgroundR 0 (x)
Rules for predicates Done-Access i AcM . We consider two kinds of transitions: the loop transitions going from one state to itself and the crossing transitions going from one state to another state.

Rule for loop transitions. Let d = (s i , ψ d , s i ) be a loop transition. Due to Condition (Deterministic-Access-Method), there exists an access method AcM such that ψ d + is equal to ∃x IsBind AcM (x) ∧ ρ d (x), where ρ d does not contain any atom with relation name IsBind AcM ′ .

The formula ValidBind d (x), where x are the free variables, is obtained from ψ d as follows:

-The atom IsBind AcM (x) is replaced by Bind AcM (x).

-Each atom T pre (ȳ) is replaced by ⋁ j≤i ViewT j (ȳ), where s i is the state referenced in

d -Each atom T post (ȳ) such that T is different from R is replaced by ⋁ j≤i ViewT j (ȳ),
where s i is the state referenced in d. We are now ready to give the rule associated with this transition from s i to itself:

-Each atom R post (ȳ) is replaced by Answer(AcM) i (x, ȳ) ∨ ⋁ j≤i ViewT j (ȳ),
Done-Access i AcM (x) ∶-ReachC i , ValidBind d (x)
Since ValidBind d is a guarded safe positive formula, the rule uses a guarded safe positive formula. Rule for ReachC i . The predicate ReachC 1 is always true. Let i be an integer strictly greater than 1. Let d = (s i-1 , ψ d , s i ) be a transition. Due to Condition (Deterministic-Transition), there exists one access, denoted by (AcM, b), such that the positive part (ψ d )

+ is equal to IsBind AcM ( b) ∧ ρ d for some ρ d . We define the predicate ReachC i to be true iff the sentence IsValidBinding d is true and the predicate ReachC i-1 is true, where the sentence IsValidBinding d is obtained from (ψ d )

+ by performing the replacements below:

-the atom IsBind AcM (x) is replaced by Bind AcM ( b), -each atom T pre (ȳ) is replaced by ⋁ j<i ViewT j (ȳ), -each atom T post (ȳ) where T is different from R is replaced by ⋁ j<i ViewT j (ȳ), -each atom R post (ȳ) is replaced by IntAnswer(AcM) i-1 ( b, ȳ) ∨ ⋁ j<i ViewR j (ȳ), where R is equal to Rel(AcM).
Due to the fact that ψ d + is a sentence, IsValidBinding d is a guarded safe positive formula.

It will turn out (see Claim 2) that sentence IsValidBinding d is true on an input instance D for the Datalog program iff the access transition (I, (AcM, b), I ′ ) satisfies ψ d + , where for each R ∈ Sch, the tuples in I(R) are those in any of the sets of tuples P f ull A (D)(ViewR k ), for k less or equal to i and I ′ (R) is the union of I(R) and the wellformed output of (AcM, b) on D(IntBackgroundR i-1 ).

Rules for IntAnswer(AcM) i and Answer(AcM) i . Let i be an integer greater than 0, R be a relation of Sch and AcM an access method of Sch such that Rel(AcM) = R. Let ȳ and x be two vectors of variables such the length of ȳ is equal to the arity of R and the length of x is equal to the size of Inp(AcM). We say ȳ = y 1 . . . y e is compatible with AcM and x if x consists of the y i corresponding to input positions of AcM in increasing order.

We have the rules:

IntAnswer(AcM) i (x, ȳ) ∶-IntBackgroundR i (ȳ)
where ȳ is compatible with AcM and x.

Answer(AcM) i (x, ȳ) ∶-BackgroundR i (ȳ)
where ȳ is compatible with AcM and x.

The positive query P ′

A . We now give the construction of the positive query P ′ A . Let i be an integer less than h. Let Φ - i be the smallest set containing the following formulas: -Φ - i contains the formula Ω Datalog (Ω(s i )) that is obtained from Ω(s i ) by replacing each atom R(x) by

⋁ j ≤ i BackgroundR j (x) ∨ ⋁ j ≤ i-1 IntBackgroundR j (x); -for the transition (s i-1 , ϕ, s i ) of A, Φ - i contains the formula Ω Datalog (ϕ -) that is obtained from ϕ -by replacing each atom R pre (x) by ⋁ j ≤ i-1 BackgroundR j (x) ∨ ⋁ j ≤ i-2 IntBackgroundR j (x)
and each atom R post (x) by

⋁ j ≤ i-1 BackgroundR j (x) ∨ ⋁ j ≤ i-1 IntBackgroundR j (x)
We define P ′ A to be dual(⋀ i ≤ h Φ - i ) where h = height(A). For a propositional formula ρ, dual(ρ) is its DeMorgan dual. Note that P ′ A is a positive formula, as the DeMorgan dual of a formula is equivalent to its negation. Thus a structure that satisfies the negation of the positive query will need to satisfy the translation of the negative invariants to the Datalog schema.

4.4.3. From "extended Datalog program" to Datalog program. We finish this subsection with a lemma explaining that allowing positive formulas in the body of the rules of a Datalog program was only syntactic sugar. LEMMA 4.14. Let P be an "extended Datalog program", allowing guarded safe positive formulas, even allowing equality predicates in the body of the rules of P. Then there exists a classical Datalog program P ′ of size polynomial in the size of P such that for any instance I, I satisfies P iff I satisfies P ′ . PROOF SKETCH. First, we remove the equality predicate from the extensional schema and we add a corresponding predicate Equal to the intentional schema. The only rule associated with the intentional relation Equal is Equal(x, x) ∶ -Adom(x). This rule uses a new intentional predicate Adom, and we thus add rules to define this. Intuitively, all the values belonging to an instance appear in the relation Adom.

The rules for the relation Adom are of the form Adom(x j ) ∶ -BackgroundR i (x) or Adom(x j ) ∶ -IntBackgroundR i (x) or Adom(x j ) ∶ -Bind AcM (x) where i is less than h and j is an integer. For each constant c in C, the rule Adom(c) ∶ -is added. The remainder of the lemma follows from the folklore theorem that any guarded safe positive query can be rewritten into an non-recursive equivalent Datalog program of size polynomial in the size of the positive query.

From the containment of the Datalog program in the positive query to emptiness of the linear progressive automaton

We consider the Datalog program P A constructed from the linear A-automaton A in Lemma 4.13. We will show that if there is a database D that is a model of P A but not of P ′ A , then A has an accepting run over the database instance Sch(D) for the original schema Sch, where Sch(D) is such that for each relation R ∈ Sch, the tuples in

Sch(D)(R) are those in ⋃ k≤height(A) D(ViewR k ).
This subsection is split in four parts. The first part makes the link between the satisfaction of the formula appearing in the transitions of A and the formula appearing in the rule of P A and P ′ A . The second part explains that the P A can be decomposed into an equivalent sequence of datalog programs. The third part is concerned with the construction of partial LTrans paths associated with each of the subprograms built in the previous part. The last part explains how to use the partial LTrans paths to obtain an accepting LTrans path. Given database K over schema Sch, an integer i and a set of facts M of the relation R, we define -by K + M the instance over Sch such that:

-for each T different from R, the tuples in K + M (T ) are those in K(T ), -the tuples in K + M (R) are those in K(R) along with those associated with the facts in M .

CLAIM 1. Let: -Sch be a schema, -A be a linear A-automaton, d = (s i , ψ, s i ) be a transition of A, -AcM be the access method associated with ψ following Condition (Deterministic-Access-Method), -b be a binding of AcM, -ValidBind d be the formula obtained from d in the construction of P A , -I be an instance of Sch and K 1 , ⋯, K i be a set of instances of Sch such that K i ⊆ I, -K be the union of K j (that is, each relation symbol in K is interpreted by the union of the interpretations in K j ), -D be the database instance for the Datalog schema in which (i) each relation ViewR The proof of this claim is from unwinding the definition of ValidBind d . For completeness, it is proven in detail in the online appendix.

The second claim analogously gives the relationship between the formula ψ + of a transition d of the form (s i-1 , ψ, s i ) (that is, between components) and the formula IsValidBinding d . CLAIM 2. Let: -Sch be a schema, -A be a linear A-automaton, d = (s i-1 , ψ, s i ) be a transition in A from s i-1 to s i , -AcM and b be the unique access method and the binding associated with ψ + following Condition (Deterministic-Transition), -IsValidBinding d be the formula built from d in the construction of P A , -I be an instance of Sch and K 1 , ⋯, K i-1 be a set of instances of Sch, -K be the union of the K k , -D be a database instance for the Datalog Schema in which (i) each relation The proof of this claim also comes from simply unwinding the definition of ValidBind d , and is analogous to the proof of the previous claim.

ViewR j , j ≤ i -1, of D is interpreted as in the relation R of K j ; (ii) each relation IntAnswer(AcM) i-1 is
For the next two claims, we need the following definition. Let Sch be a schema, D be an instance over Sch ext and i and j be integers. Let I D,i,j be the instance over Sch such that for each relation name R, the tuples in I D,i,j (R) are the tuples in

⋃ m≤i D(BackgroundR m ) ∪ ⋃ k≤j D(IntBackgroundR k ).
The third claim is concerned with the relationship between the satisfaction of Ω(s i ) and the satisfaction of Ω Datalog (Ω(s i )). We recall that Ω(s i ) is a Boolean combination of negated positive sentences over Sch, where s i is the i th state of A. The sentence Ω Datalog (Ω(s i )) is obtained from Ω(s i ) by replacing each atom R(x) by

⋁ j ≤ i BackgroundR j (x) ∨ ⋁ j ≤ i-1 IntBackgroundR j (x); CLAIM 3. Let:
-Sch be a schema, -A be a linear A-automaton, s i be the i th state of A, -D be an instance over Sch ext Then Ω(s i ) is satisfied by

I D,i,i-1 iff Ω Datalog (Ω(s i )) is satisfied by D.
The proof of this claim is also basically by definition, in this case using the definition of Ω Datalog (Ω(s i )).

Let (s i-1 , ψ, s i ) be the transition from the i-1 st state and the i th state of A. The fourth and last claim of this subsubsection is concerned with the relationship between the formula ψ -and Ω Datalog (ψ -). We recall that the formula ψ -is a Boolean combination of negated positive sentences over Sch Acc and these sentences do not have any atom of the form IsBind AcM (x). The sentence Ω Datalog (ψ -) is obtained from ψ -by replacing each atom R pre (x) by

⋁ j ≤ i-1 BackgroundR j (x) ∨ ⋁ j ≤ i-2 IntBackgroundR j (x)
and each atom R post (x) by

⋁ j ≤ i-1 BackgroundR j (x) ∨ ⋁ j ≤ i-1 IntBackgroundR j (x) CLAIM 4. Let:
-Sch be a schema, -A be a linear A-automaton, d = (s i-1 , ψ, s i ) be the transition of A from the state s i-1 to the state s i , -(AcM, b) be the access associated with the transition d, -D be a database over Sch ext Then ψ -is satisfied by

(I D,i-1,i-2 , (AcM, b), I D,i-1,i-1 ) iff Ω Datalog (ψ -) is satisfied by D.
The proof of this claim follows from the definition of Ω Datalog (ψ -).

4.5.2. Decomposition of the Datalog program P A . The next claim shows that P can be decomposed into subprograms P 0 , P 0,1 , P 1 , P 1,2 , P 2 . . . , P h , h = height(A), that can be evaluated "in sequence": (i) the program P 0 contains the rules related to predicate Answer(AcM) j and IntAnswer(AcM) j for any access method AcM and any integer j less or equal to h; (ii) letting i be an integer between 1 and h, the Datalog program P i-1,i contains all rules of P A related with the transition from s i-1 to s i , in particular the rules related to ReachC i and the Datalog program P i contains all the rules of P A related with the transitions from s i to itself in A.

CLAIM 5. P f ull A (D) = P f ull h (P h-1,h (P f ull h-1 (. . . P f ull 1 (P f ull 0 (D)) . . .)))
for every database D over the extensional schema of P A .

PROOF OF CLAIM 5. It is obvious that the right hand side is included in the left hand side. The other direction follows from the fact that if head ∶-body is a rule in P i then body contains only atoms that appear as heads of rules in P 0 ∪ P 1 ∪ . . . ∪ P i . -D j i is the instance equal to P f ull,j i (D i-1,i ) Thus D i is the result of performing the first i stages of the Datalog program until they reach a fixed point, J →si (D) is the instance obtained on the Datalog schema corresponding to entering state s i , D j i is the result of performing the first i -1 stages completely followed by j iterations of the i th stage of the Datalog program. We consider in this paper a non-deterministic semantics of Datalog evaluation. At each iteration, only one new fact is added. Recall that Sch(D ′ ) for any D ′ above is the translation of these to the original schema.

The construction of the LTrans path accepted by A is done in several steps. The first step, Lemma 4.15, concerns creating the transitions that jump between components. It shows that for each i > 1, if D i (ReachC i ) is true then there exists a LTrans transition t from the instance Sch(D i-1 ) to the instance J →si (D), such that t satisfies the formula of the transition of A going from the i -1 st state to the i th state. The second lemma, Lemma 4.16, shows that when the Datalog program adds certain tuples, then there is a corresponding path consisting of self-loops in the automaton that adds these tuples. Formally, it shows that for each i ≥ 1 if D i (ReachC i ) is true and Sch(D i ) -J →si (D) is true, then there exists a LTrans path ρ from J →si (D) to Sch(D i ) and a run r on ρ from s i to itself. The subpaths and subruns obtained from the two lemmas are concatenated to obtain a path accepted by A.

We now prove our first lemma about mimicking Datalog instances by schema instances that are reachable via runs of the automaton. LEMMA 4.15. Let: -Sch be a schema, -A = (S, s 1 , F, δ) be a linear A-automaton, -P A and P ′ A be the Datalog program and the positive sentence obtained from A, -D be an instance over Sch ext . D does satisfy P A and D does not satisfy P ′ A , i be an integer strictly greater than 1, d = (s i-1 , ψ, s i ) be the transition of A from the i -1 st state to the i th state If D i (ReachC i ) is true then there exists a LTrans transition t from the instance Sch(D i-1 ) to the instance J →si (D) and this transition satisfies ψ.

PROOF OF LEMMA 4.15. We assume that D i (ReachC i ) is true. Let (AcM, b) be the access associated with d following Condition (Deterministic-Transition). Let t be the LTrans transition equal to (Sch(D i-1 ), (AcM, b), J →si (D)): one can easily see that this is an LTrans transition. The lemma is proven in two steps: first we show that t satisfies ψ + , then we prove that t satisfies ψ -.

Satisfaction of ψ + . We recall that IsValidBinding d is the formula built from ψ + in the construction of P A , obtained from ψ + as follows:

-The atom IsBind AcM (x) is replaced by Bind AcM ( b).

-Each atom R pre (ȳ) is replaced by ⋁ j<i ViewR j (ȳ).

-Each atom R post (ȳ) is replaced by IntAnswer(AcM) i-1 ( b, ȳ) ∨ ⋁ j<i ViewR j (ȳ).

Let AcM be the access method associated with the transition d. We define by K D the following instance: -for each relation T which is different than Rel(AcM), K D (R) contains the tuples in

⋃ j<i D i-1 (ViewT j ), -for the relation R which is equal to Rel(AcM), K D (R) contains the tuples in ⋃ j<i D i-1 (ViewR j ) ∪ D 0 (IntAnswer(AcM) i-1 ). Because D i (ReachC i ) is true, IsValidBinding d is satisfied by K D . Also re- call that J →si (D) is the instance obtained from Sch(D i-1 ) by performing the access (AcM, b) in any instance I ′ such that I ′ (Rel(AcM)) is inter- preted as in D(IntBackground(Rel(AcM)) i-1 ). By Claim 2, ψ + is satisfied by (Sch(D i-1 ), (AcM, b), J →si (D)).
Satisfaction of ψ -. Because D does not satisfy P A ′ , D satisfies Ω Datalog (ψ -). Due to Claim 4, ψ -is not satisfied by (I D,i-1,i-2 , (AcM, b), I D,i-1,i-1 ). We deduce that J →si (D) is included in I D,i-1,i-1 . Thus by monotonicity of ψ -, t satisfies ψ -.

We can conclude that t satisfies ψ.

We denote by Access j i the set of accesses (AcM, b) such that b is in D j i (Done-Access i AcM ( b)). We can associate a total order in these accesses such that

(AcM, b) is less than (AcM ′ , b′ ) iff for each k ≤ j, if (AcM, b) is in Access k i then (AcM ′ , b′ ) is in Access k i .
The next lemma explains how to build a LTrans path that adds the same tuples that appeared in the ViewR i relations during the j th iteration of P i .

In the following lemma, we use the notation P 0 i (D) which is equal to D. LEMMA 4.16. Let -Sch be a schema, -LTrans be the LTS associated with Sch, -A be a linear A-automaton, -P A and P ′ A be the Datalog program associated with A and the positive sentence associated with A, i and j be two integers such that 1 ≤ i ≤ h and 0 ≤ j, -D be an instance over the extensional schema of P A such that D satisfies P A and does not satisfy P ′

A

If there exists an access method AcM such that D i j (Done-Access i AcM ) is not empty then there exists an LTrans path ρ such that (1) the initial instance is J →si (D), (2) the accesses appearing in ρ are the accesses in Access j i ., and the order defined in Access j i is the same as the order defined by ρ, (3) the final instance of ρ denoted by J ρ satisfies that for each access

(AcM, b) in Access j i , (AcM, b, J ρ ) is equal to (AcM, b, I D,i,i-1 ). Sch(D j i ) is included in J ρ , (4
) there exists a run from s i to s i on ρ.

Otherwise ρ is empty and we define J ρ by J →si(D) .

PROOF OF LEMMA 4.16. We proceed by an induction on on the number of iterations j of the subprogram P i that have been applied.

Base Case j = 0. Access 0 i is empty. Thus ρ is empty and J ρ is equal to J →si(D) . Inductive case j ≥ 1. Let ρ be the path built for j -1 by using the induction hypotheses. Let v be the tuple added at the j th iteration of P i . We notice that there are two main cases: either v is added to a relation ViewR i or v is added to a relation Done-Access i AcM . Case 1: Tuple v is added to ViewR i . We consider two subcases following if ρ is empty or not.

-If ρ is empty. Then all the relations Done-Access i AcM are empty. Due to the construction of the body formula ϕ of the rule associated with ViewR i , ϕ cannot be satisfied by D j and thus the tuple v cannot be added to ViewR i . Therefore, we have a contradiction of the inductive hypotheses.

-Suppose now that ρ is not empty. Due to the construction of the body formula associated with the rule associated with ViewR i , there exists an access (AcM, b) such that v belongs to (AcM, b, I D,i,i-1 ) and b belongs to D j-1 i (Done-Access i AcM ). By the induction hypothesis on ρ, v belongs to I ρ (R). Therefore, ρ still satisfies the inductive invariant for j.

Case 2: tuple v is added to Done-Access i AcM .

The goal is to extend the path ρ. Because v is added to Done-Access i AcM there exists a transition d of the form (s i , ψ, s i ) such that ψ + is equal to ∃x IsBind AcM (x) ∧ ψ 1 following Condition (Deterministic-Access-Method) of linear automata. -ValidBind d is satisfied by D j-1 i . We construct ρ ′ by addying to ρ the transition t = (J ρ , AcM, b, J ρ + (AcM, b, I D,i,i-1 )). We now have to prove that t satisfies ψ. Satisfaction of Ω(s i ). We first prove that J ρ + (AcM, b, I D,i,i-1 ) satisfies Ω(s i ). We recall that Ω(s i ) is a Boolean combination of negated positive sentences over Sch associated with s i due to Condition (Negative-Invariant). The sentence Ω Datalog (Ω(s i )) is obtained from Ω(s i ) by replacing each atom R(x) by

⋁ j ≤ i BackgroundR j (x) ∨ ⋁ j ≤ i-1 IntBackgroundR j (x);
Because D does not satisfy P ′ A , D satisfies Ω Datalog (Ω(s i )). Due to Claim 3, I D,i,i-1 satisfies Ω(s i ). Due to Property 3 of Lemma 4.16,

I ( ρ) + (AcM, b, I D,i,i-1 ) is included in I D,i,i-1 . Because Ω(s i ) is monotone, J ρ + (AcM, b, I D,i,i-1 ) satisfies Ω(s i ). Satisfaction of ψ + . Due to Claim 1, the transition (Sch(D j-1 i ), (AcM, b), Sch(D j-1 ) + (AcM, b, I D,i,i-1 )) satisfies ψ + . Because Sch(D j-1 i ) is included in J ρ and ψ + is monotone, t satisfies ψ + .
Satisfaction of ψ -. First, we have proven above (in the paragraph headed by "Satisfaction of Ω(s i )") that J ρ + (AcM, b, I D,i,i-1 ) satisfies Ω(s i ). We recall Property (Neg-ativeInv +) of linear A-automata A (see the text after Definition 4.11): For each transition (s, ψ, s) if any instance I satisfies Ω(s) then for any LTrans transition t = (I ′ , (AcM, b), I ′′ ), if I ′ ⊆ I ′′ ⊆ I then t satisfies ψ -. Applying Property (NegativeInv +) of linear A-automata, t satisfies ψ -.

Because t satisfies ψ -and ψ + , t satisfies ψ. Therefore r.d is a run to s i on ρ.t. This finishes the induction.

4.5.4. Construction of the accepted path. Let D be an instance satisfying P A and not satisfying P ′ A . We now build the path ρ and the accepting run r on ρ showing that A is not empty. First, we recall that for each i > 1, the rule of ReachC i has in its body formula the atom ReachC i-1 . Because D satisfies P A , P f ull A (D)(ReachC h ) is true. Therefore for each i, D i-1,i (ReachC i ) holds. Due to Lemma 4.15, for each i > 1, there exists an LTrans transition t i-1,i from the instance D i-1 to J →si (D) and the transition (s i-1 , ψ i , s i ) is a run on t i-1,i . For each i ≥ 1, a LTrans path ρ i and a run r i on ρ i are built as follows: -if J →si (D) is equal to Sch(D i ) then ρ i and r i are empty; -otherwise let j be an integer such that D j i is equal to D i . Let ρ i from J →si (D) to D i and r i from s i to itself be the path and run obtained using Lemma 4.16. We define the LTrans

path ρ = ρ 1 ⋅ t 1,2 ⋯ρ h-1 ⋅ t h-1,h and the run r = r 1 ⋅ (s 1 , ψ 2 , s 2 )⋯r h-1 ⋅ (s h-1 , ψ h , s h ).
Then r is an accepting run on ρ, and therefore A is not empty. We now show that if A has an accepting run, then there is a database D of Sch ext that is a model of P A but not of P ′ A . Towards this goal, let ρ = t 1 , . . . , t n with t j = (I l , (AcM l , bj k , I l+1 ) be a path on which A has an accepting run r = d 1 , . . . , d n with

d l = (s i l , ϕ i l , s i l+1 ) ∈ δ for 1 ≤ l ≤ n.
We define a set of instances K i and J i and H i over Sch. These instances are used to build D. The instance K 0 is equal to I 1 . Let i be an integer less or equal to n, and d m(i) be the transition in r going from the state s i to the state s i+1 . Let t m(i) = (I m(i) , (AcM m(i) , bm(i) ), I m(i)+1 ) be the LTrans transition of ρ associated with d m(i) . We define:

-K i to be I m(i)+1 -I m(i) , -H i to be I m(i) , -if i = 1 then J 1 = H 1 -K 0 otherwise J i = H i -(H i-1 ∪ K i-1 ).
We build the database D over Sch ext as follows: for each

1 ≤ i ≤ h and each relation R ∈ Sch, D(BackgroundR i ) is interpreted as in J i (R) and D(IntBackgroundR i-1 ) is in- terpreted as in K i-1 (R).
For each AcM, the tuples in Bind AcM (D) are the tuples b such that (AcM, b) appearing in ρ.

We first show that D is a model of P A . Let P f ull A (D) be the fixed point of applying P A to D, and we claim that for all i ≤ h, where h is the height of A, for each relation name R

H i (R) ⊆ ⋃ j≤i P f ull A (D)(ViewR i )
This can be shown easily by induction on the length of the run r. Note that by the definitions of P A and D it holds that

H i (R) ⊇ ⋃ j≤i P f ull A (D)(ViewR i )
It follows that D satisfies P A . We prove now that D does not satisfy P ′ A . We recall Property (NegativeInv †) of a linear A-automaton: For each transition (s, ψ, s ′ ) if a LTrans transition (I, (AcM, b), I ′ ) satisfies ψ then I ′ satisfies Ω(s).

For each i ≤ h, -By construction of D, H i is equal to D i,i-1 and H i ∪ K i is equal to D i,i .

-Due to the Property (NegativeInv †) of linear A-automaton, H i satisfies Ω(s i ). Due to Claim 3, Ω Datalog (Ω(s i )) is satisfied by D.

-(H i , (AcM, b), H i ∪ K i ) satisfies ψ - i where (s i , ψ i , s i+1
) is a transition of A and (AcM, b) is the access associated with ψ i following Condition (Deterministic-Transition) . Due to Claim 4, Ω Datalog (ψ - i ) is satisfied by D.

Because P ′

A is the dual of the conjunction of the sentences Ω Datalog (Ω(s i )) and Ω Datalog (ψ - i ) for i ≤ h, D does not satisfy P ′ A .

Containment of Datalog in positive queries, and completion of the proof of the main A-automaton theorem

Let us review what we have accomplished thus far: we have reduced questions about our logic to non-emptiness of the automata, and we have reduced checking nonemptiness of an automaton to determining whether a Datalog program is contained in a positive query. To complete the proof of Theorem 4.9 we need the following new result, that generalizes a theorem of Chaudhuri and Vardi [Chaudhuri and Vardi 1997a]:

PROPOSITION 4.17. The containment problem of a Datalog program P in a positive first-order sentence ϕ, where both P and ϕ may contain constants, is in 2EXPTIME.

Theorem 4.9 follows from the proposition and the reduction given earlier.

PROOF. We first show the argument in the absence of constants and equality atoms. We adapt the proof that containment of a Datalog program P in a union of conjunctive queries can be decided in 2EXPTIME [Chaudhuri and Vardi 1997b]. First, we briefly recall the idea of this proof. Let P be a Datalog program and let ⋃ i θ i be a union of conjunctive queries. The main idea is to associate P with a non deterministic tree automaton, A P , of size exponential in the size of P . In the same way, each θ i is associated with a non-deterministic tree automaton, A θi , which is of size exponential in P and θ i . Theorem 5.11 of [Chaudhuri and Vardi 1997b]

states that P is included in ⋃ i θ i iff A P is included in ⋃ i A θi .
Next, we explain how to use this theorem for the case of positive queries. Let ϕ be a positive query and ⋃ i θ ′ i be a union of conjunctive queries equivalent to ϕ. Without loss of generality, we can assume that the number of formulas θ ′ i is exponential in the size of ϕ and each θ i is polynomial in the size of ϕ. For each i, A θ ′ i is the tree automaton associated with θ ′ i in Theorem 5.11 of [Chaudhuri and Vardi 1997b]. It is known that for any non-deterministic tree automaton A and A ′ , there exists an automaton A ′′ such that A ′′ is equivalent to the union of A and A ′ and A ′′ ∈ O( A + A ′ ) [START_REF] Comon | Tree Automata Techniques and Applications[END_REF]]. We can deduce that there exists a non-deterministic tree automaton A ϕ of size exponential in ϕ equivalent to ⋃ i A θ ′ i . The inclusion of two non deterministic tree automata A ′ and A ′′ is EXPTIME in their sizes.

So it follows from this and Theorem 5.11 of [Chaudhuri and Vardi 1997b] that the problem of containment of a Datalog program in a positive query is in 2EXPTIME.

To handle constants and equality atoms, we can translate a containment problem of P and ϕ to another containment problem P ′ and ϕ ′ where there are no constants or equality atoms. This is done by considering an extended signature with unary predicate symbols for each constant symbol, and rewriting P and ϕ to be disjunctions of constant-and equality-free queries in the larger signature. The disjunction considers the ways in which repeated variables can be realized by a constant c, replacing the repeated variable by distinct variables that satisfy the unary predicate for c. This can be done without a blow-up in the Datalog program P , by introducing an intensional predicate Eq(x, y) that is defined by a disjunction. Eq(x, y) is then re-used in every other rule. Within ϕ, a blow-up does occur, so we have thus reduced to checking whether P is contained in ⋁ i ϕ i , where the disjunction is exponential. By expanding ϕ i , we can assume that the right-hand side is an exponential disjunction of conjunctive queries, and then proceed as in the case without constants above.

Hardness of A-automata non-emptiness

We recall that we promised to use the connection of A-automata to Datalog to show a hardness result for A-automata. Specifically, earlier in this section we stated Theorem 4.10 without proof: Satisfiability of AccLTL + and emptiness of A-automata are 2EXPTIME-hard

We prove only the statement about A-automata; the same proof technique applies to the logic.

We reduce the containment problem of a Datalog program in a union of conjunctive queries to our problem. This problem is known to be 2EXPTIME-hard [Chaudhuri and Vardi 1997a].

Let Sch be a schema, P = (q, R) a Datalog program with input relations in Sch with head predicate q, and ϕ be a positive query over Sch. We denote by Sch idb the set of intentional relations used in the rule of P . For each R ∈ Sch ∪ Sch idb , we have an access method AcM R on it with all positions as input.

Let A = (S, S 0 , F, δ) be the following automaton over the schema Sch ∪ Sch idb : -S = {s 0 , s f }, S 0 = {s 0 }, F = {s f }, A:31 -For each R ∈ Sch, there exists a transition d in δ, d = (s 0 , ¬ϕ pre ∧ ¬ϕ post ∧ ∃ x AcM R ( x), s 0 ) -For each rule r = R( x) ∶ -B r ( x), there exists a transition d in δ, d = (s 0 , ¬ϕ pre ∧ ¬ϕ post ∧ ∃ xB pre r ( x) ∧ AcM R ( x), s 0 ). -For each rule r = q() ∶ -B r (), there exists a transition (s 0 , B pre r (), s f ) ∈ δ. For any query Q over Sch, Q pre is the query obtained by changing R to R pre .

Thus the automaton simply checks that ϕ is never satisfied, and that whenever we have the body of a rule satisfied, we do an access on the head predicate. It then accepts if the goal predicate is ever satisfied. Clearly, if the automaton accepts a path, the final instance in the path cannot satisfy ϕ, and will have a chain of witnesses for the goal predicate. The automaton does not enforce that the intentional predicates of this instance represent a least fixedpoint (i.e. that they have their appropriate definitions). But if we take the fixedpoint of the resulting configuration, it will still satisfy ¬ϕ, since we are changing only intentional predicates.

Conversely, suppose there is an instance I satisfying the Datalog query P along with ¬ϕ; we will construct a path that is accepted in the automaton. We start with an access path p 0 that does membership tests for all tuples in I, obtaining true as a result. We then consider the chain of rule instantiations f 1 . . . f n that witness the truth of P on I. Each f i can be identified with a grounding of a rule r i with head predicate H( x) in P , with bi being the corresponding evaluation of the variables in the body. For each f i we have an access AC i using method AcM H on the restriction of bi to x, with the response being true. It is easy to check that the access path formed from concatenating p 0 with the accesses AC i and their responses is accepted by A.

We now give the formal proof that the reduction is correct. Given an instance I for the schema Sch ∪ Sch idb , we let I Sch (resp. I Sch idb ) be the restriction to the relations in Sch (resp. Sch idb ).

From automaton non-emptiness to non-containment. We prove that for each access path ρ recognized by A, ending with instance I n , I n+1 Sch is a witness to noncontainment of P in ϕ. We first show that this instance satisfies the Datalog query P . To do this we show that at any instance I i on the path, for each intentional predicate R in P , I i (R) is a subset of the tuples calculated by P for R on I i Sch.

Base case. ρ = ∅, the initial instance is empty, so clearly containment holds.

Induction step. Let ρ be an access path recognized by A of length i + 1. By the induction hypothesis, I i (R) is included in the value of R computed by P on I i Sch. We denote by d the last transition associated to the last access in ρ, and divide up into cases.

-the transition was on an access to a predicate R ∈ Sch. Such accesses are unconstrained by the automaton A, so they may bring a new tuple into extensional relation R. In moving from I i to I i+1 the values of the intentional predicates are unchanged, but by monotonicity of the Datalog program P , the values of the intentional predicates calculated by the program can only increase when moving from I i Sch to I i+1 Sch. Hence the inductive invariant is preserved. d is associated with an access to R ∈ Sch idb . We consider the case where the matching automaton transition is not the one associated with the rule for the head predicate q.

Thus the access may bring a new tuple t into R, and for some rule r = R( x) ∶ -B r ( x) of P t must satisfy B pre r ( x) in the transition structure, hence t must satisfy B r ( x) in I i . By the induction hypothesis, t satisfies the corresponding predicates computed by P (I i Sch). Thus t satisfies R in P (I i Sch) and hence by monotonicity satisfies R in P (I i+1 Sch). The case where the transition does correspond to the head predicate q of P is similar.

Let ρ be a path accepted by A. By construction, the restriction of the final instance I n to intentional predicates is a subrelation of the intentional predicates calculated by the Datalog program P . In addition, since an accepting state is reached, the goal predicate must be non-empty. Thus (again by monotonicity), the Datalog query P must be true on the restriction of I n . On the other hand, the negation of the positive query ϕ is globally required to hold on all instances I i in the ρ, hence it holds in the final instance. Thus we have that I n is a witness of the failure of containment of P in ϕ.

From non-containment to automaton non-emptiness. Let I be a witness of the failure of containment of P in ϕ. Let P 1 (I) . . . P n (I) be successive approximations of the fixpoint P . We prove by induction that for each i, there exists a path ρ whose final instance I i has its restriction to Sch predicates being I and its restriction to the intentional predicates matching the values calculated in P i (I Sch).

Base case. We take a path that populates only the predicates of Sch so that they match I.

Induction step. Let ρ be a path recognized by A associated to I i = P i (I), which exists by induction. We show how to extend ρ, abiding by the automaton rules, mimicing each rule in P firing on I i Sch. We consider a rule r, focusing on the case where r is of the form R( x) ∶ -B r ( x) (the case of the head rule is similar). Consider an arbitrary tuple t such that B r (t) is satisfied in P i (I). By construction the corresponding transition is possible from I i by reading the access (AcM R , t, {t}). We thus extend ρ by adding on transitions for each such t.

Exact and Idempotent accesses. The above argument was under the standard semantics for access paths. But we note that in the reduction, we used a schema with only one access method per relation, and only boolean accesses. Hence every path is exact for such a schema. Thus we also have hardness when the semantics is restricted to exact accesses and idempotent accesses.

TRADING OFF EXPRESSIVENESS FOR COMPLEXITY OF ANALYSIS

We now look for path query languages where the satisfiability problem has lower complexity. We will do this by giving up the ability to talk about the exact dataflow from data instances to bindings. This will allow us to get verification algorithms based on reduction to standard Propositional Linear Temporal Logic verification, a well-studied problem for which many tools are available [START_REF] Clarke | Model Checking[END_REF].

For a relational schema Sch, we define the vocabulary Sch 0-Acc as in Sch Acc but instead of the n-ary predicates IsBind AcM , we have only a 0-ary predicate IsBind AcM . A transition t i = (I i , (AcM i , b), I i+1 ) is now associated with the relational structure M ′ (t i ) in which S pre , S post are interpreted as before, and IsBind AcM () holds exactly if AcM = AcM i . We will now consider AccLTL(FO ∃+ 0-Acc ), in which the first-order formulas use only Sch 0-Acc . That is, in the logic we can refer to which access was performed, but can not express anything about the bindings used.

Going back to Example 2.3 and 2.4 we say that the basic relevance properties are in this language, provided that we do not impose any dataflow restrictions -including any restrictions that access paths are grounded. On the other hand, we can still use this restricted logic to express the access order restrictions of Example 2.4. We now see that by curtailing the expressiveness, the complexity goes down significantly. THEOREM 5.1. Satisfiability of an AccLTL(FO ∃+ 0-Acc ) formula (over all access paths) is PSPACE-complete. The same holds if particular access methods must be exact or idempotent.

PROOF. The PSPACE-hardness of our problem comes from the PSPACE-hardness of the satisfiability problem of a LTL formula over finite words [START_REF] Emerson | Temporal and modal logic[END_REF]]. The upper bound is proven by bounding the size of the underlying data, and then applying results about propositional LTL.

We now prove the upper bound, focusing on the case of general access paths. Let Sch be a schema, and ϕ be a formula of AccLTL(FO ∃+ 0-Acc ). First, we demonstrate that if there exists an access path that satisfies ϕ then there exists one where the size of each instance is bounded by a polynomial function in the sizes of ϕ and Sch.

The key is the following "Boundedness Lemma":

LEMMA 5.2. An AccLTL(FO ∃+ 0-Acc ) formula ϕ is satisfiable iff there exists a path ρ which satisfies ϕ and which has the following properties: (1) The instances in ρ have sizes bounded by a polynomial function in the sizes of ϕ and Sch. (2) The set of bindings used in ρ has size bounded by a polynomial function in the sizes of ϕ and Sch.

PROOF. The if-part is trivial, so we turn to the only-if. Let some ϕ be given. Suppose that ϕ is satisfiable. Then there exists a path ρ that satisfies ϕ. We define the positive sentences of ϕ to be the maximal subsentences of ϕ that belong to FO ∃+ 0-Acc . Consider the following rewrite rules: for each AcM ∈ Sch we replace the formula IsBind AcM ∧ψ, where IsBind AcM is a predicate, by the formula ψ. We also replace the formula IsBind AcM ∨ψ where IsBind AcM is a predicate by the formula ψ. We denote by Q f (ϕ) the set of FO ∃+ 0-Acc sentences that have been obtained from a positive sentence of ϕ by inductively applying the above rules until there are no more occurrences of predicates IsBind AcM in the result.

Let {q 1 , . . . , q m } be the set of sentences appearing in Q f (ϕ) that are satisfied by the last instance I n . Let ρ i1 , . . . , ρ im be the set of transitions in the path ρ such that ρ ij is the minimal transition in ρ that satisfies q j . Let h j be a homomorphism from q j to ρ ij . We let (I f -1 , AC f , I f ) be the last transition in ρ. Let I ′ f be the minimal subinstance of I f such that for all i h i (q i ) ⊆ (I ′ f ) pre ∪ (I ′ f ) post ), where for any instance I of the original schema, I pre is obtained from I by interpreting relations R pre by the interpretation of R in I, while I post is obtained from I by interpreting relations R post by the interpretation of R in I.

Since we only need to consider witnesses to positive queries, it is easy to check that I ′ f can be constructed and has size polynomial in the sizes of ϕ and Sch. We can thus construct a path ρ ′ that contains the intersection of the instances of ρ with the instance I ′ . ρ ′ satisfies ϕ, and the size of the instances of ρ ′ are bounded by a polynomial function in the size of ϕ and Sch.

We now restrict the bindings used in ρ ′ . Let p be a path. An access (AcM i , bi ) is necessary for p if new tuples are returned by it (i.e. tuples not in the previous instance within p), and unnecessary otherwise. Note that if we have a path and we change the binding on some unnecessary access to anything of the appropriate arity, while returning emptyset, then it is still a valid access path.

So without loss of generality, we can arrange that the set of bindings used in ρ ′ consists of the necessary accesses in ρ ′ plus a single binding for each access method, used in place of every unnecessary access on that method. Therefore the number of bindings used is bounded by a polynomial function in the sizes of ϕ and the schema.

Given the lemma, we can now apply the following algorithm which is easily seen to be in NPSPACE:

(1) First, we guess a finite sequence of instances I 1 . . . I n and a sequence of accesses A, each of polynomial size (with the polynomial given by Lemma 5.2). In the remaining steps, we will check whether there is a witness path using the bindings of these accesses and only these instances.

(2) We translate the AccLTL(FO ∃+ 0-Acc ) formula ϕ into an ordinary LTL formula ϕ in a propositional alphabet that encodes information about which of the instances and bindings are used. This formula will be constructed so that it is satisfiable over words iff ϕ is satisfiable.

(3) Then, we apply any PSPACE algorithm for LTL satisfiability of ϕ over finite words.

We now explain in more detail the translation to ordinary LTL that is the key step in the high-level algorithm above. Fix a sequence s = I 1 . . . I n of distinct instances as well as a sequence of accesses A, both of polynomial size. We denote by B, the union of the set of bindings used in A and the set ∪ AcM {b AcM } where b AcM is a binding of AcM using some values appearing in B.

We associate propositions with transitions of any of the following forms: -Transitions of form (I i , (AcM, b), I i ) where b is in B and compatible with AcM.

-Transitions of form (I i , A i , I i+1 )

The set of transitions that match the two forms above is denoted T (I, B). For each i, we denote by ( 1) T (i) the set of transitions of the form (I i , (AcM, b), I i ). (2) t i,→ the transition (I i , A(i), I i+1 ). (3) P (i) the set of propositions associated with the transitions of the form (I i , (AcM, b), I i ). (4) p i,→ the proposition associated with the transition (I i , A i , I i+1 ). The set of all such propositions is denoted Σ. The formula ϕ that we will present will define words over alphabet 2 Σ . Intuitively, each letter of a word is used to describe a transition (I, (AcM, b), I ′ ).

We now describe the construction of ϕ. First, we describe some "sanity axioms" stating that a run associated with ϕ really corresponds to some access path. This requires: -Every position has exactly one proposition of Σ.

-The order of the instances in s is respected. This is expressed by the formula:

⋀ i,p ∈ P (i) G p ⇒ ⋁ p ′ ∈P (i) p ′ U p i,→ ∧ ⋀ i p i,→ ⇒ X ⋁ p ′′ ∈P (i+1) p ′′ ∨ p i+1,→ ∧ ⋁ p ′′′ ∈P (0) p ′′′ ∨ p 0,→
Next we rewrite ϕ to ϕ by replacing each positive sentence q of ϕ by the union over of p ∈ Σ over all the previous transitions that satisfy it.

We claim that the ϕ is satisfiable over ordinary words iff ϕ is satisfiable over access paths that conform to the sequence s and the bindings in B. The direction from right to left requires taking an access path and performing the obvious propositional abstraction. In the other direction, we take a propositional word w 1 . . . w n satisfying ϕ. The first sanity axiom implies that exactly one transition proposition p is associated with w i . The second sanity axiom implies that the instance reached in the transition associated with w(i) is the same as the initial instance of the transition associated with w(i + 1). One can check that this gives the required access path for ϕ.

Extension of the Proof of Theorem 5.1 for exact and idempotent paths. Recall the result:

Satisfiability of an AccLTL(FO ∃+ 0-Acc ) formula (over all access paths) is PSPACE-complete. The same holds over exact access path, idempotent access paths, and paths that are both exact and idempotent.

We refer to the proof of Theorem 5.1, and we explain the modifications needed for idempotent and exact accesses. We first claim that Lemma 5.2 still holds with these conditions. For idempotent accesses, we can use the same process as in the proof of Lemma 5.2: if the original path was idempotent, the diminished path will be as well. For exact access paths, we must ensure that when we shrink the size of instances we do not destroy exactness. We can think of performing the shrinking in two stages, where the first stage involves throwing in query witnesses as in the proof of Lemma 5.2 for general access paths. After doing this, we may have lost exactness: we may have two accesses a i and a j in the initial path p (prior to shrinking), where the shrinking maintains a certain tuple t in a i but throws the same t out of a j . But we can repair this by just making sure that a tuple is left in a j if it is left in any other a i .

Given Lemma 5.2, the rest of the argument proceeds via rewriting as above.

Restricting LTL operators

Let LTL X be the subset of LTL that only uses the temporal operator X. We denote by AccLTL(X)(FO ∃+ 0-Acc ) the corresponding sublanguage of AccLTL(FO ∃+ Acc ). AccLTL(X)(FO ∃+ 0-Acc ) is extremely limited in expressiveness, since it can only talk about paths of some fixed length. However, there are properties for which such small paths are sufficient. Consider Example 2.4. It is easy to see that Q is LTR over all accesses iff it is LTR over access paths of size Q -a counter example to long-term relevance has only polynomially length. But LTR over small paths can be expressed in AccLTL(X)(FO ∃+ 0-Acc ). Thus AccLTL(X)(FO ∃+ 0-Acc ) is sufficient to tell whether an access might have an impact on answering a query, but without taking into account of even the most basic dataflow restriction on paths. THEOREM 5.3. Satisfiability of AccLTL(X)(FO ∃+ 0-Acc ) is Σ P 2 -complete, even when certain accesses are restricted to be exact or idempotent.

PROOF. We start out with the proof for general accesses.

Hardness For brevity, we explain the argument only when an initial instance for paths can be fixed, leaving the general proof for the reader. Given a boolean combination σ of positive existential first-order sentences, along with S a "schema" restricting positions R[i] of relation R to take values only in some finite set T ype (R[i]). We can efficiently create an initial instance I 0 and an AccLTL(X)(FO ∃+ 0-Acc ) sentence ϕ such that there is a path from I 0 satisfying ϕ exactly when there is a database instance conforming to S and satisfying σ: we let the signature for ϕ contain the predicates of σ, along with unary predicates for R [i], where the predicates of σ have free access while those for R[i] have no access. We let I 0 contain T ype (R[i]) as the values for predicate R[i]. ϕ will simply use next operators to assert that the given path consists of a sequence of accesses to each predicate of σ in turn, reaching a position satisfying a final condition consisting of σ conjoined with predicates R[i](x) whenever x occurs in position i of relation R within σ. Thus ϕ asserts that after all of the relations are revealed, σ holds. It is easy to verify that this reduction is as required.

In particular, non-containment of positive relational algebra queries in which positions of particular attributes can be restricted to have "finite type" -to take values in some finite set -can be reduced to the complement of the satisfiability problem of either language -this problem is known to be Π P 2 -hard.

Upper-Bound. Let an AccLTL(X)(FO ∃+ 0-Acc ) formula ϕ be given. We make use of the "boundedness lemma", Lemma 5.2, which can be seen also to hold for AccLTL(X)(FO ∃+ 0-Acc ):

An AccLTL(X)(FO ∃+ 0-Acc ) formula ϕ is satisfiable iff there exists a path ρ that satisfies ϕ and which further has the following properties: -The instances have sizes bounded by a polynomial function in the sizes of ϕ and Sch. -The set of bindings used in ρ has size bounded by a polynomial function in the size of ϕ.

We will adapt the technique used in the proof of Theorem 5.1. Our algorithm will guess first of all a sequence Ī of instances and a sequence ĀC of accesses of size polynomial in ϕ. We denote by n the length of Ī, minus one. Let B be the set of bindings used in the sequence ĀC and let Q be the set of positive subformulas of Φ in which all predicates IsBind AcM have been removed (as in the proof of Lemma 5.2).

We denote by T ( Ī, B) the set of transitions of any of the following forms: -(I i , (AcM, b), I i ) where b is in B and compatible with AcM.

-(I i , A i , I i+1 ), where A i is any access.

For each i, we denote by T (i) the set of transitions of the form (I i , (AcM, b), I i ). For each i, we denote by t i,→ the transition (I i , A i , I i+1 ).

For each transition t ∈ T ( Ī, B), we let Q + t be the elements of Q which are satisfied by t and we let Q - t be the elements of Q that are not satisfied by t. For each query q in Q + t , there is a witness vector v q,i for the satisfaction of q in t. By making calls to NP and co-NP subalgorithms, our algorithm can verify that each of these guesses is correcte.g. that each query in Q + t really is satisfied in t. We now translate ϕ into a propositional LTL X formula ψ such that ψ is satisfiable iff there is a model of ϕ that satisfies the regular expression T (0) * , t 0,→ , . . . , t n-1,→ T (n) * . The translation from ϕ to ψ can be obtained in polynomial time. The main difference from the proof of Theorem 5.1 is that we need to express the "sanity axioms" using only the operator X, whereas in the proof of Theorem 5.1, these axioms are encoded using the operator G. However, we notice that the constraints imposed by the formula ϕ on the path are all restricted to the first ϕ accesses. Hence, the "sanity axioms" have to be checked only on the initial ϕ accesses, and can thus be rewritten using only the next-time operator X.

Finally, our algorithm checks the satisfiability of the rewritten sentence ψ, which can be done in NP.

We now explain the revision when access methods are required to be exact or idempotent. The conclusion of Lemma 5.2 still applies in this case, and our algorithm begins as before by guessing instances and accesses, and guessing and verifying the positive queries that hold in each instance. One will need to verify as well that the accesses satisfy idempotence or exactness, as required by the underlying access method. Again it suffices to consider paths in

T (0) * , t 0,→ , . . . , t n-1,→ , T (n) *
We do this using the same propositional rewriting as above. Note that accesses in T (i) * always return empty, and are all incompatible with each other and the accesses in t i,→ . Therefore these accesses are always exact. The others accesses have already been verified to have the required properties.

Additional Note. We notice that the conclusion of Lemma 5.2 also holds for AccLTL(X)(FO ∃+,≠ 0-Acc ). The correctness of the queries can be checked in the same complexity for positive first-order formulas with inequalities. Thus the previous arguments are still correct in this context. We can conclude that these results can be extended for formulas with inequalities.

Branching Time Formulas

Thus far we have discussed only linear time properties of the LTS of a schema with access relations. What about branching time logics, which can consider the relationship of multiple paths? For example, a branching time logic could express that we have reached a point where no further information about boolean query Q can be obtained without guessing values to enter into forms -e.g. there are possible worlds consistent with the known facts where Q is true and also consistent worlds where Q is false, but the truth of Q can not be revealed by any further sequence of grounded accesses. Unfortunately, we will show that even very limited branching time expressiveness leads to undecidability.

Let L be a fragment of first-order logic over the smallest vocabulary we have considered thus far: two copies S pre , S post of each relation symbol S and the proposition IsBind AcM .

We will consider a small fragment of branching time logic built up from L-formulas, analogously to the way we built up AccLTL formulas over sentences of L in the linear time logic. Traditional branching time logic allows the combination of path quantification with modal operators. In our setting we will consider a very simple kind of branching, which looks ahead only one step -we will refer to it as CTL EX (L), but instead of CTL we might as easily have said "basic modal logic" or Hennessy-Milner Logic [Emerson 1990], since we only need the power of the most basic existential modality to get undecidability. CTL EX (L) has the rules: every L sentence is a formula, boolean combinations of formulas are formulas, and if ϕ is a formula then EXϕ (in modal logic notation, ◇ϕ) is a formula.

The semantics is defined as a relation (S, t) ⊧ ϕ, where t is a transition (I, AC, I ′ ) in the labelled transition system S associated with a schema Sch. When ϕ is an L formula, this holds iff the relational structure associated to t, M ′ (t), satisfies ϕ in the usual sense of first-order logic. The semantics of boolean operators is the usual one. Finally, (S, t) ⊧ EXϕ iff there is a successor t ′ of t such that (S, t ′ ) ⊧ ϕ. Note that Deutsch et. al. [Deutsch et al. 2007] have shown undecidability for some branching time logics over LTS's associated with a similar model of relational transducers -but in their case the logics (e.g. Theorem 4.14 of [Deutsch et al. 2007]) allow one to describe properties of the input (analogous to our larger signature Sch Acc ), while here we can only describe the access propositionally.

We show that even this restricted logic is undecidable, even when the base formulas are existential. THEOREM 6.3. Satisfiability of CTL EX (FO ∃+ 0-Acc ) is undecidable.

PROOF. We reduce from the problem of implication of a functional dependency from a set of functional dependencies and inclusion dependencies for relational databases. This is known to be undecidable [START_REF] Chandra | The implication problem for functional and inclusion dependencies is undecidable[END_REF].

Let Γ be a set of inclusion and functional dependencies over a relational schema Sch and σ an FD. For simplicity, we will assume all positions in the schema have the same type (say, integer type). We will first extend Sch with additional relations, along with access patterns.

For each relation R of Sch, we have an access method Fill R on R with no inputs. Thus each access (Fill R , ∅) returns an essentially random configuration of R. We also have additional relations Chk FD (R), having twice the arity of R and CheckIncDep(R) having the same arity as R. We have boolean access methods on all of these additional relations -that is, methods where all positions are in the input.

Our reduction will create a formula ψ(Γ, σ) of the form:

EX Fill R1 ∧EX ⋯ ∧ EX(Fill Rn ⋀ fd∈Γ ϕ fd ∧ ⋀ id∈Γ ϕ id ∧ ϕ ¬σ )
where ϕ fd , ϕ id , and ϕ ¬σ will be defined below, but we explain their mission now. For each functional dependency fd ∈ Γ, the formula ϕ fd will hold on a transition t = (I, AC, I ′ ) exactly when fd holds on the restriction of I ′ to the schema predicates from Sch, and similarly for ϕ id . The formula ϕ ¬σ checks that I ′ does not satisfy the functional dependency σ. Thus this formula will imply that the configuration is a witness showing that Γ does not imply σ.

We now explain how the different formulas are built. Let fd = R ∶ P → p where P are positions of relation R and p is a position of R. The formula ϕ fd will be:

AX ∃ x y Chk FD (R) post ( x, y) ∧ ⋀ i∈P x i = y i ∧ R post ( x) ∧ R post ( y) ⇒ ∃ x ′ y Chk FD (R) post ( x ′ , y ′ ) ∧ x ′ p = y ′ p
Here we use the derived "box" modality AXϕ = ¬EX¬ϕ. Note that ϕ fd occurs in formula ψ(Γ, σ) in a context where we know that only accesses to R i have been done -hence only in contexts where Chk FD (R) must be empty. Since the only access methods for the relations Chk FD (R) are boolean, this means that after one transition we can have at most one tuple in Chk FD (R) post ( x, y). Thus doing a modality AX followed by a test that Chk FD (R)( x, y) ∧ R post ( x) ∧ R post ( y) holds amounts to testing an arbitrary pair x, y satisfying R prior to the access. The formula thus asserts that for any such pair of tuples in R, if they agree on all positions in the source of the FD, they agree on the target of the FD. We can use a similar trick with the formula ϕ ¬σ :

EX ∃ x y Chk FD (R) post ( x, y) ∧ ⋀ i∈P x i = y i ∧ R post ( x) ∧ R post ( y)∧ ¬∃ x ′ y Chk FD (R) post ( x ′ , y ′ ) ∧ x ′ p = y ′ p Now fix an id R[A 1 , ⋯, A n ] ⊆ S[B 1 , ⋯, B n ],
and we define ϕ id to be

AX IsBind CheckIncDep(R) ∧R post ( x) ∧ ∃ x CheckIncDep(R) post ( x) ⇒ EX IsBind CheckIncDep(S) ∧∃ x CheckIncDep(R) post ( x) ∧ ∃ y CheckIncDep(S) post ( y) ∧ ⋀ i≤n x Ai = y Bi
This states that whenever we do a "test access" that returns an element of R, there is some access we can do immediately afterwards in the LTS that reveals a matching tuple in S. As in the case of ϕ fd above, the accesses we perform are boolean, and hence cannot be creating any new elements of S -thus the revealed match must have been in the configuration prior to the access.

CONCLUSIONS AND RELATED WORK

In this work we introduced the notion of querying the access paths that are allowed by a schema. We presented decidable specification languages for doing this, and gave undecidability results showing several limits of such languages. Figure 4 shows the inclusions of the languages considered in the paper, excluding those for branching time.

All of the containments shown in the diagram are straightforward. The containment of FO ∃+ 0-Acc in AccLTL + does require one to deal with the fact that FO ∃+ 0-Acc sentences are not required to be binding-positive. The inclusion follows by first rewriting negated 0-ary IsBind AcM predicates using the rule IsBind AcM = ⋁ AcM ′ ≠AcM IsBind AcM ′ , then replacing the 0-ary predicate by existentially-quantified n-ary predicates.

All the inclusions in the diagram also turn out to be strict. We omit the proofs for this, which use standard techniques: e.g. A-automata can express parity conditions on the length of paths, which first-order languages like AccLTL + , or even AccLTL(FO ∃+ Acc ), can not do.

Table 3 shows the complexity of satisfiability for each specification formalism, along with application examples. DjC indicates that the language can express relevance of an access in the presence of disjointness constraints, while FD, DF, AccOr refer to functional dependencies, dataflow restrictions, and access order restrictions, respectively.

Our work leaves open a number of questions concerning the logics we study. We believe that examination of the translation to A-automata, along with a finer analysis of A-automata emptiness will show that satisfiability of AccLTL + is 2EXPTIMEcomplete; but the results presented here give a triple-exponential upper bound and a double-exponential lower bound. We also do not have tight bounds for our more re-stricted fragments (e.g. with only the 0-ary version of IsBind AcM ) in the important case of grounded access paths.

Although this is, to the best of our knowledge, the first work on languages for describing access paths through a schema with binding patterns, there is a strong formal connection to work on verifying data-driven services, as well as other work in the area of hidden Web querying. We review the closest connections below.

Data-driven services. Our work is closely related to a line of research on relational transducers and models for data-driven services, beginning with [START_REF] Abiteboul | Relational transducers for electronic commerce[END_REF], and continuing through work of Spielmann [START_REF] Spielmann | Verification of relational transducers for electronic commerce[END_REF]], Deutsch, Su and Vianu (e.g. [Deutsch et al. 2007]), [START_REF] Fritz | Automatic construction of simple artifact-based business processes[END_REF]], and Deutsch al. [START_REF] Deutsch | Automatic verification of data-centric business processes[END_REF]]. All of these works deal with specification languages for transition systems in which transitions may involve the consuming of relational inputs from an external environment, the production of output tuples, and the modification of internal state (perhaps in the form of an additional relational store). In our application, we talk of accesses rather than inputs from an environment, with a response consisting of revealing a hidden database instance, rather than updating an internal store. But in the results of this paper, one can just as easily think of identifying the hidden Web database with an internal store, with the accesses being nondeterministic inserts into the store.

Nevertheless, the logics that arise naturally in our setting appear orthogonal to those studied in prior work. The initial Abiteboul et. al. paper [Abiteboul et al. 2000] focused on "Spocus transducers" (semi-positive output and cumulative state) which take full relational inputs, with their internal relations only accumulating them. A direct comparison with our model is difficult, since we do not have a notion of "output" -but if we restrict Spocus transducers to boolean output and singleton inputs, they are not as powerful as our model, since in our case the internal state can be modified in nontrivial ways. [START_REF] Abiteboul | Relational transducers for electronic commerce[END_REF]] proves an undecidability result for an extension of Spocus transducers in which the inserted data is allowed to be a projection of the "input relations" (Prop. 3.1 of [START_REF] Abiteboul | Relational transducers for electronic commerce[END_REF]). The technique applied is similar to that in Theorem 6.2, but projection is orthogonal to the update given by access methods. In our terms, this extension would amount to having the information added to the hidden database be a projection of the accessed relations. On the other hand, the addition of projection does not give the ability to model access methods, which restrict the input relations by requiring them to satisfy a selection criterion.

Later works [START_REF] Spielmann | Verification of relational transducers for electronic commerce[END_REF]Deutsch et al. 2007;[START_REF] Deutsch | Automatic verification of data-centric business processes[END_REF][START_REF] Fritz | Automatic construction of simple artifact-based business processes[END_REF]] deal with transducers that can delete as well as insert into their internal state. A key restriction is input-guardedness, which insures decidability [Deutsch et al. 2007] -input guardedness requires quantifications to be restricted to tuples generated from the environmental inputs. The analogous restriction in our setting would be to restrict quantification to the bindings, which would be much weaker than the logics we consider. Thus our decidability and complexity results are not subsumed by these works. On the other hand, guarded quantification over relational inputs is not supported by our logics, and hence we do not claim to subsume results in these works. In addition, [START_REF] Deutsch | Automatic verification of data-centric business processes[END_REF]] allows a built-in linear order on the domain, which we do not consider for our largest logics. Later work by Damaggio et. al. considers even richer signatures, including arithmetic [START_REF] Damaggio | Artifact systems with data dependencies and arithmetic[END_REF]]. [START_REF] Hariri | Verification of relational data-centric dynamic systems with external services[END_REF]] obtains decidability for a different variant of the "artifact model", notably even for a branchingtime logic. [START_REF] Belardinelli | An abstraction technique for the verification of artifact-centric systems[END_REF] isolates conditions on artifact-based systems that imply the existence of finite-state abstractions (and hence decidability via a reduction to traditional model-checking).

Hidden Web querying. Our work is directly inspired by previous results on static analysis of schemas with limited access patterns, a line of work tracing back (at least) to Ullman's work [START_REF] Ullman | Principles of Database and Knowledge-Base Systems[END_REF]] and [START_REF] Rajaraman | Answering queries using templates with binding patterns[END_REF], continuing with Chang/Li's work in the early 2000s [START_REF] Li | Answering queries with useful bindings[END_REF][START_REF] Li | Computing complete answers to queries in the presence of limited access patterns[END_REF]] Ludäscher/Nash's andDeutsch et. al.'s work in the mid-2000's [Nash and[START_REF] Nash | Processing first-order queries under limited access patterns[END_REF]Deutsch et al. 2007] andCali et. al. [Calì and[START_REF] Calì | Conjunctive query containment under access limitations[END_REF]. All of them deal in one way or another with what sequences can occur within a sequence with limited access patterns. For example, the question of whether a query can always be answered using exact grounded access paths -the focus of most of these works above -can be expressed as a property of the LTS. Exact complexity bounds for query answering derived from the works above. Containment under access patterns has also been studied, particularly in [START_REF] Calì | Conjunctive query containment under access limitations[END_REF], which establishes a coNEXPTIME upper bound for conjunctive queries. [START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF]] proves a matching coNEX-PTIME lower bound for containment for conjunctive queries, and a co-2NEXPTIME upper bound for positive queries. [START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF]] also defines the notion of longterm relevance (LTR). They prove a Σ p 2 -completeness result for LTR over general access paths ("independent accesses", in their terminology) while providing a NEXPTIMEcompleteness result for conjunctive queries and a 2NEXPTIME bound for LTR of positive queries over grounded accesses paths ("dependent accesses").

Our work provides a general framework where we can express properties of access paths, including containment, LTR, their combinations, and their restrictions to constraints. By providing these within a boolean closed logic, we give a flexible means of combining properties that one wishes to verify. Our 2EXPTIME result for nonemptiness of A-automata gives a bound on containment under access patterns and long-term relevance, as mentioned in the discussion after Theorem 4.9. This is better than the prior bounds from [START_REF] Calì | Conjunctive query containment under access limitations[END_REF][START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF].

Note that [START_REF] Benedikt | Determining relevance of accesses at runtime[END_REF]] also makes an erroneous claim: A co2NEXPTIME lower bound for containment of positive queries under access patterns, which is at odds (relative to complexity-theoretic hypothesis) with our 2EXPTIME upper bound.

First order linear and modal logics. First order linear temporal logic (FOLTL) formulas are evaluated over linear sequences of first-order structures, mixing both temporal and first-order modal operators. A comprehensive reference for this can be found in Chapters 11 and 12 of [START_REF] Kurucz | Many-Dimensional Modal Logics: Theory and Applications[END_REF]]. As mentioned in the body of the paper, full FOLTL is easily seen to subsume all of the logics considered here, but undecidability is inherited of FOLTL from first-order logic. Prior work has shown much smaller sublogics that are undecidable. For example, in Theorem 11.3 of [START_REF] Kurucz | Many-Dimensional Modal Logics: Theory and Applications[END_REF]], the two-variable fragment with only monadic relations is shown undecidable. This does not subsume our undecidability result, given that the logic in Theorem 11.3 allows one to compare elements across arbitrary time points, while our logic only allows comparison at adjacent times, and only via the bindings of the access methods. In addition, the logic used to compare within a world in Theorem 11.3 allows arbitrary quantifier alternation, while our logic has only boolean combinations of positive existential formulas. Similar comments apply to undecidability for the Guarded Fragment of first-order temporal logic (Theorem 11.17 of [START_REF] Kurucz | Many-Dimensional Modal Logics: Theory and Applications[END_REF]).

In terms of decidability results, prior work has also identified a family of decidable fragments, all lying within the Monodic fragment, in which Until formulas are allowed to have at most one free domain element variable: see [START_REF] Hodkinson | Decidable fragments of first-order temporal logics[END_REF] or Chapter 11 of [START_REF] Kurucz | Many-Dimensional Modal Logics: Theory and Applications[END_REF]. For example Theorem 11.12 of [START_REF] Kurucz | Many-Dimensional Modal Logics: Theory and Applications[END_REF] shows that the two variable Monodic fragment is decidable. These results are easily seen not to imply our decidability results, for several reasons: first, our formalism allows an arbitrary arity in the free variables to be shared between time points (in our case, consecutive time points), while in the two-variable Monodic fragment the number of shared variables is limited. Secondly, our results consider satisfiability not over arbitrary sequences, but those that successively reveal a single underlying model. Although this property of a sequence can be axiomatized in full FOLTL, it certainly cannot be axiomatized in the decidable fragments.

While the above results concern temporal logics, decidability and undecidability has also been studied for multi-dimensional modal logics, which are evaluated on structures connected by multiple binary relations, which are not a priori required to be linear orderings. For example, Chapters 5, 6, and 7 of [START_REF] Kurucz | Many-Dimensional Modal Logics: Theory and Applications[END_REF]] analyze multi-dimensional modal logics evaluated over structures built up as "products" of traditional Kripke structures, possibly satisfying additional axioms -e.g. one binary relation might be restricted to be a linear order.

Chapter 5 and 7 of [START_REF] Kurucz | Many-Dimensional Modal Logics: Theory and Applications[END_REF]] include a number of undecidability results concerning products. Some of the results exploit specific restrictions on the structures or the connecting binary relations. For example, Theorem 5.38 of [START_REF] Kurucz | Many-Dimensional Modal Logics: Theory and Applications[END_REF]] concerns undecidability where a product is taken using two linear orders, even when the individual worlds are propositional. These results do not subsume our undecidability result, because the logics allow arbitrary nesting of negation within a world and nesting of the multiple available modalities for relating two worlds. In contrast, our logic allows only a single un-nested reference to consecutive worlds, with only boolean combinations of positive existential formulas available at the world level.

There are also a number of decidability results for multi-dimensional modal logics based on products (see, e.g. Theorems 6.18, 6.24, 6.33 from Chapter 6 of [START_REF] Kurucz | Many-Dimensional Modal Logics: Theory and Applications[END_REF]). All of these are easily seen not to subsume our main decidability result, since they deal only with underlying relational structures of arity 2, while our results deal with arbitrary arity. Naturally, some of the other reasons for incomparability cited above also hold here. For example, in the case of propositional worlds, decidability can be regained by allowing one of the connecting binary relations to be arbitrary (in contrast to Theorem 5.38 of [START_REF] Kurucz | Many-Dimensional Modal Logics: Theory and Applications[END_REF]] which restricts both relations to be linear orders). But naturally this does not subsume our decidability results, since our setting is not propositional, we have additional restrictions on the evolution of the structures (as mentioned above), and the connecting relations have additional shared parameters corresponding to the method binding.

Also in this line is the work of [START_REF] Wolter | Modal description logics: Modalizing roles[END_REF], which gives decidability results for "modalized description logics", a variant of description logics appropriate for worlds that evolve via a binary relation. They likewise deal only with arity 2, so are incomparable with our decidability results. In addition, many of the decidability results (e.g. Theorem 22 of [START_REF] Wolter | Modal description logics: Modalizing roles[END_REF]) do not apply to the chase where the binary relation (frame) is a linear order, which is the case of interest to us. Indeed [START_REF] Wolter | Modal description logics: Modalizing roles[END_REF]] also provides undecidability results for linear-ordered frames (e.g. Theorem 25). But again the logic is incomparable with the one used in our undecidability results, allowing nesting of modalities and negation.

Fig. 2 .

 2 Fig. 2. An A-automaton.

  where s i is the state referenced in d. Notice that ValidBind d is of the form ∃ Bind AcM (x) ∧ γ(x), and is thus a guarded safe positive formula. Claim 1 presented in Subsubsection 4.5.1 explains that a tuple b appears in ValidBind d iff there exists a LTrans transition t = (I, (AcM, b), I ′ ) satisfying ψ + such that for each relation name T in Sch, I(T ) contains all the tuples in ⋃ k≤i ViewT k and for each relation name T different from R, I ′ (T ) contains the tuples in I(T ) and I ′ (R) contains the tuples in I(R) along with any tuples in the maximal well-formed output for (AcM, b) on the relation R accessed by AcM, interpreted as in D(BackgroundR i ).

  Rule for crossing transitions. Let i > 2. Let d = (s i-1 , ψ, s i ) be a transition. Due to Condition (Deterministic-Transition), there exists one access denoted by (AcM, b) such that ψ + is equal to IsBind AcM ( b) ∧ ψ 1 . The rule associated to d isIDone-Access iAcM ( b) ∶-ReachC i The body formula of this rule is a conjunctive query, and thus clearly a guarded safe positive formula.

  4.5.1. Correctness of translations between formula from A-automaton and Datalog Program. The first claim is concerned with the relationship between the formula ψ + in a self-loop transition d = (s i , ψ, s i ) and the formula ValidBind d . We first need some notation. For a database I and relation R we let R AcM ( b)(I) denote the maximal well-formed answer for the access (AcM, b) on I where Rel(AcM) = R. The set of facts in R composed of the tuples in R AcM ( b)(I) is denoted by (AcM, b, I).

  j , j ≤ i, of D is interpreted as in the relation R of K j ; (ii) each relation Answer(AcM ′ ) i is interpreted by the set of tuples b′ ⋅ t where t ranges over tuples in R AcM ′ ( b′ )(I) for each access (AcM ′ , b′ ) where R = Rel(AcM ′ ); (iii) the relation Bind AcM is interpreted by the singleton tuple b Then ψ + is satisfied by (K, (AcM, b), K + (AcM, b, I)) iff ValidBind d ( b) is satisfied by D.

  interpreted by the set of the tuples b ⋅ t where t is a tuple in R AcM ( b)(I); (iii) the relation Bind AcM contains only the tuple b Then ψ + is satisfied by (K, (AcM, b), K + (AcM, b, I)) iff IsValidBinding d is satisfied by D.

(

  4.5.3. Construction of the partial LTrans paths associated with the partial evaluations of P A .First, we need the following notation: -D i is the instance equal to P f ull i -J →si (D) is the instance over Sch such that -if i = 1 then each relation T is interpreted as in the relation D(IntBackgroundT 0 ), -Otherwise, let AcM and b be the access method and the binding associated with the formula ψ in the transition (s i-1 , ψ, s i ) following Condition (Deterministic-Transition), -for each relation name T different from Rel(AcM), the tuples in J →si (D)(T ) are those in Sch(D i-1 )(T ), -the tuples in J →si (D)(Rel(AcM)) are those in the union of Sch(D i-1 )(Rel(AcM)) along with those in the maximal well-formed output for the access (AcM, b) on a instance I where I(Rel(AcM)) is interpreted as in D(IntBackground(Rel(AcM)) i-1 ) -P f ull,j i (D) is the result of the first j iterations of the rules of P i over D,

4. 6 .

 6 From the emptiness of the linear automaton to the containment of the Datalog program in positive query.

Fig. 3 .

 3 Fig. 3. Complexity and application examples for path specifications.

Fig. 4 .

 4 Fig. 4. Inclusions between language classes.

  , IntBackgroundR h-1 . The tuples in BackgroundR i , i ≤ h, are those that the background database might return when A accesses relation R whilst remaining in the same state s i . The tuples in IntBackgroundR 0 are the tuples of the initial instance. The tuples in IntBackgroundR i , 0 < i < h, are those that the background database returns when A accesses relation R whilst crossing from s i into state s i+1 . -The relation Bind AcM contains the tuples b such that (AcM, b) is an access done in the LTrans path accepted by A. -The union of the relations ViewR 1 , . . . , ViewR i corresponds to the relation R in the instance that A stores internally when it is in s i . Thus each ViewR i will be derived as a union of selections from suitable BackgroundR j and IntBackgroundR j . -The relation Done-Access AcM contains the tuples b such that (AcM, b) is an access leading the path from a state s i to the state s i . -The relation IDone-Access AcM contains the binding leading the path from a state s i-1 to s i . -The predicate ReachC i indicates that there is a path ρ of LTrans and a run r of A that starts in the initial state and ends in the state s i such that r is a run of A on ρ. -A tuple b⋅ t is in Answer(AcM) i iff t is in BackgroundR i and { t} is a well-formed output with the access (AcM, b). A tuple b⋅ t is in IntAnswer(AcM)

i iff t is in IntBackgroundR i and { t} is a well-formed output with the access (AcM, b).

ACM Transactions on Database Systems, Vol. V, No. N, Article A, Publication date: January YYYY.

Acknowledgements This work was funded by EPSRC EP/H017690/1, the Engineering and Physical Sciences Research Council UK. The second author was partially funded by the INRIA project Northern European associate teams between INRIA Lille and University of Oxford.

EXTENSIONS AND LIMITS

We look at the impact of two natural extensions on our decidability results: allowing inequalities and branching formulas.

Extension To Inequalities

Our results on decidable fragments did not use inequalities, and inequalities are useful for expressing data integrity constraints. The most obvious example involves keys and functional dependencies, as discussed in Example 2.5.

By making a straightforward modification of the proofs without inequalities, we can see that inequalities add nothing to the complexity of AccLTL(FO ∃+ 0-Acc ) and its sublanguages. THEOREM 6.1. Letting FO ∃+,≠ 0-Acc be the language of positive queries with inequalities over the restricted vocabulary with only the 0-ary predicates IsBind AcM , we have that -satisfiability of AccLTL(FO ∃+,≠ 0-Acc ) is in PSPACE (and hence PSPACE-complete by Theorem 5.1) -satisfiability of AccLTL(X)(FO ∃+,≠ 0-Acc ) is in Σ P 2 (hence Σ P 2 -complete by Theorem 5.3) Using the language above, one can express relevance or containment in the presence of functional dependencies, access order constraints, and disjointness constraints, but not dataflow constraints.

For the language AccLTL + , shown decidable in Theorem 4.2, inequalities make a dramatic difference. The proof of the theorem below shows that we cannot capture both dataflow restrictions like groundedness along with rich integrity constraints such as functional dependencies, while retaining decidability. The proof also shows that many extensions of AccLTL + with aggregation -basically, any that are expressive enough to capture FDs -will be undecidable. THEOREM 6.2. For binding-positive AccLTL(FO ∃+,≠ Acc ), satisfiability is undecidable. PROOF. Again we reduce the problem of implication of functional dependencies and inclusion dependencies for relational databases to the problem of the unsatisfiability of a AccLTL + with inequalities formula. For simplicity we again assume all positions carry the same type and verify the reduction over instances where all relations are nonempty. This proof uses the same kind of construction as in the proof of Theorem 3.1. The presence of inequalities allows us to simplify the check functional dependencies.

Let Γ be a set of inclusion and functional dependencies, and σ be a functional dependency over Sch. We first give the schema, which extends the relational schema Sch for the dependencies. As in the prior proof, we will have a relation Succ(R) of arity 2k representing a successor relation on tuples of R. There are two relations Beg(R) (with boolean access IsBind Beg(R) ) and End(R) (having boolean access IsBind End(R) ) with the same arity as R; these will store the minimal and the maximal tuples for the ordering generated by Succ(R). In addition there are relations CheckIncDep(R) with the same arity as R, having boolean accesses IsBind CheckIncDep(R) . There are used to check the inclusions dependencies for R.

We now describe the formula ψ ′ such that ψ ′ is satisfiable iff σ is not implied by Γ.

First, ϕ ′ order verifies that each relation Succ(R) represents a total order on k-tuples. To do this, we first check that positions 1 . . . k and k + 1 . . . 2k are primary keys for Succ(R). This can be easily done. For example, for the first primary key condition, we add for each i ≤ k a conjunct:

Similarly to the proof of Theorem 3.1, we can enforce that at any point relation Beg(R) has one tuple in it, and that this tuple does not have a predecessor in Succ(R) -and similarly for End(R).

The main conjunct of our sentence will assert that we fill the successor relations, and finally move into a "verification phase". We will omit further details on the first phase, which uses a variation of the construction to fill the successor relations in Theorem 3.1. We describe only the subformulas specifying the verification phase. ϕ ′ verify will be of the form

where ϕ CheckIds is the same subformula as defined in Theorem 3.1 but ϕ ′ CheckIds and ϕ ′ CheckF dF ailure are different from Theorem 3.1 as they cannot use negation.

Previously in this proof, we have shown how to express that a primary key is satisfied by the relationSucc(R). This construction can be generalized to express the satisfactions of the functional dependencies in Γ given the subformula ϕ ′ kwCheckIds . Finally, a variation of the construction, ϕ ′ CheckFdFailure checks the failure of the distinguished functional dependency σ.

We will focus on the formulas enforcing an inclusion dependency id from relation R to relation S, assuming for simplicity that the dependency requires that for each tuple u in R there is a tuple v in S such that u and v agree on the first k positions. The formula enforcing this is of the form:

This describes an access path p that begins by using a tuple that is in Beg(R), performing an access to CheckIncDep(id) with this tuple, checking that this tuple has a witness for id and adding it to CheckIncDep(i). The formula states that p will then continue doing accesses to CheckIncDep(id), using tuples whose predecessor is already in CheckIncDep(id) and which have a witness for id in the successor relation for S. p will only stop when the last tuple in the order is in CheckIncDep(id).

We claim, as in Theorem 3.1, that if this sentence is satisfied by path p, the instance J(p) will witness failure of the implication of σ from Γ, where J(p) is obtained from the final instance in p by taking tuples in the first projection of Succ(R) as well as those in End(R).

Conversely if I witnesses the failure of the implication of σ by Γ, we can form a witness p(I) to the sentence as in Theorem 3.1.

The reader may want to look at Figure 4 for a view to how the languages with inequalities relate to the languages defined previously.