Greta Yorsh
email: gretay@post.tau.ac.il

Alexander Rabinovich

Mooly Sagiv
email: msagiv@post.tau.ac.il

Antoine Meyer
email: ameyer@liafa.jussieu.fr

Ahmed Bouajjani

A Logic of Reachable Patterns in Linked Data-Structures

Keywords: Program Verification, Shape Analysis, Heap-manipulating programs, Decidable logic with reachability, Reachability, Routing expression, Pattern, Transitive closure logics, Weak monadic second-order logic 1991 MSC: 03B25, 11U05, 03B45, 03B15, 68N15, 68N30, 68N19

We define a new decidable logic for expressing and checking invariants of programs that manipulate dynamically-allocated objects via pointers and destructive pointer updates. The main feature of this logic is the ability to limit the neighborhood of a node that is reachable via a regular expression from a designated node. The logic is closed under boolean operations (entailment, negation) and has a finite model property. The key technical result is the proof of decidability.

We show how to express precondition, postconditions, and loop invariants for some interesting programs. It is also possible to express properties such as disjointness of datastructures, and low-level heap mutations. Moreover, our logic can express properties of arbitrary data-structures and of an arbitrary number of pointer fields. The latter provides a way to naturally specify postconditions that relate the fields on procedure's entry to the field on procedure's exit. Therefore, it is possible to use the logic to automatically prove partial correctness of programs performing low-level heap mutations.

Introduction

The automatic verification of programs with dynamic memory allocation and pointer manipulation is a challenging problem. In fact, due to dynamic memory allocation and destructive updates of pointer-valued fields, the program memory can be of arbitrary size and structure. This requires the ability to reason about a potentially infinite number of memory (graph) structures, even for programming languages that have good capabilities for data abstraction. Usually abstract-datatype operations are implemented using loops, procedure calls, and sequences of low-level pointer manipulations; consequently, it is hard to prove that a data-structure invariant is reestablished once a sequence of operations is finished [START_REF] Hoare | Recursive data structures[END_REF].

To tackle the verification problem of such complex programs, several approaches emerged in the last few years with different expressive powers and levels of automation, including works based on abstract interpretation [START_REF] Lev-Ami | TVLA: A system for implementing static analyses[END_REF][START_REF] Sagiv | Parametric shape analysis via 3-valued logic[END_REF][START_REF] Reps | Static program analysis via 3-valued logic[END_REF], logic-based reasoning [START_REF] Ishtiaq | Bi as an assertion language for mutable data structures[END_REF][START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF], and automata-based techniques [START_REF] Klarlund | Graph Types[END_REF][START_REF] Møller | The pointer assertion logic engine[END_REF][START_REF] Bouajjani | Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking[END_REF]. An important issue is the definition of a formalism that (1) allows us to express relevant properties (invariants) of various kinds of linked data-structures, and (2) has the closure and decidability features needed for automated verification. The aim of this paper is to study such a formalism based on logics over arbitrary graph structures, and to find a balance between expressiveness, decidability and complexity.

Reachability is a crucial notion for reasoning about linked data-structures. For instance, to establish that a memory configuration contains no garbage elements, we must show that every element is reachable from some program variable. Other examples of properties that involve reachability are (1) data-structure invariants, e.g., the tail of a queue is reachable from the head of a queue, [START_REF] Arnborg | Easy problems for tree-decomposable graphs[END_REF] the acyclicity of data-structure fragments, i.e., every element reachable from node u cannot reach u, (3) the property that a data-structure traversal terminates, e.g., there is a path from a node to a sink-node of the data-structure, (4) the property that, for programs with procedure calls when references are passed as arguments, elements that are not reachable from a formal parameter are not modified.

A natural formalism to specify properties involving reachability is the first-order logic over graph structures with transitive closure. Unfortunately, even simple decidable fragments of first-order logic become undecidable when transitive closure is added [START_REF] Grädel | Undecidability results on two-variable logics[END_REF][START_REF] Immerman | The boundery between decidability and undecidability of transitive closure logics[END_REF].

In this paper, we propose a logic that can be seen as a fragment of the first-order logic with transitive closure. Our logic [START_REF] Areces | Hybrid logics: characterization, interpolation and complexity[END_REF] is simple and natural to use, (2) is expressive enough to cover important properties of a wide class of arbitrary linked data-structures, and (3) allows for algorithmic modular verification using programmer's specified loop-invariants and procedure's specifications.

Alternatively, our logic can be seen as a propositional logic with atomic proposi-tions (called reachability constraints) modelling reachability between heap objects pointed-to by program variables and other heap objects with certain properties. The properties are specified using patterns that limit the neighborhood of an object.

For example, we can specify the property that an object v is an element of a doublylinked list using a the pattern inv f,b , defined by (v f → w) ⇒ (w b → v). This pattern says that if v has an emanating forward pointer f that leads to an object w, then w has a backward pointer b into v. Using the pattern inv f,b , we can describe a doubly-linked list pointed-to by a program variable x by the atomic proposition x[ f → * ]inv f,b in our logic. This reachability constraint says that any object v reachable from an object pointed-to by x using a (possibly empty) sequence of forward pointers satisfies the property inv f,b . 2The design of our logic is guided by the following principles. First, reachability constraints are closed formulas without quantifier alternations. This guarantees that we are dealing with alternation-free formulas. Second, reachability is expressed via Kleene star operator. We believe that regular expressions is a more natural notation than transitive closure operator. Third, decidability is obtained by syntactically restricting the way patterns are formed. In particular, the use of equality is limited. Semantically, the restriction means that a pattern cannot relate between two nodes that are distant from one another, unless the nodes are "named". As a result, a pattern can only describe local properties. Global properties can only be described using reachability along regular paths that start from "named" nodes. Therefore, complex properties can be enforced only between "named" nodes. For example, complex sharing patterns can be created around objects pointed-to by program variables; arbitrary sharing is allowed but cannot be enforced deep in the data-structure, because the objects that are deep are indistinguishable and distant nodes cannot be related by a pattern.

The contributions of this paper can be summarized as follows:

• We define the logic L 0 where reachability constraints such as those mentioned above can be used. Patterns in such constraints are defined by quantifier-free first-order formulas over graph structures and sets of access paths are defined by regular expressions. • We show that L 0 has a finite-model property, i.e., every satisfiable formula has a finite model. Therefore, invalid formulas are always falsified by a finite store. • We prove that the logic L 0 is, unfortunately, undecidable.

• We define a suitable restriction on the patterns leading to a fragment of L 0 called L 1 . • We prove that the satisfiability (and validity) problem is decidable. The fragment L 1 is the main technical result of the paper and the decidability proof is non-trivial. The main idea is to show that every satisfiable L 1 formula is also satisfied by a tree-like graph. Thus, even though L 1 expresses properties of arbitrary data-structures, because the logic is limited enough, a formula that is satisfied on an arbitrary graph is also satisfied on a tree-like graph. Therefore, it is possible to answer satisfiability (and validity) queries for L 1 using a decision procedure for weak monadic second-order logic (MSO) on trees. • We show that despite the restriction on patterns we introduce, the logic L 1 is still expressive enough for use in program verification: various important data-structures, and loop invariants concerning their manipulation, are in fact definable in L 1 . • We show that the proof of decidability of L 1 holds "as is" for many useful extensions of L 1 .

We define Logic of Reachable Patterns (LRP for short) to be one of the decidable extension of L 1 (see Section 9 for details). The new logic LRP forms a basis of the verification framework for programs with pointer manipulation, which is a subject of an ongoing work. For instance, in contrast to decidable logics that restrict the graphs of interest (such as weak monadic second-order logic on trees), our logic allows arbitrary graphs with an arbitrary number of fields. We show that this is very useful even for verifying programs that manipulate singly-linked lists in order to express postcondition and loop invariants that relate the input and the output state. By restricting the syntax, we guarantee that queries posed over arbitrary graphs can be answered by considering only tree-like graphs. This approach allows us to automate the reasoning about limited but interesting properties of arbitrary graphs. Moreover, our logic strictly generalizes the decidable logic in [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF], which inspired our work. Therefore, it can be shown that certain heap abstractions including [START_REF] Hendren | Parallelizing Programs with Recursive Data Structures[END_REF][START_REF] Sagiv | Solving shape-analysis problems in languages with destructive updating[END_REF] can be expressed using LRP formulas.

The rest of the paper is organized as follows: Section 2 defines the syntax and the semantics of L 0 , and shows that it has a finite model property; Section 3 shows that L 0 is undecidable; Section 4 defines the fragment L 1 , demonstrates the expressiveness of L 1 on several examples, and defines an interesting extension of L 1 , called L 2 ; Section 5 presents the decidability proof for L 1 , with a detailed proof of the main theorem given in Section 6; Section 7 sketches the proof of decidability of L 2 , which does not immediately follow from the one of L 1 ; Section 8 contains the complexity results for L 1 ; Section 9 discusses the limitations and the extensions of the new logics; finally, Section 10 discusses the related work.

The L 0 Logic

In this section, we define the syntax and the semantics of our logic. For simplicity, we explain the material in terms of expressing properties of heaps. However, our logic can actually model properties of arbitrary directed graphs. Still, the logic is powerful enough to express the property that a graph denotes a heap.

Syntax of L 0

L 0 is a propositional logic over reachability constraints. That is, an L 0 formula is a boolean combination of closed formulas in first-order logic with transitive closure that satisfy certain syntactic restrictions.

Let τ = C, U, F denote a vocabulary, where

• C is a finite set of constant symbols usually denoting designated objects in the heap, pointed to by program variables; • U is a set of unary relation symbols denoting properties, e.g., color of a node in a Red-Black tree; • F is a finite set of binary relation symbols (edges) usually denoting pointer fields. 3For example, we can describe a doubly-linked list with forward pointer f and backward pointer b, pointed-to by a program variable x, using the vocabulary in which C = {x}, U = {}, and F = {f, b}. We can describe a Red-Black tree pointed-to by a program variable root using the vocabulary in which C = {root}, U = {red, black}, and F = {right, lef t}.

A term t is either a variable or a constant. An atomic formula is an equality t = t ′ , a monadic formula u(t) for some u ∈ U , or an edge formula t f → t ′ for some f ∈ F , and terms t, t ′ . A quantifier-free formula ψ(v 0 , . . . , v n ) over τ and variables v 0 , . . . , v n is an arbitrary boolean combination of atomic formulas. We say that a sub-formula ψ appears positively (negatively) in ϕ, if ψ appears under an even (odd) number of negations in ϕ. Let F V (ψ) denote the free variables of the formula ψ.

Definition 2.1 A neighborhood formula N (v 0 , . . . , v n ) is a conjunction of edge formulas of the form v f → v ′
, where f ∈ F and v, v ′ ∈ {v 0 , . . . , v n }, and monadic formulas of the form u(v) or ¬u(v), where u ∈ U . Definition 2.2 Let N (v 0 , . . . , v n ) be a neighborhood formula. The Gaifman graph of N , denoted by B N , is an undirected graph with a vertex for each free variable of N . There is an edge between the vertices corresponding to v i and v j in B N if and only if (v i f → v j ) appears in N , for some f ∈ F . The distance between logical variables v i and v j in the formula N is the minimal edge distance between the corresponding vertices v i and v j in B N .

For example, for the formula

N = (v 0 f → v 1 ) ∧ (v 0 f → v 2 )
the distance between v 1 and v 2 in N is 2, and its underlying graph B N looks like this:

v 1 -v 0 -v 2 .

Definition 2.3 A routing expression is an extended regular expression, defined as follows:

R ::= ∅ empty set

| ǫ empty path | f → f ∈ F forward along edge | f ← f ∈ F backward along edge | u u ∈ U test if u holds | ¬u u ∈ U test if u does not hold | c c ∈ C test if c holds | ¬c c ∈ C test if c does not hold | R 1 .R 2 concatenation | R 1 |R 2 union | R * Kleene star
Intuitively, a routing expression describes a path in the heap.

A routing expression can require that a path traverse some pointer fields backwards. For example, the routing expression f → * . f ← * describes a sequence of f -edges that may look like this:

f → f → f ← f ← f ← .
We use this routing expression in Section 4.2 to describe disjoint data-structures.

A routing expression has the ability to test properties of heap objects along the path. For example, a routing expression ( f → .¬y) * describes a path which does not traverse an object pointed-to by the program variable y. We use this routing expression to describe a path along which some property holds until the path reaches the object pointed-to by y (see Section 4.2).

Definition 2.4 (Syntax of L

0 ) A reachability constraint is a closed formula of the form: ∀v 0 , . . . , v n .R(c, v 0 ) ⇒ (N (v 0 , . . . , v n ) ⇒ ψ(v 0 , . . . , v n )) (1)
where c ∈ C is a constant, R is a routing expression, N is a neighborhood formula, and ψ is an arbitrary quantifier-free formula, such that F V (N ) ⊆ {v 0 , . . . , v n } and F V (ψ) ⊆ F V (N ) ∪ {v 0 }. In particular, if the neighborhood formula N is true (the empty conjunction), then ψ is a formula with a single free variable v 0 .

An L 0 formula is a boolean combination of reachability constraints.

The subformula N (v 0 , . . . , v n ) ⇒ ψ(v 0 , . . . , v n ) defines a pattern, denoted by p(v 0 ). Here, the designated variable v 0 denotes the "central" node of the "neighborhood" reachable from c by following an R-path. Intuitively, neighborhood formula N binds the variables v 0 , . . . , v n to nodes that form a subgraph, and ψ defines more constraints on those nodes. 4For example, the pattern det f (v 0 ) defined by the formula

(v 0 f → v 1 ) ∧ (v 0 f → v 2 ) ⇒ (v 1 = v 2 ) ensures that v 0 has at most one outgoing f -edge. The neighborhood formula (v 0 f → v 1 )∧(v 0 f → v 2 )
contains two edges emanating from the central node v 0 . The restriction on the neighborhood is that the edges are in fact the same, because they have the same source, v 0 , the same target, v 1 = v 2 , and the same label f . We use let expressions to specify the scope in which the pattern is declared:

let p 1 (v 0 ) def = N 1 (v 0 , . . . , v n ) ⇒ ψ 1 (v 0 , . . . , v n ) in ϕ
This allows us to write more concise formulas via reuse of pattern definitions. For example, we can say that program variables x and y are pointing to (potentially shared) doubly-linked lists:

let inv f,b (v 0 ) def = (v 0 f → v 1 ⇒ v 1 b → v 0 ) in x[ f → ]inv f,b ∧ x[ f → ]inv f,b

Shorthands

We use c[R]p to denote a reachability constraint [START_REF] Areces | Hybrid logics: characterization, interpolation and complexity[END_REF]. Intuitively, the reachability constraint requires that every node that is reachable from c by following an R-path satisfy the pattern p.

We use

c 1 [R]¬c 2 to denote let p(v 0 ) def = (true ⇒ ¬(v 0 = c 2 )) in c 1 [R]p.
In this simple case, the neighborhood is only the node assigned to v 0 . Intuitively, c 1 [R]¬c 2 means that the node labeled by constant c 2 is not reachable along an R-path from the node labeled by c 1 . We use c 1 R c 2 as a shorthand for ¬(c 1 [R]¬c 2 ). Intuitively, c 1 R c 2 means that there exists an R-path from c 1 to c 2 . We use c 1 = c 2 to denote c 1 ǫ c 2 , and

c 1 = c 2 to denote ¬(c 1 = c 2 ). We use c[R](p 1 ∧ p 2 ) to denote (c[R]p 1 ) ∧ (c[R]p 2 )
, when p 1 and p 2 agree on the central node variable. When two patterns are often used together, we introduce a name for their conjunction (instead of naming each one separately):

let p(v 0 ) def = (N 1 ⇒ ψ 1 ) ∧ (N 2 ⇒ ψ 2 ) in ϕ.
For a quantifier-free formula ψ(v 0 ) with a single free variable v 0 , we write c

[R]ψ instead of let p(v 0 ) def = (true ⇒ ψ(v 0 )) in c[R]p. If ψ(v 0
) has only monadic formulas, we omit the free variable v 0 from it. In particular, for a unary relation symbol u, we use c

[R]u to denote let p(v 0 ) def = (true ⇒ u(v 0 )) in c[R]p.
We use u(c) to denote the formula c ǫ u (equivalently, c[ǫ]u). We abuse the notations slightly by writing

N ∧ ψ 1 ⇒ ψ 2 instead of N ⇒ (ψ 1 ⇒ ψ 2 ).
In routing expressions, we use Σ → to denote the routing expression

( f 1 → | f 2 → | . . . | fm →
), the union of all the fields in F . Similarly, Σ ← denotes the routing expression

( f 1 ← | f 2 ← | . . . | fm ← ). For example, c 1 [ Σ → *
]¬c 2 means that c 2 is not reachable from c 1 by any path. Finally, we sometimes omit the concatenation operator "." in routing expressions.

Semantics of L 0

L 0 formulas are interpreted over labeled directed graphs. A labeled directed graph

G over a vocabulary τ = C, U, F is a tuple V G , E G , C G , U G where: • V G is a set of nodes modelling the heap objects, • E G : F → P(V G × V G ) are labeled edges, • C G : C → V G
provides interpretation of constants as unique labels on the nodes of the graph, and • U G : U → P(V G ) maps unary relation symbols to the set of nodes in which they hold.

The language L(R) of words accepted by a routing expression R is defined as usual for regular expression. The semantics of L 0 formulas is formally defined as follows.

Definition 2.5 Consider a routing expression R and w ∈ L(R). We say that there is a path labeled by w from a node s 1 to a node s 2 in G if one of the following conditions holds:

• s 1 = s 2 and w = ǫ,

• s 1 = s 2 , w = u for a unary relation symbol u and s 1 ∈ U G (u),

• s 1 = s 2 , w = ¬u for a unary relation symbol u and Remark. The translation from L 0 to MSO in Section 5.1 provides an alternative definition for the semantics of L 0 .

s 1 / ∈ U G (u), • s 1 = s 2 , w = c for a constant c and C G (c) = s 1 , • s 1 = s 2 , w = ¬c for a constant c and C G (c) = s 1 , • w = f → for an edge f ∈ F and s 1 , s 2 ∈ E G (f ), • w = f ← for an edge f ∈ F and s 2 , s 1 ∈ E G (f ), • w = w 1 .

Finite Model Property

We are interested in checking validity (and satisfiability) of L 0 formulas only over finite graphs. The graphs are finite because they represent data-structures allocated by a program. (However, the graphs may be unbounded, due to dynamic allocation of memory.) In general, finite validity problem is considered more difficult than validity. For example, in first-order logic, validity problem is recursively enumerable while finite validity is not. In a logic with finite model property, the notions of validity and finite validity coincide. Thus, finite model property is desirable. 3 Undecidability of L 0

L 0 with
The satisfiability and the validity problems of L 0 formulas are undecidable. Since L 0 is closed under negation, it is sufficient to show that its satisfiability problem is undecidable. The proof uses a reduction from the tiling problem. It is well-known that tiling problems of this flavor are undecidable. Therefore, if a logic can express tilings, its satisfiability problem is also undecidable. Given a tiling problem T , we construct a formula ϕ T , such that ϕ T is satisfiable if and only if there exists a solution to T .

The idea is that each node in the graph that satisfies ϕ T describes a tile, with unary relation symbols T 0 , . . . , T k encoding the tile types t 0 , . . . t k . There is a b-edge between every two nodes that are vertically adjacent in the grid. There is an n-edge between every two nodes that are horizontally adjacent in the grid, and from the last node of every row to the first node in the subsequent row. The constant c labels the top left node of the grid, the constant c ′ labels the top right node of the grid, the constant c ′′ labels the first node of the second row of the grid, and the constant c ′′′ labels the bottom right node of the grid (see sketch in Fig. 1). The unary relation red labels the nodes of the last column of the grid.

The most interesting part of the formula ϕ T ensures that all graphs that satisfy ϕ T have a grid-like form. It states that for every node v that is n-reachable from c, if there is a b-edge from v to u, then there is a b-edge from the n-successor of v to the n-successor of u:

let p(v) def = (v b → u) ∧ (v n → v 1 ) ∧ (u n → u 1 ) ⇒ (v 1 b → u 1 ) in c[( n → ) * ]p (2)
Theorem 3.2 (Undecidability) The satisfiability problem of L 0 formulas is undecidable.

Proof: Given a tiling problem T = T, R, D , we construct an L 0 formula ϕ T as a conjunction of the following formulas:

(1) There is n-path from c to c ′ : c

( n → ) * c ′ (2) There is n-edge from c ′ to c ′′ : c ′ n → c ′′ (3) There is n-path from c ′′ to c ′′′ : c ′′ ( n → ) * c ′′′ (4) There is b-edge from c to c ′′ : c b → c ′′ . (5) No n-edge exits t: c ′′′ [ n → ]f alse. ( 6
) For every node v that is n-reachable from s, if there is a b-edge from v to u, then there is a b-edge from the n-successor of v to the n-successor of u:

let p(v) def = (v b → u) ∧ (v n → v 1 ) ∧ (u n → u 1 ) ⇒ (v 1 b → u 1 ) in c[( n → ) * ]p. (7)
The n-edges and the b-edges reachable from s are deterministic:

let det n (v) def = (v n → v ′ ) ∧ (v n → v ′′ ) ⇒ (v ′ = v ′′ ) in s[( n → ) * ]det n , similarly, for b-edges. (8)
The top left node of the grid has a t 0 tile type, and the bottom right node of the grid has a t k tile type: T 0 (c) ∧ T k (c ′′′ ). (9) Each node in the grid has exactly one tile type: [START_REF] Bozga | On logics of aliasing[END_REF] Every node in the last column of the grid is labeled with red: c ′ [( b → ) * ]red. [START_REF] Burdy | An overview of jml tools and applications[END_REF] To express that only nodes in the last column of the grid are labeled with red, we say that the first row is not labeled with red, except its last node, and if a node is labeled with red, then its b-predecessor is labeled: [START_REF] Calcagno | From Separation Logic to First-Order Logic[END_REF] Two horizontally adjacent tiles are compatible according to R: [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF] Two vertically adjacent tiles are compatible according to D:

c[( n → ) * ]   0≤i<j≤k ¬(T i ∧ T j )   ∧   0≤i≤k T i   (
c[( n → .¬c ′ ) * ]¬red ∧ let p(v) def = (w b → v) ∧ red(v) ⇒ red(w) in c[( n → ) * ]p (
let p(v) def = (v n → w) ∧ ¬red(v) ⇒   R(t i ,t j ) (T i (v) ∧ T j (w))   in c[( n → ) * ]p (
let p(v) def = (v b → w) ⇒ D(t i ,t j ) (T i (v) ∧ T j (w)) in c[( n → ) * ]p
Remark. The reduction uses only two binary relation symbols and a fixed number of unary relation symbols. It can be modified to show that the logic with three binary relation symbols (and no unary relations) is undecidable.

4 Decidable and Useful Fragments of L 0

In this section we define two fragments of L 0 and show their usefulness. In the next section, we show that these fragments are decidable.

First, we define the L 1 fragment of L 0 , by syntactically restricting the patterns. We show that L 1 naturally describes some commonly-used data-structures, and express verification conditions. Second, we define L 2 by extending L 1 with constants in patterns, and show that this extension allows us to describe more complex datastructures.

The L 1 Fragment

The L 1 fragment is defined by syntactically restricting the patterns which can be used. The fragment L 1 permits arbitrary boolean combinations in patterns, but it restricts the distance between variables and forbids the use of constants in positive occurrences of equality and edge formulas. • (equality restriction) If ψ contains a positive occurrence of an equality between variables v i = v j , then the distance between v i and v j in N is at most 2 (distance is defined in Def. 2.2). • (edge restriction) If ψ contains a positive occurrence of an edge formula of the form v i f → v j , then the distance between v i and v j in N is at most 1.

• (constant restriction) Positive occurrences of formulas of the form v f

→ c, c f → v, and v = c in ψ are not allowed.

Remark. Note that formula [START_REF] Arnborg | Easy problems for tree-decomposable graphs[END_REF], which is used in the proof of undecidability in Theorem 3.2, is not in L 1 , because p contains a positive v 1 b → u 1 with distance 3 between v 1 and u 1 , while L 1 allows edge patterns with distance at most 1.

Pattern Name Pattern Definition

Meaning

det f (v 0 ) (v 0 f → v 1 ) ∧ (v 0 f → v 2 ) ⇒ (v 1 = v 2 ) f -edge from v 0 is deterministic uns f (v 0 ) (v 1 f → v 0 ) ∧ (v 2 f → v 0 ) ⇒ (v 1 = v 2 ) v 0 is not heap-shared by f -edges uns f,g (v 0 ) (v 1 f → v 0 ) ∧ (v 2 g → v 0 ) ⇒ f alse v 0 is not heap-shared by f - edge and g-edge inv f,b (v 0 ) (v 0 f → v 1 ⇒ v 1 b → v 0 ) every f -edge from v 0 to v 1 has a b-edge in the opposite direction. same f,g (v 0 ) (v 0 f → v 1 ⇒ v 0 g → v 1 ) ∧ (v 0 g → v 1 ⇒ v 0 f → v 1 )
edges f and g emanating from v 0 are parallel Table 1 Useful pattern definitions (f, b, g ∈ F are edge labels).

Describing Linked Data-Structures in L 1

In this section, we show that L 1 can express properties of data-structures. Table 1 lists some useful patterns and their meanings. For example, the first pattern det f means that there is at most one outgoing f -edge from a node. Another important pattern uns f means that a node has at most one incoming f -edge. We use the subscript f to emphasize that this definition is parametric in f .

Well-formed heaps

We assume that C (the set of constant symbols) contains a constant for each pointer variable in the program (denoted by x, y in our examples). Also, C contains a designated constant null that represents NULL values. Throughout the rest of the paper we assume that all the graphs denote wellformed heaps, i.e., the fields of all objects reachable from constants are deterministic, and dereferencing NULL yields null. In L 1 this is expressed by the formula:

( c∈C f ∈F c[Σ * ]det f ) ∧ ( f ∈F null f → null) (3)
Using the patterns in Table 1, Table 2 defines some interesting properties of datastructures using L 1 . The formula reach x,f,y means that the object pointed-to by the program variable y is reachable from the object pointed-to by the program variable x by following an access path of f field pointers. We can also use it with null in the place of y. For example, the formula reach x,f,null describes a (possibly empty) linked-list pointed-to by x. Note that reach x,f,null implies that the list is acyclic, because null is always a "sink" node in a well-formed heap. We can also express that there are no incoming f -edges into the list pointed to by x, by conjoining the previous formula with unshared x,f . Alternatively, we can specify that x is located on a cycle of f -edges: cyclic x,f . Disjointness can be expressed by the for-Name Formula reach x,f,y x ( f → ) * y the heap object pointed-to by y is reachable from the heap object pointed-to by x. cyclic x,f

x ( f → ) + x cyclicity: the heap object pointed-to by x is located on a cycle. unshared x,f

x[( f → ) * ]uns f every heap object reachable from x by an f -path has at most one incoming f -edge.

disjoint x,f,y,g x[( f → ) * ( g ← ) *
]¬y disjointness: there is no heap object that is reachable from x by an f -path and also reachable from y by a g-path. same x,f,g

x[( f → | g → ) * ]same f,g the f -path and the g-path from x are parallel, and traverse same objects. inverse x,f,b,y reach x,f,y ∧ x[( f → .¬y) * ]inv f,b doubly-linked lists between two variables x and y with f and b as forward and backward edges.

tree root,r,l root[( l → | r → ) * ](uns l,r ∧ uns l ∧ uns r ) ∧ ¬(root ( l → | r → ) + root) tree rooted at root. tree root,r,l,b tree root,r,l ∧ root[( l → | r → ) * ]inv l,b ∧ inv r,
b tree rooted at root with parent pointers b from every tree node to its parent. mula disjoint x,f,y,g that uses both forward and backward traversal of edges in the routing expression. Disjointness of data-structures is important for parallelization (e.g., see [START_REF] Hendren | Abstractions for recursive pointer data structures: Improving the analysis and the transformation of imperative programs[END_REF]). For example, we can express that the linked list pointed to by x is disjoint from the linked-list pointed to by y, using the formula disjoint x,f,y,f . This formula guarantees that every node v that is reachable from the node pointed-to by x using an f -path must not be reachable from y using an f -path. However, v may be reachable from y using other edges, or v maybe a part of another data-structure which shares elements with y. 2 specify data-structures with multiple fields. The formula inverse x,f,b,y describes a doubly-linked list with variables x and y pointing to the head and the tail of the list, respectively. First, it guarantees the existence of an f -path. Next, it uses the pattern inv f,b to express that if there is an f -edge from one node to another, then there is a b-edge in the opposite direction. This pattern is applied to all nodes on the f -path that starts from x and that does not visit y,

The last three examples in Table

Node reverse(Node x){

[0] Node y = null; [START_REF] Areces | Hybrid logics: characterization, interpolation and complexity[END_REF] while (x != null){ [START_REF] Arnborg | Easy problems for tree-decomposable graphs[END_REF] Node t = x.n; [START_REF] Balaban | Shape analysis by predicate abstraction[END_REF] x.n = y; [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF] y = x; [START_REF] Berdine | A Decidable Fragment of Separation Logic[END_REF] x = t; [6] } [START_REF] Bonatti | On the undecidability of logics with converse, nominals, recursion and counting[END_REF] return y; } Fig. 2. The reverse procedure performs in-place reversal of a singly-linked list expressed using the test "¬y" in the routing expression.

The formula tree root,r,l describes a binary tree. The first part requires that the nodes reachable from the root (by following any path of l and r fields) not be heap-shared. The second part prevents edges from pointing back to the root of the tree by forbidding the root to participate in a cycle. The formula tree root,r,l,b describes a binary tree rooted at root with parent pointers b from every tree node to its parent.

The ability to express properties like tree root,r,l is non-trivial, because we are operating on general graphs, and not just trees. Operating on general graphs allows us to verify that the data-structure invariant is reestablished after a sequence of low-level mutations that temporarily violate the invariant data-structure.

Expressing Verification Conditions in L 1

The Reverse Procedure

The reverse procedure shown in Fig. 2 performs in-place reversal of a singlylinked list. This procedure is interesting because it destructively updates the list and the natural specification of its partial correctness requires reasoning about two fields. Moreover, it manipulates linked lists in which each list node can be pointedto from the outside. We show that the verification conditions for the procedure reverse can be expressed in L 1 . If the verification conditions are valid, then the program is partially correct with respect to the specification. The validity of the verification conditions can be checked automatically because the logic L 1 is decidable, as shown in the next section. In [START_REF] Yorsh | Verification framework based on the logic of reachable patterns[END_REF], we show how to automatically generate verification conditions in L 1 for arbitrary procedures that are annotated with preconditions, postconditions, and loop invariants in L 1 .

Notice that in this section we assume that all graphs denote valid stores, i.e., satisfy [START_REF] Balaban | Shape analysis by predicate abstraction[END_REF]. The precondition requires that x point to an acyclic list, on entry to the

x 0 y 1 x 1 , y 6 x 6 • n 0 / / • n 0 / / n 1 b b n 6 [ [ • n 0 / / n 1 b b n 6 [ [ • n 0 / / n 1 : : n 6 ^• n 0 / / n 1 < < n 6
C C • Fig. 3. An example graph that satisfies the V C loop formula for reverse.

procedure. We use the symbols x 0 and n 0 to record the values of the variable x and the n-field on entry to the procedure.

pre reverse def = x 0 ( n 0 → ) * null
The postcondition ensures that the result is an acyclic list pointed-to by y. Most importantly, it ensures that each edge of the original list is reversed in the returned list, which is expressed in a similar way to a doubly-linked list, using inverse formula. We use the relation symbols y 7 and n 7 to refer to the values on exit.

post reverse def = y 7 ( n 7 → ) * null ∧ inverse x 0 ,n 0 ,n 7 ,y 7
The loop invariant ϕ shown below relates the heap on entry to the procedure to the heap at the beginning of each loop iteration (label L1). First, we require that the part of the list reachable from x be the same as it was on entry to reverse.

Second, the list reachable from y is reversed from its initial state. Finally, the only original edge outgoing of y is to x.

ϕ def = same x 1 ,n 0 ,n 1 ∧ inverse x 0 ,n 0 ,n 1 ,y 1 ∧ y 1 n 0 → x 1
Note that the postcondition uses two binary relations, n 0 and n 7 , and also the loop invariant uses two binary relations, n 0 and n 1 . This illustrates that reasoning about singly-linked lists requires more than one binary relation.

The verification condition of reverse consists of two parts, V C loop and V C, explained below.

The formula V C loop expresses the fact that ϕ is indeed a loop invariant. To express it in our logic, we use several copies of the vocabulary, one for each program point. Different copies of the relation symbol n in the graph model values of the field n at different program points. Similarly, for constants. For example, Fig. 3 shows a graph that satisfies the formula V C loop below. It models the heap at the end of some loop iteration of reverse. The superscripts of the symbol names denote the corresponding program points.

To show that the loop invariant ϕ is maintained after executing the loop body, we assume that the loop condition and the loop invariant hold at the beginning of the iteration, and show that the loop body was executed without performing a null- dereference, and the loop invariant holds at the end of the loop body:

Node append(Node x, Node y) { [0] Node t = x; [1] if (t == null) [2] return y; [3] while (t.n != null) { [4] t = t.n; [5] } [6] t.n = y; [7] return x; }
V C loop def = (x 1 = null)
loop is entered ∧ϕ loop invariant holds on loop head

∧(y 6 = x 1 ) ∧ x 1 n 1 x 6 ∧ x 1 n 6 y 1 loop body ∧same y 1 ,n 1 ,n 6 ∧ same x 6 ,n 1 ,n 6 rest of the heap remains unchanged ⇒ (x 1 = null)
no null-derefernce in the body ∧ϕ 6 loop invariant after executing loop body

Here, ϕ 6 denotes the loop-invariant formula ϕ after executing the loop body (label L6), i.e., replacing all occurrences of x 1 , y 1 and n 1 in ϕ by x 6 , y 6 and n 6 , respectively. The formula V C loop defines a relation between three states: on entry to the procedure, at the beginning of a loop iteration and at the end of a loop iteration.

The formula V C expresses the fact that if the precondition holds and the execution reaches procedure's exit (i.e., the loop is not entered because the loop condition does not hold), the postcondition holds on exit:

V C def = pre ∧ (x 1 = null) ⇒ post.

The Append Procedure

The append procedure given in Fig. 4 concatenates two singly-linked lists.

To describe the effect of a procedure on the heap, we sometimes use auxiliary relations and constants, whose interpretation is constrained in the precondition, and used in the postconditions. It allows us to relate the values after a call to a procedure return to the values before the call. Note that the auxiliary constant does not have an index, because it is not part of the program. In this example, we use the auxiliary constant last to label the last node of the first list.

The precondition for append requires that x and y point to acyclic and disjoint lists, and defines the meaning of the new constant last:

pre append = x 0 n 0 → * null ∧ y 0 n 0 → * null ∧ x 0 [ n 0 → * . n 0 ← * ]¬y 0 ∧ x 0 ( n 0 → .¬null) * last ∧ last n 0 → null
The postcondition for append uses x 7 to denote the return value, which points to an acyclic list. It uses the constant last to identify the object whose next field was modified by the procedure.

post append = x 7 n 7 → * null ∧ x 7 = x 0 ∧ last n 7 → y 0 ∧ x 0 [( n 0 → .¬last) * ]same n 0 ,n 7 ∧ y 0 [ n 0 → * ]same n 0 ,n 7
Unary relations symbols can be used to describe data values from a limited domain, and their interaction with the structural properties of the heap. For example, for a Red-Black tree we can specify that both children of every red node are black:

let rb(v 0 ) def = (red(v 0 ) ∧ lef t(v 0 , v 1 ) ⇒ black(v 1 )) ∧ (red(v 0 ) ∧ right(v 0 , v 1 ) ⇒ black(v 1 )) in root[(lef t|right) * ]rb
Moreover, unary information can be used to describe states of objects, and sets of objects, as shown by the following example.

The Mark Procedure

The mark procedure shown in Fig. 5 implements the mark phase of a Mark&Sweep garbage collector. 5The procedure operates on a general graph, pointed by root. Therefore, the precondition is simply true. There is an f -edge from v 1 to v 2 if either v 2 = v 1 .car or v 2 = v 1 .cdr. Note that unlike the previous examples, f is not deterministic. As an optimization, we do not create copies of f and root for each label of the mark procedure, because the procedure does not modify f and root. We use unary relations p and m to denote objects in the pending and marked sets of nodes, respectively.

The postcondition for mark states that a node is marked if and only if it is reachable from root: post

mark def = post if mark ∧post only-if mark .
The "if" part can be easily expressed using the positive monadic formula m 14 (v 0 ) in the pattern, allowed in L 1 :

post if mark def = root[ f → * ](¬null ⇒ m 14 ) void mark(Node root, NodeSet marked) { [0] Node x; [1] if(!root.isEmpty()){ [2]
NodeSet pending = new NodeSet(); [START_REF] Balaban | Shape analysis by predicate abstraction[END_REF] pending.addAll(root); [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF] marked.clear(); [START_REF] Berdine | A Decidable Fragment of Separation Logic[END_REF] while (!pending.isEmpty()) { [START_REF] Bonatti | Towards service description logics[END_REF] x = pending.selectAndRemove(); [START_REF] Bonatti | On the undecidability of logics with converse, nominals, recursion and counting[END_REF] marked.add(x); [START_REF] Bouajjani | Verifying Programs with Dynamic 1-Selector-Linked Structures in Regular Model Checking[END_REF] if (x.car != null && [START_REF] Bozga | Quantitative Verification of Programs with Lists[END_REF] !marked.contains(x.car)) [START_REF] Bozga | On logics of aliasing[END_REF] pending.add(x.car); [START_REF] Burdy | An overview of jml tools and applications[END_REF] if (x.cdr != null && [START_REF] Calcagno | From Separation Logic to First-Order Logic[END_REF] !marked.contains(x.cdr)) [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF] pending.add(x.cdr); [START_REF] Calvanese | Reasoning in expressive description logics with fixpoints based on automata on infinite trees[END_REF] } } } The "only if" part requires reasoning about nodes that are not necessarily reachable from root. Moreover, it requires reasoning about nodes that need not be reachable from any program variable. To address it, we introduce a new constant c m which represents an arbitrary node, because it is not restricted in the precondition, and write the postcondition and the loop invariant in terms of c m . Intuitively, when checking validity of these formulas, the constant c m can be treated as a universally quantified variable. In the postcondition, we require that if c m is marked, then it is reachable from root:

post only-if mark def = m 14 (c m ) ⇒ root f → * c m
The loop invariant for mark consists of two parts. First, before the loop at label [START_REF] Berdine | A Decidable Fragment of Separation Logic[END_REF] is entered for the first time, the only pending node is root, and no nodes are marked. In particular, root and c m are not marked. Second, after the loop was executed at least some number of times, (i) root remains either marked or pending, (ii) a node cannot be both marked and pending, and (ii) most importantly, if a node is marked then its f -successor is either marked or pending. It means that the "frontier" of the exploration consists of pending nodes: there is no edge from a mark node to a node that is neither marked nor pending. Finally, if a node is marked or pending, then it is reachable from root, which implies the postcondition, because the loop terminates when there are no pending nodes.

p 5 (root) ∧ (c m = root ⇒ ¬p 5 (c m )) ∧ (root[ f → * ]¬m 5 ) ∧ ¬m 5 (c m ) (m 5 (root) ∨ p 5 (root)) ∧ root[ f → * ](¬p 5 ∨ ¬m 5 ) ∧ (¬m 5 (c m ) ∨ ¬p 5 (c m )) ∧ let t(v) def = f (v, v ′ ) ∧ m 5 (v) ⇒ (m 5 (v ′ ) ∨ p 5 (v ′ )) in root[ f → * ]t ∧ m 5 (c m ) ⇒ c m [ f → ](p 5 ∨ m 5 ) ∧ p 5 (c m ) ∨ m 5 (c m ) ⇒ root f → * c m 4.4 The L 2 Fragment
The fragment L 2 extends L 1 by allowing constants to be freely used in patterns, removing the last restriction of Def. 4.1. For example, the property that a general graph is a tree in which each node has a pointer b back to the root is expressible in L 2 , using the pattern true ⇒ b(v 0 , root), but this pattern is not in L 1 . It can be shown that the property cannot be expressed in L 1 , using the same arguments as in Section 7.

Decidability of L 1

In this section, we show that L 1 is decidable for validity and satisfiability. Since L 1 is closed under negation, it is sufficient to show that it is decidable for satisfiability. The proof proceeds as follows:

(1) Translate an L 0 formula into an equivalent MSO formula (Lemma 5.2).

(2) Define a class of simple graphs A k , for which the Gaifman graph (Def. 5.4) is a tree with at most k additional edges (Def. 5.5). (3) Show that the satisfiability of MSO logic over A k is decidable, by reduction to MSO on trees [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF] (Lemma 5.6). We could have also shown decidability using the fact that the tree width of all graphs in A k is bounded by k, and that MSO over graphs with bounded tree width is decidable [START_REF] Courcelle | The monadic second-order logic of graphs, ii: Infinite graphs of bounded width[END_REF][START_REF] Arnborg | Easy problems for tree-decomposable graphs[END_REF][START_REF] Seese | Interpretability and tree automata: A simple way to solve algorithmic problems on graphs closely related to trees[END_REF]. (4) Every formula ϕ ∈ L 1 can be effectively translated into an equi-satisfiable normal-form formula that is a disjunction of formulas in CL 1 (Def. 5.9 and Theorem 5.12). It is sufficient to show that the satisfiability of CL 1 is decidable.

(5) Show that if formula ϕ ∈ CL 1 has a model, ϕ has a model in A k , where k is proportional to the size of the formula ϕ (Theorem 5.14). This is the main part of the proof, given in detail in Section 6.

In Section 7, we extend this proof to show decidability of L 2 .

Translation from L 0 to MSO

Every regular expression R can be effectively translated into an MSO formula ϕ R (x, y), that describes the paths from x to y labeled with w, for every word w in R.

(R)(v 1 , v 2 ).
Sketch of Proof: For atomic regular expressions and concatenation, we define tr(R)(v 1 , v 2 ) as follows:

tr(R)(v 1 , v 2 ) def =                            f (v 1 , v 2 ) if R is f → f (v 2 , v 1 ) if R is f ← ¬(c = v 1 ) ∧ (v 1 = v 2 ) if R is ¬c u(v 1 ) ∧ (v 1 = v 2 ) if R is u ¬u(v 1 ) ∧ (v 1 = v 2 ) if R is ¬u tr(R 1 .R 2 )(v 1 , v 2 ) def = ∃v 3 .tr(R 1 )(v 1 , v 3 ) ∧ tr(R 2 )(v 3 , v 2 )
The formula tr(R * )(v 1 , v 2 ) holds when the minimal set Y that contains v 1 and is closed under R, contains v 2 . Formally, we define

tr(R * )(v 1 , v 2 ) def = ∃Y.(v 2 ∈ Y ) ∧ Q(v 1 , Y ) ∧ ∀Y ′ .Q(v 1 , Y ′ ) ⇒ Y ⊆ Y ′ where Q(v 1 , Z) is (v 1 ∈ Z) ∧ ∀v ′ 1 , v ′ 2 .(v ′ 1 ∈ Z) ∧ ϕ R (v ′ 1 , v ′ 2 ) ⇒ (v ′ 2 ∈ Z).
For example, the routing expression

R def = ( n → .¬y) * is translated into the MSO formula tr(R)(x, v) def = ∃Y.(v ∈ Y ) ∧ Q(x, Y ) ∧ ∀Y ′ .Q(x, Y ′ ) ⇒ Y ⊆ Y ′ , where Q(x, Z) is (x ∈ Z) ∧ ∀v ′ 1 , v ′ 2 .(v ′ 1 ∈ Z) ∧ ∃v ′ 3 .(f (v ′ 1 , v ′ 3 ) ∧ ¬(x = v ′ 3 ) ∧ (v ′ 3 = v ′ 2 )) ⇒ (v ′ 2 ∈ Z).
Using the translation of regular expressions as defined above, it is easy to translate a general L 0 formula to an equivalent MSO formula. For ϕ ∈ L 0 over τ , T R 2 (ϕ) is an MSO formula over the same vocabulary τ . The translation T R 2 is defined inductively:

T R 2 (c[R]p) def = ∀v 0 , v 1 , . . . , v n .ϕ R (c, v 0 ) ⇒ p(v 0 , . . . , v n ) T R 2 (ϕ 1 ∧ ϕ 2 ) def = T R 2 (ϕ 1 ) ∧ T R 2 (ϕ 2 ) T R 2 (¬ϕ 1 ) def = ¬T R 2 (ϕ 1 )
For example, the L 0 formula

ϕ def = x n → * y ∧ x[( n → .¬y) * ]inv n,n ′ which is part of a loop invariant of the reverse procedure (Section 4.3.1), is translated into the MSO formula T R 2 (ϕ) = tr( n → * )(x, y) ∧ ∀v 0 , v 1 .tr(( n → .¬y) * )(x, v 0 ) ⇒ (n(v 0 , v 1 ) ⇒ n ′ (v 1 , v 0 ))
where tr( n → * ) and tr(( n → .¬y) * ) are defined as above.

Lemma 5.2 For all ϕ ∈ L 0 and all graphs S, S |= ϕ iff S |= T R 2 (ϕ).

Decidability of MSO on Ayah Graphs

We define a notion of T k , a set of undirected graphs each of which is a tree 6 with at most k extra edges.

Definition 5.3

An undirected graph B is in T k if removing self loops and at most k additional edges from B results in an acyclic (undirected) graph.

For a directed graph we define the corresponding undirected graph: Definition 5. [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF] Let G(S) denote the Gaifman graph of the graph S, i.e., an undirected graph obtained from S by removing node labels, edge labels, and edge directions (and parallel edges).

We define a notion of simple tree-like (directed) graphs, called Ayah graphs.

Definition 5.5 (Ayah Graphs)

For k ≥ 0, an Ayah graph of k is a graph S for which the Gaifman graph is in T k : A k = {S|G(S) ∈ T k }.
Examples of graphs in A 0 , A 1 , and A 2 are shown in Fig. 6. For j = 0, . . . , 2, a structure S j ∈ A j is shown in the left column, and the corresponding Gaifman graph G(S j ) ∈ T j is shown in the right column; with j dashed edges. Removing the dashed edges from G(S j ) yields a tree.

S 0 G(S 0 ) S 1 G(S 1 ) S 2 G(S 2 )
The graph S 0 describes an acyclic singly-linked list pointed-to by x. The node labeled with null does not represent an element of the list: it is a "sink" node which models the null value, as explained in Section 4.2. In G(S 0 ), the self-loop is not dotted because Def. 5.3 ignores self-loops. (As we show later, self-loops can be easily handled, while larger cycles require a more complex treatment.) The graph S 1 describes a cyclic doubly-linked list. In G(S 1 ), a single edge represents the parallel edges of S 1 with different directions and different labels. The graph S 2 describes a tree with pointers from every tree node to the root. In G(S 2 ), removing a single edge cannot break both cycles, thus the graph S 2 is in A 2 , but not in A 1 .

Remark. For every graph S in A k , the tree width [START_REF] Robertson | Graph minors. ii. algorithmic aspects of tree-width[END_REF][START_REF] Diestel | Graph Theory[END_REF] of G(S) is at most k + 1, but can it can be strictly less than that. For example, a graph which consists of 17 simple disjoint cycles is in A 17 , but its tree width is 2.

The satisfiability problem of MSO logic on Ayah graphs can be reduced to the satisfiability problem of MSO logic on trees, which is decidable, using a classical result due to Rabin [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF]. This reduction provides a constructive way to check sat-isfiability of L 1 formulas, using an existing decision procedure for MSO on trees, MONA [START_REF] Henriksen | Mona: Monadic second-order logic in practice[END_REF].

The reduction consists of two satisfiability-preserving translations: The first is a translation T R 3 from MSO on Ayah graphs to MSO on Σ-labeled trees, defined below. The second is a translation T R 4 from MSO on Σ-labeled trees to MSO on (infinite) binary trees.

Lemma 5. [START_REF] Bonatti | Towards service description logics[END_REF] There are translations T R 3 and T R 4 between MSO-formulas such that for every MSO-formula ϕ, there exists a graph S ∈ A k that satisfies ϕ if and only if there exists a binary tree S ′ such that

S ′ |= (T R 3 • T R 4 )(ϕ).
In this paper, we describe only the translation T R 3 , and omit the (standard) translation, T R 4 .

Encoding A k Graphs as Σ-Labeled Trees

Given the vocabulary τ = C, U, F and a number k we define a new vocabulary

τ ′ = C ′ , U ′ , {E}
, where E is the only binary relation,

C ′ = C ∪ {c 1 , . . . , c k } ∪ {d 1 , . . . , d k }, and U ′ = {F f , B f , L f , F d i f , B d i f |f ∈ F, i = 1, . . . , k}).
Let Σ = P(C ′ ∪ U ′ ) be the set of all possible node labels from τ ′ . A Σ-labeled tree is a graph S over τ ′ that satisfies the following:

(1) The E-edges form a directed forest: each node in S has at most one incoming E edge. An E-edge from node u 1 to node u 2 means that u 2 is a child of u 1 in the tree. (2) If a node has no incoming E-edge, then it must not be labeled by F f , B f , for any f ∈ F .

We use T Σ to denote the set of all Σ-labeled trees.

Every graph in A k can be represented by a Σ-labeled tree. For example, consider the cyclic doubly-linked list S 1 from Fig. 6, defined over the vocabulary τ with C = {x}, U = {}, and

F = {f, b}. The new vocabulary τ ′ consists of C = {x, c 1 , d 1 }, U = {F f , F b , F d 1 f , F d 1 b , B d 1 f , B d 1 b
}, and F = {E}. The graph S 1 can be represented by the following Σ-labeled tree (actually, it is a list in this example):

B d 1 f , F d 1 b F f , B b F f , B b F f , B b f / / f / / f / / x, c 1 d 1
The graph S represented by a Σ-labeled tree has the same set of nodes as the tree.

The labels of S are defined as follows. A graph node is labeled with the constants and unary relation symbols that hold for the corresponding node in the tree. An edge in the tree from node v to v ′ represents edges between the corresponding nodes v and v ′ in the graph. Additional labels on tree nodes represent the direction and the labels of the graph edges adjacent to the corresponding nodes in the graph, as follows.

For each binary relation symbol f ∈ F , we introduce two unary relation symbols F f and B f , denoting forward and backward f -edge. If there is an edge from v to v ′ in the tree, and v ′ is labeled with F f in the tree, then there is an f -edge from v to v ′ in S. Similarly, if there is an edge from v ′ to v in the tree, and v is labeled with B f in the tree, then there is an f -edge from v to v ′ in S. There is a self-loop of f on a node v in S if the node v in the tree is labeled with L f . Also, each of the k pairs of constants c i and d i in a tree represents edges between the nodes corresponding to c i and d i in the graph. If v is labeled with c i and F d i f in the tree, then there is an f -edge from v to the node labeled with d i in S. If v is labeled with c i and B d i f in the tree, then there is an f -edge from the node labeled with d i to v in S.

For an MSO formula ϕ over τ , T R 3 (ϕ) is an MSO formula over the vocabulary τ ′ . The translation T R 3 is defined inductively on ϕ, where the only interesting part is the translation of a binary relation formula f ∈ F :

T R 3 (f (v 1 , v 2 )) = (E(v 1 , v 2 ) ∧ F f (v 2 )) ∨(E(v 2 , v 1 ) ∧ B f (v 1 )) ∨(E(v 1 , v 2 ) ∧ v 1 = v 2 ∧ L f (v 1 )) k i=1 ((c i = v 1 ∧ d i = v 2 ∧ F d i f (v 1 )) ∨ (c i = v 2 ∧ d i = v 1 ∧ B d i f (v 2 )))
Lemma 5.7 Let ϕ be an MSO formula. There is a graph S ∈ A k such that S |= ϕ if and only if there is a Σ-labeled tree T ∈ T Σ such that T |= T R 3 (ϕ).

Proof: Given a graph S in A k , we can encode it as a Σ-labeled tree T as follows.

First, remove all self loops and at most k additional edges from the Gaifman graph of S to obtain an acyclic undirected graph, U . It is easy to transform the undirected graph U into a directed forest T , by choosing one node in every connected component of U as a root, and directing all edges from it downwards. Then, we can set the labels of T uniquely from the labels of the corresponding nodes in S. To encode that an edge in S is labeled with f , we identify the corresponding edge in T , and label the target of the edge with a unary relation to remember the label f .

Given T ∈ T Σ , we can uniquely reconstruct the graph S ∈ A k that corresponds to it. Every node in T that is labeled with F f has exactly one incoming edge, which defines the corresponding edge in S, labeled with f . For each F d i f , at most one edge can be created in S, because T R 3 guarantees that in T the source is labeled with c i , and the target is labeled with d i , which are constants.

Theorem 5.8 The satisfiability problem of MSO formulas is decidable on A k .

Proof: Follows from Lemma 5.6 and [START_REF] Rabin | Decidability of second-order theories and automata on infinite trees[END_REF].

Normal Form of L 0 Formulas

We define a normal-form formula to be a disjunction of conjunctions of formulas of the form c R c ′ and c[R]p. Definition 5.9 (Normal-form formulas) A formula in CL 0 is of the form

i ¬(c i [R i ]¬c ′ i ) ∧ j c j [R j ]p j A normal-form formula is a disjunction of CL 0 formulas.
A formula ϕ is in CL 1 if and only if ϕ ∈ CL 0 and ϕ ∈ L 1 , i.e., all the patterns that appear in ϕ satisfy the requirement of Def. 4.1.

For a formula ϕ ∈ CL 0 , we use ϕ ✸ to denote the first part of ϕ, namely i ¬c i [R i ]¬c ′ i , and ϕ ✷ to denote the second part of ϕ, namely j c j [R j ]p j . We use |ϕ ✸ | to denote the number of conjuncts in the formula ϕ ✸ .

Note that while L 0 is closed under negation, CL 0 is not. The following theorem shows that every L 0 -formula can be effectively translated into an equi-satisfiable normal-form formula. The main difficulty is to translate a formula of the form ¬c[R]p, where p is an arbitrary pattern, into a formula in which negation appears only in front of constraints of the form c ′ [R]¬c ′′ . Definition 5.10 Let θ be the formula ¬c[R]p over τ , where p(v 0 ) = N (v 0 , . . . , v n ) ⇒ ψ(v 0 , . . . , v n ). We introduce new constant symbols c 0 , . . . , c n , and define τ ′ = τ ∪ {c 0 , . . . , c n }. We define tr(θ) as follows:

• Translate ¬ψ into an equivalent negated normal form formula ψ ′ , • Let θ ′ be c R c 0 ∧ N (c 0 , . . . , c n ) ∧ ψ ′ (c 0 , . . . , c n )), where every edge formula v i f → v j that appears in N or ψ ′ is replaced by c i f → c j . 7 • If ¬c R c ′ appears in θ ′ , replace it with c[R]¬c ′ , to obtain θ ′′ . • Transform θ ′′ into an equivalent disjunctive normal form formula θ ′′′ . • Let tr(θ) be θ ′′′ .
The formula tr(θ) is a normal-form formula by Def. 5.9, because it is a disjunction of CL 0 -formulas. In fact, tr(θ) is a very simple formula: all the patterns in it are of the form true ⇒ c = v 0 . Thus, negation can appear only in front of reachability constraints of the form c[R]¬c ′ where R is star-free. Lemma 5.11 For a graph S over τ , if S satisfies θ, then there exists an expansion of S to τ ′ , that satisfies tr(θ). For a graph S ′ over τ ′ , if S ′ |= tr(θ) then the restriction S of S ′ to τ satisfies ϕ. Theorem 5.12 There is a computable translation T R 1 from L 0 to a disjunction of formulas in CL 0 that preserves satisfiability. Sketch of Proof: For every formula ϕ ∈ L 0 over τ , the formula T R 1 (ϕ) is a disjunction of formulas in CL 0 over τ ′ such that ϕ is satisfiable if and only if T R 1 (ϕ) is satisfiable. The vocabulary τ ′ is an extension of τ with new constant symbols. The translation T R 1 (ϕ) is defined as follows:

(1) Translate ϕ into an equivalent formula ϕ ′ in negated normal form using de-Morgan rules to push negations inwards. ( 2

[R]¬c ′ . The result of T R 1 (ϕ) is ϕ ′′′ .
The translation is applicable to the full L 0 logic, in which case the reachability constraints in ϕ ✷ can contain arbitrary patterns.

The translation T R 1 may introduce only patterns of the form true ⇒ c 2 = v 0 beyond those patterns that appear in the input formula. This observation yields the following corollary:

Corollary 5.13 For ϕ ∈ L 1 , the translation T R 1 returns a disjunction of formulas in CL 1 (and preserves satisfiability).

Decidability of L 1

The following theorem states that CL 1 has an Ayah-model property, i.e., every satisfiable CL 1 formula ϕ has a model in A k where k is defined by

f (ϕ) def = 2 × n × |C| × |ϕ ✸ | (4)
Here, we assume that for every routing expression that appears in ϕ ✸ there is an equivalent automaton with at most n states.

Theorem 5.14 (Ayah model property of

L 1 ) If ϕ ∈ CL 1 is satisfiable, then ϕ is satisfiable by a graph in A f (ϕ)
, where f is defined in [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF].

A non-trivial proof of this theorem is presented in Section 6.

Theorem 5. [START_REF] Courcelle | The monadic second-order logic of graphs, ii: Infinite graphs of bounded width[END_REF] The satisfiability problem of L 1 is decidable.

Proof: Follows from combining the results of Theorem 5.12, Theorem 5.14, Lemma 5.2, Theorem 5.8.

Ayah Model Property of L 1

In this section we provide a detailed proof of the main technical theorem of the paper, Theorem 5.14. Before diving into the details, we explain the main proof at a high-level.

Given a normal-form formula ϕ ∈ CL 1 and a graph S such that S |= ϕ, we construct a graph S ′ and show that S ′ |= ϕ and S ′ ∈ A k .

The construction operates as follows. We construct a pre-model S 0 of S and ϕ, which satisfies all constraints of the form c R c ′ in ϕ. The idea is to extract from S a witness path for each constraint of the form c R c ′ in ϕ, and define S 0 to be the union of these witness paths (Section 6.5).

The pre-model S 0 may violate some of the constraints of the form c[R]p in ϕ.

Consider the case when the pattern p contains a positive occurrence of edge formula or equality formula. If a graph G violates a constraint c[R]p, then there is an enabled merge operation or edge-addition operation, depending on the pattern p (Section 6.3).

For example, if p is of the form N (v 0 , v 1 , v 2 ) ⇒ v 1 = v 2 , it defines a merge operation. We say that this merge operation is enabled in a graph G (by c[R]p) when G contains a node w 0 reachable by an R-path from c and distinct nodes w 1 and w 2 forming the neighborhood N (w 0 , w 1 , w 2 ). Applying this operation means merging the nodes w 1 and w 2 . After merging w 1 and w 2 , other merge operations may still be enabled in G by c[R]p. If there are no more enabled operations in G, then

G |= c[R]p. Similarly, if p is of the form N (v 0 , v 1 , v 2 ) ⇒ v 1 f → v 2 ,
it defines an edge-addition operation. Applying this operation means adding an f -edge.

Given a pre-model S 0 , we apply all enabled operations in any order, producing a sequence of distinct graphs S 0 , S 1 , . . . until the last graph S ′ has no enabled operations. Thus, S ′ satisfies all constraints of the form c[R]p where p contains a positive occurrence of edge formula or equality formula. We show that applying any enabled operation preserves witness paths for the constraints of the form c R c ′ . Thus, S ′ also satisfies all constraints of the form c R c ′ . This construction also guarantees that S ′ satisfies all the constraints of the form c[R]p where p is a negative formula. To show this formally, we use homomorphism (Section 6.4) which preserves ex-istence of edges and both existence and absence of labels on nodes (preserving absence of labels is non-standard).

Finally, the fact that S ′ is in A k is proved by induction. By construction, S 0 is in A k (Lemma 6.11), and A k is closed under operations enabled by L 1 formulas (Lemma 6.5). The proof of closure properties of A k is based on closure properties for a class of undirected graphs, T k (Lemma 6.1).

The rest of the section describes the building blocks of the proof of Theorem 5.14: closure properties of T k (Section 6.1), closure properties of A k (Section 6.2), the definition of operations enabled by L 1 formulas (Section 6.3), the definition of homomorphism relation and its properties (Section 6.4), and the definition of witness splitting and properties of a pre-model (Section 6.5). The proof of Theorem 5.14 concludes the section.

Trees with Extra Edges

Recall from Def. 5.3 that T k is a set of undirected graphs that are trees with k extra edges. In this section we prove that T k is closed under merging of vertices at distance at most 2.

The distance between the vertices v 1 and v 2 in an undirected graph B is the number of edges on the shortest path between v 1 and v 2 in B.

Merging two vertices in an undirected graph is defined in the usual way, by gluing these vertices. Formally, let the undirected graph B ′ denote the result of merging nodes v 1 and v 2 in B. The set of vertices of

B ′ is V B ′ def = (V B \ {v 1 , v 2 }) ∪ {v 12 }
, where v 12 is a new vertex. Let m : V B → V B ′ be defined as follows:

m(v) =      v 12 if v = v 1 or v = v 2 v otherwise
If there is an edge e between the vertices v 1 and v 2 in B then there is an edge m(e) between m(v 1 ) and m(v 2 ) in B. If there is an edge e between v ′ 1 and v ′ 2 in B ′ then there exist vertices

v 1 and v 2 in B such that m(v 1 ) = v ′ 1 , m(v 2 ) = v ′ 2 ,
and there is an edge between v 1 and v 2 in B. Proof: By definition of T k , there exists a set of edges D ⊆ E such that B \ D, denoted by T , is acyclic and |D| ≤ k. We show how to transform D into D ′ ⊆ E ′ such that B ′ \ D ′ , denoted by T ′ , is acyclic and |D ′ | ≤ k. We consider only the case when v 1 and v 2 are at distance of exactly two in B, i.e., there is a vertex v 0 distinct form v 1 and v 2 , an edge e 1 between v 1 and v 0 , and an edge e 2 between v 0 and v 1 . We consider three cases, depicted in Fig. 7.

• If e 1 , e 2 / ∈ D, let D ′ = {m(e)|e ∈ D}. • Assume that e 1 / ∈ D and e 2 ∈ D. If v 2 is not reachable from v 1 in T , let D ′ = {m(e)|e ∈ D}, thus |D ′ | ≤ k.
If v 2 is reachable from v 1 in T , there is at most one (simple) path from v 1 to v 2 in T , because T is acyclic. If the path contains e 1 , we define D ′ as before:

D ′ = {m(e)|e ∈ D}.
If the path from v 1 to v 2 does not contain e 1 , let e 3 be the first edge on the path from v 1 to v 2 (see the second case in Fig. 7). 8 To obtain D ′ from D, we remove If v 2 is reachable from v 1 , let e 3 be the first edge on the path. We define D ′ = {m(e)|e ∈ D} ∪ {m(e 3 )} (see the third case in Fig. 7). Same construction applies when v 1 or v 2 are reachable from v 0 .

Ayah Graphs

In this section we prove that A k is closed under edge-addition operations at distance at most one (Lemma 6.2), and under merge operations at distance at most 2 (Lemma 6.3).

The distance between nodes v 1 and v 2 in a graph S is the distance between v 1 and v 2 in G(S), i.e., the number of edges on the shortest path between v 1 and v 2 in G(S).

It is easy to see that A k is closed under edge-addition operations at distance at most one, which means adding an edge in parallel to an existing one (distance one) or adding a self-loop (distance zero). Proof: Distance at most 1 between v 1 and v 2 means that there is already an edge between v 1 and v 2 . Addition of edges to S in parallel to existing edges does not affect the G(S), and self-loops do not affect T k .

Merging two nodes in a graph is defined in the usual way by gluing these nodes. Formally, let S ′ be the result of merging the nodes v 1 and v 2 in S. The set of nodes of

S ′ is V S ′ def = (V S \ {v 1 , v 2 }) ∪ {v 12 }
, where v 12 is a new node. We define m : V S → V S ′ as follows:

m(v) =      v 12 if v = v 1 or v = v 2 v otherwise
The interpretation of constant and relation symbols in S ′ is defined as follows:

(1) For every constant symbol c ∈ τ , and for every node v ∈ S, v is labeled with c in S if and only if m(v) is labeled with c in S ′ . (2) For every unary relation symbol σ ∈ τ , and for every node v ∈ S, if v is labeled with σ in S then m(v) is labeled with σ in S ′ . (3) For every unary relation symbol σ ∈ τ , and for every node v ′ ∈ S ′ , if v ′ is labeled with σ in S ′ then there exists a node v in S such that m(v) = v ′ and v is labeled with σ in S. (4) For every binary relation symbol σ ∈ τ , and every pair of nodes w 1 , w 2 ∈ S, if there is an edge from w 1 to w 2 labeled with σ then there is an edge from m(w 1 ) to m(w 2 ) in S ′ labeled with σ. (5) for every binary relation symbol σ ∈ τ , and every pair of nodes w ′ 1 , w ′ 2 ∈ S ′ , if there is an edge from w ′ 1 to w ′ 2 labeled with σ in S ′ then there are nodes w 1 and w 2 in S such that m(w 1 ) = w ′ 1 , m(w 2 ) = w ′ 2 , and there is an edge from w 1 to w 2 in S labeled with σ.

Later, we guarantee that merge operations are applied only to those nodes which are labeled by the same unary relations and constants.

The proof that A k is closed under merge operations at distance at most two is based on the result of Lemma 6.1 from the previous section.

Lemma 6.3 (Merging nodes at distance

≤ 2 in A k ) Assume that the graph S ′ is obtained from S by merging v 1 and v 2 in S. If S is in A k and nodes v 1 and v 2 are at distance at most 2 in S, then S ′ is in A k .
Proof: To show that S ′ ∈ A k , it is sufficient to show that G(S ′ ) ∈ T k . We use the definitions of a Gaifman graph and a merging operation. First, merging the nodes of G(S) that correspond to v 1 and v 2 in G(S), results in G(S ′ ). Second, the distance between v 1 and v 2 in G(S) is at most 2 because the distance between the corresponding nodes in S is at most 2. Third, G(S) ∈ T k , because S ∈ A k . Thus, using Lemma 6.1, we get that G(S ′ ) ∈ T k .

Graph Operations Enabled by L 1 Formulas

The notion of enabled operations defined in this section is used for defining the construction in the proof of Theorem 5.14.

Let p(v 0 ) def = N (v 0 , . . . , v n ) ⇒ ψ(v 0 , . . . , v n ) be an L 1 pattern.
Let S be a graph, and w 1 , w 2 nodes in S.

We say that merge operation of w 1 and w 2 is enabled (by c[R]p) when (a) the equality between variables (v 1 = v 2 ) appears positively in ψ, (b) we can assign nodes w 0 , . . . , w n to v 0 , . . . , v n , respectively, such that there is an R-path from c to w 0 , N (w 0 , . . . , w n ) holds but ψ(w 0 , . . . , w n ) does not hold, and (b) w 1 and w 2 are distinct nodes. Merging the nodes w 1 and w 2 disables this merge operation (other merge operations may still be enabled after merging w 1 and w 2 ).

We say that edge-addition between w 1 and w 2 is enabled (by c[R]p) when (a) the edge formula (v 1 f → v 2 ) appears positively in ψ, (b) we can assign nodes w 0 , . . . , w n to v 0 , . . . , v n , respectively, such that there is an R-path from c to w 0 , N (w 0 , . . . , w n ) holds but ψ(w 0 , . . . , w n ) does not hold, and (c) there is no f -edge from w 1 to w 2 . We can add an f -edge from w 1 and w 2 to discharge this assignment. Lemma 6. [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF] Let N (v 0 , . . . , v n ) be a neighborhood formula, and S be a graph with an assignment to v 0 , . . . , v n that satisfies N . If the variables v 1 and v 2 are at distance at most k in N , then the nodes assigned to v 1 and v 2 are at distance at most k in S.

Proof: Follows from the definition of neighborhood as a conjunction of edges (Def. 2.2).

The following lemma is the key observation of the proof.

Lemma 6.5 Let p(v 0 ) def = N (v 0 , v 1 , . . . , v n ) ⇒ ψ(v 0 , . . . , v n ) be an L 1 pattern.
Let S be a graph, and w 1 , w 2 nodes in S. Assume that a merge (an edge-addition) operation is enabled in a graph S between nodes w 1 and w 2 by a reachability constraint c[R]p. If S ∈ A k , then the result of merging (adding an edge) between w 1 and w 2 is a graph in A k .

Proof: Suppose that a merge operation is enabled in S between nodes w 1 and w 2 . It is possible to assign nodes w 0 , . . . , w n to the variables v 0 , . . . , v n , such that N holds. In particular, w 1 is assigned to v 1 and w 2 is assigned to v 2 , and the equality v 1 = v 2 appears positively in ψ. According to the equality restriction on L 1 patterns, v 1 and v 2 are at distance at most 2 in N . By Lemma 6.4, w 1 and w 2 are at distance at most 2 in S. Thus, by Lemma 6.3 we get that the result of merging w 1 and w 2 is a graph in A k , because S is in A k . The proof for edge-addition is similar, using Lemma 6.2.

Homomorphism Preservation

In this section, we give a slightly non-standard definition of homomorphism between graphs. It preserves existence of edges and both existence and absence of labels on nodes (preserving absence of labels is non-standard). The homomorphism relation is preserved by CL 1 formulas, and also by merging operations. Definition 6.6 (Homomorphism) Let S 1 and S 2 be graphs over the same vocabulary τ . A homomorphism from S 1 to S 2 is a mapping h : V S 1 → V S 2 such that [START_REF] Areces | Hybrid logics: characterization, interpolation and complexity[END_REF]

Sketch of Proof:

If S 1 |= c 1 R c 2 ,
there exists an R-path from c 1 to c 2 . By definition of homomorphism from S 1 to S 2 , the same path exists in S 2 . Thus,

S 2 |= c 1 R c 2 .
For the sake of contradiction, assume that

S 2 |= c[R]p but S 1 |= c[R]p.
That is, there exists an R-path from c to some node v in S 1 and v does not satisfy the pattern p. The same path exists in S 2 , due to the homomorphism from S 1 to S 2 . To obtain a contradiction, we show that h(v) does not satisfy the pattern p in S 2 . The formula p is of the form N ⇒ ψ, where N contains only positive occurrences of edge formulas. By assumption, we get that ψ does not contain positive occurrences of edge formulas or equality formulas. Thus, the formula p does not contain positive occurrences of edge formulas and equality formulas. If S 1 does not satisfy p, there exists a subgraph in S 2 which satisfies ¬p. This subgraph exists in S 2 as well, due to homomorphism.9 Thus, S 2 satisfies ¬p, and a contradiction is obtained.

Lemma 6.8 Assume that f is a homomorphism from S 1 to S, and S 2 is obtained by merging the nodes

v 1 and v 2 in S 1 . If f (v 1 ) = f (v 2 )
then there is a homomorphism from S 2 to S.

Witness Splitting

A witness W for c 1 R c 2 in a graph S, is a path in S, labeled with a word w ∈ L(R), from the node labeled with c 1 to the node labeled with c 2 . Note that the nodes and edges on a witness path for R need not be distinct. S contains a witness for

c 1 R c 2 if and only if S |= c 1 R c 2 .
Using a witness W for c 1 R c 2 in S, we construct a graph W ′ that consists of a path, also labeled with w, that starts at the node labeled by c 1 and ends at the node labeled by c 2 . Intuitively, we create W ′ by duplicating a node of S each time the witness path W traverses it, unless the node is labeled with a constant. The nodes in W ′ are named t v,l where v is a node in S and l ≥ 0 is an integer. For l > 0, a node t v,l in W ′ corresponds to the l-th occurrence of v on the witness path W , if a node v in S is not labeled with a constant. If v is labeled with a constant, we create for it S S 0 S 1 Fig. 8. The graph S satisfies the formula in ( 5), and S ∈ A 1 . A pre-model of S is S 0 . Note that S 0 ∈ A 0 . The graph S 1 is the result of applying a merge operation to S 0 . Note that S 1 satisfies the formula in ( 5), and S 1 ∈ A 0 . The graph S 1 is the final result of the construction used in the proof of Theorem 5.14.

a unique node t v,0 in W ′ even if v is traversed several times by W . As a result, all shared nodes in W ′ are labeled with constants. Also, every cycle contains a node labeled with a constant. By construction, W ′ satisfies c 1 R c 2 .

For example, consider the formula

ϕ def = x f → * z ∧ y f → .( g → + .(c|u). f → ) * z ∧ c[ǫ]uns f ( 5
)
where u is a unary relation symbol and c is a constant symbol. Fig. 8 shows a graph S which satisfies ϕ. The shortest witness path for x f → * z is labeled with the word

f → . f → . f → . The shortest witness path for y f → .( g → + .(c|u). f → ) * z is labeled with the word f → . g → . g → . g → .u. f → . g → .c. f → .
Note that this witness traverses each of the nodes labeled by u and by c twice. To split this witness, the node marked by u is duplicated, while the node marked by c is not duplicated, because c is a constant. After splitting the witnesses, we construct a pre-model of S, denoted by S 0 , by taking the union of both witness paths and merging the nodes of the different witness paths which are labeled with the same constant.

Formally, the witness path W is a sequence of nodes from S: t 1 , t 2 , . . . , t r , where t i ∈ S. Let C(t i ) denote the set of constant symbols that label the node t: C(t i ) def = {σ ∈ C|C S (σ) = t i }. We define a mapping d(t i ) as follows: We say that W ′ is the result of splitting the witness W . We say that W is the shortest witness for c 1 R c 2 if any other witness path for c 1 R c 2 is at least as long as W .

d(t i ) def =      t v,0 if C(t i ) = ∅
For a formula ϕ ∈ CL 1 and a graph S such that S |= ϕ, we define a pre-model of a S and ϕ to be the graph S 0 constructed as follows.

• Let W i denote a shortest witness in S for every

c i R c ′ i in ϕ ✸ . • Let W ′
i be the result of splitting the witness W i . Let t i v,l be the names the nodes of

W ′ i . • Let S ′ 0 be a disjoint union of all W i 's. • For every c ∈ C, if S ′
0 does not contain any node labeled with c, add a new node t 0 v,0 to S ′ 0 , where v is the node in S labeled with c. For all σ ∈ C ∪ U , t 0 v,0 is labeled with σ in S ′ 0 if and only if v is labeled with σ in S. • The graph S 0 is the result of merging all nodes that are labeled with the same constants, i.e., nodes t i v,0 for all i are merged and the new node named t 0 v,0 .

Note that S ′ 0 cannot be used as a legal interpretation for L 0 formulas over τ , because it may contain several nodes labeled with the same constant, or no interpretation for some constants. These problems are addressed by the last two steps of the construction.

By construction, S 0 contains a witness for each c 1 R c 2 in ϕ ✸ . Lemma 6.9 If S |= ϕ and S 0 is a pre-model of S and ϕ, then S 0 |= ϕ ✸ . Lemma 6.10 Let S 0 be a pre-model of S and ϕ. There is a homomorphism h 0 : S 0 → S defined by h 0 (t i v,l ) = v.

Proof: We define h ′ 0 : S ′ 0 → S by h ′ 0 (t i v,l ) = v.
The mapping h ′ 0 preserves existence of edges and the presence and absence of node labels between S ′ 0 and S because it is preserved for every W ′ separately, by definition of witness splitting, and

S ′ 0 is a disjoint union of W ′ i s. Thus, h ′ 0 is a homomorphism.
Because S 0 is obtained from S ′ 0 by merging nodes that are mapped by h ′ 0 to the same node in S, the mapping h 0 is also a homomorphism, by Lemma 6.8.

Lemma 6.11

For ϕ ∈ CL 1 , if S 0 is a pre-model of S and ϕ, then S 0 ∈ A f (ϕ) , where f is defined in [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF].

Proof:

Recall that for every routing expression that appears in ϕ ✸ there is an equivalent automaton with at most n states. If a node is visited more than once in the same state of the automaton, the path can be shortened by removing the part traversed between the two visits. Thus, a shortest witness visits a node at most n times. In the worst case, each time a shortest witness visits a node, it enters and exits the node with a different edge. Because S 0 consists of |ϕ ✸ | shortest witnesses, there are at most 2 × n × |ϕ ✸ | edges adjacent to any node.

In fact, by construction of S 0 , only nodes labeled by constants in S 0 can have more than two adjacent edges. Thus, every (simple) cycle in S 0 must go through a constant. To break all cycles in S 0 (and, thus, in its Gaifman graph), it is sufficient to remove all the edges adjacent to nodes labeled with constants, i.e., at most

k = 2 × n × |ϕ ✸ | × |C| edges. It follows that S 0 ∈ A k . 10 6.6 A k -Model Property of L 1 Theorem 5.14(Ayah model property of L 1 ) If ϕ ∈ CL 1 is satisfiable, then ϕ is satisfiable by a graph in A f (ϕ)
, where f is defined in [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF].

Proof: Given a graph S such that S |= ϕ, we construct a graph S ′ and show that S ′ ∈ A k and S ′ |= ϕ.

First, we construct a pre-model S 0 of S and ϕ, and define the mapping h 0 : S 0 → S according to Lemma 6.10. Then, we apply all enabled merge operations and all enabled edge-addition operations in any order, producing a sequence of distinct graphs S 0 , S 1 , . . . , S r , until S r has no enabled operations. The result S ′ = S r .

Formally, for every c[R]p ∈ ϕ and ever pair of nodes w 1 , w 2 ∈ S j ,

• If a merge operation is enabled, and h j (w 1 ) = h j (w 2 ) in S j then construct S j+1 by merging w 1 and w 2 , and define h j+1 : S j+1 → S to be h j+1 (w) = h j (w 1 ) if w is the result of merging w 1 and w 2 , otherwise h j+1 (w) = h j (w). • If an edge-addition operation is enabled for f ∈ F , and there is an f -edge from h i (w 1 ) to h j (w 2 ) in S j then construct S j+1 by adding an f -edge from w 1 to w 2 , and define h j+1 : S j+1 → S to be the same as h j .

For example, the pre-model S 0 shown in Fig. 8 does not satisfy the constraint c[ǫ]uns f from (5), which requires that the node labeled with c have at most one incoming f -edge. The result of applying the corresponding merge operation is the structure S 1 , also shown in Fig. 8.

An enabled merge operation is not applied to S j if the corresponding nodes in the original model S are distinct. Similarly, an enabled edge-addition is not applied, unless the corresponding edge is present in S. This allows us to deal with disjunctions in patterns. For example,

let p(v 0 ) def = (v 0 f → v 1 ) ⇒ (v 0 = v 1 ∨ (v 0 g → v 1 ) ∨ (v 0 g ′ → v 1 )) in c f → * c ′ ∧ c[ f → * ]p ∧ (c = c ′ )
Suppose that S 0 looks like this: ?>=< 89:; w 1 f / / ?>=< 89:; w 2 c c ′

The nodes w 1 and w 2 are labeled with the constants c and c ′ , respectively. Both merge and edge-addition operations are enabled in S 0 by c[ f → * ]p. Had we applied the merge operation, we would have immediately obtained a contradiction with c = c ′ . However, if we consult the original model, we find out that the corresponding nodes are distinct, 11 but there is a g-edge between them. Therefore, adding a g-edge to S 0 would not lead to a contradiction.

Remark. Even when we consult with S whether to apply an enabled operation or not, we do not merge more than necessary, or add more edges than necessary.

In the previous example, after adding g the formula holds, i.e., the edge-addition operation of g ′ is not enabled any more. However, a different order of application of the enable operations may produce different graphs at the end. Fortunately, it does not affect the size of A k , or the decidability.

The process described above terminates after a finite number of steps, because in each step either the number of nodes in the graph is decreased (by merge operations) or the number of edges is increased (by edge-addition operations). For a fixed vocabulary and a fixed number of nodes, the number of edges that can be added to the graph is bounded, because a pair of nodes in a graph can have at most one f edge in each direction, for every f ∈ F .

To show that S ′ ∈ A k , we prove a stronger claim that for all j, S j ∈ A k . In particular, it follows that S ′ ∈ A k . Recall that all operations applied in the process above are enabled by L 1 patterns. The key observation of the proof is that A k is closed under all operations enabled by L 1 patterns (Lemma 6.5). This is the only place in our proof where we use the distance restriction of L 1 patterns. The proof proceeds by induction on the process described above. Initially, S 0 is in A k , by Lemma 6.11. By inductive hypothesis, S j ∈ A k . Because S j+1 is obtained from S j by an operation that is enabled by an L 1 pattern, we get that S j+1 ∈ A k , using Lemma 6.5.

To show that S ′ |= ϕ, we observe that the graphs generated by the process above are related to each other by different homomorphism relations (Def. 6.6), as depicted in Fig. 9.

First, each step of the process can be seen as a transformation t j from S j-1 to S j , which is defined by an operation applied at step j. That is, t j is either a merge operation or an edge-addition operation. It is easy to see that both operations are homomorphisms. Therefore, each t j is a homomorphism, for all j.

Second, we define a mapping f j from S 0 to S j as a composition t j • . . . • t 0 ; the mapping f j is a homomorphism, because it is a composition of homomorphisms. Initially, S 0 |= ϕ ✸ , according to Lemma 6.9. For all S j , from the existence of a homomorphism f j from S 0 to S j we get that S j |= ϕ ✸ , by Lemma 6.7. In particular, S ′ |= ϕ ✸ .

Third, we show that for all j, h j defined by the process above is a homomorphism. Initially, h 0 : S 0 → S is a homomorphism, according to Lemma 6.10. If t j is merge operation of w 1 and w 2 , then the process applies this operation only if h j (w 1 ) = h j (w 2 ). From the inductive hypothesis that h j is a homomorphism, we get that h j+1 is a homomorphism, by Lemma 6.8.

For every c[R]p ∈ ϕ ✷ , if p does not contain positive occurrences of edge formulas or equality formulas, then by Lemma 6.7 and the existence of a homomorphism h r from

S ′ to S, S ′ |= c[R]p, because S |= c[R]p.
For the sake of contradiction, assume that the process terminates, but

S ′ |= c[R]p, where p(v 0 ) def = N (v 0 , . . . , v n ) ⇒ ψ(v 0 , . . . , v n ).
That is, we can assign nodes w 0 , . . . , w n to v 0 , . . . , v n , respectively, such that there is an R-path from c to w 0 , N (w 0 , . . . , w n ) holds but ψ(w 0 , . . . , w n ) does not hold. Consider the assignment h r (w 0 ), . . . , h r (w n ) in S. Because homomorphism preserves existences of paths and edges, there is an R-path from c to h r (w 0 ), and N (h r (w 0 ), . . . , h r (w n )) holds. Because S |= c[R]p, we know that ψ(w 0 , . . . , w n ) holds. Therefore, there is an atomic formula θ that appears positively in ψ and evaluates to f alse in S ′ and to true in S.

If θ is an equality formula v 1 = v 2 , then the merge operation of w 1 and w 2 in S ′ is enabled (because θ is f alse in S ′ ), and h(w 1 ) = h(w 2 ) in S (because θ is true in S), contradiction to the assumption that the process terminated. Similarly, if θ is an edge formula v 1 f → v 2 , then the edge-addition operation of w 1 and w 2 in S ′ is enabled (because θ is f alse in S ′ ), and there is an f -edge from h(w 1 ) to h(w 2 ) in S (because θ is true in S), contradiction to the assumption that the process terminated. Thus, S ′ |= ϕ ✷ .

Decidability of L 2

In this section, we show how to modify the proof of decidability of L 1 , to prove the decidability of L 2 .

We start by explaining why the proof of Theorem 5.14 does not go through for L 2 . Recall that if a graph is in A k , and an operation that is enabled by an L 1 reachability constraint is applied, then the result is in A k , due to the distance restrictions in L 1 patterns (see Lemma 6.5). In L 2 , this nice property no longer holds.

For example, consider the L 2 constraint

let p(v 0 ) def = (v 0 f → v 1 ) ⇒ (v 1 g → c) in c[ f → * ]p
Given k, we construct a graph G k that consists of an f -path of k + 3 disjoint nodes, but only k + 1 nodes on the path have a g-edge back to c. Fig. 10 shows G 4 . The graph G k is in A k , but violates the reachability constraint above. Thus, it has an edge-addition operation enabled for adding a g-edge between the first and the last nodes. It is easy to see that after adding the edge, we get a graph G ′ k that is not in A k . 12If the construction of Theorem 5.14 is applied to an L 2 formula, it might generate a graph in which the number of extra edges is proportional to the number of nodes, due to the use of constants in patterns, and not bounded by the size of the formula. The good news is that the extra edges have one of the endpoints labeled with a constant, except, possibly a small number of them. The proof of decidability of L 2 is based on the fact that the extra edges have one of its endpoints labeled with a constant.

We define a graph operation rem that removes all edges to and from nodes labeled with constants. Formally, the result of rem(S) is a graph S ′ with the same set of nodes as S, such that there is an f -edge from v 1 to v 2 in S ′ if and only if there is an f -edge from v 1 to v 2 in S and the nodes v 1 and v 2 are not labeled by any constants in S. A rem k is the set of graphs on which rem yields a graph in A k , i.e.,

A rem k def = {S | rem(S) ∈ A k }. 7.1 A rem k -Model Property of L 2
We define graph operations enabled by L 2 formulas (similarly to Section 6.3), and prove that A rem k is closed under those operations (similarly to Lemma 6.5).

Let p(v 0 ) def = N (v 0 , . . . , v n ) ⇒ ψ(v 0 , . . . , v n ) be an L 2 pattern. Let S be a graph, w 1 be a node in S, and c 2 ∈ C.

We say that edge-addition between w 1 and c 2 is enabled

(by c[R]p) when (a) (v 1 f → c 2 ) (resp. (c 2 f → v 1 )
) appears positively in ψ, (b) we can assign nodes w 0 , . . . , w n to v 0 , . . . , v n , respectively, such that there is an R-path from c to w 0 , N (w 0 , . . . , w n ) holds, but ψ(w 0 , . . . , w n ) does not hold, and (c) there is no f -edge from w 1 to the node labeled with c 2 in S (resp. to w 1 from the node labeled with c 2 ). Proof: For graph operations that do not involve constants, the result follows directly from Lemma 6.5.

Assume that S ∈ A rem k . Suppose that an edge-addition operation between a node w 1 and c 2 is enabled in a graph S. The graph S ′ is the result of adding the edge between w 1 and the constant c. In this case, rem(S) and G(S ′ ) is the same graph. Thus, S ∈ A rem k .

Remark. We can show that A rem k is closed under merge operations enabled by a pattern with v 1 = c. However, this situation never occurs in the construction used in Theorem 5.14, because we do not split nodes that are labeled with constants, when we create a pre-model.

The following theorem shows that L 2 has A rem k -property, i.e., every satisfiable L 2 formula has a model in A rem k . The proof is similar to the proof of Theorem 5.14, except the use of Lemma 7.1 to show that the result S ′ ∈ A rem k .

Theorem 7.2 (A rem k -Model Property) If ϕ ∈ L 2 is satisfiable, then there exists a graph S such that S |= ϕ and S ∈ A rem k , where k = f (ϕ) and f is defined in (4).

MSO is decidable on A rem k

In this section, we show a reduction from the satisfiability problem of MSO logic on A rem k to the satisfiability of MSO on A k , which is decidable by Theorem 5.8. This reduction completes the proof of decidability of L 2 .

Lemma 7.3

There is a translation T R 5 between MSO-formulas such that for every MSO-formula ϕ, there exists a graph S ∈ A rem k such that S |= ϕ if and only if there exists a graph S ′ ∈ A k such that S ′ |= T R 5 (ϕ).

Given the vocabulary τ = C, U, F and a number k we define a new vocabulary τ ′ = C, U ′ , F , where

U ′ = U ∪ {F c f , B c f |f ∈ F, c ∈ C}.
For an MSO formula ϕ over τ , T R 5 (ϕ) is an MSO formula over the vocabulary τ ′ . The translation T R 5 is defined inductively on ϕ, as usual. For a binary relation formula f ∈ F , we define:

T R 5 (f (v 1 , v 2 )) = (E(v 1 , v 2 ) ∧ F f (v 2 )) ∨ (E(v 2 , v 1 ) ∧ B f (v 1 )) c∈C∪{d 1 ,...,d k } (c = v 1 ∧ F c f (v 2 )) ∨ (c = v 2 ∧ B c f (v 1 ))
Intuitively, a tree node v is labeled with F c f if and only if there is an f -edge from v to the node labeled by c in the corresponding Ayah graph. A tree node v is labeled with B c f if and only if there is an f -edge to v from the node labeled by c in the corresponding Ayah graph. This allows us to encode both the direction and the label of the extra edges.

Remark. We have chosen a simple encoding that is not parsimonious in the number of additional unary relations. For example, if an edge has two constants on its adjacent nodes, it can be encoded in more than one way. This ambiguity can be resolved using ordering between constants, but we ignore it here, to simplify the presentation.

Theorem 7. [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF] The satisfiability problem of MSO formulas is decidable on A rem k .

Proof: Follows from Lemma 7.3 and Theorem 5.8.

Theorem 7.5

The satisfiability problem of L 2 is decidable.

Proof: Follows from combining Theorem 5.12, Theorem 7.2, Lemma 5.2, and Theorem 7.4.

Complexity

In Section 5, we proved decidability by reduction to MSO on trees, which allows us to check satisfiability of L 1 formulas using MONA decision procedure [START_REF] Henriksen | Mona: Monadic second-order logic in practice[END_REF]. Alternatively, we can directly construct a tree automaton from an L 1 formula, and can then check emptiness of the automaton, which yields a double-exponential procedure. 13However, a naive translation of L 1 formulas to automata does not yield a practical decision procedure. First, the size of the automaton is exponential in the input vocabulary, regardless of the complexity of the input formula. Second, a naive translation produces two-way alternating tree automata. To the best of our knowledge, there are no tools that can check emptiness of such automata. A translation from two-way alternating tree automata to tree automata that can be handled by existing tools, such as MONA [START_REF] Henriksen | Mona: Monadic second-order logic in practice[END_REF], Timbuk [START_REF] Genet | Reachability analysis of term rewriting systems with timbuk[END_REF], or H1 [START_REF] Nielson | Normalizable horn clauses, strongly recognizable relations, and spi[END_REF], is at least exponential.

We are investigating tableaux-based techniques to implement a decision procedure for validity, satisfiability, and model generation for L 1 . A tableaux-based decision procedure can be adaptive to specific formulas, and the formulas that come up in practice are quite simple.

The worst case complexity of the satisfiability problem of L 1 formulas is at least NEXPTIME (Section 8.1), but it remains elementary (in contrast to MSO on trees, which is non-elementary [START_REF] Meyer | Weak monadic second-order theory of successor is not elementary recursive[END_REF]). The complexity depends on the bound k of A k models, according to Theorem 5.14. Proof: Let T be a tiling problem as in Def. 3.1, and let n be a natural number. We define a formula ϕ n that exactly expresses a solution to the tiling problem. When ϕ n is satisfiable, it has a minimal model of size 2 Ω(n) .

We use two constants: s, denoting the top left node of the grid, and t, denoting the bottom right node of the grid. The desired model will consist of 2 2n tiles:

s = [1, 1, t 0 ] • • • [1, 2 n , t] [2, 1, t ′ ] • • • [2, 2 n , t ′′ ] . . . . . . [2 n , 1, t ′′′ ] • • • [2 n , 2 n , t k ] = t
The binary relation n holds between each pair of consecutive tiles, including, for example, [1, 2 The formula ϕ n is the conjunction of the following assertions.

There is a path from s to t:

s n → * t (6)
All E edges reachable from s are deterministic and unshared:

s[ n → * ]det n ∧ uns n (7)
The node labeled with s is the first tile, has tile type t 0 , and the node labeled with t is the last tile and has tile type t k :

T 0 (s) ∧ n i=1 (¬H i (s) ∧ ¬V i (s)) ∧ T k (t) ∧ n i=1 (H i (t) ∧ V i (t)) (8)
We have chosen for simplicity to encode the tile types in unary so we need to say that tile types are mutually exclusive and every node has a tile:

s[ n → * ]   0≤i<j≤k ¬(T i ∧ T j )   ∧   0≤i≤k T i   (9)
The arrangement of tiles honors T 's horizontal and vertical adjacency requirements:

let p(v) def = Next h (v, v ′ ) ⇒ Hor(v, v ′ ) in s[ n → * ]p (10) let p(v) def = Next v (v, v ′ ) ⇒ Vert(v, v ′ ) in s[ n → * ]p (11)
The abbreviation Next v , Next h , Vert, Horz, and Next denote formulas which contain only unary relation symbols and variables, and no equality. We rely on the fact that a neighborhood of a pattern need not be connected.

The abbreviation Next h (x, y) means that x and y have the same vertical position and y's horizontal position is one more than that of x. Next v (x, y) means that x and y have the same horizontal position and y's vertical position is one more than that of x.

Next h (x, y) ≡ n i=1 V i (x) ↔ V i (y) ∧ PlusOne h (x, y) Next v (x, y) ≡ n i=1 H i (x) ↔ H i (y) ∧ PlusOne v (x, y)
The abbreviations PlusOne h (x, y) and PlusOne v (x, y) are nearly identical. Thus, we restrict our attention to PlusOne h (x, y), which means that the horizontal position of y is one greater than the horizontal position of x. (Our convention is that the bit positions are numbered 1 to n, with 1 being the high-order bit, and n the low-order bit.) PlusOne h (x, y) can be written as follows:

PlusOne h (x, y) ≡ n i=1 [ j>i (H j (x) ∧ ¬H j (y)) ∧ (¬H i (x) ∧ H i (y)) ∧ j<i (H j (x) ↔ H j (y))]
The length of the formula PlusOne h (x, y) is O(n 2 ).

The abbreviation Hor(x, y) (resp. Vert(x, y)) is a disjunction over the tile types asserting that the tiles in positions x and y are horizontally (resp. vertically), compatible. For example, Hor(x, y) ≡ R(t i ,t j )

(T i (x) ∧ T j (y)) (12)
The abbreviation Next(x, y) means Next h (x, y) or x has horizontal position 2 n , y has horizontal position 1, and y's vertical position is one more than that of x:

Next(x, y) ≡ Next h (x, y) ( n i=1 H i (x)) ∧ ( n-1 i=1 ¬H i (y)) ∧ H n (y) ∧ PlusOne v (x, y)
Finally, if there is an edge from x to y, then there N ext(x, y) holds:

let p(v) def = v n → v ′ ⇒ Next(v, v ′ ) in s[ n → * ]p (13)
Remark. The length of the formula ϕ n described above is O(n 2 ). The only difficulty in keeping ϕ n to total size O(n) is in writing the formulas PlusOne h (x, y) and PlusOne v (x, y). We can decrease the size by keeping track of the position i using 2n addition unary relation symbols, similarly to the proof of [START_REF] Immerman | The boundery between decidability and undecidability of transitive closure logics[END_REF]Lemma 14].

Limitations and Further Extensions

Despite the fact that L 2 is useful, there are interesting program properties that cannot be expressed directly. For example, transitivity of a binary relation, that can be used, e.g., to express partial orders, is naturally expressible in L 0 , but not in L 2 .

There are of course interesting properties that are beyond L 0 , such as the property that a general graph is a tree in which every leaf has a pointer to the root of a tree.

In the future, we plan to generalize L 2 while maintaining decidability, perhaps beyond L 0 . We are encouraged by the fact that the proof of decidability in Section 5 holds "as is" for many useful extensions. For example, more complex patterns can be used, as long as they do not violate the A k -model property.

The Logic L 3

In the L 0 logic, reachability constraints describe paths that start from nodes labeled by some constant. The requirement that a path start with a constant is not necessary for decidability. We define L 3 that generalizes L 0 with paths that start from any node that satisfies a quantifier-free positive formula θ: θ[R]p def = ∀w 0 , . . . , w m , v 0 , . . . , v n .R(w 0 , v 0 ) ∧ θ(w 0 , . . . , w m ) ⇒ p(v 0 , . . . , v n )

A simple and very useful fragment of L 3 is L 4 in which θ is fixed to be true. We use [R]p to denote true[R]p. For example, we can specify that all f -edges in the graph are deterministic, and not only those reachable from some constant: [ǫ]det f .

The fragment L 3 provides several ways to express the same property; this flexibility can be useful when writing specifications manually. For example, the formula

(x ∨ y)[R]p in L 3 is equivalent to x[R]p∨y[R]p in L 1 , and to [x + y.R]p in L 4 . The formula (x ∧ y)[R]p in L 3 is equivalent to (x = y) ⇒ x[R]p in L 1 and to [x.y.R]p in L 4 .
We can translate every L 0 formula to L 4 using constants in routing expressions:

x[R]p ∈ L 0 is translated into [x.R]p.
We can show that L 3 has a finite model property. The logic LRP that results from L 3 by restricting it to L 2 patterns is decidable.

For example, recall the mark procedure from Section 4. We can modify it to scan the heap from a set of roots, instead of a single root. To write specifications for the modified version of mark, we can model the set of root objects using a unary relation root, instead of the constant symbol with the same name, which is used in Section 4. The rest of the specification remains unchanged. The resulting formulas are in LRP.

The Logic UL 1

We can extend L 1 with (a possibly restricted use of) quantifiers, going beyond the proposition logic L 0 . This extension provides a more general way to write specifications. In fact, the auxiliary constants used in the specification of append and mark procedures in Section 4, can be thought of as universally quantified variables.

We extend L 1 with universal quantification over constants, as follows. For a vocabulary τ , a formula in UL 1 over τ is a positive boolean combination of formulas of the form ∀c 1 , . . . , c n .ϕ ′ , where ϕ ′ is in L 1 over the vocabulary τ ′ = τ ∪ {c 1 , . . . , c n }). The semantics of the universal quantifiers is defined as usual.

The problem of validity of UL 1 -formulas is decidable by reduction to validity in L 1 .

Lemma 9.1 Let ϕ ∈ UL 1 be of the form ∀c 1 , . . . , c n .ϕ ′ . The formula ϕ is valid if and only if ϕ ′ is valid.

Note that UL 1 is not closed under negation (whereas L 1 is closed under negation).

It is possible to add quantification over sets and relations, while preserving decidability, as long as there are no quantifier alternations. Quantification of binary relations can be useful for writing modular specifications, and analysis that does not violate abstraction layers. For example, if a procedure's formal parameter x is a pointer to an abstract data-type, we can specify that the field of objects that implement the abstract data-type are not modified by the procedure, without exposing the implementation:

∀Σ.∀f, f ′ .x[ Σ → * ]same f,f ′ .

Related Work

There are several works on logic-based frameworks for reasoning about graph/heap structures. We mention here the ones which are, as far as we know, the closest to ours.

The logic L 0 can be seen as a fragment of the first-order logic over graph structures with transitive closure (TC logic [START_REF] Immerman | Languages that capture complexity classes[END_REF]). It is well known that TC is undecidable, and that this fact holds even when transitive closure is added to simple fragments of FO such as the decidable fragment L 2 of formulas with two variables [START_REF] Mortimer | On languages with two variables[END_REF][START_REF] Graedel | On the decision problem for two variable logic[END_REF][START_REF] Grädel | Undecidability results on two-variable logics[END_REF].

It can be seen that our logics L 0 and L 1 are both uncomparable with L 2 + TC.

Indeed, in L 0 no alternation between universal and existential quantification is allowed. On the other hand, L 1 allows us to express patterns (e.g., heap sharing) that require more than two variables (see Table 1, Section 4).

In [START_REF] Benedikt | A decidable logic for describing linked data structures[END_REF], decidable logic L r (which can also be seen as a fragment of TC) is introduced. The logics L 0 and L 1 generalize L r , which is in fact the fragment of these logics where only two fixed patterns are allowed: equality to a program variable and heap sharing.

In [START_REF] Immerman | The boundery between decidability and undecidability of transitive closure logics[END_REF][START_REF] Balaban | Shape analysis by predicate abstraction[END_REF][START_REF] Lahiri | Verifying properties of well-founded linked lists[END_REF][START_REF] Berdine | A Decidable Fragment of Separation Logic[END_REF] other decidable logics are defined, but their expressive power is rather limited w.r.t. L 1 since they allow at most one binary relation symbol (modelling linked data-structures with 1-selector). For instance, the logic of [START_REF] Immerman | The boundery between decidability and undecidability of transitive closure logics[END_REF] does not allow us to express the reversal of a list. Concerning the class of 1-selector linked data-structures, [START_REF] Bozga | Quantitative Verification of Programs with Lists[END_REF] provides a decision procedure for a logic with reachability constraints and arithmetical constraints on lengths of segments in the structure. It is not clear how the proposed techniques can be generalized to larger classes of graphs.

Other decidable logics [START_REF] Bozga | On logics of aliasing[END_REF][START_REF] Kuncak | Generalized records and spatial conjunction in role logic[END_REF] are restricted in the sharing patterns and the reachability they can describe.

Other works in the literature consider extensions of the first-order logic with fixpoint operators. Such an extension is again undecidable in general but the introduction of the notion of (loosely) guarded quantification allows one to obtain decidable fragments such as µGF (or µLGF ) (Guarded Fragment with least and greater fixpoint operators) [START_REF] Grädel | Guarded Fixed Point Logic[END_REF][START_REF] Grädel | Guarded fixed point logic and the monadic theory of trees[END_REF]. Similarly to our logics, the logic µGF (and also µLGF ) has the tree model property: every satisfiable formula has a model of bounded tree width. However, guarded fixpoint logics are incomparable with L 0 and L 1 . For instance, the L 1 pattern det f that requires determinism of f -field, is not a (loosely) guarded formula.

The PALE system [START_REF] Møller | The pointer assertion logic engine[END_REF] uses an extension of the weak monadic second order logic on trees as a specification language. The considered linked data structures are those that can be defined as graph types [START_REF] Klarlund | Graph Types[END_REF]. Basically, they are graphs that can be defined as trees augmented by a set of edges defined using routing expressions (regular expressions) defining paths in the (undirected structure of the) tree. L 1 allows us to reason naturally about arbitrary graphs without limitation to tree-like structures. By restricting the syntax, we guarantee that satisfiability queries posed over arbitrary graphs can be answered precisely by considering only tree-like graphs. This approach allows us to automate the reasoning about limited but interesting properties of arbitrary graphs.

Moreover, as we show in Section 4, our logical framework allows us to express postconditions and loop invariants that relate the input and the output state. For instance, even in the case of singly-linked lists, our framework allows us to express properties that cannot be expressed in the PALE framework: in the list reversal example of Section 4, we show that the output list is precisely the reversed input list, by expressing the relationships between fields before and after the procedure, whereas in the PALE approach, a postcondition can only express that the output is a list that is a permutation of the input list. In particular, a postcondition that relates fields before and after the procedure involves two binary relations with arbitrary interpretation. This can be easily done in L 0 which supports an arbitrary number of binary relations. This is not supported by PALE, which allows two binary relations with a specific interpretation as tree edges. In the PALE approach, a postcondition can only express that the output is a list that is a permutation of the input list.

In [START_REF] Immerman | Verification via structure simulation[END_REF], we tried to employ a decision procedure for MSO on trees to reason about reachability. However, this places a heavy burden on the specifier to prove that the data-structures in the program can be simulated using trees. The current paper eliminated this burden by defining syntactic restrictions on the formulas and showing a general reduction theorem.

Other approaches in the literature use undecidable formalisms such as [START_REF] Hendren | Abstractions for recursive pointer data structures: Improving the analysis and the transformation of imperative programs[END_REF], which provides a natural and expressive language, but does not allow for automatic property checking.

Separation logic has been introduced recently as a formalism for reasoning about heap structures [START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF]. The general logic is undecidable [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF] but there are few works showing decidable fragments [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF][START_REF] Berdine | A Decidable Fragment of Separation Logic[END_REF]. One of the fragments is propositional separation logic where quantification is forbidden [START_REF] Calcagno | Computability and Complexity Results for a Spatial Assertion Language for Data Structures[END_REF][START_REF] Calcagno | From Separation Logic to First-Order Logic[END_REF] and therefore seems to be incomparable with our logic. The fragment defined in [START_REF] Berdine | A Decidable Fragment of Separation Logic[END_REF] allows one to reason only about singly-linked lists with explicit sharing. In fact, the fragment considered in [START_REF] Berdine | A Decidable Fragment of Separation Logic[END_REF] can be translated to L 1 , and therefore, entailment problems as stated in [START_REF] Berdine | A Decidable Fragment of Separation Logic[END_REF] can be reduced to validity of implications in L 1 .

The logic L 0 integrates features of such prominent formalisms as the modal logics, the classical first-order logic, and the regular expressions. The hybrid logics [START_REF] Areces | Hybrid logics: characterization, interpolation and complexity[END_REF] also combine features of modal and classical logics. The most relevant is the hybrid µ-calculus [START_REF] Sattler | The hybrid -calculus[END_REF] which extends the µ-calculus with the following features: (i) nominals, that correspond to constants in L 1 , (ii) universal program, that corresponds to the fragment L 4 , and (iii) the ability to reasoning about the past, that corresponds to the use of backward edges in routing expressions. The hybrid µ-calculus is incomparable in its expressive power to L 1 : on one hand, it supports a more general reachability via the least and greatest fixpoint operators; on the other hand, the equality is restricted to nominals. For example, it cannot express that a graph is a tree. Unlike L 0 , the hybrid µ-calculus does not have a finite model property. Every satisfiable formula in hybrid µ-calculus has a tree-like model. The complexity of hybrid µ-calculus is EXPTIME-complete, but currently, there is no decision procedure available. Reportedly, a tableaux-based decision procedure for the alternationfree fragment of hybrid µ-calculus is being developed.

L 0 shares some common features with description logics [START_REF] Baader | The Description Logic Handbook: Theory, Implementation, and Applications[END_REF], which is tradition-ally used for knowledge representation, databases, semantic web, with the notable exception of [START_REF] Georgieva | Description logics for shape analysis[END_REF], which shows the description logics can be used for reasoning about data-structures. The basic notions of Description Logics are concepts, that correspond to unary relations in L 0 , and roles, that correspond to binary relations in L 1 . In addition, expressive Description Logics support (iii) nominals, that correspond to constants in L 0 ; quantified role restrictions, that can encode determinism; and inverse roles, that correspond to backward edges in routing expressions. The combination of quantified role restrictions and inverse roles provides a way to express sharing. The need for transitivity and fixpoints arises in many contexts [START_REF] Calvanese | Reasoning in expressive description logics with fixpoints based on automata on infinite trees[END_REF], including, service description logics [START_REF] Bonatti | Towards service description logics[END_REF]. It has been shown that a description logic which combines with nominals, inverse roles, determinism, and least fixpoints is undecidable [START_REF] Bonatti | On the undecidability of logics with converse, nominals, recursion and counting[END_REF]. In light of the negative results, it is interesting to investigate the usefulness of L 1 for specifying web services. There are a variety of efficient reasoning tools for description logics, both tableaux-based and resolution-based, which provide some support for expressive features, such as nominals and inverse roles, e.g., FaCT, Racer. To the best of our knowledge, none of the existing tools supports transitive closure of roles or fixpoints.

Conclusions

Defining decidable fragments of first order logic with transitive closure that are useful for program verification is a difficult task (e.g., [START_REF] Immerman | The boundery between decidability and undecidability of transitive closure logics[END_REF]). In this paper, we demonstrated that this is possible by combining three principles: (i) allowing arbitrary boolean combinations of the reachability constraints, which are closed formulas without quantifier alternations, (ii) defining reachability using regular expressions denoting pointer access paths (not) reaching a certain pattern, and (iii) syntactically limiting the way patterns are formed. Extensions of the patterns that allow larger distances between nodes in the pattern either break our proof of decidability or are directly undecidable.

The decidability result presented in this paper improves the state-of-the-art significantly. In contrast to [START_REF] Immerman | The boundery between decidability and undecidability of transitive closure logics[END_REF][START_REF] Balaban | Shape analysis by predicate abstraction[END_REF][START_REF] Lahiri | Verifying properties of well-founded linked lists[END_REF][START_REF] Berdine | A Decidable Fragment of Separation Logic[END_REF], LRP allows several binary relations. This provides a natural way to (i) specify invariants for data-structures with multiple fields (e.g., trees, doubly-linked lists), (ii) specify post-condition for procedures that mutate pointer fields of data-structures, by expressing the relationships between fields before and after the procedure (e.g., list reversal, which is beyond the scope of PALE), (iii) express verification conditions using a copy of the vocabulary for each program location. Operating on general graphs allows us to verify that the data-structure invariant is reestablished after a sequence of low-level mutations that temporarily violate the invariant data-structure.

We are encouraged by the expressiveness of this simple logic and plan to explore its usage for program verification and abstract interpretation.

Fig. 1 .

 1 Fig. 1. A sketch of a grid model for a tiling problem T . The n-edges are depicted with solid lines, the b-edges are depicted with dashed lines. The filled circles denote nodes labeled with "red".

Definition 4 . 1 (

 41 The syntax of L 1 ) In every reachability constraint c[R]p that appears in L 1 formula, the pattern p(v 0 ) def = N (v 0 , . . . , v n ) ⇒ ψ(v 0 , . . . , v n ) satisfies the following restrictions on ψ:

Fig. 4 .

 4 Fig.4. The append procedure concatenates two singly-linked lists.

Fig. 5 .

 5 Fig. 5. The mark phase of a Mark&Sweep garbage collector.

Fig. 6 .

 6 Fig.6. Examples of graphs in A 0 , A 1 , and A 2 . For j = 0, . . . , 2, S j ∈ A j (left column) and G(S j ) ∈ T j (right column). Dashed edges denote extra edges removing which results in a tree.

Lemma 6 . 1

 61 Assume that B is in T k and vertices v 1 and v 2 are at distance at most two in B. The graph B ′ obtained from B by merging v 1 and v 2 in B is also in T k .

e 2 and add e 3 :

 3 D ′ = ({m(e)|e ∈ D} \ {m(e 2 )}) ∪ {m(e 3 )}. The size of D ′ is the same as the size of D, because e 2 ∈ D. • Assume that e 1 , e 2 ∈ D. If v 2 is not reachable from v 1 , we can use the simple construction D ′ = {m(e)|e ∈ D}. It follows that |D ′ | = |D| -1, because both e 1 and e 2 are mapped to the same edge e ′ = m(e 1 ) = m(e 2 ), and no multiple edges are allowed.

Lemma 6 . 2 (Fig. 7 .

 627 Fig. 7. Merge operation on T k -graphs. Dotted lines represent additional edges, i.e., edges of a T k -graph that do not belong to the tree. The vertex v 12 and the edge e 12 in T ′ result from merging the vertices v 1 and v 2 , and the edges e 1 and e 2 in T .

Fig. 9 .

 9 Fig. 9. Construction and homomorphisms in the proof of decidability.

Fig. 10 .

 10 Fig. 10. The graph G 4 .

Lemma 7 . 1

 71 Assume that a graph operation is enabled in a graph S by an L 2 reachability constraint. If S ∈ A rem k then the result of applying the operation is a graph S ′ ∈ A rem k .

  w 2 and there exists a node s 3 such that there is a path labeled by w 1 from s 1 to s 3 and there exists a path labeled by w 2 from s 3 to s 2 . and for every node tuple s 0 , . . . , s n in G, if there is a path labeled by w from c to s 0 , then the tuple s 0 , . . . , s n , satisfies p with s 0 used as the central node for p. The meaning of Boolean connectives is defined in a standard way. For an edge s 1 , s 2 ∈ G and f ∈ F , we say that s 1 , s 2 is labeled with f , if s 1 , s 2 ∈ E G (f ). In the rest of the paper, graph denotes a directed labeled graph, in which nodes are labeled by constant and unary relation symbols, and edges are labeled by binary relation symbols, as defined above.

A node tuple in G satisfies a pattern p if it satisfies the quantifier-free formula that defines p, according to the usual semantics of the first-order logic over graph structures.

The satisfaction relation |= between a graph G and L 0 formulas is defined similarly to the usual semantics the first-order logic with transitive closure over graphs. A graph G satisfies a formula c[R]p (and we write G |= c[R]p) if and only if for every w ∈ L(R)

We say that node s ∈ G is labeled with σ if σ ∈ C and s = C G (σ) or σ ∈ U and s ∈ U G (σ).

Theorem 2.6 (Finite model property) Every satisfiable L 0 formula is

	arbitrary patterns has a finite model property. If formula ϕ ∈ L 0 has an
	infinite model, each reachability constraint in ϕ that is satisfied by this model has a
	finite witness.
	satisfiable
	by a finite graph.
	Sketch of Proof: We show that L 0 can be translated into a fragment of an infinitary
	logic that has a finite model property. Observe that c[R]p is equivalent to an infinite
	conjunction of universal first-order sentences. Therefore, if G is a model of c[R]p
	then every subgraph of G is also its model. Dually, ¬c[R]p is equivalent to an
	infinite disjunction of existential first-order sentences. Therefore, if G is a model of
	¬c[R]p, then G has a finite subgraph G ′ such that every subgraph of G that contains
	G ′ is a model of ¬c[R]p. It follows that every satisfiable boolean combination of
	formulas of the form c[R]p has a finite model. Thus, L 0 has a finite model property.

Definition 3.1 Define a tiling problem, T

	= T, R, D , to consist of a finite list of
	tile types, T = [t 0 , . . . t k ], together with horizontal and vertical adjacency relations,
	R, D ⊆ T 2 . Here R(a, b) means that tiles of type b fit immediately to the right of
	tiles of type a, and D(a, b) means that tiles of type b fit one step down from those of
	type a. A solution to a tiling problem is an arrangement of instances of the tiles in
	a rectangular grid such that a t 0 tile occurs in the top left node of the grid, and a
	t k tile occurs in the bottom right node of the grid, and all adjacency relationships
	are respected.

Table 2

 2 Properties of data-structures expressed in L 1 .

  To encode the Kleene star expression, we use a least fixpoint operation, expressible in MSO.

Lemma 5.1 Every routing expression R can be translated into an MSO formula tr(R)(v 1 , v 2 ) with two (first-order) free variables v 1 and v 2 such that for every graph S and nodes a, b ∈ S, there is an R-path from a to b if and only if S, a, b |= tr

  ) Replace every sub-formula ¬c[R]p that appears in ϕ ′ with tr(¬c[R]p), as in Def. 5.10. The resulting formula ϕ ′′ is satisfiable if and only if ϕ ′ is satisfiable, by Lemma 5.11. Note that this translation only preserves satisfiability (not equivalence).(3) Translate ϕ ′′ into an equivalent disjunctive normal form formula ϕ ′′′ . All atomic formulas are of the form c

  for every constant symbol and unary relation symbol σ ∈ τ , and for everyv ∈ S 1 , v is labeled with σ in S 1 if and only if h(v) is labeled with σ in S 2 .(2) for every binary relation symbol σ ∈ τ , and every pair of nodes v 1 , v 2 ∈ S 1 , if there is an edge from v 1 to v 2 in S 1 labeled with σ, then there is an edge from h(v 1 ) to h(v 2 ) in S 2 labeled with σ. Let h :S 1 → S 2 be a homomorphism. If S 1 |= c 1 R c 2 then S 2 |= c 1 R c 2 . Dually, if S 2 |= c[R]p,and p does not contain positive occurrences of edge formulas or equality formulas, then S 1 |= c[R]p.

	Lemma 6.7

  and t i is the node v t v,l if t i is the l-th occurrence of the node v ∈ S on the path W W ′ is a graph with nodes {d(t 1 ), . . . , d(t r )}. If the witness path W goes from t i to t i+1 through an edge labeled with f i ∈ F , then there is an edge in W ′ labeled with f i from d(t i ) to d(t i+1 ). Note that W ′ contains only edges traversed by the witness path. For every unary relation and constant symbol σ ∈ C ∪ U and node t i ∈ W , d(t i ) is labeled with σ in W ′ if and only if t i is labeled with σ in S.

8.0.0.1 Bounded-Model Property of

  L 1 We can show that L 1 has a bounded model property: every satisfiable L 1 formula has a model whose size is a (elementary) function of the size of the formula. The translation of L 1 formulas to automata and the finite-model property (Theorem 2.6) yield a double-exponential bound on the size of a model. We believe that it can be improved. Bounded-model property is important for example for guaranteeing termination of tableaux-based decision procedures. Lemma 6.11 implies that an upper bound on the branching of a node in a Σ-labeled tree is r = 2 × n × ϕ ✸ × |C|. If a node is not labeled with a constant, we can improve the bound to be 2 × n × ϕ ✸ . The branching does not increase as a result of merging and edge additions enabled by L 1 patterns. Thus, for checking satisfiability of L 1 it is sufficient to consider only Σ-labeled trees with a branching bounded by r.

	8.0.0.2 Bounded Branching of L 1 8.0.0.

3 The Use of Constants in Routing Expressions

  If the routing expressions do not contain positive occurrences of constant symbols, then the bound k for L 1 does not depend on the routing expressions: Assume that ϕ ∈ L 1 is satisfiable, and that the routing expressions that appear in ϕ do not contain positive occurrences of constant symbols. Then, there exists a graph S ∈ A k where k = |ϕ ✸ |, and S |= ϕ. To prove this, we modify the proof of Theorem 5.14. The main observation is that we cannot force a path to visit a node labeled with a constant, except at the endpoints of a path. (a) when creating a pre-model, duplicate nodes with constants, (b) witness splitting results in a pre-model with at most |ϕ ✸ | extra edges, (c) use homomorphism which only preserves existence of constants, not their absence, and (d) merge operation enabled by L 1 preserve homomorphism, because they do not require merging a node with a constant, because a pattern may not contain a positive occurrence of equality between a variable and a constant (unlike L 2 ).Constant symbols can be eliminated from routing expressions, but the complexity of this operation is prohibitive. The LRP formulas that come up in practice are well-structured, and we hope to achieve a reasonable performance.

	Theorem 8.1 Sketch of Proof: 8.1 L 1 is NEXPTIME-hard
	The proof in this section is an adapted version of the NEXPTIME-hardness proof
	from [29, Theorem 5]. [29, Theorem 5] uses universal quantification over nodes,
	which is not available in L 0 . Instead, the proof in this section use reachability con-
	straints and patterns.

Let T be a tiling problem as in Def. 3.1, and let n be a natural number. It is an NEXPTIME-complete problem to test on input (T , 1 n ) whether there is a T -tiling of a square grid of size 2 n by 2 n

[40]

.

Theorem 8.2

The satisfiability of L 1 formulas is NEXPTIME-hard.

  n , t] and [2, 1, t ′ ]. We include the following unary relation symbols: H 1 , . . . H n , indicating the horizontal position as an n-bit number; V 1 , . . . V n , indicating the vertical position; and T 0 , . . . T k , indicating the tile type.

This and other examples are explained in detail in Section 4.2.

We can also allow auxiliary constants and fields including abstract fields[START_REF] Burdy | An overview of jml tools and applications[END_REF].

In all our examples, a neighborhood formula N used in a pattern is such that B N (the Gaifman graph of N ) is connected.

This version is simplified because it assumes a single root object; a set of roots can be handled as shown in Section 9.

In this paper, we use the term "tree" instead of the term "forest" to refer to an acyclic graph, possible undirected.

Recall from Section 2.1.1 that c R c ′ is a shorthand for ¬c[R]¬c ′ .

Note that we cannot use the simple D ′ definition as before, because merging v 1 and v 2 in T to obtain T ′ creates a cycle that does not involve e 1 . We observe that, in this case, the subgraph reachable from v 1 through e 1 in T remains acyclic after the merge operation, because it is disjoint from the subtree of v 2 . Thus, e 1 need not be removed from T .

Note that ¬p may contain negative occurrences of unary formulas, but these are also preserved under the (non-standard) homomorphism relation we are using.

This bound is not tight.

The nodes h 0 (w 1 ) and h 0 (w 2 ) in S are distinct, because our construction of pre-model S 0 does not split nodes labeled by constants.

The tree width of G(G k ) is k and the tree width of G(G ′ k ) is k + 1.

The proof is not included in the paper, because we are investigating tighter upper and lower bounds.

 [START_REF] Areces | Hybrid logics: characterization, interpolation and complexity[END_REF]This research was supported by THE ISRAEL SCIENCE FOUNDATION (grant No 304/03).