Computer Science
ComputerScience,1970-2008-Computer Science-2004.jsonl.gz.gz
Computer Science
0b3a134f6ca871bb3b02d004d3e847ce65dd8e98
Typestate Checking and Regular Graph Constraints

We introduce regular graph constraints and explore their decidability properties. The motivation for regular graph constraints is 1) type checking of changing types of objects in the presence of linked data structures, 2) shape analysis techniques, and 3) generalization of similar constraints over trees and grids. We define a subclass of graphs called heaps as an abstraction of the data structures that a program constructs during its execution. We prove that determining the validity of implication for regular graph constraints over the class of heaps is undecidable. We show undecidability by exhibiting a characterization of certain"corresponder graphs"in terms of presence and absence of homomorphisms to a finite number of fixed graphs. The undecidability of implication of regular graph constraints implies that there is no algorithm that will verify that procedure preconditions are met or that the invariants are maintained when these properties are expressed in any specification language at least as expressive as regular graph constraints.

trees and grids. Typestate checking for recursive and potentially cyclic data structures requires verifying the validity of implication for regular graph constraints. The implication of regular graph constraints also arises in shape analysis algorithms such as role-analysis and some analyses based on threevalued logic.
Over the class of lists regular graph constraints reduce to a nondeterministic finite state automaton as a special case. Over the class of trees the constraints reduce to a nondeterministic top-down tree automaton, and over the class of grids our constraints reduce to domino system and tiling problems.
We define a subclass of graphs called heaps as an abstraction of the data structures that a program constructs during its execution. We show that satisfiability of regular graph constraints over the class of heaps is decidable. However, determining the validity of implication for regular graph constraints over the class of heaps is undecidable. The undecidability of implication is the central result of the paper. The result is somewhat surprising because our simple constraints are strictly less expressive than existential monadic second-order logic over graphs. In the key step of our proof we introduce the class of corresponder graphs which mimic solutions of Post correspondence problem instances. We show undecidability by exhibiting a characterization of corresponder graphs in terms of presence and absence of homomorphisms to a finite number of fixed graphs.
The undecidability of implication of regular graph constraints implies that there is no algorithm that will verify that procedure preconditions are met or that the invariants are maintained when these properties are expressed in any specification language at least as expressive as regular graph constraints.

Introduction
Types capture important properties of objects in the program. In an imperative language properties of objects change over time. It is therefore desirable that types capture changing properties of objects. A typestate system is a system where types of objects change over time. A simple typestate system was introduced in [25], more recent examples include [14,23,28,5]. We view typestate as a step towards statically checking properties of objects [17,8].
One of the difficulties with defining object properties in object-oriented languages is that a property of an object may depend on properties of other objects in the heap. Some systems allow programmers to identify properties of an object x in terms of properties of objects y such that x references y. The idea that important properties of an object x may depend on properties of objects z such that z references x was introduced in the role system [14].
In general, properties of objects may be mutually recursive and the referencing graph of objects may be cyclic. Due to cycles in the heap the least fixpoint solution for the recursive object properties is not acceptable because there is no basis to ground the inductive definitions of these properties. We therefore say that a heap satisfies a set of properties if there exists some choice of predicates that satisfy the mutually recursive definitions. The existential quantification over predicates leads to constraints that have the form of existential monadic second-order logic [7]. For a presentation of role analysis and related systems from the perspective of monadic second-order logic, see [15].
In this paper we present a very simple form of constraints that we call regular graph constraints. A set of regular graph constraints can be specified by a single graph G. A heap H satisfies the constraints iff there exists a graph homomorphism from H to G. Regular graph constraints abstract the problem of mutually recursive definitions of properties over potentially cyclic graphs. The existential quantification over predicates is modeled in regular graph constraints as the existence of a homomorphism to a given fixed graph. Regular graph constraints are closed under conjunction and in certain cases are closed under disjunction (Section 2.9). Moreover, regular graph constraints generalize the notion of tree automata [27,3] and domino systems [12], without going all the way to monadic second-order logic for richer domains. In this paper we consider as the domain of interpretation the class of heaps. Our notion of heap is an abstraction of garbage collected heap in a programming languages like Java or ML. Heaps contain a "root" node and a "null" node, all nodes are reachable from the root, and all edges are total functions mapping nodes to nodes.
In Section 2.8 we show that there is a simple and efficient algorithm that decides if regular graph constraints have a heap model. This results in a simple sanity test on regular graph constraint specifications that rules out the contradictory specifications.
We next turn to the problem of checking if one set of regular graph constraints implies another set of regular graph constraints over the set of heaps. Our main contribution (Section 3) is the proof that the implication problem is undecidable.
The implication problem of graphs arises in compositional checking of programs if procedure preconditions or postconditions are given as regular graph constraints. In Section 3.5.4 we show that the implication problem also arises when proving that an invariant holds after every program step. These verification problems are therefore undecidable. Our result places limitations on the completeness of systems such as role analysis [14] and shape analysis [20] that use homomorphic images to represent the abstraction of the heap. The undecidability of regular graph constraints means that semantically checking the implication of such homomorphic graph images is undecidable.
A common way of showing the undecidability of problems over graphs is to encode the Turing machine computation histories [22] as a special form of graphs called grids. The difficulty with showing the undecidability of implication of regular graph constraints is that regular graph constraints cannot define the subclass of grids among the class of heaps. Indeed, this is why satisfiability of regular graph constraints over heaps is decidable. To show the undecidability of the implication of regular graph constraints, we use the constraints on both sides of the implication to restrict the set of possible counterexample models for the implication. For this purpose we introduce a new class of graphs called corresponder graphs. Satisfiability of regular graph constraints over corresponder graphs mimics the solution of a Post correspondence problem instance, and is therefore undecidable. We give a method for constructing an implication such that all counterexamples for the validity of implication are corresponder graphs which satisfy a given regular graph constraint. This shows that the validity of the implication is undecidable.
Due to closure under conjunction, the implication is reducible to the equivalence of regular graph constraints. As a result, the equivalence of two regular graph constraints is also undecidable.

Regular Graph Constraints
In this section we define the class of graphs considered in this paper as well as its subclasses heaps, trees, lists, grids, and corresponder graphs. We present our regular graph constraints, give several equivalent formulations of the constraints and show that our constraints capture tree automata and domino systems as special cases. We then review some decidability properties, show that satisfiability of regular constraints over heaps is efficiently decidable and state some closure properties of regular graph constraints.

Preliminaries
If r ⊆ A × B and S ⊆ A, relational image of set S under r is defined as We use to mark the end of a proof and to mark the end of an example.

Graphs
We will be considering the following class of directed graphs in this paper. Our graphs contain two kinds of edges, which we represent by relations s1 and s2. These relations may represent fields in an object-oriented program. The constant root represents the root of the graph. We use edges terminating at null to represent partial functions and abstractions of graphs with partial functions.
• root, null ∈ V are distinct constants, root = null; • s1, s2 ⊆ V × V are two kinds of graph edges, such that for all nodes x null, x ∈ si iff x = null for i ∈ 1, 2.
We use G to denote the class of all graphs.
An s1-successor of a node x is any element of the set s1[{x}], similarly an s2-successor of x is any element of s2 [{x}]. Note that there are exactly two edges originating from null. When drawing graphs we never show these two edges.
Definition 2 A heap is a graph G = V, s1, s2, null, root where relations s1 and s2 are total functions and where for all x = null, node x is reachable from root. We use H to denote the class of all heaps.

Definition 3
The in-degree of a node x in a graph is the number of edges terminating at x.
inDegree(x) = |{y | ∃i y, x ∈ si}| Definition 4 A tree is a connected acyclic graph such that inDegree(x) ≤ 1 for every node x.
Definition 5 A list is a tree with at most one non-null outgoing edge: for every node x, s1(x) = null or s2(x) = null.

Graphs as Constraints
A regular constraint on a graph G is a constraint stating that G can be homomorphically mapped to another graph G ′ .

Definition 6
We say that a graph G satisfies the constraints given by a graph G ′ , and write G → G ′ , iff there exists a homomorphism from G to G ′ .
A homomorphism between graphs is defined as follows.
root ′ iff all of the following conditions hold: We can think of a homomorphism h : V → V ′ as a coloring of the graph G. The color h(x) of a node x restricts the colors of the s1-successors of x to the colors in s1[{h(x)}] and the colors of the s2-successors to the colors in s2[{h(x)}].
Example 8 A graph G can be colored by k colors so that the adjacent nodes have different colors iff G is homomorphic to a complete graph without self-loops, . . , k}, and The identity function is a homomorphism from the graph to itself. Therefore, G → G for every graph G. The following fundamental property of homomorphisms also holds.

Proposition 9 (Homomorphisms compose) Let
A consequence of Proposition 9 is that → is a transitive relation.
Definition 10 (Satisfiability) A graph G ′ is satisfiable over the class of graphs C iff there exists a graph G ∈ C such that G → G ′ . Satisfiability problem over the class of graphs C is: given a graph G ′ , determine if G ′ is satisfiable.
Definition 11 (Implication) We say that G1 implies G2 over the class of graphs C, and write for all graphs H ∈ C.
We will omit C in ;C if the class of graphs is clear from the context. The following fact provides a sufficient condition for the graph implication to hold. It is a direct consequence of Proposition 9.
Proposition 12 Let C be any class of graphs. Let G → G ′ . Then G ;C G ′ .
In Section 3 we show that the implication of graphs is undecidable over the class of heaps.

Paths
We next state several simple properties of paths that will be useful in Section 3.
Then if e is any regular expression over the alphabet {1, 2} such that G0 contains some slice p ∈p e, then G contains some slice p ′ ∈p e.

Proof.
Let p be a slice in G0 and word(p) ∈p e. By Proposition 16 we have that h[p] is a slice in G and word(h[p]) = word(p) ∈p e.
We will use the contrapositive of Proposition 18 in the proof of Proposition 37 (Section 3).

Regular Constraints and EMSOL
We can express the property of being homomorphic to a fixed graph G ′ by an existential monadic second-order logic formula (EMSOL) of a special form. Let expressing that G is homomorphic to G ′ . We use the uppercase identifiers X0, . . . , X k−1 to denote the second order variables. These variables range over the subsets of V . The lowercase identifiers are first-order variables ranging over the elements of V . Notation Xi(z) means that z is an element of the set Xi. The predicate si(x, y) means that x, y ∈ si holds in the graph G.
(For the precise definition of monadic second-order logic see e.g. [10], pp28.) Viewing graph as a formula justifies our previous definitions of graph satisfiability and implication. We can similarly talk about the graph conjunction, disjunction etc.
We may increase the ease of expression of some properties by relaxing the form of EMSOL formula (1) without changing the expressive power. The reason is that that the relaxed form can be converted into a normal form that can be described by a graph homomorphism. Let B f (B0, B1, . . . , Bn−1; A0, . . . , Am−1) denote an arbitrary propositional combination of formulas B0, . . . , Bn−1, A0, . . . , Am−1 in which B0, . . . , Bn−1 occur only negatively. Then every formula of the following form is expressible as a graph constraint.
Compared to (1), the form (2) does not require X0, . . . , X k−1 to form a partition of the set of all nodes, it has the quantifiers from Pj lifted to the topmost level, and allows arbitrary propositional combinations of predicates Xi(x) and Xi(y).

Example 19
The following formula is of the form (2). Let us assume that the formula is interpreted over the class of heaps. The formula states that the node root has in-degree 0.
The formula uses the set X2 that contains null as well as the nodes reachable from root along the s1 edges. The formula states explicitly that X1 and X2 are disjoint. Because s1 edges from X2 can only lead to X2, there are no s1 edges to root. The constraint that root has no s2 edges is specified directly, without introducing an auxiliary set of nodes. In general, negation and the implicit absence of constraints are often more convenient to express with a formula than with a graph homomorphisms.
Note that if we replaced the subformula (X0(x) ⇒ X2(x)) with ¬(X0(x) ∧ X2(x)) the resulting formula would require the existence of a cycle in the graph.

Proposition 20
The two families of formulas (1) and (2) denote the same family of sets of graphs.

Proof. (Sketch)
Given a formula of form (1) we construct a formula of form (2) by transforming . This allows us to write constraints on s1 and s2 separately. We then lift the universal quantification over y to the top level. The partition constraint is expressible as a formula that has no occurrences of si.
Conversely, suppose we are given a formula in form (2) and suppose that the formula holds for a graph G with the set of nodes V . This means that there exist sets S1, . . . , S k−1 that satisfy B1 and B2. We construct a family of sets Ti 1 ,...,i k−1 that forms a partition of set V such that every set Sj is expressible as a union of some sets Ti 1 ,...,i k−1 . Namely, we define This motivates a construction where the second-order variables X0, X1, X2, . . . , X k−1 are replaced with up to 2 + 2 k−2 new variables X0, X1, Y0, . . . , Yn−1. We then express variables X2, . . . , X k−1 in terms of X0, X1, Y0, . . . , Yn−1, write the boolean combinations B f in disjunctive normal form and use the fact that X0, X1, Y0, . . . , Yn−1 denote disjoint sets. As a result, it is possible to write the original formula in form (1).
Note that, over any class containing all heaps, not every EMSOL formula corresponds to a regular graph constraint. This is in contrast with trees [27] and grids [12]. Even firstorder logic can express a constraint that the graph is a grid.
On the other hand, we have shown in ( [13], pp93) that not even constraints stronger than regular graph constraints can express the gridness property. For a normal form construction using full existential monadic second-order logic see see [21]. For using higher order logic to express heap properties more general than regular graph constraints, see [15].

Related Systems
In this section we show the relationship of our regular graph constraints with some other systems for defining sets of graphs. We also illustrate that decidability of satisfiability and implication are sensitive to the subclass of the graphs considered, and change in a non-monotonic way.

Words
Regular graph constraints over lists correspond to regular word languages. A regular graph constraint corresponds to a nondeterministic finite state automaton with the initial state root and the final state null.

Trees
Satisfiability and implication of regular graph constraints are decidable over the class of trees. The reason is that the entire MSOL is decidable over trees [27], and regular graph constraints are expressible in MSOL.

Pictures
Domino systems [12] are regular graph constraints over the grids.
Definition 21 A grid m × n is a graph isomorphic to The chapter [12] uses the term pictures for grids. It is easy to see that over the domain of grids, regular graph constraint are equivalent to a domino system with s1 edges denoting horizontal dominoes and s2 edges denoting vertical dominoes. The graph homomorphism corresponds to the use of projection. [12] states the equivalence of domino systems over pictures with negation-free regular expressions with projections, on-line tessellation automata, existential monadic second-order formulas and tiling systems.
We view the fact that, over the grids, regular graph constraints are equivalent to each of the systems above as an indication that the definition of regular graph constraints is natural.
Note When comparing our regular graph constraints to trees and domino systems, we notice that in our definition of a model there are no fixed labels associated with nodes. The only labeling of nodes comes from the graph homomorphism, which corresponds to projection in tree and picture languages. Our simplification makes our undecidability result strictly stronger. Furthermore, regular graph constraints can capture the distinction between a node with an edge terminating at null and a node with an edge terminating at a node that is not null. This distinction can be used for encoding in the structure of the graph any fixed labeling of graph nodes.

Decidability of Implication over Graphs
Satisfiability problem over the class of graphs is trivial. Namely, G → G, so every graph is satisfiable. The implication problem over graphs is also decidable, in contrast to the implication problem over the class of heaps, which we will show undecidable in Section 3.

Proposition 22
Our regular graph constraints are weaker than finite graph acceptors of [26]. It is easy to see that finite graph acceptors can define the gridness property. Therefore, domino system satisfiability is reducible to satisfiability of finite graph acceptors, which makes finite graph acceptor satisfiability undecidable.
GraphCleanup: Repeat the following operations until the graph stabilizes: 1. if x is marked then return, otherwise: 3. pick a s1-successor y of x; select( x, y ); mark(y) 4. pick a s2-successor z of x; select( x, y ); mark(z) SatisfiabilityCheck: Repeat the following operations until the graph stabilizes: 2. if the resulting graph is empty, then G ′ is unsatisfiable; 3. otherwise a heap satisfying G ′ can be obtained as follows: 4. let all graph nodes be unmarked; 5. mark(root); 6. return subgraph containing selected nodes

Satisfiability over Heaps
We show that satisfiability for heaps is efficiently decidable by the nondeterministic algorithm in Figure 1. The goal of the algorithm is to find, given a graph G ′ , whether there exists a heap G such that G → G ′ . Recall that the property of a heap is that every node has exactly one s1 outgoing edge and exactly one s2 outgoing edge. This property need not be satisfied by G ′ , so we cannot take G = G ′ to be the heap proving satisfiability of G ′ . The algorithm updates the current graph until it becomes a heap or an empty graph. (For the purpose of this algorithm we allow even null and root to be removed from the graph.) If nonempty, the result is a heap G such that G → G ′ .

Proposition 23
The procedure in Figure 1 is a correct algorithm for determining satisfiability of a graph over the class of heaps.
Proof. The procedure consists of two parts: GraphCleanup and SatisfiabilityCheck. The GraphCleanup part eliminates useless nodes and determines whether there exists a heap H such that H → G ′ . Graph Cleanup terminates because it decreases the size of the current graph G in every step. The mark phase terminates because it does a simple breadth-first search.
Observe that GraphCleanup does not reduce the set of heaps homomorphic to G ′ . Namely, if a node x of G is removed in GraphCleanup, then no node is mapped to x under any homomorphism h. Therefore, if GraphCleanup returns an empty graph, then G ′ is unsatisfiable.
Assume that GraphCleanup returns a nonempty graph G. Then G contains root and every node in x has a s1successor and a s2-successor, but some of the nodes may have two s1-successors or s2-successors. Invoking mark will do a depth-first search on G and pick a subgraph H where every node has exactly one s1-successor and one s2successor. The resulting graph H will therefore be a heap. We have H → G ′ because H is a subgraph of G ′ .

Closure Properties
In this section we give a construction for computing the conjunction of two graphs and a construction for computing the disjunction of two graphs. We will use these constructions in Section 3.

Conjunction
We show how to use a Cartesian product construction to obtain a conjunction of two graphs G1 and G2.

Definition 24 (Cartesian Product) Let
such that: In other words, G1 × G2 is a conjunction of G1 and G2.
Proof. (=⇒) : Let G → G 1 and G → G 2 with h 1 : V → V 1 and h 2 : V → V 2 where G 1 and G 2 are defined as in Definition 24 and It is straightforward to verify that properties 2 and 3 of homomorphism hold for h 0 . Let i ∈ {1, 2}. If x, y ∈ si then h 1 (x), h 1 (y) ∈ s 1 i and h 2 (x), h 2 (y) ∈ s 2 i . Because h 1 and h 2 satisfy properties 2 and 3 of homomorphism, we have h 1 (x), h 2 (x) , h 2 (y), h 2 (y) ∈ V 0 regardless of whether x, y ∈ {null, root} or not. We therefore con- Let's show that h 1 is a homomorphism (an analogous argument holds for h2). It is straightforward to see that properties 2 and 3 hold for h1. For property 1, let i ∈ {1, 2} and let x, y ∈ si. Let h 0 (x) = x 1 , x 2 and h 0 (y) = y 1 , y 2 . Because h 0 is a homomorphism, we have

Disjunction
Given our definition of graphs, there is no construction that would yield disjunction of arbitrary graphs over the family that contains all heaps. We illustrate this fact with an example. We then give a simple condition on graphs that ensures that the disjunction construction is possible over the domain of heaps.

Example 26
Let In the class of heaps, the only model for G 1 is G 1 itself, and the only model of G 2 is G 2 . Now assume that there exists graph Therefore for the graph we have G3 → G 0 as well. So there is no graph G 0 such that for all heaps G, To ensure that we can find union graphs over the set of heaps, we will require s2(root) = null.

Definition 27 (Orable Graphs) A graph
The following simple fact allows us to form arbitrary finite sums of orable graphs.
Proposition 29 If G 1 and G 2 are orable graphs, then G 1 + G 2 is also orable.

Proposition 30 (Disjunction via Sum)
Let G be a heap and G 1 and G 2 be orable graphs. Then Proof. (⇐=) : Assume without loss of generality G → G 1 . Because G 1 is a subgraph of G 1 +G 2 , there exists an identity homomorphism from G 1 into G 1 + G 2 . By Proposition 9 we conclude G → G 1 + G 2 .
(=⇒) : Let G 0 = G 1 + G 2 where G 1 and G 2 are as as in Definition 28, and G → G 0 with a homomorphism h : Suppose the claim does not hold. Then there exist x 0 , y 0 ∈ V such that where x 1 = h(x 0 ) and y 2 = h(y 0 ). By definition of heap, there exists a sequence of nodes p = root, z 0 , . . . , x 0 forming a path from root to x 0 in G. Because x 0 / ∈ {null, root}, the path has length at least two and z 0 / ∈ {null, root} (it may or may not be z 0 = x 0 ). Because G 1 + G 2 is orable, the edge from root to z 0 cannot be from s2, so s1(root) = z 0 . We claim h(z 0 ) ∈ V 1 \ V 2 . Indeed, suppose h(z 0 ) ∈ V 2 . By the properties of homomorphism and because in G 1 + G 2 there are no edges from nodes V 1 \ {null, root} to nodes V 2 \ {null, root}, we have h(w) ∈ V 2 for every node w of the path p. This is a contradiction with h(x 0 ) ∈ V 1 \ V 2 . We conclude Repeating an analogous argument for node y 0 , we conclude is the unique s1-successor of root in the heap G. We have arrived at contradiction, so (3) is true.
A product of orable graphs is orable.
Proposition 31 Let G 1 and G 2 be orable graphs. Then In the sequel we will deal only with orable graphs.

Undecidability of Implication
This section presents the central result of this paper: The implication of graphs is undecidable over the class of heaps.
Our proof proceeds in two steps. We first introduce a family of corresponder graphs. We show that satisfiability of graphs over the family of corresponder graphs is undecidable.
In the second step we show that satisfiability over corresponder graphs can be reduced the question of whether an implication between two graphs fails to hold. The key to the construction in the second step is that a conjunction of certain regular graph constraints and negations of regular graph constraints can precisely characterize the class of corresponder graphs.

Corresponder Graphs
Corresponder graphs are a subclass of the class of heaps. Figure 3 shows an example corresponder graph.

Corresponder Graph Satisfiability
For completeness we define the Post correspondence problem, PCP ( [22], pp183).  [22] contains the proof for the following theorem.

Theorem 34
The following problem is undecidable: given a PCP instance, does it have a solution.
We will use the following proposition to establish undecidability of graph implication.
Proposition 35 Satisfiability of graphs over the class of corresponder graphs is undecidable.
Proof. We give a reduction from PCP. Let m ≥ 2 and let v0, w0 , v1, w1 , . . . , vm−1, wm−1 be an instance of PCP where vi, wi are nonempty words. Introduce names a j i and b j i for letters in words vi, wi: where pi = |vi| and qi = |wi|. We construct a graph G such that there exists a corresponder graph G0 with the property G0 → G iff the PCP instance has a solution. Figure 4 illustrates how a corresponder graph G0 with a homomorphism from G0 to G encodes a solution of the PCP instance c, bc , ab, a .
Let G = V, s1, s2, null, root   i . The a-nodes will summarize U -nodes and the bnodes will summarize the L-nodes of the corresponder graph. Introduce also the additional nodes b 2j,1 i to encode the information that a 2j,0 i node has an incoming edge from a c-node. As we will see below, the b 2j,1 i nodes have s2 pointing to root as opposed to null, which ensures that every a 0,0 i node has an incoming edge from a c-node. For analogous reasons we introduce a 2j+1,1 i nodes. Let Define s1 graph edges as follows.
The ci nodes are connected into a list that begins with root and every c2i is followed by c2i+1. The pairs c2i, c2i+1 for different i can repeat in the list any number of times and in arbitrary order. This list will encode a PCP instance solution.
The nodes representing word positions are linked in the order in which they appear in the word. The last position in a word can be followed by the first position of any other word, or by null. The nodes for the vi words and the nodes for the wi words form disjoint lists along the s1 edges.
We define s2 graph edges as follows.
Every cj edge points to the position at the beginning of the word. Even numbered nodes point to the a 0 -positions; odd numbered nodes point to b 1 -positions.
The ai and bj word positions are connected so that an a-node points to a b-node for even indices, whereas a b-node points to an a-node for odd indices.
This completes the definition of G.

Claim 36
The PCP instance has a solution iff there exists a corresponder graph G0 such that G0 → G. be a corresponder graph. We construct a homomorphism h from G0 to G as follows. We map C-nodes of G0 into c-nodes of G: For 0 ≤ f < n, let du(f ) denote the largest index i such that ui ≤ f . We map the U -nodes into a nodes as follows. Consider a node U 2f . Let i = d(f ). Then U 2f is the even node that represents the letter v f −u i i of the word vi: The mapping of U 2f +1 is similar. In this case we also encode the information whether L 2f +1 has an s2-edge from a Cnode.
The mapping of L-nodes is analogous. Let d l (f ) denote the largest index i such that li ≤ f . Then It is straightforward to verify that h is indeed a homomorphism.
is a corresponder graph and h is a homomorphism from G0 to G. Because in graph G all paths given by the regular expression 1 * lead to ci-nodes or null, we conclude that each Cj node is mapped to some ci node. For 0 ≤ j < k we define From the properties of homomorphism we derive We will show that tj is a solution of the PCP instance. Let u0 = l0 = 0 and un+1 = ln+1 = n. Let for 0 ≤ j < n. To prove vt 0 vt 1 . . . vt k−1 = wt 0 wt 1 . . . wt k−1 it therefore suffices to show for 0 ≤ j < k. Let tj = i. Then h(C2j ) = c2i. We have C2j , U2u j ∈ s2 in the corresponder graph G0. On the other hand, c2i, a 0,0 i ∈ s2 is the only s2-outgoing edge of c2i in G. Therefore, h(U2u j ) = a 0,0 i . From this, we first conclude so h ′ (U2u j ) = v 0 i . Next, by construction of s1 edges of G and G0 we get To establish (4) it suffices to show uj + pi = uj+1. To see that the equality holds, suppose first uj + pi > uj+1. Then h(U2u j+1 ) = a 2f,0 i where f > 0. Because h is a homomorphism, following s2 edge once we conclude h(L2u j+1 ) = b 2r,0 g for some g and following s2 for the second time we obtain the contradiction because in corresponder graph s2(L2u j+1 ) = root but in G we have s2(b 2r,0 g ) = null. Similarly, suppose now uj + pi < uj+1. Then s1(U 2(u j +p i −1) ) = null, so let U 2(u j +p i ) = s1(s1(U 2(u j +p i −1) )). Because uj + pi / ∈ {u0, . . . , u k−1 }, we get s2(s2(U 2(u j +p i ) )) = null On the other hand, h(U 2(u j +p i ) ) = a 0,0 f for some f , so s2(s2(h(U 2(u j +p i ) ))) = root which is again a contradiction. Therefore uj + pi = uj+1. Showing (5) is analogous. We conclude that t0, . . . , t k−1 is a solution for PCP instance.
Our claim is therefore true and satisfiability over corresponder graphs is undecidable.

Defining Corresponder Graphs
In this section construct graphs P and Q such that iff G0 is a corresponder graph. When presenting the graphs P, Q0, . . . , Q16 we use the following conventions. We use the label r to denote the root of the graph. We label the edges of the relation s1 relation by 1 and the edges of s2 by 2. Note that if a node has no outgoing edges, it would be useless in the graph in terms of specifying a set of models G0. Every graph node will therefore have at least one outgoing edge for every label. However, in order to make the graph sketches clearer, if a node x has an outgoing edge with label a to every node in the graph, we will simply omit all a edges of node x from the sketch. In particular, if a node has no outgoing edges in the graph sketch, it means that its outgoing edges are unconstrained. A double-headed arrow from node x to node y with label a denotes two single arrows, one from x to y and one from y to x, both labeled with a. We do not show the edge root, null ∈ s2 that is always present in an orable graph. We also do not show the edges originating from null. We will be free to display null several times in the same picture, all these occurrences denote to the unique root node in the graph.
The graph P in Figure 5 is our first approximation of a corresponder graph. Unfortunately, P allows some models that are not corresponder graphs, such as the example in Figure 6. This is why we introduce the graph Q. The graph Q appears in (6) negated and we design it to contain models of P that are not corresponder graphs. We construct Q as a sum of orable graphs: The idea behind the construction of these graphs comes from the proof of Proposition 37; we now give only an informal overview of the graphs. The graphs Q0 (  Figure 16) ensure that different paths in the graph lead to the same object. The graphs Q7 ( Figure 14) and Q8 ( Figure 15) ensure that there is the same number of U and L-nodes in a model of P . The graphs Q10 ( Figure 17) and Q11 (Figure 18) ensure that U or L nodes have an s2 edge to root iff the U or L node in the same column has an s2-edge from a C-node. The graphs Q12 ( Figure 19) and Q13 (Figure 20) ensure that a C-node that is later in the C-list has an edge to a node that is later in the U or L list. Finally, graphs Q14 (Figure 21), Q15 ( Figure 22) and Q16 (Figure 23) ensure that C-nodes have s2 edges only to U and L-nodes, and that an L or U node can only have an edge to root, null, a U -node, or an L-node. We can now show the key step in the undecidability proof for the implication of graph constraints.
(G0 → P ) : Define homomorphism h from G0 to P as follows.
It is straightforward to verify that h is indeed a homomorphism, so G0 → P . we conclude h(U1) = a2, which is a contradiction.
(¬ G0 → Q5) : Suppose h is a homomorphism from G0 to Q5. By mapping the slice in 121 * with h we conclude that there exists a node Uj in G0 such that h(Uj ) = a0. Now as in the previous case we get that h(Uj+1) = a1 and h(Uj+1) = a2, which is a contradiction.
(¬ G0 → Q6) : Similarly to the previous case, map the slice in 1221 * to conclude that for some node Lj we have h(Lj ) = b0 and then obtain a contradiction.
(¬ G0 → Q7) : Similarly to the previous cases, suppose h is a homomorphism from G0 to Q7. By mapping the slice in 1221 * via h, we conclude that there exists a node Lj in G0 such that h(Lj ) = b0. By construction of Q7 it must be s1(Lj ) = null. Furthermore, h(Uj ) = a0 and s1(Uj ) = null. This is a contradiction with the fact that G0 is a corresponder graph.
(¬ G0 → Q8) : This fact is analogous to the previous one.
(¬ G0 → Q11) : This case is analogous to the previous one.
(¬ G0 → Q13) : This case is analogous to the previous one.
(¬ G0 → Q14) : Suppose h is a homomorphism from G0 to Q14. Then h(Ci) = c2 for some i. Let S = s2(Ci). Then S = Uj or S = Lj for some j and h(S) = a2. On the other hand, by mapping the slices 121 * and 1221 * , we conclude that all U -nodes are mapped to a0 and a1 whereas all Lnodes are mapped to b0 and b1. This is a contradiction with h(S) = a2.
(¬ G0 → Q15) : Suppose h is a homomorphism from G0 to Q15. Then for some node Lj we have h(Lj ) = b2 and therefore h(Uj ) = a2. On the other hand by mapping the slice 121 * we conclude that all U -nodes are mapped to a0 and a1, which is a contradiction.
(¬ G0 → Q16) : This case is analogous to the previous one.
(=⇒) : Let G0 = V, s1, s2, null, root Assume that G0 → P and for all 0 ≤ i ≤ 16 it is not the case that G0 → Qi. We will show that G0 is a corresponder graph. Let Then for all Ci ≥ 0 we have Ci = root, because G0 → P . We claim that there must exist t such that Ct = null and Ct−1 = null. Suppose the claim is false. Because the graph is finite, the nodes Ci form a cycle with s1 edges: there exist i1, i2 such that 0 < i1 < i2, Ci 1 = Ci 2 and Ci 1 = null. We can then show G0 → Q0, a contradiction.
Let t be the smallest index such that Ct = null. Then t = 2k for some k ≥ 2 because G0 → P . The nodes root, null, C0, . . . , C 2k−1 are all distinct.  Figure 24 shows the shape of the portion of G0 identified so far. By construction, In the sequel we will show that s2[V0] ⊆ V0 holds as well. By definition of heap, all nodes in G0 are reachable from root, which will imply V \ V0 = ∅. We will also show that n1 = n2 and that G0 satisfies the invariants that make it isomorphic to a corresponder graph. We first observe that s2(C1) = L1. Indeed, suppose that s2(C1) = L1. From G0 → P follows s2(C1) / ∈ {null, root}. We can then show G0 → Q9, which is a contradiction.
We now show that the s2 edges between U -nodes and L-nodes form a (2 × n)-grid where n = n1 = n2. First we observe s2(L1) = U1, otherwise we would have G0 → Q4. Next we claim that every non-null s2 edge originating from a U -node terminates at an L-node. Suppose s2(Uj ) is not an L-node. It cannot be a C-node or a U -node because G0 → P . The only remaining possibility is that s2(Uj ) is a node outside V0. But then G0 → Q16, a contradiction. Similarly, because ¬ G0 → Q15, every non-null s2 edge of an L-node terminates at a U -node. Finally, we claim that for all j ≥ 0, either U2j = L2j = null, or all of the following holds: We have already established the claim for j = 0. Suppose the claim does not hold for all j. Consider the least j > 0 for which the claim does not hold. Then one of the nodes U2j , L2j is not null. Assume U2j = null and L2j = null. Then G0 → Q7, a contradiction. Similarly, if U2j = null and L2j = null, then G0 → Q8, again a contradiction. So U2j = null and L2j = null. Then from G0 → P follows U2j+1 = null and L2j = null. From the previous discussion and G0 → P we conclude for some i ≥ 0. We want to show i = j. Suppose i < j.

The Undecidability Result
Theorem 38 The implication of graphs is undecidable over the class of heaps.

Proof.
We will reduce satisfiability of graphs over the class of corresponder graphs to the problem of finding a counterexample to an implication of graphs over the class of heaps. Given the reduction in Proposition 35, this will establish that the implication of graphs is Turing corecognizable and undecidable.
Let G be a graph. Consider the implication We claim that G0 is a counterexample for this implication iff G0 is a corresponder graph such that G0 → G. Assume that G0 is a corresponder graph and G0 → G. By Proposition 37, we have G0 → P and ¬G0 → Q. We then have G0 → (G × P ). Since ¬G0 → Q, we conclude that G0 is a counterexample for (10).

Discussion
In this section we give comments on our proof of the undecidability of implication and state some implications of this result for checking properties of programs.

Graph Equivalence and Negation
Definition 39 We say that graphs G1 and G2 are equivalent over the class of graphs C and write for every graph G0 ∈ C.
Proposition 40 Equivalence of graphs over the class of heaps is undecidable.
Proof. From Proposition 25 we have The result then follows from Proposition 38.
We also observe that regular graph constraints over heaps are not closed under the negation. Indeed, assume that for every graph G there exists a graph G such that the heap models of G are all heaps that are not models of G. Then finding a counterexample to an implication P ;H Q is reduced to satisfiability of the graph P × G This is a contradiction because Proposition 23 implies that satisfiability over heaps is decidable whereas Proposition 38 implies that finding a counterexample to P ;H Q is undecidable.

Implication of Acyclic Heaps
Corresponder graphs are a cyclic subclass of the class of heaps. The cyclicity, however, is not at all essential for our construction. We argue that implication of graphs is also undecidable over the class of acyclic heaps. We can define a minor variation of corresponder graphs where U and L nodes never point back to root. Instead, we introduce a special node different from null to indicate the difference between columns j for j ∈ {u1, . . . , u k−1 } ∪ {l1, . . . , l k−1 } and the remaining columns. The resulting graphs are acyclic heaps. As a result, we have the following fact.
Proposition 41 Implication of graphs is undecidable over the class of acyclic heaps.

Alternative Proofs
An alternative way to prove undecidability would be to show that conjunction of regular graph constraints and their negations can express graphs similar to grids (instead of corresponder graphs). While the construction using grids may be possible, we have found the construction using corresponder graphs to be simpler. The reason is that corresponder graphs, unlike grids, are essentially one-dimensional structures.
Our proof of Proposition 37 could potentially be simplified by showing that a larger fragment of MSOL can be written in the form of negation of an implication of graphs. We consider formulas that can be reduced to checking negation of an implication between graphs. Let a literal be a formula constructed from an orable graph as in Section 2.5. Define a homogeneous clause as a disjunction of positive literals: or a disjunction of negative literals: Then any conjunction of positive and negative clauses C0 ∧ · · · ∧ Cn−1 ∧ D0 ∧ · · · ∧ Dm−1 is expressible as a negation of implication of graph constraints. This fragment appears quite expressive, but we have not been able to obtain a characterization of the fragment that allows a natural encoding a subclass like grids or corresponder graphs in a way simpler than in Proposition 37.

Consequences for Program Checking
Implication of graphs arises if procedure specifications are regular graph constraints.
Example 42 Consider a procedure p whose precondition is that the program heap is homomorphic to a graph G1 and a procedure q whose precondition is that the program heap is homomorphic to a graph G2 (Figure 26). If the first statement in the body of p is a call to q(), a program checker must ensure that implication G1 ; G2 holds. Suppose that we have a program checking system that verifies that a graph constraint is true after every statement. Consider the statement root.1.2 := null Let G 0 = V 0 , s 0 1 , s 0 2 , null 0 , root 0 be the graph before the statement. After the statement the resulting graph is where the value of 2-edge from x has changed so that it points to null: s 1 2 = s 0 2 [x := root] Our program checking system needs to verify that for all heaps G0, Let h a homomorphism from G 0 to G. Let x = s 0 1 (s 0 1 (root 0 )). Then Moreover, root 1 and root 2 are reachable only through the path root 0 , 1, a, 1, so no nodes other than x may be mapped to root 1 or root 2 . We can therefore show that the implication (12) is equivalent to G1 ; G2 As explained in Section 3.5.2, we can modify the construction in the proof of Proposition 37 such that P and Q have no edges terminating at root. We then let G 1 = P and G 2 = Q. From the undecidability of the implication of graphs over the domain of heaps it follows that maintaining an invariant expressed as a regular graph constraint is undecidable, even across a simple assignment statement such as (11).

Related Work
The idea of typestate as system for statically verifying changing properties of objects was proposed in [25] and extended in [24]. The original typestate system as well as the more recent work in the context object oriented programming [6] do not support constraints over dynamically allocated objects, which is the focus of our paper. Several recent systems support tree-like dynamically allocated data structures [23,28,9,18]. The restriction to tree-like data structures is in contrast to our notion of heap, which allows cycles. The presence of non-tree data structures is one of the key factors that make the implication of regular graph constraints undecidable.
The idea of representing properties of a statically unbounded number of heaps by homomorphically mapping them to a bounded family of graphs is pervasive in the work on shape analysis [16,2,11,19,20]. These analyses use abstractions that capture approximate properties of data structures even if they are not tree-like. This feature of shape analyses makes our results directly applicable. Our undecidability result implies inability to semantically check implication or equivalence of such abstractions.
Shape analysis techniques were applied to a typestate checking problem in role analysis [14]. The compositionality of the analysis and the presence of procedure specifications made the need for solving the implication of constraints in [14] explicit. The algorithm [14] uses "context matching" as a decidable approximation for the implication of constraints. In [13] it was suggested that the implication problem for role constraints is undecidable. The argument makes use of acyclicity constraints as well as the constraints on the number of incoming edges of a node. In the present paper, we have shown that undecidability holds even for the regular graph constraints, which cannot directly specify acyclicity or the number of incoming edges of a node. This makes the present undecidability result strictly stronger than the result in [13].
We were pleased to discover that the constraints derived as a simplification of role analysis constraints generalize the notions of tree automata [27,3] and a whole family of equivalent systems over grids [12]. The remarkable fact that MSOL over trees is equivalent to tree automata inspired the question which classes of graphs have decidable MSOL theory [4]. In this paper we have introduced regular graph constraints which can be seen as a alternative to MSOL in generalizing projections of local properties over trees and grids. Although regular graph constraints are strictly weaker than MSOL (and in fact the satisfiability of regular graph constraints is decidable over heaps), we have shown that the implication for regular graph constraints over heaps is undecidable.

Conclusion
We have proposed regular graph constraints as an abstraction of mutually recursive properties of objects in potentially cyclic graphs. We presented some evidence that regular graph constraints are a natural generalization of the tree automata and domino systems. We have shown that satisfiability of regular graph constraints is decidable over the domain of heaps. As a main result, we have shown that the implication of regular graph constraints is undecidable. The consequence of this result is that verifying that procedure preconditions are satisfied as well as maintaining program invariants is undecidable if these properties are expressed as regular graph constraints.
We have seen that decidability of problems with regular constraints is sensitive to the choice of the class of graphs. In particular, a smaller class of graphs need not imply better decidability properties. This indicates that techniques for reasoning about different classes of graphs may be substantially different. We conclude that a good support for mechanized reasoning about data structures would likely contain a set of specialized reasoning techniques for different classes of graphs.