Querying Data Graphs with Arithmetical Regular Expressions

1 Introduction

Recently, there has been a growing interest in graphs as means of representing data (see surveys [Barcel´o, 2013; Angles and Gutierrez, 2008]), where besides querying the stored data, one can reason about the links among the data.

In these applications, the graph databases tend to be too big to fit in the modern computers' memory. Therefore, a typical criterion of feasibility of a query language is having data complexity in NL, the class of problems solvable in non-deterministic logarithmic space [Calvanese et al., 2006; Artale et al., 2007; Barcel´o et al., 2012]. Checking whether there is a path between two given nodes is already NLcomplete, so NL is the best complexity we can obtain for any reasonable language.

Our contribution. We propose a query language, called LARE, which subsumes several previous formalisms, allows to express new interesting properties and at the same time keeps data complexity of query answering in NL.

LARE allows for writing queries against both nodes and paths given as input. A query can existentially quantify nodes and paths and check relationship between many paths using relational conditions defined by arithmetic regular expressions (ARE), which are regular expressions with registers that allow for various arithmetic comparisons between registers as well as for nesting. The main innovation of the LARE queries lays in the ability to express various arithmetic and aggregative properties of nodes and paths, hence we assume natural numbers as the data values. Nevertheless, our approach can be adjusted to different data domains.

LARE is powerful enough to find, for example, nodes s↪ t such that there is a path p from s to t such that p visits a node with the maximal value in the graph and the total sum of all the elements of p is in a given interval. LARE allows for using nested queries and their negation. This facilitates formulation of properties such as there is a one-way path from s to t, i.e. a path in which for any two consecutive nodes v↪ v′ , there is no path from v′ to v. Properties like these occur naturally in reasoning about multi-agent systems. Agents are often represented by a Kripke structure, which is basically a labelled graph with distinguished initial states. The considered Kripke structures are typically very large due to the state explosion problem. The query answering algorithm we propose works in (non-deterministic) logarithmic space in size of the generated Kripke structure, but can be easily adjusted to reason in polynomial space in size of a succinct representation of a multiagent system, i.e., without generating the exponentially large Kripke structure. Further examples are in Section 5.

We associate with each graph a separate finite automaton, which recognizes the paths of this graph satisfying the query. Based on this idea, we introduce effective relational conditions, a succinct formalism for representing a family of such automata, containing one automata for each graph. The query answering problem for effective relational conditions is NL-complete. We provide a translation from LARE queries into effective relational conditions, which proves that the data complexity of the query answering problem for LARE queries is in NL. The combined complexity is PSPACE-complete.

Query languages for graphs and LARE. Many of the query languages for graphs are extensions of Regular Path Queries (RPQ) [Cruz et al., 1987]. RPQs can be written in the form x →⇡ y ∧ ⇡ ∈ L(e) where e is a (standard) regular expression. Such queries return pairs of nodes (v↪ v′ ) connected by a path ⇡ such that the labelling of ⇡ form a word in L(e). Conjunctive Regular Path Queries (CRPQs) (see QCRPQ on Fig. 1) are closure of RPQs under conjunction and existential quantification [Consens and Mendelzon, 1990; Mendelzon and Wood, 1995], CRPQs with inverse [Calvanese et al., 2000] allow traversing graph edges back.

Barcelo et al., [2012] considered extended CRPQs (ECRPQs) that have the ability to output and compare not only tuples of nodes, but also tuples of paths (see rECRPQ on Fig. 1).

Tuples of paths can be compared by regular relations [Elgot and Mezei, 1965; Frougny and Sakarovitch, 1993]. Examples of such relations are path equality, length comparisons, prefix (i.e., a path is a prefix of another path), fixed edit distance etc. Regular relations on n-tuples of paths can be defined by the standard regular expressions over alphabet of n-tuples of edge symbols. Such regular expressions are the basic building block of LARE, in particular LARE queries without register assignment and constraints can be seen as unions of ECRPQs. Query answering for ECRPQs is computationally feasible: its combined complexity is PSPACE-complete and data complexity is NL.

The formalisms mentioned above assume that graph edges are labelled by a finite alphabet. In practice, graph nodes often store data values from infinite alphabet and there is a strong need for query formalisms that can combine graph topology and data values tests. In such graphs, paths are interleaved sequences of data values and edge labels. This is closely related to data words [Neven et al., 2004; Demri et al., 2007; Segoufin, 2006; Boja´nczyk et al., 2011]. Data complexity of query answering for most of the formalisms for data words is NP-hard [Libkin et al., 2016].

Regular Queries with Memory (RQMs) [Libkin and Vrgoˇc, 2012; Libkin et al., 2016] are again of the form x →⇡ y ∧ ⇡ ∈ L(e), however e is now Regular Expression with Memory (REM). Such queries return pairs of nodes connected by a path in L(e). REMs resemble standard regular expressions but they can store in a register the data value at the current position and test its equality with other values stored already in registers (see rRQM on Fig. 1). Data complexity of RQMs is NL. Arithmetical regular expressions of LARE, called ARE, have been inspired by REM-essentially ARE over single path and with constraints having only (dis)equality tests on data values are equivalent to REMs. However, in contrast to REM, ARE work over tuples of paths, which can be compared by regular relations (as in ECRPQs), registers of ARE store nodes of the graph rather than data values and ARE incorporate arithmetical functions and arbitrary comparisons in register constraints. REMs together with their weaker versions (REWB and REWE) have been further studied in [Libkin et al., 2015].

Walk Logic [Hellings et al., 2013] is a powerful extension of FO with path quantification, and tests of equality of data values on paths. Query answering for WL is decidable but its data complexity is not elementary [Barcel´o et al., 2015].

Finally, Register Logic [Barcel ´o et al., 2015], is essentially, the language of REMs closed under Boolean combinations, node, path and register assignment quantification. Interestingly, it allows for comparing data values in different paths. Its query answering is costly but for the positive fragment RL+ data complexity drops to NL. A particularly interesting fragment is nested RL+ where nested REMs (NREMs) can be used instead of REMs. Nested REMs extend REMs with a branching operator that can filter those nodes in a graph that are the starting point of a path that can be parsed by a nested query which can be NREM again. Data complexity for NRL+ stays in NL. Constraints of ARE allow for nested queries which capture this kind of branching.

Our language LARE can express all the ECRPQ and NRL+

"x and y have a common descendant":

QCRPQ(x↪ y) = x →⇡ z ∧ y →⇡′ z ∧⇡↪ ⇡′ ∈ L(desc∗ ) "x and y are connected to some node by paths having the same labelling from the alphabet ⌃":

"x and y are connected by a path in which a data value is repeated": QRQM = x →⇡ y ∧ ⇡ ∈ L(⌃∗ ⋅ ↓ r ⋅ ⌃+ ⋅ [r= ] ⋅ ⌃∗ ).

Figure 1: Basic features of formalisms that LARE builds over. ↓ r stores the current data value in a register r and [r= ] tests whether the data value stored in r equals the current one.

properties and more, as LARE can test various arithmetical conditions rather than just the equality and refer to nodes' neighbourhood. We provide some concrete examples in the paper, e.g. in Example 1 we show a query ↵fad that looks for paths that always choose the next node with the most occurring value in a set of candidates. This query is not expressible in NRL+ or ECRPQ.

Figueira and Libkin [2015] proposed a language to express properties of edge labels of paths, such as the number of aedges following b-edges is the same as the number of b-edges following a-edges. Data complexity of its query answering problem is in NL, and the proof relies on a tailored version of Parikh automata. We note that it is possible to combine the result with ours, i.e., to have a query language able to express both kind of properties with NL complexity.

2 Graphs and queries

Graphs. We fix a finite set of edge labels ⌃. A ⌃↪ N-labelled graph, or simply a graph, is a tuple G = ￿V↪E↪ λ￿ where V is a finite set of nodes, E ⊆ V ×⌃ ×V is a set of edges labelled

A word is an element of the language defined by V (⌃V )∗ . A node v′ is an e-successor of v if E(v↪ e↪ v′ ). A path is a word p = v0e1v1 ▷ ▷ ▷ vk such that vi is an ei-successor of vi-1

by ⌃, and λ ∶ V → N is a labelling of nodes. The size of a graph G is defined as ￿G￿ = ￿V ￿ + ￿E￿ + ∑v∈V λ(v), i.e., the labels of nodes are represented in the unary notation, which means that their binary representation is logarithmic in the size of the graph. This allows us to compute arithmetical relations on these labels in logarithmic space. The question, which arithmetical relations can be computed in logarithmic space w.r.t. input number given in binary, is related to long-standing open problems, e.g., whether linear programming admits strongly-polynomial algorithm.

for every i ∈ {1↪ ▷ ▷ ▷ ↪ k}. An n-ary relational condition is a graph indexed family of relations R = {RG ∶ G is a graph} such that each RG is an n-ary relation on the paths from G. This may be seen as an n-ary relation on paths, which depends on a graph.

Syntax of queries. Queries Q are defined by the BNF expression Q ∶∶= Q∨Q ￿ Q∧Q ￿ xi →xk xj ￿ R(xi1 ↪ ▷ ▷ ▷ ↪ xin ), where n↪ i↪ j↪ k↪ i1↪ ▷ ▷ ▷ ↪ in ∈ N ￿ {0}, R ranges over n-ary relational conditions and x1↪ x2↪ ▷ ▷ ▷ are variables.

Variables are intended to range over paths; nodes are considered as special cases of paths. Free variables of a query can be distinguished by listing them after the query name, e.g., Q(x1↪ ▷ ▷ ▷ ↪ xk) denotes a query whose variables x1↪ ▷ ▷ ▷ ↪ xk are free; the remaining variables are existentially quantified. Semantics of queries. The satisfaction relation ￿G, which takes a vector of paths ￿ p = (p1↪ p2↪ ▷ ▷ ▷ ). and a query Q, is recursively defined as follows. We assume that for each i, the path pi is the value of the query variable xi.

• ￿ p ￿G Q1 ∧Q2 if ￿ p ￿G Q1 and ￿ p ￿G Q2, · ￿ p ￿G xi →xk xj if pi, pj are single-node paths and pk is a path from pi to pj,
• ￿ p ￿G Q1 ∨Q2 if ￿ p ￿G Q1 or ￿
• p ￿G Q2,

· ￿ p ￿G R(xi1 ↪ ▷ ▷ ▷ ↪ xin ) if RG(pi1 ↪ ▷ ▷ ▷ ↪ pin ). A query Q(x1↪ ▷ ▷ ▷ ↪ xl) holds for paths p1↪ ▷ ▷ ▷ ↪ pl of a graph G, denoted as QG(p1↪ ▷ ▷ ▷ ↪ pl), if there are paths pl+1↪ pl+2↪ ▷ ▷ ▷ such that (p1↪ p2↪ ▷ ▷ ▷ ) ￿G Q. For example, Q(x1) = x1 →x2 x3 ∧x4 →x5 x1 ∧R(x2↪ x5) states that there are two paths, one starting and one ending in x1 satisfying R.

The query-answering problem is formalised as follows: given a graph G, a query Q(x1↪ ▷ ▷ ▷ ↪ xl) and (input) paths p1↪ ▷ ▷ ▷ ↪ pl, does QG(p1↪ ▷ ▷ ▷ ↪ pl) hold? We are interested in the data complexity of the problem, where the size of a query and its input paths is treated as constant, and combined complexity, where there is no such restriction.

3 Arithmetical regular expressions

Different relational conditions lead to different expressive power and complexity of queries. As we are interested in queries regarding large systems, representing, for example, Web topology, social networks or Kripke structures, we restrict our attention to relational conditions defining queries whose data complexity is in NL. In this section, we propose n-ary arithmetical regular expressions (ARE), which define relational conditions satisfying this complexity requirement. ARE are regular expressions with arithmetical functions and memory. The memory is formalized as an infinite set of reg-

of all nodes. By X￿ we denote the set X extended with ￿. We assume a finite set Φ of functions f ∶ (N￿ ∪ {∞})∗ → N ∪ {∞} computable by a non-deterministic Turing machine whose size of working tape and output tape while computing f(x1↪ ▷ ▷ ▷ ↪ xk) is O(logk + max(￿x1￿↪ ▷ ▷ ▷ ↪ ￿xk￿)), assuming binary representation and ￿∞￿ = ￿￿￿ = 1. These conditions are satisfied by aggregative functions such as summation, maximum, minimum (∞ is included for empty set), counting and conditional functions like if x1 is odd then x2 else x3.

isters R = {ri ￿ i ∈ N}, storing nodes. It is convenient to reason about paths of the same length. To cope with paths of different lengths, we use ￿ as a special blank (padding) symbol for nodes and edges and assume E(v↪ ￿↪ ￿) for any v ∈ V￿ and λ(￿) = ￿. One may think that G has an additional dummy node ￿, which is a ￿-successor

Syntax of ARE. We define register constraints C and n-ary arithmetical regular expressions ↵ as follows

where r ranges over R, f ranges over Φ, P ranges over expressions of the form λ(r) or f[r ∶ C], e ∈ ⌃, ￿ e ∈ ⌃n ￿ ,

j ∈ {1↪ ▷ ▷ ▷ ↪ n↪ ￿} and Q is a (nested) query. By AREn we denote the class of all n-ary arithmetical regular expressions. We allow standard logical abbreviations, such as ∧↪∀↪⇒, defined as usual. We put E(r↪ ↪ r′ ) = ￿a∈⌃E(r↪ a↪ r′ ) to express there is a (⌃-labelled) edge between r and r′ . Notice that our constraints are standalone entities rather than evaluations applied to subexpressions.

To simplify presentation we require that the register constraints and arithmetical functions only express properties of nodes stored in registers. Hence, all the nodes of the paths have to be stored in registers using the [r←i] syntax prior to their access. However, it is easy to circumvent this by assuming n distinguished registers storing the values of the current nodes.

Register constraints allow for Boolean operators (including negation), comparing arithmetical formulas, quantification, checking equality and connectedness of nodes stored in registers and checking nested queries. Note that we allow for negation in front of nested queries, and that the parameters of nested queries are only (nodes stored in) registers. The arithmetical formulas are the way of expressing properties of values of the nodes stored in registers. The construction f[r ∶ C], that can be read as the function f applied to the values of all r satisfying a given condition. For example, max[r1 ∶ E(r2↪ e↪ r1)] stands for the maximum value of e-successors of the node stored in r2.

Let f￿X￿ denote the result of function f ∈ Φ whose arguments are elements of X given in a non-decreasing order. Semantics of register constraints. A graph G = (V↪E↪λ) and a valuation σ satisfy a constraint C, denoted by G↪ σ ￿ C, if one of the following holds:

A valuation σ ∶ R → V￿ is a function that assigns nodes to the registers. For a valuation σ, we define σ[r ← vi] as the valuation such that σ[r←vi](r) = vi and σ[r←vi] coincides with σ on all inputs except r.

• C ≡ C1 ∨ C2 and G↪ σ ￿ C1 or G↪ σ ￿ C2,
• C ≡ ℜC ′ and G↪ σ ￿￿ C ′ ,
• C ≡ r = r′ and σ(r) = σ(r′ ),
• C ≡ ∃r▷C ′ and there is v ∈ V s.t. G↪ σ[r←v] ￿ C ′ , · C ≡ f(P 1 1 ▷ ▷ ▷P 1 k ) ≤ g(P 2 1 ▷ ▷ ▷P 2 l ) and f(v1 1 ▷ ▷ ▷ v1 k ) ≤ g(v2 1 ▷ ▷ ▷ v2 l ), where vj i = λ(σ(r)) if P j i ≡ λ(r) and vj i = f￿{λ(v) ￿ G↪ σ[r←v] ￿ C}￿ if P j i ≡ f[r ∶ C].

· C ≡ ￿Q￿(ri1 ↪ ▷ ▷ ▷ ↪ rik ) and QG(σ(ri1 )↪ ▷ ▷ ▷ ↪ σ(rik )). The convolution of sequences s1↪ ▷ ▷ ▷ ↪ sn, denoted by s1 ⊗ ▷ ▷ ▷ ⊗ sn, is the sequence s of the length k of the longest sequence among s1↪ ▷ ▷ ▷ ↪ sn, such that for every i ∈ {1↪ ▷ ▷ ▷ ↪ k}, the ith element of s is the vector (a1↪ ▷ ▷ ▷ ↪ an), where aj is the ith element of sj if it exists and ￿ otherwise. In plain English, convolution joins n sequences into one sequence of the length of the longest sequence and fills the missing places

• C ≡ E(r↪ e↪ r′ ) and E(σ(r)↪ e↪ σ(r′ )),

with ￿. An n-path of G is the convolution of n paths of G. We define a concatenation ▷ of two n-paths p1 = v0e1 ▷ ▷ ▷ vk and p2 =

v′0 e′1 ▷ ▷ ▷ v′k such that vk = v′0 as p1▷p2 = v0e1 ▷ ▷ ▷ vke′1 ▷ ▷ ▷ v′k (i.e., the common node is not repeated). A splitting of an n-path p is a sequence of n-paths p1↪ ▷ ▷ ▷ ↪ pl such that p = p1▷p2▷ ▷ ▷ ▷ ▷pl.

• ↵ ≡ ✏, p is a single element and σ = σ′ ,

Language of ARE. We define the relation ￿ with the following meaning: (↵↪ p↪ σ) ￿G σ′ if evaluating an expression ↵ over a n-path p of a graph G with a valuation σ results in valuation σ′ , i.e., if one of the following holds.

• ↵ ≡ ￿C￿, p is a single element, G↪ σ ￿ C and σ = σ′ , · ↵ ≡ [r←j], p is a single element (a1↪ ▷ ▷ ▷ ↪ an) and σ′ = σ[r ← aj] if j ≠ ￿ and ￿ otherwise,
• ↵ ≡ ￿ e, p = v1￿ ev2 where v1↪ v2 are single elements and
• ↵ ≡ ↵1 + ↵2 and (↵1↪ p↪ σ) ￿G σ′ or (↵2↪ p↪ σ) ￿G σ′ , · ↵ ≡ ↵+1 and there are a splitting p = p1▷ ▷ ▷ ▷ ▷pk and valuations σ = σ0↪ σ1↪ ▷ ▷ ▷ ↪ σk = σ′ such that for each
• σ = σ′ , · ↵ ≡ ↵1▷↵2 and there is a splitting p = p1▷p2 and a valuation σ′′ s.t. (↵1↪ p1↪ σ) ￿G σ′′ and (↵2↪ p2↪ σ′′ ) ￿G σ′ ,

i ∈ {1↪ ▷ ▷ ▷ ↪ k} we have (↵1↪ pi↪ σi-1) ￿G σi, Then, the language of an ARE ↵ is defined as LG(↵) = {p ￿ ∃σ↪ σ′ ▷(↵↪ p↪ σ) ￿G σ′}. We define ↵G(p1↪ ▷ ▷ ▷ ↪ pn) iff ￿ p1 ⊗ ⋅ ⋅ ⋅ ⊗ ￿ pn ∈ LG(↵); therefore, each ARE can be treated as a relational condition.

Example 1. Consider the following ARE.

↵gss = ([r1 ←1] + ▷ ▷ ▷ + [rn ←n] + ⌃n ￿ )∗ The language of ↵grd consists of all greedy paths, i.e., paths in which, at every position, the following node on the path has maximal value among all successors of the current node. To see that, observe that while traversing path ↵grd keeps the next-to-latest (on the path) node in register r1 and the latest node in r2. After each edge move, denoted by ⌃, a greedy condition Cgrd is checked, whether it holds that r2 is a maximal neighbour of r1. The language of ↵G fad consists of paths in which, at every position, the following node on the path has the value that has the most number of occurrences among the successors of the current node. To express that, ↵fad uses arithmetic formula P(z) counting number of occurrences of value λ(z) in the neighbourhood of r1. count is a function (fromΦ) that returns the number of elements given on input. The last example demonstrates processing multiple paths. We have ↵G com(x1↪ ▷ ▷ ▷ ↪ xn) iff paths x1↪ ▷ ▷ ▷ ↪ xn have a common node. The idea is to guess (↵gss) a common node for each path separately, and verify the equality at the end.

The query language LARE is the language containing queries whose all relational conditions are ARE. We conclude this section with a Theorem whose proof will follow from more general theorems provided later on.

Theorem1. The query answering problem for LARE queries with bounded nesting depth is in PSPACE and its data complexity is NL.

4 Effective relational conditions

We introduce the notion of effective relational conditions, which facilitates the proof of Theorem 1, and show that ARE are effective relational conditions (Theorem 4). The name effective is justified by the fact that answering queries with effective relational conditions can be done within the desired complexity bounds (Theorem 3). We assume that the reader is familiar with finite automata and Turing machines (see [Hopcroft and Ullman, 1979]).

An Automata Giving Turing Machine (AGTM) is a nondeterministic Turing Machine which works in logarithmic space and only accepts inputs of the form i?w, where i ∈ {0↪ 1}∗ , ? ∈ {?Γ ↪ ?S↪ ?I↪ ?F ↪ ?δ}, and w ∈ {0↪ 1↪ ; }∗ is such that ￿w￿ = O(log(￿i￿)). An AGTMΜgives (on-the-fly) a set of (nondeterministic) automata {Αi}i∈{0↪1}∗ such that each Αi is of the form (Γi↪Si↪ Ii↪ δi↪Fi), where

• Fi consists of final states q ∈ Si s.t. Μaccepts on i?Fq. · δi consists of transitions (q↪ e↪ q′ ) ∈ Si ×Γi ×Si s.t. Μ accepts on i?δq; e; q′ .
• Γi ⊂ {0↪ 1}∗ consists of labels e s.t. Μaccepts on i?Γ e, · Si ⊂ {0↪ 1}∗ consists of states q s.t. Μaccepts on i?Sq.
• Ii consists of initial states q ∈ Si s.t. Μaccepts on i?Iq.

An AGTM M represents a n-ary relational condition R if M gives a set of automata {Αi}i∈{0↪1}∗ s.t. for all graphs G and words w1↪ ▷ ▷ ▷ ↪ wn, the automaton ΑG accepts w1 ⊗ ▷ ▷ ▷ ⊗ wn iff (w1↪ ▷ ▷ ▷ ↪ wn) ∈ RG (we assume an encoding of graphs as binary sequences). A relational condition R is effective if there is an AGTMM that represents R. A query is effective if its all relational conditions are given as AGTMs.

Lemma 2. Let R→ be a relational condition such that RG→(x↪ x1↪ x′ ) holds iff x →x1 x′ . Then R→ is effective.

The machine Μ answers questions i?Xx regarding components (the alphabet, the set of states, etc.) of ΑG, where G is the graph encoded by i. All components are sets of tuples of nodes and labels of G extended with the padding symbol ￿. All these sets of tuples are defined using the edge relation in G, equality among components of the tuples and equality to ￿. In any reasonable representation of G; e.g., a list of nodes followed by an adjacency list, ￿G￿ is proportional to i, length of description of labels and nodes of G is logarithmic in i, and the machine Μ can compute in log i space (hence in log ￿G￿ space) whether a given word encodes a label (resp., a node or an edge) of G. Since the length of elements of tuples, i.e., labels and nodes of G is logarithmic in i, the equality among components of tuples (and equality to ￿) can be checked in

Proof. We define an AGTM Μ that gives automata {Αi}i∈{0↪1}∗ such that for a given graph G, the automaton ΑG recognizes words over the alphabet V 3 ￿ ∪⌃3￿, which encode convolutions w1 ⊗w2 ⊗w3 such that w1↪w3 are single-node paths and w2 is a path in G from the node w1 to w3. ΑG reads letters corresponding to nodes v and labels e and stores last read letters in its state. Next, while it reads a letter corresponding to a node v′ , it checks whether G has an edge from v to v′ labeled with e. Moreover, the automaton ΑG stores in its state the node vf , which is supposed to be the last node and accepts only if the last read letter is vf .

log log i space. Therefore, the machine Μ on inputs i?Xx requires log(i) space, i.e., Μ is an AGTM.

Proof sketch. Consider a query Q(x1↪ ▷ ▷ ▷ ↪ xk) whose relational conditions are effective. For any paths p1↪ ▷ ▷ ▷ ↪ pk, we define in the straightforward way an effective relational condition Rp1↪▷▷▷↪pk such that RG p1↪▷▷▷↪pk (⇡1↪ ▷ ▷ ▷ ↪ ⇡k) iff p1 = ⇡1, . . . , pk = ⇡k. This and Lemma 2 imply that we can assume that our query has no free variables and is built of conjunction, disjunction and effective relational conditions. One can observe that effective relational conditions are closed under shuffling, joining and adding spurious arguments, and therefore we can assume that all of them have the same arguments. By employing an argument similar to the standard powerset construction for finite automata, we can reduce in polynomial time a query to a single effective relational condition RQ↪p1↪▷▷▷↪pk .

Theorem 3. Answering effective queries with m conditions is in NSPACE(m+c log(n)), where c log(n) is the space bound on AGTMs representing the conditions.

Given a graph G, answering QG(p1↪ ▷ ▷ ▷ ↪ pk) amounts to checking emptiness of RG Q↪p1↪▷▷▷↪pk , which amounts to checking whether a corresponding automaton AG is empty. This can be done by employing the standard graph reachability algorithm, which checks reachability of an accepting state from initial states by guessing the consecutive states. Since states are logarithmic in i, the problem is in NL.

The AGTM for the relational condition RQ works in space proportional to the number of atomic formulas of the query (m) plus the maximum of the space usage of AGTMs representing relational conditions in Q (c log(n)). Therefore, the combined complexity is as required.

Let 0-ARE be the empty set and (d + 1)-ARE be the subset of ARE containing expressions whose all nested queries are built of relational conditions from d-ARE.

Theorem 4. Every ARE relational condition R is effective and if R is d-ARE, then an AGTM working in space ￿R￿⋅log(n) representing R is computable in polynomial time.

Proof sketch. We prove Theorem 4 by induction w.r.t. d . The basis of induction is trivial as the set 0-ARE is empty. Assume that for any R ∈ d-ARE one can compute in polynomial time in ￿R￿ an AGTM computing R that works in space ￿R￿ log(n). Evaluating register constraints. We first show that for a given register constraint C whose nested queries are built of d-ARE, one can compute in polynomial time in ￿C￿ a non-deterministic Turing machine ΜC that works in space ￿C￿ log ￿G￿ and decides, for a graph G and a registers valuation σ, whether G↪ σ ￿ C. The construction of ΜC is a topdown recursion on C and can be done in polynomial time. The space used by ΜC is bounded by O(￿C￿ log ￿G￿), which, using tape compression [Hopcroft and Ullman, 1979], can be replaced by ￿C￿ log ￿G￿. Below we discuss the most interesting recursive cases.

To compute f[r ∶ C], observe that using additional space log ￿G￿, we can implement a virtual tape storing λ(v1) ≤ ▷ ▷ ▷ ≤ λ(vl), where v1↪ ▷ ▷ ▷ ↪ vl are all nodes of G satisfying C, i.e., we can implement a subroutine that for a given i returns λ(vi). Such a subroutine iterates over all nodes v of G. For each v, it computes iv1 (resp., iv2 ) defined as the number of nodes u, which satisfy C and λ(u) < λ(v) (resp., λ(u) ≤ λ(v)), and checks whether iv1 < i ≤ iv2 . In such a case we know that all elements between iv1 + 1 and iv2 have the same value λ(v). Next, with such a virtual input tape we execute a non-deterministic Turing machine Μf computing ing NL = CONL. We execute ΜQ and ΜℜQ in parallel. Evaluating (d + 1)-ARE . Now we prove the inductive thesis. Let R be a (d + 1)-ARE relational condition defined by (d + 1)-ARE ↵. For a graph G, we define three automata ΑG1 ↪ΑG2 and ΑG3 over an alphabet Γ consisting of tuples of edge labels ⌃n ￿ , nodes V n ￿ , symbols {aC ∶ C from R} referring to register constraints and {br↪j ∶ [r ← j] from R} referring to register assignments. We substitute in ↵ subexpressions ￿C￿ (resp., [r ←j]) by letter aC (resp., br↪j). The resulting ↵reg is a regular expression and ΑG1 recognizes the language of ↵reg , i.e., ΑG1 accepts words over Γ that satisfy R while neglecting the graph structure G and the register constraints checks in R. For the register constraints checks, this automaton verifies only that the letters aC (resp., br↪j) occur at positions that correspond to register constraints checks ￿C￿ (resp., assignments [r ← j]) in R. The automaton ΑG2 checks consistency of register constraints checks marked by aC provided that register assignments are executed done according to markings br↪j, employing the machine ΜC defined above. The automaton ΑG3 recognizes words that, with letters aC and br↪j deleted, are n-paths of G. Finally, we construct ΑGR , which is the product of automata ΑG1 ↪ΑG2 and Α3 projected on the alphabet ⌃n ∪ V n . Observe that ΑGR recognizes the languages of all n-paths satisfying R. It can be shown that the construction of automata ΑG1 ↪ΑG2 andΑG3 can be performed in a way that ensures that the sets containing all such automata can be given on-the-fly.

f ∈ Φ. All such Turing machines work in space O(log ￿G￿). Consider a nested query ￿Q￿(ri1 ↪ ▷ ▷ ▷ ↪ rik ). All the relational conditions of Q are d-ARE, therefore by Theorem 3 and the inductive assumption, we can compute (in polynomial time) a non-deterministic machine ΜQ that computes ￿Q￿(ri1 ↪ ▷ ▷ ▷ ↪ rik ) in space ￿Q￿ log ￿G￿. We also compute a non-deterministic machine ΜℜQ that in space cIS ⋅ ￿Q￿ log ￿G￿ computes ℜ￿Q￿(ri1 ↪ ▷ ▷ ▷ ↪ rik ), where cIS is the constant from Immerman-Szelepcs´enyi theorem [Immerman, 1988] show-

Finally, we show how Theorems 3 and 4 imply Theorem 1. Let d > 0 and consider LARE queries of nesting depth bounded by d, i.e., queries whose relational conditions are (d + 1)-ARE. For every such query Q, Theorem 4 states that for every relational condition R from Q, one can construct in polynomial time an AGTM working in ￿R￿ log(n) space, which represents R. Next, observe that the sum of the number and the sizes of relational conditions from Q is bounded by Q. Therefore, by Theorem 3, space required to answer Q is bounded by ￿Q￿ log(n). Consequently, the query answering problem is in PSPACE and its data complexity is in NL.

Remark. We have shown that for a given query Q and a graph G we can obtain a single relational condition R

and then an automaton ΑGR accepting all n-paths w over V n (⌃nV n )∗ such that w is a convolution of paths that satisfy Q. Note that we can modify ΑGR to be able to process paths that remember also the values of the nodes, i.e., the paths over (V ×N)n (⌃n (V ×N)n )∗ . Therefore, we can state our result in the following alternative version:

Corollary 5. For each ⌃↪N-labelled graph G and a LARE query Q with k variables, there is a ⌃k ↪ Nk -labelled graph G′ of size polynomial in ￿G￿ and sets of nodes I, F such that a word w is a path from I to F in G′ iff w is a convolution of paths that satisfy Q.

5 Examples

We show how ARE power the LARE queries, and combine nicely with language features like nested queries, condition negation, or aggregative functions. For convenience, we define a macro [ n←￿] = [r1 ← 1] ▷ ▷ ▷ [rn ← n] that stores nodes from first n paths into registers 1↪ ▷ ▷ ▷ ↪ n. We allow to use different variables than xi and assume variables x↪ y↪ xi↪ yi to be nodes, this can be enforced by appending the atom x →⇡ x to query body; we treat it as implicitly written.

Basic techniques. Consider the queries

Q4▷1(x↪ y↪ z) = x →⇡1 y ∧ x →⇡2 y ∧ Q≠(x↪ ⇡1↪ ⇡2). The query Q≠ checks whether a node x appears in path ⇡1 but not ⇡2. The query Q2 checks whether a given path has unique nodes with respect to strongly connected components. The query Q3 that check whether a given graph is a directed acyclic graph. The query has no parameters, so it is considered over the 0-path consisting of one node which is an empty tuple, (). We use negation on query saying ⇡ has return edge. No return edges means that G is acyclic.

The query Q4(x↪ y) asks whether there is only one path between x and y, up to nodes rearrangement. Q4▷1(x↪ y↪ z) says that one can find two paths between x and y that differ on whether they contain node z. Expression ↵ recognizes pairs of nodes x1↪ y1 for whom it is impossible to show two paths, that would differ on some node. So, in other words, all paths between x and y take usage of same set of nodes. Q4(x↪ y) additionally checks that there is at least one path from x to y.

Aggregative properties. We show that LARE is capable of recognizing some basic aggregative properties of paths. We demonstrate this on the ARE sum≤c, stating that the sum of weights on a path do not exceed the constant c.

The register r1 is used to store the current node, registers r2↪ ▷ ▷ ▷ ↪ rc+1 contain the previous nodes whose data value was positive, and rc+2 contains ￿ (for comparing). At every node, the regular expression evaluates ↵store. If the value of the node is 0, then nothing happens. If the value is positive, then the node is stored in one of registers among r2, . . . , rc+1 containing ￿. If there is no such register, it means that there are already c nodes with positive value on the paths, meaning that sum of weights on the path exceeds c, in which case the path will not be matched. At the end, it is checked whether the sum of nodes in the registers do not exceed c.

The concept of checking lower and upper bound on the sum of path weight can be extended in natural way to n-paths. Kripke structures and multiagent systems. LARE may be seen as a handful tool to verify properties of Kripke structures, which are essentially graphs with distinguished initial states. Finite Kripke structures are often obtained from programs with unbounded numbers by means of abstraction [Clarke et al., 2000], and therefore the obtained labels may be treated as data values. We are especially interested in the multiagents setting, where edge labels correspond to agents' actions. LARE is expressive enough to express properties such as there is a path from an initial state q0 to a final state qf such that no action of one of the agents at any single state will result in reaching an undesirable state qB. For epistemic logics [ ˚Agotnes et al., 2015], node labels may be seen as a representation of a local state of an agent. The technique presented in this paper can be straightforwardly generalised to graphs with more than one node-labelling function in order to deal with more agents.

Our query language then is powerful enough to formulate indistinguishability in the epistemic interval-temporal logic EHS [Lomuscio and Michaliszyn, 2013], where two paths are indistinguishable for an agent i if they are of the same length and the corresponding states of both paths are indistinguishable/have the same label for i. In particular, QK1 (below) expresses that there is a path indistinguishable but different from ⇡. QK2 expresses that there is a path from x to y indistinguishable from ⇡1 that visits z while ⇡1 does not. In other words, an agent, who can observe only their local state (node labelling), does not know whether a given path avoids z.

6 Conclusion and future work

We introduced the query language LARE for data graphs, suited for expressing arithmetical properties of nodes, paths between nodes and their neighbourhoods. We showed that the query answering problem for LARE can be solved in logarithmic space in size of the graph by employing a new formalism called effective relational conditions.

LARE expresses some aggregative properties of paths, as exemplified in Section 5. In our future work we plan to incorporate more properties of this type. In particular, are interested in formalisms that can compare sums of values on different paths while keeping the complexity low.

Acknowledgement We would like to thank Leonid Libkin who has introduced the subject to us. This paper has been supported by Polish National Science Center grant UMO2014/15/D/ST6/00719.