Mikołaj Boja
email: bojan@mimuw.edu.pl

Diego Figueira
email: dfigueir@inf.ed.ac.uk

Efficient Evaluation for a Temporal Logic on Changing XML Documents *

Keywords: F.4.1 [Mathematical logic and formal languages]: Temporal logic; H.2.3 [Database management]: Languages-Query languages Theory, Algorithms, Languages Incremental evaluation, XML, temporal logic

We consider a sequence t1, . . . , t k of XML documents that is produced by a sequence of local edit operations. To describe properties of such a sequence, we use a temporal logic. The logic can navigate both in time and in the document, e.g. a formula can say that every node with label a eventually gets a descendant with label b. For every fixed formula, we provide an evaluation algorithm that works in time

where k is the number of edit operations and n is the maximal size of document that is produced. In the algorithm, we represent formulas of the logic by a kind of automaton, which works on sequences of documents. The algorithm works on XML documents of bounded depth.

INTRODUCTION

In this paper, we model an XML document as a finite unranked tree over a finite alphabet. Suppose that an XML * We acknowledge the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under the FET-Open grant agreement FOX, number FP7-ICT-233599.

document is modified by a sequence of local update operations. Each update adds, removes or relabels a node of the document. We want to know if these updates preserve some correctness constraint. This kind of problem is called incremental evaluation. Suppose, for instance, that the correctness constraint is given by a DTD, or more generally a regular language of unranked trees. This problem is solved by an algorithm of Balmin, Papakonstantinou and Vianu [START_REF] Balmin | Incremental validation of XML documents[END_REF]. The algorithm maintains a data structure, and every update on the tree requires an update to the data structure that is done in time

poly(Q) • log 2 (n)
where Q is the state space of the automaton for the correctness constraint and n is the size of the current document. If the correctness constraint is given by an XPath query, the translation from the query into a tree automaton can result in a state space Q that is exponential in the size of the XPath query. The problem has been addressed by [START_REF] Björklund | Incremental XPath evaluation[END_REF], which provides algorithms that work directly with XPath queries.

A limitation of incremental evaluation, as described above, is that the property talks only about the current version of the XML document. In this paper, we study properties that compare versions of the document in different times. Here are some examples:

1. Every order node eventually gets an approved child.

That is, if at some time i a node x has tag name order, then at some time j ≥ i node x has a child with tag name approved.

2. Every node with one child gets a second child in at most two steps. That is, if at some time i, a node x has one child, then node x has at least two children in any time j ≥ i + 2.

To express these examples, we need a logic or formalism that is evaluated not in a single document, but in a sequence of documents t1, . . . , t k .

We use the name document evolution for such a sequence. In this paper we define a logic for document evolutions, which captures the two examples given above. We then study the evaluation problem for formulas ϕ of the logic:

• Input. A document evolution t1, . . . , t k .

• Output. Does ϕ hold in the document evolution?

As in incremental evaluation, the document evolution on the input is not an arbitrary sequence of documents, but a sequence where t1 is an empty document and ti+1 is obtained from ti by doing a local update that consists of adding, removing or relabeling a single document node. In this case, the size of document ti is bounded by i. If the updates consist exclusively of adding nodes, then after time k the combined size of the documents t1, . . . , t k is quadratic in k.

We want an algorithm that works well for large XML documents, with millions of nodes or more. For documents of this size an algorithm that is linear in the combined size of the documents t1, . . . , t k , and therefore quadratic in k, may be impractical. However, when the document evolution is a result of local updates, there is no reason to read the whole document ti for every i ∈ {1, . . . , k}, because this document is almost identical to ti-1. The principal contribution of this paper is an algorithm for the evaluation problem that runs in time

O(k • log(n)),
where k is the duration of the document evolution and n is the maximal document size (of course n ≤ k). We present the algorithm only for XML documents of bounded depth, although we believe it should work for documents of unbounded depth.

To the best of our knowledge, the problem of efficiently evaluating logics on document evolutions has not been studied before. In this paper, we try to optimize the data complexity of the problem, and we assume that the formula of the logic is fixed. Unfortunately, the query complexity of our algorithm is very bad: the constant hidden in the expression O(k • log(n)) is nonelementary in the size of the formula of the logic. That is why this paper is more like a proof of concept: even when the correctness property compares different versions of the document, it is still possible to have an algorithm with very good data complexity.

In this paper, we only talk about the tag names and tree structure of XML documents. That is, we model an XML document as an unranked tree over a finite and fixed alphabet (the tag names). Any additional data in the document, such as attribute values, is ignored. Logics and automata that talk about such additional data are a lively research topic, see the survey [START_REF] Segoufin | Automata and logics for words and trees over an infinite alphabet[END_REF], and in the future we would like to extend our results to the richer logics. Note that for logics that depend on attribute values, such as XPath, the incremental evaluation problem seems to be difficult already for formulas that talk about only the current state of the document. In particular, we are not aware of any algorithm that would be significantly faster than simply reevaluating the XPath query on every new version of the document. By significantly faster we mean an algorithm that would require polylogarithmic time per update operation. Observe that in the presence of additional data, an evalution algorithm for XPath (without any time aspects, just evaluating a query in a given document) with linear data complexity has appeared only recently [START_REF] Miko | XPath evaluation in linear time[END_REF].

Related work.

As already mentioned, [START_REF] Björklund | Incremental XPath evaluation[END_REF] studies the problem of incrementally maintaining the result set of a XPath query on a changing XML document. Algorithms are provided for several fragments of XPath. The queries from [START_REF] Björklund | Incremental XPath evaluation[END_REF] talk only about the current document, and cannot study the change of the structure of the document in time.

There have been efforts to extend the XPath query language to make it time-aware [START_REF] Fourny | A time machine for XML: PUL composition[END_REF]. In this work we choose to work with a temporal logic to talk about different instants of the evolution of a document.

In a similar setup, there have been works on the incremental maintenance of the validity of regular languages [START_REF] Balmin | Incremental validation of XML documents[END_REF][START_REF] Barbosa | Efficient incremental validation of XML documents[END_REF], where the validity of an XML Schema, a DTD or a specialized DTD is checked to be preserved throughout the document evolution.

Abiteboul, Herr and Van den Bussche [START_REF] Abiteboul | Temporal connectives versus explicit timestamps to query temporal databases[END_REF] study the expressive power of some of the logics we work with.

The model of evolution of documents is also related to regular model checking [START_REF] Parosh | A survey of regular model checking[END_REF]. In this field, the evolution of the document is dictated by a regular transducer, whereas here updates can occur anywhere and in any order, in an incremental way. In this context, [START_REF] Parosh | Regular model checking for LTL(MSO)[END_REF] treats a logic similar to ours, LTL(MSO), where first and second order variables are interpreted over positions of the document, and tempral operatores are used to navigate the word in time.

TWO LOGICS

In this section, we define the logics that we use to describe document evolutions. As presented in the introduction, the update operations are: adding and removing nodes, as well as relabeling. In order to simplify the complicated evaluation algorithm, and the definitions of the logics, for the most part of the paper we only use relabeling, and do not add or remove nodes. In particular, all documents in a document evolution will have the same nodes. In Section 7, we come back to the implementation of adding and removing nodes.

Fix an input alphabet A. We deal with finite, unranked, sibling-ordered trees with nodes labeled by A. The domain of a tree is the tree without the labels. A document evolution is a sequence of trees t1, . . . , t k . The number k is the duration of the document evolution, and the number n of nodes in the domain is the document size of the evolution. We work with the assumption that all documents have the same domain. This assumption is made for technical reasons to simplify the algorithm, but this assumption can be lifted, as explained in Section 7. Throughout the paper, we will preserve the convention that n refers to the document size and that k refers to the duration. We use x, y, z to refer to nodes in the domain and variables i, j to refer to moments in time.

In this section we define two logics to describe document evolutions. The first logic is a variant of first-order logic. The second logic is a variant of temporal logic. The evaluation algorithms of this paper are for the temporal logic, and the first-order logic is described mainly to provide some background.

First-order logic. A document evolution t1, . . . , t k with domain X can be treated as a relational structure. The elements of the structure are pairs

(x, i) ∈ X × {1, . . . , k}.
The relational structure is equipped with the following predicates. For each letter a ∈ A in the input alphabet, we have a unary predicate a, which holds for an element (x, i) if node x has label a in the document ti. There are three binary relations:

• The descendant order ≤ desc which ignores the time coordinate of its arguments and compares the nodes for descendant relationship.

• The document order ≤ doc which ignores the time coordinate of its arguments and compares the nodes for document order relationship. This corresponds to the total order induced by the preorder visit of the tree.

• The time order ≤t which ignores the node coordinate of its arguments and compares the times.

Because the predicates above ignore one of the coordinates, they are not antisymmetric when k ≥ 2 or n ≥ 2. Using these predicates, we can write formulas of first-order logic to express properties of document evolutions. For instance, the following formula says that once a document node gets label a, none of its descendants ever have label b afterwards. (We use p, q for the variable names, because x, y, z are reserved for positions, and not space/time pairs.)

∀p∀q. a(p) ∧ p ≤t q ∧ p ≤ desc q ⇒ ¬b(q) (1)
Two-dimensional temporal logic. We now define a logic with temporal syntax, with operators that travel in the time dimension and the space dimension. In particular, formulas of this logic will have no variables. We use the name two-dimensional temporal logic for this logic. This is the principal logic studied in the paper.

In the two-dimensional temporal logic, a formula is evaluated in a pair (x, i) ∈ X × {1, . . . , k} of a document evolution of document domain X and duration k. Instead of quantifiers, formulas use modal operators such G for Globally or U for Until. For instance the property from example (1) is stated as

G desc Gt(a ⇒ G desc Gt¬b).
In the formula above, we begin in the root node in the first document. We then use the G desc Gt operators to say that a ⇒ G desc Gt¬b occurs in all descendants in all later times, and likewise for the smaller formula.

We believe that when describing document evolutions, it is important to allow past operators in the space dimension (i.e. descendants and preceding nodes in document order). For example, consider an XPath unary query α, which selects a position x in a document if it has an ancestor with label a. In XPath syntax this query looks like this: //a// * One might want to say that for every document node x and time i, if node x has label b in time i, then at all later times the node x satisfies the XPath query α

G desc Gt(b ⇒ Gtα).
In the particular example of α, we can write F -1 desc a to search for an ancestor of the current node in the current document.

We now provide the formal syntax and semantics of the temporal logic. As remarked above, a formula of the logic is evaluated in a pair (x, i) of a document evolution t1, . . . , t k . We fix this document evolution in the definition below.

• For every letter of the alphabet, a is a formula. This formula is true in (x, i) if node x has label a in document ti.

• Boolean connectives are allowed, with the usual semantics.

• If ϕ, ψ are a formulas, then ϕU desc ψ is a formula, which is true in (x, i) if there exists a node y > desc x such that ϕ is true in all the pairs (z, i) with x < desc z < desc y and ψ is true in the pair (y, i). Observe that we use the strict until operator, which does not use the current position. Often, one uses the non-strict until, which is defined by

ψ ∨ (ϕ ∧ (ϕU desc ψ)).
The strict until allows one to define all other operators as derived constructs:

X desc ϕ def = ⊥U desc ϕ F desc ϕ def = ( U desc ϕ) ∨ ϕ G desc ϕ def = ¬F desc ¬ϕ
• If ϕ, ψ are formulas, then ϕU -1 desc ψ is a formula, which is the inverse of the U desc operator. This operator is often called since. As in the previous item, we can define all sorts of derived operators.

• Let ≤ sib be sibling order, where x ≤ sib y if x and y are siblings, and x is to the left of y. If ϕ, ψ are formulas, then ϕU sib ψ and ϕU -1 sib ψ are formulas, defined in the same way as before, for the sibling order ≤ sib .

• Finally, we allow an until operator Ut that works in the time dimension, i.e. ϕUtψ holds in (x, i) if there is a time moment j > i such that ϕ is true in the pairs (x, i + 1), . . . , (x, j -1)

and ψ is true in the pair (x, j).

Observe that we do not allow a since operator in the time dimension. Such a logic would make perfect sense, but we do not know how to extend our evaluation algorithm to cover a since operator in the time dimension. In fact, it seems that the two dimensional temporal logic with since and until is strictly more expressive than with only until, the witness property being "there is a time moment i such that t1 = ti".

As far as the space dimension is concerned, our logic behaves like two-way CTL. Two-way CTL is first-order complete, see [START_REF] Schlingloff | Expressive completeness of temporal logic of trees[END_REF]. We could even allow more powerful operations in the logic. This is because our evaluation algorithm represents the formula as an alternating automaton. Then, our algorithm works even if we make tests for any regular properties at fixed time moments.

EVALUATION

The subject of this paper is evaluation of logical formulas on document evolutions. We are not interested in the satisfiability problem, because it is undecidable for all the logics described here, by using a document evolution to describe a run of a Turing machine. 1 The evaluation problem for a logical formula ϕ is stated as follows.

• Input. A document evolution t.

• Output. Does the formula hold in t?

When measuring the complexity of the problem, we use two parameters of the document evolution t: the document size n and the duration k.

First-order logic. In this paper, we are mainly interested in the logics that are temporal in at least one of the two dimensions of space and time. Why not first-order logic where the variables range over space/time pairs? A document evolution of document size n and duration n = k can encode any graph with n vertices, since it is essentially an n × k matrix. Therefore, evaluating first-order logic on document evolutions is the same as evaluating first-order logic on graphs, or arbitrary relational structures for that matter. The latter is a fascinating and widely studied topic, but it is not the topic of this paper.

An optimal algorithm for the two-dimensional temporal logic. There is a simple optimal algorithm for the twodimensional logic.

Theorem 1. The evaluation problem for two-dimensional temporal logic can be solved in time O(k • n).

Proof. Suppose that X is the domain of the document evolution. By induction on the size of a formula ϕ, we show that the set of pairs (x, i) ∈ X × {1, . . . , k} in a document evolution t1, . . . , t k that satisfies ϕ can be computed in time

O(|ϕ| • n • k).
Suppose that we want to compute the pairs where ϕUtψ is satisfied. For document node x ∈ X, we scan the document evolution from time k to time 1. Using the precomputed information on ϕ and ψ we can compute the bigger formula. A similar argument works for the other operators. For the space operators, one needs to do a bottom-up or top-down pass through the trees.

Observe that the algorithm above would also work if we allowed a since operator in the time dimension. The since operator will be a problem in our later algorithm.

If the document evolutions are arbitrary sequences of documents, with no restriction on small differences between consecutive documents, then this naive algorithm is optimal. All n • k positions of the document evolution must be read for some queries, e.g. the query "all nodes in all times have label a."

Incremental evaluation. The incremental evaluation problem is a variant of the evaluation problem, where we assume that the document evolution is the result of applying a sequence of local updates to an initially empty document.

Here empty means that all nodes have the same blank label. Formally speaking, the input of the incremental evaluation problem consists of: a tree domain X, a duration k ∈ N, an initial letter a ∈ A and a sequence of pairs

(a1, x1), . . . , (a k-1 , x k-1 ) ∈ A × X.
Given this input, we define a document evolution t1, . . . , t k as follows. The first document t1 has all nodes labeled by a.

Once ti has been defined, ti+1 is defined as ti with position xi changing label to ai. A document evolution obtained from such a sequence of relabeling operations is called an incremental document evolution.

In the (general) evaluation problem, reading the input requires time n • k. In the incremental evaluation problem, reading the input requires time k, so the simple lower bound of O(n • k) does not hold any more. The principal contribution of this paper is that the incremental evaluation problem can be solved more efficiently, as stated in the following theorem.

Theorem 2 (Main Theorem). Fix a formula ϕ of the two-dimensional temporal logic. The incremental evaluation problem, on a document evolution of document size n and duration k can be solved in time

O(k • log(n)).
In the theorem above, the constant in the O notation depends on the formula ϕ. As a function of ϕ, the constant grows faster than any tower of exponentials. That is why this paper is intended more as a proof of concept, the concept being that the incremental evaluation problem can be done in time smaller than the obvious O(n • k).

AN AUTOMATON MODEL

In this section we define an automaton model that accepts or rejects document evolutions. This automaton can capture the two-dimensional temporal logic, and even some extensions. Our evaluation algorithm works with the automaton.

Regular queries.

A regular tree language is like a boolean query for trees: it says yes or no to each tree. In this paper we also use unary queries, binary queries and so on. An mary query over trees, with input alphabet A, is a function f which maps every tree over alphabet A to a set of m-tuples of nodes in the tree. An example of a binary query is one that maps a tree to the set of all pairs of nodes (x, y) such that there is an even number of a's on the shortest path from x to y.

We will be using regular queries, which are queries that can be defined by formulas of MSO logic with free individual variables, see e.g. [START_REF] Libkin | Logics for unranked trees: An overview[END_REF]. Regular queries can also be described in other ways, different than MSO formulas, e.g. by automata or monoids. The way we describe regular queries is not very important for our evaluation algorithm (actually, the algorithm uses monoids as its internal representation). In particular, the bad query complexity of our algorithm is not due to the use of MSO in the automaton, the algorithm would have nonelementary complexity even with regular queries represented in some less succint way, e.g. by monoids.

Document update processing automata. We now introduce the automaton model, which we call a document update processing automaton. Such an automaton, call it A, is given by the following ingredients.

• An input alphabet A.

• A set of states Q, an initial state q0 and a set of accepting states F ⊆ Q. The states are partitioned into Q ∃ and Q ∀ . (This is a kind of alternating automaton.)

• A finite set ∆ of transitions of the form (q, ϕ, p) where q, p ∈ Q and ϕ is a binary regular query over input alphabet A.

An input for the automaton is a document evolution t = t1, . . . , t k with domain X, where the trees are over alphabet A. The automaton accepts the document evolution if player ∃ wins the following perfect-information, finite duration, two-player game, call it G A t . Positions of the game are triples of the form (q, x, i) where q ∈ Q is a state of the automaton, x ∈ X is a node, and i ∈ {0, . . . , k} is a moment in time. The interpretation of i is that we are about to read the tree ti+1. The initial position is (q0, root, 0), i.e. the game starts in the initial state, in the root, and before reading the first tree in the document evolution. When in a game position (q, x, i) with i < k, the player who owns state q chooses a new game position (p, y, i + 1) such that (q, ϕ, p) is a transition of the automaton and ϕ selects the pair (x, y) in the document ti+1. When a game position of the form (q, x, k) is reached, the game is finished, and player ∃ wins if q is accepting, otherwise ∀ wins. A position in the game is called winning for ∃ if he can win the game starting in that position.

From two-dimensional logic to dupa automata Proposition 3. For every formula ϕ of the two-dimensional temporal logic there is a document update processing automaton that accepts the same document evolutions.

Proof. States of the automaton are subformulas, so the size of the automaton is quadratic in the formula. The translation is as usual when going from temporal logic to an alternating automaton.

Ordered automata. We say a transition (p, ϕ, q) in a document update processing automaton is a local transition if the formula ϕ only selects pairs of the form (x, x) in every tree (in wich case, ϕ is essentially a unary query). An automaton is called ordered if there is a ranking function Ω : Q → N on its states such that performing any transition preserves or decreases the rank, and performing a non-local transition decreases the rank. It is possible that several states have the same rank, in which case the states can be connected only by local transitions. Observe that the automaton produced in Proposition 3 is an ordered automaton, the ranking function refers to the size of the subformula corresponding to the current state.

The principal technical result of this paper is that ordered document update processing automata can be evaluated efficiently.

Theorem 4. Fix an ordered document update processing automaton. Whether or not the automaton accepts a document evolution of duration k and tree length n can be tested in time O(k • log(n)).

Thanks to Proposition 3, the theorem above also yields an evaluation algorithm for the two-dimensional temporal logic, of same complexity, as stated in Theorem 2.

The evaluation algorithm is described in Sections 5 and 6. Due to the complicated structure of the algorithm, we describe it for the case of words (which can be seen as the special case of trees with only one path). In Section 7 we comment on how to extend the algorithm for trees.

LOCAL ORDERED AUTOMATA

In this section we show how to evaluate a local automaton, which is a document update processing automaton where only local transitions are allowed. In the next section, the ideas on local automata are extended to the general case of ordered automata with non-local transitions.

As mentioned before, we describe the algorithm for words and not trees. In particular, the tree domain is now given by just specifying the word length n, in which case the domain is {1, . . . , n}. We will prove the following theorem in this section.

Proposition 5. Fix a local automaton. The automaton can be evaluated on incremental document evolutions of word length n and duration

k in time O(k • log(n)).
Actually, we prove a slightly stronger result. We will create a data structure such that for every node x ∈ {1, . . . , n}, one can tell in time O(log(n)) if the automaton accepts the word if it begins in the initial state in node x. So, in a sense, we evaluate the local automaton for all nodes in the word simultaneously.

We fix for the rest of this section a local automaton. We also fix an input to the automaton, i.e. an incremental document evolution w1, . . . , w k ∈ A n .

Our goal is to determine if the automaton accepts this word. In the algorithm, we will refer to the differences between successive words wi and wi+1, so we assume that the incremental document evolution is given by a sequence of relabeling operations.

Monoids for queries. In this section, we assume that all of the transitions are local, i.e. every transition is of the form (p, ϕ, q) where ϕ only selects tuples of the form (x, x) in every word. Therefore, we will simply treat ϕ as a unary query. Instead of MSO logic, we use monoids to describe regular queries. We describe the monoid approach to unary queries below.

Suppose that

α : A * → M is a monoid homomorphism. The unary α-type of a node x in a word a1 • • • an is the triple (α(a1 • • • ax-1), ax, α(ax+1 • • • an)) ∈ M × A × M.
We say the homomorphism α recognizes a unary query ϕ(x) if there is a set of triples

H ⊆ M × A × M
such that a node x is selected by the query ϕ in a word w if and only if the unary α-type of x in w belongs to H. For every unary MSO query there exists a monoid homomorphism that recognizes it. The monoid M might be nonelementary in the size of the query. (This translation of MSO into monoids is not the only reason for bad query complexity, our algorithm has nonelementary query complexity even when the monoids M are small.)

We fix a single monoid homomorphism α : A * → M that recognizes all the queries that appear in the transitions of the automaton. This can be done by using the direct product of all the monoids for all the queries. When referring to unary types, we omit the name of α, because it is the only homomorphism we use.

Zones. We begin by introducing some notation. We write x, y, z for positions in the words, i.e. for elements of {1, . . . , n}. A zone is defined to be any connected set of positions, i.e. a zone is a set {x, x + 1, . . . , y} for 1 ≤ x ≤ y ≤ n. We write X, Y for zones, and we also allow an empty zone. If X is a zone and w is a word with n positions, then w|X is the word obtained from w by only keeping positions from X. The type of a zone X in a word w is defined to be α(w|X). Zones X1, . . . , Xm are called consecutive if the last node in zone X1 is the predecessor of the first node in X2, and so on until Xm-1 and Xm.

The environment of a zone X inside a zone Y ⊇ X is the difference Y -X. Such an environment is the union of two disjoint zones, the one to the left of X and the one to the right of X. The type of such an environment is the pair of types of these two disjoint zones. We write

Externals def = M 2
for the set of possible types of such environments. The external type of a zone X is the type of its environment with respect to the set {1, . . . , n} of all word positions. We write τ, σ for external types. For i = 1, 2, we write τ (i) for the i-th coordinate of an external type τ . We can also insert one external type inside another inσ(τ

) def = (τ (1) • σ(1), σ(2) • τ (2)) ∈ Externals.
The idea is that if X ⊆ Y ⊆ Z and σ is the type of the environment Y -X, and τ is the type of the environment Z -Y , then inσ(τ ) is the type of the environment Z -X.

Histories. We write i, j for times, which are elements of {1, . . . , k}. A time interval is defined like a zone, but for times. For a time i ∈ {1, . . . , k} we write ext(X, i) ∈ Externals for the external type of a zone X in the word wi. Consider a zone X and a time interval I = {i, . . . , j}. We define the external history of the interval X in time interval I, denoted history(X, I), to be the sequence ext(X, i), . . . , ext(X, j) of external types of X in the times from the interval I. Since we only talk about external histories, we simply write history from now on. We only use the value history(X, I) when the zone X does not change labels in the time interval I. To underline this requirement, we assume that history(X, I) is undefined otherwise. We write Histories for the set of possible histories, this set includes the undefined history ⊥.

The history toolkit

We define some operations on histories. These operations will be used by the algorithm as a black box.

Monoid operations on histories.

There is an empty history:

empty ∈ Histories (2)
The simplest operation we can do on histories is concatenate them. When histories are represented as sequences of external types, this operation is simply sequence concatenation. Later, we represent histories in a more concise way, and the operation becomes less trivial, so we give it a name: concat : Histories × Histories → Histories.

(

) 3
Applying a history to a node. For a node x and a time i, we define Pxi ⊆ Q to be the set of states q such that the game position (q, x, i) is winning in the game G A w . Recall that (q, x, i) describes the situation between words wi and wi+1. The principal goal of our algorithm is to design an algorithm and data structure, so that after the algorithm terminates, each set Px0 can be computed in time O(log(n)) by using the data structure.

Generally speaking, our algorithm will be processing the words in the time evolution in reverse order, beginning with w k and ending with w1. All the information gathered by the algorithm will be propagated from later times to earlier times. We say that a node x does not change label in time i if the label of x is the same in words wi and wi+1. Lemma 6. Suppose that in the time interval {i, . . . , j}, the label of a position x is constantly a ∈ A. Then the set P x(i-1) is uniquely determined by: the label a, the set Pxj and history({x}, {i, . . . , j}).

Proof. Consider first a history of length one, i.e. j = i. Let history({x}, {i}) be (σ, τ ). Then the α-type of x in wi is (σ, a, τ ). The set P x(i-1) contains the states q such that either • q is owned by player ∀ and for every transition (q, ϕ, p), if (σ, a, τ ) satisfies ϕ then p ∈ Pxi, or

• q is owned by player ∃ and there is a transition (q, ϕ, p) such that (σ, a, τ ) satisfies ϕ, and p ∈ Pxi.

These conditions are necessary and sufficient for (q, x, i -1) being an accepting position in the automaton's game.

For longer histories, the lemma is obtained by iterating the statement for histories of length one.

We denote the function that realizes the dependency from the above lemma by apply :

Histories → A × P (Q) → P (Q). (4)
That is, this function is defined so that, under the assumptions of the lemma, we have

P x(i-1) = apply(history({x}, {i, . . . , j}))(a, Pxj).
Inheriting the history of a parent. Let Y be a zone that contains X. Suppose that in the time interval I, the input labels of Y -X did not change, and therefore constantly had the same type σ ∈ Externals. In this case, history(X, I) = inσ(history(Y, I))

where the operation inσ : Histories → Histories

is defined by inσ(τ1, . . . , τm) = inσ(τ1), . . . , inσ(τm).

The algorithm

We now present our algorithm. It uses a fairly natural divide-and-conquer approach (not for nothing there is log(n)). The crux is an efficient implementation of operations on histories, which is described in later sections.

We define logarithmic zones as follows: the set of all positions of {1, . . . , n} is a logarithmic zone; and if X is a logarithmic zone of w and x ∈ X is in the middle of X then X ∩{1, . . . , x} and X \{1, . . . , x} are both logarithmic zones. The properties of these zones are: they are either disjoint or one is included in the other, each position is included in a logarithmic number of them, and there are linearly many of them. We write parent(X) for the smallest logarithmic zone Y X and Logs for the set of all logarithmic zones.

The history tree. We first define the data structure used by Because the logarithmic zones have a tree structure, and because the component D.history is the most important one, we use the name history tree for such an instance D.

We will first compute a history tree for time k, and then will compute it for times k -1, k -2, . . . , 0. A history tree D is called correct at time moment i ∈ {0, . . . , k} if the following conditions hold. (The idea is that D describes the situation between words wi and wi+1.)

1. For every logarithmic zone X and its parent Y ,

D.lastupdate(X) ≥ D.lastupdate(Y ).

In other words, zones intervals are more up to date than smaller zones. (Because the algorithm starts in k and progresses towards 0, information about a smaller time is more up to date.) We say a zone X is up to date (at moment i) if

D.lastupdate(X) = i.
We require that the root logarithmic zone {1, . . . , n} is up to date.

2. Labels cannot change between the current time i and the last update. That is, for every logarithmic zone, all of its input labels have stayed the same in the time interval {i, . . . , D.lastupdate(X)} 3. For every logarithmic interval X, the value D.monoid (X) stores the monoid element corresponding to X at the time of its last update:

D.monoid (X) = α(w D.lastupdate(X) |X)
In fact we have that D.monoid (X) = α(wj|X) for every i ≤ j ≤ D.lastupdate(X) since wj|X remains unchanged.

4. Suppose that X is a logarithmic interval, and Y is its parent. Then D.history(X) stores the value history(X, {D.lastupdate(Y ), . . . , D.lastupdate(X) -1}).

In the case when D.lastupdate(Y ) = D.lastupdate(X) the above history is empty.

5. Suppose that x is a node and let j = D.lastupdate({x}) and (a, P ) = D.lastlabel (x).

Then the label of x in word wj is a and Pxj = P . Together with condition 2 this means that the input label of x is a during the interval {i, . . . , j}.

The algorithm. The algorithm begins with a history tree D k that is correct and up to date for time moment i = k. Then for each time moment i ∈ {k -1, . . . , 0}, the algorithm calculates a history tree Di that is correct for time moment i.

The algorithm that maintains this invariant will manipulate histories. In our complexity analysis, we will use the history operations empty concat apply inσ described in Section 5.1 as black boxes, with unit cost in the algorithm. Later, we will show how the operations can be implemented in constant time.

Lemma 7. D k can be computed in time O(n).
It is safe to assume k > n, because otherwise our algorithm can ignore the positions where no labels are updated. Therefore, the O(n) precomputation cost of D k will be amortized by the algorithm's O(k • log(n)) complexity.

Lemma 8. Let Di be a history tree that is correct for time i. Let x be a position. We can compute a history tree D i that is also correct for time i and which is up to date at the zone {x}. This computation can be done in time O(log(n)), assuming the history operations have unit cost.

Proof. Consider the logarithmic zones that contain x:

{x} = X0 X1 • • • Xm.
We will compute history trees D (m) , D (m-1) , . . . , D (0) = D which are all correct for time i, and such that D (r) .lastupdate(Xr) = i for r ∈ {0, . . . , m}.

Furthermore, a constant number of operations on the history tree D (r) are sufficient to compute D (r-1) . The statement of the lemma then follows, because m is logarithmic in n.

For the induction base, we simply use D (m) = Di, because item 1 of the correctness conditions says that the root logarithmic zone is always up to date.

The rest of the proof is devoted to the induction step. Suppose we computed D (r+1) and we want to compute D (r) . We simply make the zone Xr up to date in D (r) by setting D (r) .lastupdate(Xr) := i and keeping the value of lastupdate unchanged for other logarithmic zones. What else do we need to change in D (r) to make this history tree correct for time i? We examine the conditions of correctness item by item.

1. Item 1 holds because the zones Xr+1, . . . , Xm are already up to date in D (r+1) , and the root zone is unchanged.

2. We have decreased the value of D (r) .lastupdate(Xr), which makes item 2 even more true.

3. Let use j for the previously used time in Xr, i.e. j = D (r+1) .lastupdate(Xr).

We know from item 2 applied to D (r+1) that no positions have been changed in the zone Xr between the current time i and time j, so we can keep D (r) .monoid (Xr) := D (r+1) .monoid (Xr).

4. For this item, we change the histories in at most three zones. For the history of Xr, we use the empty history, because Xr is now up to date: r) .history(Xr) := empty.

D (
Suppose that r > 0. In this case, Xr has two children zones, call them Y0 and Y1 from left to right. (One of the children is Xr-1, but this plays no role in our argument.) The condition in item 4 could now be invalid for the two zones Y0, Y1, because we have changed the update time of their parent Xr. For l ∈ {0, 1} let j l be D (r) .lastupdate(Y l ) = D (r+1) .lastupdate(Y l ).

To make the history tree D (r) correct, we should have D (r) .history(Y l ) = history(Y l , {i, . . . , j l -1}), so we need to compute the history on the right of the above equation. What we have from the history tree D (r+1) is two histories: history(Y l , {j, . . . , j l -1}) history(Xr, {i, . . . , j -1}).

However, we know that from time i to j the external type of Y l inside Xr was the same, call this external type τ l . The value of this external type is taken from the monoid part of the history tree: τ0 = (1, D (r) .monoid (Y1)) τ1 = (D (r) .monoid (Y0), 1).

By applying the inτ l operation, we can compute the history of Y l between times j and i as follows:

history(Y l , {i, . . . , j -1}) = inτ l (history(Xr, {i, . . . , j -1})).

Then, the value of D (r) .history(Y l ) should be set to concat(D (r+1) .history(Y l ), inτ l (D (r+1) .history(Xr))).

5. Let y be any position. If we have the equality r+1) .lastupdate({y}), then no change in D (r) .lastlabel (y) is required preserve item 5, because of correctness of D (r+1) . The only case when the equality above can fail is when y = x and r = 0. We study this case below.

D (r) .lastupdate({y}) = D (
Let j = D (1) .lastupdate({x}). By correctness of D (1) we know that D (1) .lastlabel (x) = (a, Pxj)

where a is the label of x in time j. To make item 5 true, we need to have D (0) .lastlabel (x) = (a, Pxi), which requires knowing the set of states Pxi. By the previous item, we have the history D (0) .history({x}) = history({x}, {i, . . . , j -1}).

Therefore, we can apply the history above to the pair (a, Pxj) and get the set Pxi from apply(D (0) .history({x}))(D (1) .lastlabel (x)).

A similar proof yields the following lemma.

Lemma 9. Let x be the position where wi+1 differs from wi. Let D i+1 be a history tree that is correct for time i + 1 and up to date at x. We can compute a data structure Di that is correct for time wi. This computation can be done in time O(log(n)), assuming the history operations have unit cost.

By applying the two lemmas in alternation, we can compute successively data structures

D k , D k , D k-1 , D k-1 , . . . , D 1 , D0.
This takes O(k • log(n)) time, and O(k • log(n)) history operations. If we implement histories in a naive way, by writing down a history as a list of pairs, each of the operations will take time linear in the length of the list. This will be a problem for the algorithm, which would run in time

O(k • n • log(n)).
The essence of the algorithm is to implement histories so that the operations can be done in constant time. This will be done in Section 5.3.

A constant time implementation of histories

History congruence. Recall the operations on histories that were used as black box operations in the algorithm from the previous section.

empty ∈ Histories concat : Histories × Histories → Histories. apply : Histories → A × P (Q) → P (Q).

inσ : Histories → Histories

A history congruence is an equivalence relation ∼ on Histories that is a congruence with respect to all the above operations. Formally speaking, a history congruence must satisfy the following conditions whenever h ∼ h concat(g, h) ∼ concat(g, h ) for all g ∈ Histories concat(h, g) ∼ concat(h , g) for all g ∈ Histories

apply(h) = apply(h ) inσ(h) ∼ inσ(h ) for all σ ∈ Externals
If ∼ is a history congruence, then the history operations can be applied to equivalence classes of ∼. The family of equivalence classes together with the history operations on equivalence classes is denoted by Histories/∼.

Lemma 10. Suppose that ∼ is a history congruence. Then Histories can be replaced by Histories/∼ in the algorithm, and the computed values for Di.lastlabel ({x}) will be the same.

Proof. The algorithm accesses the histories only using the operations.

The constant time implementation of histories is based on the following lemma.

Lemma 11. There is a history congruence where the number of equivalence classes is finite and depends only on the automaton, and not its input (not on n or k).

The idea of the proof is that two histories are considered equivalent if they induce the same mapping:

τ ∈ Externals → apply(inτ (h)) : A × P (Q) → P (Q).

NON-LOCAL ORDERED AUTOMATA

In this section we generalize the algorithm from the previous section to deal with non-local transitions in an ordered automaton.

The difficulty in this section is a new notion of history. A history is still used to store information about environments of zones, but this information is now more complex.

Preliminaries

Fix an ordered document update processing automaton. Assume that the maximum rank given by the function Ω of the automaton is t. We define the sets of states

Q 1 ⊆ Q 2 ⊆ • • • ⊆ Q t where Q i def = {q ∈ Q | Ω(q) ≤ i}.
Binary types. The automaton now includes non-local transitions, which are of the form (q, ϕ, q ) where ϕ is a binary regular query that may select nodes (x, y) of the word with x = y. As in the previous section, we use monoids to recognize queries. For unary queries, we use the notion of type of a node x as in the previous section. We write Unarytypes α to denote the set of unary α-types, we omit the index α when the homomorphism α is clear from the context. We extend the notion of type to pairs of nodes. Suppose

α : A * → M
is a monoid homomorphism. We define the binary α-type of two nodes x and y in a word w as the element of

Binarytypes α def = M × A × M × A × M × {<, >, =}
containing the three types of the three infixes of the word {1, . . . , i -1}, {i + 1, . . . , j -1}, {j + 1, . . . , n}, where i = min(x, y), j = max(x, y), and the labels of positions i and j. The last component says whether x = y, x < y or x > y.

We write type α (x, y, w) ∈ Binarytypes α to denote the binary type of x and y on w. For every regular binary query ϕ there is a homomorphism α and a set F ⊆ Binarytypes α that recognizes ϕ, that is, that (x, y) is selected on w by ϕ if and only if type α (x, y, w) ∈ F . We fix a homomorphism α that recognizes all the binary queries in the transitions of the automaton. We omit the index α from the notation.

Node profiles. As in Section 5, the goal of the algorithm is to compute the sets Pxi for positions x and times i.

Suppose that a node x does not change its label between in times I = {i, . . . , j}. Due to non-local transitions, it is not enough to know the sequence of external types of x in order to update it from Pxj to P x(i-1) . There may be a state q in P x(i-1) that is triggered by some q ∈ Pyi via a non-local transition from some other node y. Due to these issues, we store more information in our data structures. We describe this information below, starting with the simplest brick: profiles of nodes.

Consider a node x ∈ {1, . . . , n}, a time i ∈ {1, . . . , k} and a rank l ∈ {1, . . . , t}. By induction on the rank l, we define the rank l profile of node x in time i to be the following information, which is denoted by π l,i

x :

• The type of node x in the word wi;

• the set of states in Pxi ∩ Q l ;

• for every binary type τ ∈ Binarytypes, the set of rank l -1 profiles of nodes y in time i such that the binary type of x and y in wi is τ .

When the rank l is not specified, it assumed to be the maximal rank l = t. Observe that the information in π i x also describes other nodes than x, due to the third item of the definition. Since the definition is recursive, a rank l profile can be seen a tree of depth t where edges correspond to Binarytypes elements, and nodes with a subtree of depth l are described by the accepting states from Q l . The data type where rank l profiles live is denoted by Nodeprofiles l , and it is described below:

Nodeprofiles def = Nodeprofiles t Nodeprofiles 1 def = Unarytypes × P (Q 1 ) Nodeprofiles l+1 def = Unarytypes × P (Q l+1 ) × Neighbours l Neighbours l def = Binarytypes → P (Nodeprofiles l )
Note that from π l,i

x we can deduce π l ,i

x for all l < l, because Q l ⊆ Q l . The size of the data type Nodeprofiles l+1 is exponential in the size of Nodeprofiles l , hence the nonelementary query complexity of our algorithm.

Zone profiles. We define the profile of a node x relative to a zone X

x by taking wi|X as the whole word. All the elements from Unarytypes and Binarytypes are relative, and the neighbours are limited to the zone X. This profile is denoted by π i x∈X . The profile of a zone X in time moment i is just the set of node profiles (relative to X) of nodes in X. We use the symbol Π to denote zone profiles. Following the same notation introduced before, Π l,i X is the zone profile of the zone X at time moment i containing the information of the states from

Q l . Π l,i X def = {π l,i x∈X : x ∈ X} ∈ Zoneprofiles l def = P (Nodeprofiles l ) Π i X def = Π t,i X ∈ Zoneprofiles def = Zoneprofiles t
The following lemma shows that zone profiles are compositional with respect to union of consecutive zones.

Lemma 12. There is an associative concatenation operation on profiles (Π1, Π2) → Π1 • Π2 such that for two consecutive zones X1 and X2, we have

ΠX 1 ∪X 2 = ΠX 1 • ΠX 2 .

One step computation.

Lemma 13. Suppose that the nodes of the word are partitioned into three consecutive zones X1, X, X2. Suppose also that in time i -1 the labels of zone X do not change. For every node x ∈ X, the node profile π i-1 x∈X depends only on:

Π i X 1 Π i X 2 and π i x∈X
Actually, the dependency is even a bit more fine grained. If we want to know the rank l profile π l,i-1 x∈X , we only need the profile of the same rank in the current node, but profiles of smaller rank in the surrounding zones:

Π l-1,i X 1 Π l-1,i X 2 and π l,i x∈X .
The idea is that any dependency on nodes that are different from x requires using a non-local transition, which decreases the rank. However, since we do not need the more fine grained dependency, we use the dependency as stated in Lemma 13, which does not indicate ranks.

Observe that we do not need the profiles π i x ∈X of other elements x ∈ X since all the information relevant to X is inside π i x∈X . Let us fix the term Externalzoneprofiles to name zone profiles of the environment of zones.

Externalzoneprofiles def = Externalzoneprofiles t Externalzoneprofiles l def = Zoneprofiles l × Zoneprofiles l
We define the ext function to work with Externalzoneprofiles.

ext(X, i) def = (Π i X 1 , Π i X 2 )
∈ Externalzoneprofiles for (X1, X2) the environment of X in wi. By Lemma 13, there exists a function update : Externalzoneprofiles → Nodeprofiles → Nodeprofiles such that the following holds.

π i-1 x∈X = update(ext(X, i), π i x∈X )
This function can be extended to zones update : Externalzoneprofiles → Zoneprofiles → Zoneprofiles by lifting the previous definition to sets of profiles, and we then have

Π i-1 X = update(ext(X, i), Π i X ) .

Histories

We now generalize the notion of histories, as they were defined in Section 5, to the non-local case. Let i ≤ j be times and let X be a zone, with (X1, X2) its environment. Suppose that the labels of X do not change in times i, . . . , j (and therefore they are the same as in the word wj+1). We define the history of X between i and j, denoted by history(X, {i, . . . , j}), to be the following sequence: ext(X, i), ext(X, i + 1), . . . , ext(X, j) ∈ Externalzoneprofiles.

We write Histories for the set of possible histories. We next define the apply and in functions on Histories.

Lemma 14. Suppose that in time interval {i, . . . , j}, the labels of a zone X do not change. Then the zone profile Π i-1 X is uniquely determined by Π j X and history(X, {i, . . . , j}). Proof. By iterating the function update : Externalzoneprofiles → Zoneprofiles → Zoneprofiles.

for each item on the list in the history.

Let the dependency in the above lemma be realized by the function:

apply : Histories → Zoneprofiles → Zoneprofiles That is, under the assumptions of the lemma we have

Π i-1 X =
apply (history(X, {i, . . . , j})) (Π j X ). In the algorithm for local transitions from Section 5, one important part has to do with the possibility to compute, given the history h of a zone X in an interval {i, . . . , j} (and assuming that there were no changes on X between times i and j), the history h of a smaller zone X0 ⊆ X having as environment inside X the subzones X1 and X2. In the previous section, this was obtained simply with inσ(h) where σ ∈ Externals corresponds to the types of (X1, X2). But here the operation is somewhat more complicated, since to obtain the history h we need at the same time to update the zone profiles of X1 and X2 to the time j -1 (remember that a history element is from Externalzoneprofiles), then to time j -2 until we update it to time i. Thus, in some sense the apply() and inσ() functions of the previous section are done simultaneously for the non-local automata. Another issue to solve is that in order to update the zone profile of, say X1, we need the updated profiles of X0, X2. But these need at the same time the updated profile of X1. However, this will not be a problem because of the ordered condition we impose to the automaton.

Lemma 15. Let Y be a zone partitioned into three consecutive zones X1, X, X2. Suppose that in time interval {i, . . . , j} the labels of zone Y do not change. Then history(X, {i, . . . , j}) is uniquely determined by history(Y, {i, . . . , j})

Π j X 1 Π j X 2 Π j X .
Let the operation that realizes the dependency of the above lemma be denoted by in : Histories → Externalzoneprofiles → Zoneprofiles → Histories.

That is, under the assumptions of the lemma we have history(X, {i, . . . , j}) = in (history(Y, {i, . . . , j})) (Π j X 1 ) (Π j X 2 ) (Π j X ).

The algorithm

The high level structure of the algorithm is the same as in Section 5. We keep a tree of histories and update one branch with each iteration, performing O(log(n)) operations. The main difference is that we also retain the profiles of each of the logarithmic zones, which become necessary to transfer a history of a zone to a history of a smaller zone.

The history tree. We also maintain a structure as the one showed previously. An instance D of the data structure consists of the following labeling. D.lastupdate : Logs → {0, . . . , k} D.lastprofile : Logs → Zoneprofiles D.history : Logs → Histories Note that instead of using D.lastlabel and D.monoid we have a D.lastprofile which contains the profile of the logarithmic zone. In particular it contains the label and external value for each node.

As before, we first compute a history tree for time k, then for times k -1 and so on, down to 0. We call a history tree correct at time moment i ∈ {0, . . . , k} if conditions 1, 2, and 4 of the previous definition of correctness hold (with the new notions of history) and 6. D.lastprofile(X) is the updated zone profile of X, i.e., after applying D.history(X) to it. Suppose that X ∈ Logs and let j = D.lastupdate(parent(X)) and

Π = D.lastprofile(X) ,
then Π is equal to the zone profile Π j X of X in the time moment j. If X is the root, then it is the zone profile at time moment i: D.lastprofile(X) = Π i X .

Like with the algorithm of previous section we begin with a history tree D0 that is correct for time moment i = k and then for each time moment i = k-1, . . . , 0 the algorithm calculates the history tree Di that is correct for time moment i. The algorithm manipulates histories and zone profiles. Here we use as black boxes the following operations on histories that have unit cost in the algorithm. empty concat apply in emtpy and concat have the exact same definition as in the previous section: the empty history and the concatenation of histories. apply and in follow the definitions seen in Section 6.2.

One states analogues of Lemmas 8 and 9 for the new setup, with the exact same statements, only with the new notion of history tree. Then, one proves that the history operations can be implemented in constant time, also using a history congruence.

IMPROVEMENTS

Offline vs online

There are two ways of looking at the incremental evaluation problem, when the input is a document evolution w1, . . . , w k .

In the offline view, the algorithm begins its work once all of the document evolution is known.

In the online view, the words of the document evolution come one at a time, and the algorithm should do logarithmic processing for each word, without knowing the words that are going to come in the future.

Is our algorithm offline or online?

The answer depends on the order in which the words come, or equivalently stated, the direction of time in the temporal logic. As we had defined the temporal logic, time flows to the right, with the first time moment being 1 and the last time moment being k. As the reader will recall, our algorithm begins by analyzing time k, then k -1 and so on down to 1. An inspection of the algorithm reveals that operations of the algorithm when doing step i do not depend on the part of the document evolution w1, . . . , wi-1. Therefore, our algorithm actually is an online algorithm, assuming that the flow of time in the logic or automaton works in the opposite direction as the development of the document evolution.

Summing up, our algorithm is online (i.e. it does a logarithmic computation per each new word of the document evolution, and the computation does not depend of the words that are about to come in the future) if the temporal logic uses past operators on the time dimension, and not future operators. Although future operators are more common in temporal logics (which is why we defined the logic with future operators), it seems that past operators might actually be a better idea for the application at hand.

Insertion and deletion

In our evaluation algorithm we dealt with only one kind of update operation: relabeling. In this section we show that the algorithm still works if we allow insertions and deletions.

In the presence of insertions and deletions, one has to take care to distinguish between a node and its distance from the beginning of the word. For instance, suppose that we start with a word a and then apply the operation "insert a node with label b before the first position". The resulting document evolution is a, ba. However, the first and only node in the word a corresponds to the second node in the word ba, and not the first one.

To solve the issue presented above, we redefine a word as a connected graph where every node has outdegree and indegree at most one, and the nodes are labeled by letters from the alphabet. This way, we can assume that every node has a unique identifier, and the identifier does not change even if the distance of the node from the beginning of the word changes as a result of an insertion or deletion. A document evolution is a sequence of such words, which share nodes with the same identifiers.

Using identifiers, we adapt the semantics of the temporal and first order logic to document evolutions that include insertions and deletions. In the first-order logic, the quantifiers range over pairs (identifier/time), and not (distance from beginning/time) pairs. In the temporal logic, a modality that stays in a node stays in an identifier. For instance, the formula ¬Xt says that the current node will be deleted in the next time moment. Another example is the formula Gt (¬Xt ) ⇒ a , which says that the label of the current node is a just before it gets deleted (if it gets deleted).

Thanks to the insertion and deletion operations, we may assume that an incremental document evolution begins in an empty word.

Theorem 16. Suppose that, apart from label changes, we also allow insertions and deletions as update operations. For any fixed formula ϕ of the temporal logic, the incremental evaluation problem can be solved in time O(k • log(k)), where k is the number of updates.

The same online/offline remarks as in the previous section apply to the algorithm above. That is, it works online if the words are given in reverse order, or the temporal logic uses past instead of future operators in the time dimension. (But not both changes simultaneously.)

Trees

In the previous sections, we have described the evaluation algorithm for ordered document update processing automata, assuming input document evolution was a sequence of words. What about the trees? Bounded depth trees. One solution is to reduce trees to words. For a tree t, we define its word representation word(t), which is like the text representation of an XML tree. If the labels of t are A, then the labels of word(t) are {open, close}× A. Every node of t corresponds to two nodes in w, one with an opening tag and one with a closing tag. If the depth of the tree is known in advance, and can be encoded in the states of the automaton, then this representation can be decoded by document update processing automata, as stated in the following lemma.

Lemma 17. Fix d ∈ N. For any document update processing automaton on trees A, one can compute a document update processing automaton on words A d such that A accepts a document evolution (consisting of trees) t = t1, . . . , t k if and only if A d accepts the document evolution word( t) = word(t1), . . . , word(t k ), provided all the trees in t have depth at most d.

From the lemma above, it follows that all results on evaluation can be transferred from the bounded depth words to bounded depth trees.

Unbounded depth trees. We believe that, after some modifications, our algorithm can actually work directly on trees, without the need for the reduction t → word(t). That is, we believe that Theorem 16 holds for trees, without any restriction on the depth. The idea is to use forest algebra [START_REF] Bojańczyk | Forest algebras[END_REF], instead of monoids. Observe that this would improve the algorithm of Balmin, Papakonstantinou and Vianu [START_REF] Balmin | Incremental validation of XML documents[END_REF] in two ways: first, a more general problem is considered, and second the data complexity per update is improved from O(log 2 (n)) to O(log(n)). On the other hand, the query complexity of our algorithm is very bad.

CONCLUSIONS

We have designed an algorithm for evaluating a logic that inspects documents evolutions. The logic has operators that travel in the time dimension, and operators that travel in the space dimension. The algorithm works in time O(k • log(k))

where k is the length of the document evolution.

Below we list some topics for future work. We would like to investigate a logic with past and future operators on the time axis. We would also like to investigate a hybrid logic, where quantifiers are used for the space dimension and temporal operators are used for time dimension. Finally, we would like to improve the query complexity of the algorithm, possibly at the cost of using weaker logics.

where D .lastlabel (x) = (a , R). We also update D .monoid ({x}) to α(a) and D .lastupdate({x}) to i.

For any other Xj with j > 1 we proceed as follows. Suppose Y is the right sibling of Xj-1, i.e. such that parent(Xj-1) = parent(Y ) = Xj and Y is to the left of Xj-1. We then update D .monoid (Xj) to D .monoid (Xj-1) • D .monoid (Y ) and D .lastupdate(Xj) to i. Finally, we need to propagate this changes by using the history on Y . We then update D .history(Y ) to conc(D .history(Y ), τ ) with τ = in (D .monoid(X j-1 ),1) (σj), where σj is the already precomputed the external type of Xj in wi. A similar update occurrs if Y is a left sibling of Xj-1.

B.3 Proof of Lemma 11

To a history h we associate the mapping τ ∈ Externals → apply(inτ (h)) : A × P (Q) → P (Q) which we call its signature of h and denote by sig h .

Consider the equivalence relation on histories which considers two histories equivalent if they have the same signature. There are finitely many equivalence classes because there are finitely many signatures. We will prove that this equivalence is a history congruence. We need to show the following items.

• The signature of the concat(g, h) depends only of the signatures of g and h.

τ ∈ Externals → a ∈ A → fa,τ )

where fa,τ : P (Q) → P (Q) is the composition of the functions sig h (τ )(a) : P (Q) → P (Q) sigg(τ )(a) : P (Q) → P (Q).

• The value of apply(h) depends only on the signature of h. Indeed,

apply(h) = sig h (σ)
where σ is the empty external type (1, 1).

• For any external type σ, the value of inσ(h) depends only on the signature of h. Indeed, the signature of inσ(h) is the function τ ∈ Externals → sig h (inσ(τ )).

C. APPENDIX TO THE SECTION ON NON-LOCAL TRANSITIONS

Proof of Lemma 12.

Given two zone profiles ΠX 1 and ΠX 2 with X1 and X2 consecutive zones, we write ΠX 1 • ΠX 2 for the zone profile ΠX 1 ∪X 2 . This is an operation that depends solely on the information contained in ΠX 1 and ΠX 2 .

ΠX 1 • ΠX 2 def = out (1,τ 2 ) (ΠX 1 ) ∪ out (τ 1 ,1) (ΠX 2 )
where τ1 is the zone type of ΠX 1 , and τ2 that of ΠX 2 (these are the monoid's identity if the zones are empty), and out (τ 1 ,τ 2 ) (Π) is defined as follows by induction on l of the type Zoneprofiles l of Π. Assume Π ∈ Zoneprofiles, Π l ∈ Zoneprofiles l .

out (τ 1 ,τ 2 ) (Π) def = out (τ 1 ,τ 2 ) (Π t ) out (τ 1 ,τ 2 ) (Π 1 ) def = {((τ1 • σ1, σ2 • τ2), ρ) | ((σ1, σ2), ρ) ∈ Π 1 } out (τ 1 ,τ 2 ) (Π l+1 ) def = {((τ1 • σ1, σ2 • τ2), ρ, f ) | ((σ1, σ2), ρ, f ) ∈ Π l+1 , f = [(σ 1 , σ 2 ) → out (τ 1 ,τ 2 ) (f (τ1 • σ 1 , σ 2 • τ2))]}
Proof of Lemma 15.

We give a rough idea of how in can be defined, which realizes the dependency stated in the Lemma. Given a oneelement history h = (Π t,i+1 X 1 , Π t,i+1 X 2 ) and Π t,i Y 1 , Π t,i Y 0 , Π t,i Y 2 three consecutive zone profiles, we can calculate in(h)(Π t,i Y 1 , Π t,i Y 2 )(Π t,i Y 0 ) defined as

in(h)(Π t,i Y 1 , Π t,i Y 2 )(Π t,i Y 0 ) = (Π t,i+1 X 1 • Π t,i+1 Y 1 , Π t,i+1 Y 2 • Π t,i+1 X 2 ) with Π 0,i+1 Y 0 = Π 0,i Y 0 Π 0,i+1 Y 1 = Π 0,i Y 1 Π 0,i+1 Y 2 = Π 0,i Y 2 τ l-1 0 = (Π l-1,i+1 X 1 • Π l-1,i+1, Y 1 , Π l-1,i+1, Y 2 • Π l-1,i+1 X 2 ) Π l,i+1 Y 0 = update l (τ l-1 0 )(Π l,i Y 0 ) τ l-1 1 = (Π l-1,i+1 X 1 , Π l-1,i+1, Y 0 • Π l-1,i+1, Y 2 • Π l-1,i+1 X 2 ) Π l,i+1 Y 1 = update l (τ l-1 1 )(Π l,i Y 1 ) τ l-1 2 = (Π l-1,i+1 X 1 • Π l-1,i+1 Y 1 • Π l-1,i+1, Y 0 , Π l-1,i+1 X 2 ) Π l,i+1 Y 2 = update l (τ l-1 2 )(Π l,i
Y 2 ) for every l ∈ {1, . . . , t}. This definition can be extended to any number of history items by iterating the above definition.

C.1 The algorithm

As stated in Section 6.3, we show that the analogues of Lemmas 8 and 9 hold for the new notion of history tree.

Lemma 19. Let Di be a history tree that is correct for time i. Let x be a position. We can compute a history tree D i that is also crrect for time i and which is up to date at x. This computation can be done in time log(n), assuming the history operations have unit cost.

Proof. In our structure, in order to make a position x at time i up to date, we first find the biggest logarithmic zone X

x such that it is not up to date, i.e., such that Di.lastupdate(X) > i. Suppose Y and Y are the children logarithmic zones of X. By

  our algorithm. An instance D of the data structure consists of four labelings: D.lastupdate : Logs → {0, . . . , k} D.lastlabel : {1, . . . , n} → A × P (Q) D.history : Logs → Histories D.monoid : Logs → M

  in(D.history(X), (∅, D.lastprofile(Y )), D.lastprofile(Y )) we obtain the history hY and we define D.history(Y ) = conc(D.history(Y ), hY ) and by in(D.history(X), (D.lastprofile(Y ), ∅), D.lastprofile(Y )) we obtain the history h Y and we define D.history(Y ) = conc(D.history(Y ), h Y ).

In fact, it has been shown that the two-dimensional temporal logic is undecidable even if we only allow future modalities in both dimensions[START_REF] Gabelaia | Products of 'transitive' modal logics[END_REF].

APPENDIX A. IMPORTANCE OF THE ORDER

In this section we provide some evidence that the order, in ordered automata, is important. The evidence is the following implication: If we could evaluate document update processing automata in time O(k • log(n)) without the order assumption, then we would get an implausibly fast algorithm for evaluating cellular automata. Consider a onedimensional cellular automaton, with cell colors C, given by a function

We can extend this function in the natural way to configurations

Consider an input word w ∈ C * and a duration k ∈ N. Suppose that we want to compute the value of the first cell in the word f k (w). It seems unlikely that there is a better algorithm than computing all the cells on which this cell depends, which takes time O(k•n). The following lemma shows that evaluating cellular automata can be reduced to evaluating document update processing automata, and therefore it is unlikely that the O(k • log(n)) works without the assumption on order.

Lemma 18. Let f be a one-dimensional cellular automaton f with cell colors C and let c ∈ C. One can compute a document update processing automaton A f,c such that any word w ∈ C * , the automaton AC accepts the document evolution w = k-times w, . . . , w if and only if f k (w) has c on the first cell position. In the above, the word w is treated as a tree with a single path.

B. APPENDIX TO SECTION 5 B.1 Proof of Lemma 7

The history tree D k is built bottom-up. We first define D k for all the leaves, and we continue by levels up to the root.

We start with the singleton zones {x} for every node x of w k . We define D k .lastlabel ({x}) = (a, F ), where a is the label of node x in w k and F is the set of accepting states of the automaton. We define D k .monoid ({x}) = α(a), D k .lastupdate({x}) = k and D k .history({x}) = empty.

Once we have computed D k for all the tree nodes of depth at least l + 1 > 0, we compute the logarithmic zones of depth l by combining pairs of logarithmic zones of depth l + 1 in order, from left to right. For each such logarithmic zone X we define D k .lastupdate(X) = k, D k .history(X) = empty and D k .monoid (X) to be the product of the monoid elements of its children logarithmic zones.

B.2 Proof of Lemma 9

Suppose that the label of x in wi is a. Consider all the logarithmic zones that contain x,

We first precompute the following information. For every Xj we compute the external type σj of Xj in wi. This can be done in linear time in m.

We iterate from X1 up to Xm making updates to the history tree. We first start with X1 = {x}. We update D .lastlabel (x) to If X = {x}, we apply the history to the label of x, and define D.lastlabel (X) = apply(D.history(X))(D.lastlabel (X)) . Now X is up to date, and we set D.lastupdate(X) = i and D.history = empty. We iterate at most O(log(n)) times (i.e., the height of the logarithmic tree) to arrive to the desired state of our structure, where x is up to date.

Lemma 20. Let x be the position where wi+1 differs from wi. Let D i+1 be a history tree that is correct for time i and up to date at x. We can compute a data structure Di that is correct for time wi. This computation can be done in time log(n), assuming the history operations have unit cost.

Proof. Consider X1, . . . , Xm the logarithmic zones such that

• Xj and Xj+1 are consecutive zones for every j < m,

• there exists some Xr = {x}, • m is minimal. Then m ≤ log(n). Note that from D i+1 we have that D i+1 .lastprofile(Xj) = Π i+1 X j for every j ∈ {1, . . . , m}, this is granted by D i+1 being updated for all logarithmic zones containing x at time i+1. Given Π i+1 X 1 , . . . , Π i+1 Xm and Π i Xr we obtain Π i X 1 , . . . , Π i Xm using the update operation. This is done in O(m). To obtain Di we modify each D i+1 .lastprofile(Xj) to Π i X j and D i+1 .history(Xj) to conc(D i+1 .history(Xj), τ ), with

X j for all j in one pass, starting from j = 1 up to j = m, and then all Π i+1

Xm from j = m to j = 1 in another pass. Finally, we set

C.2 Constant time implementation of non-local histories

In a very similar way as for the section on local transitions, we give a congruence of finite index over Histories. We define a history congruence such that whenever h ∼ h concat(g, h) ∼ concat(g, h ) for all g ∈ Histories concat(h, g) ∼ concat(h , g) for all g ∈ Histories apply(h) = apply(h )

for all τ ∈ Externalzoneprofiles,

Π ∈ Zoneprofiles

Lemma 21. There is a history congruence where the number of equivalence classes is finite and depends only on the automaton, and not its input (not on n or k).

Proof. To a history h we associate the signature of h sig h : Zoneprofiles 2 → Zoneprofiles → Zoneprofiles

The idea is that a history signature sig h describes, for a given zone X, how to split the history into two smaller zones Y ⊆ X. In order to do this, we need the zone profiles of the environment of Y in X. Let Y1 and of Y2 be the left and right environment, such that Y1 ∪ Y ∪ Y2 = X, and let Π1, Π2 be the two respective zone profiles of Y1 and Y2. Then sig h (Π1, Π2) is defined as the result of applying the history that corresponds to Y on Π.

Consider the equivalence relation on histories which considers two histories equivalent if they have the same signature. There are finitely many equivalence classes because there are finitely many signatures. We will prove that this equivalence is a history congruence. We need to show the following items.

• The signature of the concat(g, h) depends only of the signatures of g and h.

where Π = sig h (Π1, Π2)(Π) ,

• The value of apply(h) depends only on the signature of h. Indeed,

• The value of in(h) depends only on the signature of h. Indeed, the signature of in(h)(Π1, Π2)(Π) is the function

D. APPENDIX TO SECTION 7

D.1 Proof of Theorem 16

The basic idea is to rebalance the history trees. Since the set of positions changes dynamically, our notion of logarithmic zone will change. A decomposition into zones, as in the logarithmic zones, will be called a zone tree. A zone tree for a word w is a family X of zones in w subject to the following conditions.

• Every two zones in X are disjoint or one is included in the other.

• The zone with all nodes of the word belongs to X .

• Every singleton zone belongs to X .

• Every non-singleton zone in X is a union of two zones in X .

There is a natural tree structure on a zone tree, which we use to talk about things like children zones or the height of a zone tree. The family of logarithmic zones is a special case of a zone tree, which has logarithmic height. We now show how to adapt the evaluation algorithm to take into account insertion and deletion operations. Suppose that we have an incremental document evolution w1, . . . , w k where the update operations are insertions, deletions and relabelings. Without loss of generality, we assume that w k is empty. Our algorithm will process the evolution from last word to first word. We will compute:

• Zone trees X1, . . . , X k for the words w1, . . . , w k of height at most O(log(k)). These zone trees are balanced in the sense of AVL trees: for every two siblings, the difference in depths of their subtrees is in {-1, 0, 1}. Because the last word w k is empty, the zone tree X k is empty, too.

• History trees D0, . . . , D k-1 , such that Di is correct in time i, with Xi+1 playing the role of the logarithmic intervals.

Maintaining the zone trees. We begin with describing the zone trees X1, . . . , X k . Suppose that we have the zone tree Xi+1 and we want to compute the zone tree Xi. If the words wi+1 and wi have the same positions, then we do not need to do anything. Suppose that wi has a position x, that does not appear in wi+1 (i.e. there is a deletion between wi and wi+1). The insertion case is done the same way. Let y be a position adjacent to x (to the left or right, does not matter). To all the zones in Xi+1 that contain y we add position x, and then we add two singletons {x} and {y}. Now we need to rebalance the tree.

As is known from AVL trees, rebalancing requires a logarithmic number of rotations. What is a rotation in the case of zone trees? We say a zone tree X is obtained from a zone tree X by a right rotation, if there are three consecutive zones X1, X2, X3 in the zone tree X such that

In particular, a right rotation removes one zone and adds another. A left rotation is the inverse operation.

The key property of the zone trees is as follows: the zone tree Xi is obtained from the zone tree Xi+1 by first removing O(log(k)) zones, and then adding O(log(k)) zones.

Maintaining the history trees. We now give a very rough sketch of how the history trees are maintained. Suppose that we have computed Di and we want to compute Di-1. The history tree Di+1 consists of mappings defined on the zones from Xi+1, and the history tree Di consists of mappings defined on the zones from Xi.

Consider the case when wi has a position x, that does not appear in wi+1. The case of an insertion from wi to wi+1 is done the same way, and the case of relabeling was already studied.

Using the non-local version of Lemma 8, we prepare Di so that all of the zones from Xi+1 -Xi are up to date. This requires time logarithmic in the depth of the history tree. We now need to define the zone profile of the zone {x} in Di-1. Since the node is new (i.e. it does not exist in wi+1) and because the zone has one element, this zone profile is easy to compute (actually, the zone profile a new singleton zone is always the same). We are still missing the zone profiles assigned to the zones of Xi -Xi+1. These can be built using the concatenation operation from Lemma 12.


Maria A Zuluaga

M Hernandez Hoyos

Eduardo Enrique

Davila Serrano

Luis F Uriza

Maciej Orkisz

Marcela Hernández Hoyos

Julio C Dávila

A fast lesion registration to assist coronary heart disease diagnosis in CTA images

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Ischaemic heart disease (IHD) is the main cause of mortality worldwide. Although invasive coronary angiography still remains the clinical gold standard in its diagnosis, computed tomography angiography (CTA) has dramatically progressed so that a reliable visualization of the coronary artery lumen and the identication of coronary plaques are now feasible. However, the diagnostic value of the cardiac CTA images depends on the image quality, which can be strongly aected by the coronary artery motion during the heart beat. Motion patterns dier between the left and right coronary systems and often also between proximal and distal portions of the same artery. The velocity of the arteries also varies along the cardiac cycle and among patients. Such heterogeneous movements and deformations of the coronary arteries lead to motion correction problems and motion artifacts in CTA images. Consequently, the clinicians use at least two cardiac phases (time points), typically one at the diastole and another one at the systole, in order to nd an optimal representation of each arterial segment and create a mental image of the whole coronary tree. Searching for every structure of interest in each evaluated phase is time consuming and prone to errors.

An alternative to reduce the navigation through the cardiac cycle might be an automatic registration of the arteries at dierent time points. However, this is a challenging task. The correspondence and alignment ambiguities are inherent to the task of automatically registering 3D images of tubular shapes [START_REF] Aylward | Registration and analysis of vascular images[END_REF].

The registration process is further complicated by the fact that vessels are typically surrounded by larger organs that swamp the similarity metric. In a rst attempt [START_REF] Laguitton | Temporal tracking of coronaries in MSCTA by means of 3D geometrical moments[END_REF], arterial landmarks have been followed through dierent time points of the cardiac cycle, using local vascular characteristics. The reported results are interesting, but the method has only been tested on simulated data and on a few points in two real sequences. More recently, a non-rigid registration strategy has been adapted to obtain a 4D deformation model of the coronary arteries on CTA images at dierent phases [START_REF] Metz | Patient specic 4D coronary models from ECG-gated CTA data for intra-operative dynamic alignment of CTA with X-ray images[END_REF]. A non-rigid image registration algorithm has also been used to segment and track the coronary arteries in 3D+t sequences [START_REF] Zhang | 4D motion modeling of the coronary arteries from CT images for robotic assisted minimally invasive surgery[END_REF].

Both approaches have been aimed at estimating the coronary motion in order to subsequently exploit it in surgery planning. Since such a procedure is carried out o-line, the computational time has not been a critical factor. In applications such as daily clinical diagnosis faster methods are required.

In this paper, we propose a 3D+t coronary artery registration strategy that minimizes the navigation and facilitates the evaluation of coronary lesions. Our approach mimics the procedure followed by physicians: after detecting a potential lesion in a particular time point of the cardiac cycle, the physician seeks the lesion in another time point to conrm the initial diagnosis. For this matter, only specic volumes of interest (VOI) in the arteries containing potential lesions are registered instead of the whole CTA volume. We demonstrate that our proposal can achieve good results without requiring information of the complete cardiac volume nor of the complete cardiac cycle.

The Method

The method rst automatically denes the extent of the sub-volumes to be aligned. The aim of this step is to construct a VOI that encompasses the lesioned vessel segment at two dierent time points to be registered. Then the registration is performed in two steps. A coarse rigid alignment rst reduces the displacement between the structures of interest (vessels with lesions) in both images. Subsequently, a deformable registration is applied to capture vessel deformations. Further details of each stage are provided in the subsequent sections.

VOI Denition

Let I M (x) denote the image at one time point, which will be locally deformed to t the image from another time point, denoted I F (x). The below-described procedure is repeated for each structure of interest (i.e. potential lesion) located in I F . The identication of the structures of interest is not the focus of this paper and can be performed either manually or by means of a lesion detection algorithm [START_REF] Zuluaga | Automatic detection of abnormal vascular cross-sections based on Density Level Detection and Support Vector Machines[END_REF][START_REF] Zuluaga | Learning from only positive and unlabeled data to detect lesions in vascular CT images[END_REF].

We dene a VOI I * F that is expected to be discriminant, i.e. contain enough information about the lesioned vessel, so that the latter can be unambiguously identied. The algorithm seeks for the volume that best matches I *

VOI Registration

Let us rst recall that image registration seeks to deform one image, denoted the moving image, to t another image, denoted the xed image, by applying a transformation T(x) to the moving image. The registration problem is formulated as an optimization problem that seeks to minimize a metric S with respect to the transformation T(x). Under this premise, our registration stage is a combination of two transformations T(x): a (coarse) rigid one and a deformable one.

The coarse rigid registration algorithm is applied to perform an initial alignment of I * F and I * M . Its result is used as an input to a subsequent stage where deformations of the lesioned vessels are captured. The deformable registration consists of a non-rigid transform using a free form deformation (FFD) model based on B-cubic splines [START_REF] Rueckert | Non-rigid registration using free-form deformations: application to breast MR images[END_REF]. The rigid registration is performed at a single resolution, whereas the deformable registration uses a coarse-to-ne multi-resolution strategy. For every resolution, at most 500 iterations are executed by an adaptive stochastic gradient descent optimizer [START_REF] Klein | elastix: a toolbox for intensity-based medical image registration[END_REF]. On every optimization iteration, 2048 samples are obtained from I * F using a random sampler [9] and a linear in- terpolator is used to evaluate the transformed I * M for both rigid and deformable registrations. A 3 rd order B-spline interpolator is employed to apply the nal deformation transform to I * M .

The above-described framework can be used with various similarity metrics S at both rigid and non-rigid registration stages. The choice was done by a careful empiric evaluation, which will be described in the next sections.

3 Experimental Setup

Experiments

We rst tested various values of the parameters D M and D F , respectively ranging from 1.0 to 2.5 cm and from 0. Once a metric selected, an experiment was performed to evaluate whether the direct registration of two time points (end-systole and end-diastole) degrades the quality of the results compared to an incremental registration strategy [START_REF] Metz | Patient specic 4D coronary models from ECG-gated CTA data for intra-operative dynamic alignment of CTA with X-ray images[END_REF][START_REF] Zhang | 4D motion modeling of the coronary arteries from CT images for robotic assisted minimally invasive surgery[END_REF],

in which a time point t is registered to time point t+1, the resulting transform is used to initialize the registration between phases t and t + 2 and so on. From the available data, two datasets containing all the cardiac time points were used for incremental registration. Afterwards, a direct registration was performed between time points 40% and 75% to compare with the results of the incremental registration.

Registration results assessment was done by evaluating the displacement be- F was then measured as an in- dicator of vessel displacement. Let C F be the vessel centerline from I * F and C M the deformed centerline from I * M , the average distance between centerlines [4] is dened as:

D(I * F , I * M , T) = 1 NF N F i=1 vi -l(vi, T(I * M )) + 1 NM N M j=1 pj -l(pj, I * F ) , (1)
where N F and N M are the total numbers of vertices in C F and C M , respectively.

For each vertex v ∈ C F , the function l(v, T(I * M )) calculates the closest vertex to v on C M . Similarly, for each vertex p ∈ C M , the function l(p, (I * F )) calculates the closest vertex to p on C F .

Results and Discussion

VOI selection. Results obtained from a visual inspection of the generated VOIs I * M showed that D M = 1 and 1.5 cm were not enough to capture the movement between end-diastole and end-systole. VOIs formed with D M = 2 and 2.5 cm succeeded in always containing the structure of interest. Since our goal was to reduce the amount of processed information D M = 2 cm was selected. Visual inspection of dierent I * F VOIs showed that D F ≥ 1 cm achieves the construction of a VOI with sucient information. In this case, we preferred to conservatively keep a value larger than the lower limit and dened D F = 1.5 cm for the remaining experiments.

Time point registration. Registration results in terms of average centerline distance (Eq. 1) using dierent metrics are presented in Figure 1. As a reference, the initial displacement of the arteries (no registration) was also computed. In general, the best results were obtained when using mutual information, so this metric was kept for the subsequent experimentations.

An analysis of the nal vessel displacement in terms of image quality (Fig. 2)

showed that the initial displacement has a higher incidence in the results than the image quality. The algorithm performs well on poor quality images but cannot recover excessively large displacements. We consider that the registration does not compensate the initial displacement when the nal distance between centerlines is above the average maximum vessel diameter.

Table 1 compares the results obtained by direct and incremental frame registration on two datasets. In 9 cases the direct frame registration outperforms incremental frame registration, while the latter is better in the remaining 9. Although the incremental approach performs better in most of the cases where the initial displacement between vessels is large (as in RCA and LCX segments), the method does not perform well for very large distances, where the direct approach also fails. From the obtained results it is not possible to say that one of the methods is better than the other. The incremental registration tends to produce smoother images (Figure 3) than the direct approach and to introduce distortion of important structures such as calcied plaques. This can be explained by the higher number of deformations applied in the incremental registration approach. The overall process time for an artery segment was of 6 min in the direct approach and of 37 min for the incremental approach using a Pentium 4 with 3 GHz and 4 GB RAM. We can state that the direct approach is comparable to the incremental one, in terms of the nal vessel displacement results, while remaining computationally less expensive.

Conclusions

We have presented an approach for the registration of potential vascular lesions in order to speed up the diagnosis process of IHD. The proposed approach registers the potential lesion and its surroundings to a corresponding vessel segment of the image reconstructed at a dierent time point. The quality of the results and the computational times obtained on a standard desktop PC make us believe that it is feasible to apply this approach in clinical practice. Future work will focus in dening a metric to more formally validate the values of D F and D M , as well as in combining the method with a lesion detection algorithm [START_REF] Zuluaga | Automatic detection of abnormal vascular cross-sections based on Density Level Detection and Support Vector Machines[END_REF][START_REF] Zuluaga | Learning from only positive and unlabeled data to detect lesions in vascular CT images[END_REF] to provide the complete diagnosis pipeline.

F

  within a VOI of I M denoted I * M . The size of both I * F and I * M is a trade-o. While a too small I * F generally leads to the so called aperture problem, a too large I * F is likely to contain a predominant proportion of other structures (e.g. heart ventricles) that may swamp the similarity metric. Similarly, I * M is expected to entirely encompass the structure of interest dened in I * F , but be not too large to avoid long computations and possible confusion with other similar structures located nearby. For this purpose, we construct a parallelepipedal I * F by adding up a thickness D F around the bounding box of the suspected lesion. Similarly, the construction of I * M starts by mapping the spatial location of I * F to I M , then a thickness D M is added to build up I * M . This parameter corresponds to the maximum displacement magnitude observed on a coronary branch during the cardiac motion [7]. Both thickness parameters D F and D M were determined empirically, then xed for the remaining experiments.

3. 1

 1 CTA DataA total of 92 images from patients undergoing CT coronary angiography at the Hôpital Louis Pradel (Bron, France) were used. The datasets were acquired on a 64-row CTA scanner (Brilliance 64 -Philips Healthcare, Cleveland, OH) with a standard scan protocol. According to their quality, images were classied as poor (25), moderate (26) or good (41). This information was used to assess the performance of the method as a function of the image quality. Twenty paired datasets (systole/diastole pairs) were randomly selected and vessel centerlines were manually traced on three arteries: the right coronary artery (RCA), left anterior descending artery (LAD) and left circumex artery (LCX). The annotated pairs of centerlines were used to evaluate the quality of the registration by measuring the distance between the reference and the registered artery. The remaining datasets were used in additional optimization and evaluation stages of the work.

5 to 1 . 5

 15 cm. I * F and I * M were respectively built in end-diastolic and end-systolic images, after a manual choice of the arterial segments of interest. These were selected from three coronary arteries (RCA, LAD and LCX) in the proximal (P), distal (D) and intermediate (O) part of each artery. The selection of D M and D F was assessed through a visual inspection by means of a user interface that allows the user to simultaneously navigate in both images [10]. Subsequent experiments aimed at the selection of the most appropriate similarity metric amongst the following: Mean Squared Dierences (MSD), Normalized Correlation Coecient (NCC), Mutual Information (MI) and Normalized Mutual Information (NMI). For this matter, 90 pairs I * F , I * M were generated: 3 locations per artery on 3 arteries in 10 datasets.

  tween the registered lesioned vessel and the corresponding vessel in the xed image. For this matter, we used previously annotated vessel centerlines as an evaluation criterion. The transformation obtained from the registration of I * F and I * M was used to deform the centerline from I * M . The distance between the deformed centerline from I * M and the one from I *

Fig. 1 .

 1 Fig. 1. Metric evaluation. Initial and nal vessel centerline average distance (mm) after non-rigid registration using SSD, NCC, MI and NMI metrics for (a) LAD, (b) LCX and (c) RCA arteries.

Fig. 2 .

 2 Fig. 2. Eect of image quality in the registration results -Final vessel centerline average distance (mm) in good (a), moderate (b) and poor (c) quality images. On each plot, 1 denotes initial displacement of the artery , and 2 the nal one.

Fig. 3 .

 3 Fig. 3. Direct vs. incremental registration. The calcication and the vessel shape in (a) are better conserved with direct registration (b). Incremental registration results (c) are more blurred.

Table 1 .

 1 Direct vs. incremental registration. Distance (mm) between the center-

	line at the end-diastole and the end-systole before applying any transformation (BT)
	and after directly (DR) and incrementally (IR) registering three segments of the RCA,
	LAD and LCX.
	Segment Dataset I Dataset II
	BT DR IR BT DR IR
	RCA P 9.18 1.20 3.61 14.98 0.55 0.50
	RCA D 5.42 1.78 1.26 18.25 5.01 4.60
	RCA O 6.31 1.31 2.48 15.03 7.82 6.68
	LAD P 9.08 0.44 0.55 10.90 0.49 0.75
	LAD D 7.98 1.96 0.98 8.67 0.52 0.68
	LAD O 8.03 0.68 1.00 10.52 0.49 0.83
	LCX P 13.33 0.73 1.15 14.21 1.03 0.80
	LCX D 13.27 2.16 0.87 14.93 3.30 2.92
	LCX O 13.31 1.54 1.07 14.72 2.81 2.75

Acknowledgements

This work has been partly funded by ECOS Nord C11S01, Uniandes Interfacultades 06-2010 and Colciencias 1204-519-28996 grants.