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.


s2fieldsofstudy:
Computer Science
Mathematics

text:
2-Sensor Problem

Ad-hoc networks of sensor nodes are in general semi-permanently deployed. However, the topology of such networks continuously changes over time, due to the power of some sensors wearing out to new sensors being inserted into the network, or even due to designers moving sensors around during a network re-design phase (for example, in response to a change in the requirements of the network). In this paper, we address the problem of covering a given path by a limited number of sensors — in our case to two, and show its relation to the well-studied matrix multiplication problem.

Introduction
Ad-hoc sensor networks are emerging as a new sensing paradigm and have thus, received massive research interest recently. Usually sensor nodes are semi-permanently deployed, since the sensors themselves barely have any moving capacity. However, the topology of such networks continuously changes over time due to a variety of reasons: For example, a sensor node may wear out due to its very limited battery power, a new sensor node may be inserted into the network, or the layout of a sensor network may need to be changed in order to improve the quality of the network coverage in response to a change in the network requirements, which is accomplished by changing the placement of current (or inserting, deleting) sensors in network.
In this paper, we address a problem of covering a path in the network using a limited number of sensors. In a sensor network, each sensor bears the ability to detect objects around it. The coverage of a sensor is limited by its energy level. Assume the sensor's detecting ability is omnidirectional, then we can model the coverage of a sensor as a disk (under 2-norm on the Euclidean plane 1 ) centered at the sensor. The radii of such disks are determined by the energy level of the sensors. The coverage area (or simply coverage) of the sensor network is the union of all such disks.
A sensor network is often used to detect intruders. An intruder may start at a point S on the plane, may follow an arbitrary trajectory (path), and may stop at some other point T on the plane. In some applications, a sensor network may need to keep track of the intruder at all times, as it follows its trajectory; in some other applications, the network's function may be simply to detect the presence of an intruder, in which case the network only needs to cover some part of the trajectory. Thus, given two points S and T , two relevant types of trajectories are proposed [1]: The maximum breach path and the maximum support path (In [1], these paths are called maximal breach path and maximal support path, respectively).
The maximum breach path measures the vulnerability of a sensor network by, as the name suggests, completely avoiding the coverage area of the sensor network: It is a trajectory between the start point S and the stop point T that stays "as far away" from the sensors as possible. On the other hand, the maximum support path measures the efficiency of the network coverage: This path is a trajectory between S and T , which stays "as close to the sensors" as possible. The distance of a point P to the sensor network is defined as the smallest Euclidean distance from P to one of the sensor nodes. A maximum breach path from S to T is a path from S to T such that the minimum distance from a point P in the path to the sensor network is maximized: This distance is called the worst-case coverage distance of the network. Similarly, a maximum support path from S to T is a path such that the maximum distance of a point P in the path to the sensor network is minimized: This distance is called the best-case coverage distance of the network.
We consider this problem of covering an entire trajectory using two sensors only, where each of the sensors should be located on opposite sides of the trajectory. This problem is an extension of the well-studied two-center problem, which we describe in the next section "Two-sensor-problem". We O n time algorithm for this problem, improving on the exhaustive search bound of 3 ( ) O n . The solution proposed is of interest on its own, since it establishes an interesting relation to the matrix multiplication problem. In the section "Two-sensor-problem" we define our problem formally and give an efficient solution for it.

Two-sensor problem
We consider the following problem: There are two groups of sensors A and B of total size n divided by a polygonal xy -monotone path P containing n edges, such that each group is located on opposite sides of P . A path Each sensor i s has its covering area radius i R , so it can detect any object at a distance at most i R from it. We are interested in determining whether there exists a sensor from group A and a sensor from group B that cover the entire path P . The path P is playing role of a possible way for intruder penetration inside the sensors area and each group of sensors wants to catch the intruder while it is important to keep a visual guard of him all the time. We will refer to our problem as the two-sensor problem. Some similar problem has been considered by Huang and Tseng [2], who tried to cover a target area by k sensors from a set consisting of n sensors. Clearly, our task can be performed in O n runtime algorithm based on matrix multiplication and Matoušek algorithm [3] for computing dominance in n -dimensional space. The two-sensor problem naturally extends a list of optimization problems related to the famous two-center problem. In the two-center problem, we want to cover a set S of n points on the plane by two disks of smallest possible common radius. Agarwal and Sharir give an 2 ( log ) O n n -time algorithm in [4] for determining whether S can be covered by two disks of radius r . Plugging this algorithm into the parametric search machinery, one obtains an 2 3 ( log ) O n n -time algorithm for the two-center problem. The runtime of the decision algorithm of Agarwal and Sharir was improved by Hershberger [5]  ( log ) O n n -time algorithm for the discrete two-center problem, where the disks should be centered at the input points. Shin et al. [11] considered the problem of covering convex polygons using two disks of smallest possible radius by giving two algorithms: The first algorithm runs in time 3 ( log ) O n n and assumes that the disks are constrained to be centered at the input points; the second algorithm runs in 2 3 ( log ) O n n time and assumes arbitrary disks location. Huang et al. [12] considered a variation of the two-center problem, where the distance between two solution disks should be below some given constant, providing a 2 2 ( log ) O n n runtime algorithm for this problem.
The two-sensor problem considered in this paper is harder than all of the related variations of the two-center problem in the literature. The hardness comes from two sources: First, we need to cover the entire path and not just a set of discrete points; second, in the solution obtained, an edge may be partially covered by each of the sensors, implying that the sets of edges covered by each sensor may overlap significantly and, therefore, a simple binary search can no longer be used. We follow the notation used by Matoušek [3]. Let X be an × n n matrix of real numbers; we will use the notation , * i x for the i -th row of X ; we say that , * Matoušek [3] presents an algorithm for computing an × n n matrix C , whose element ,

O n .
In what follows, we show how to apply Matoušek's algorithm in order to get a solution to our problem. We start with the following observation, which is crucial for the solution of the 2-sensor problem.

Observation 1. Given an ×
n n matrix of real numbers X and ∈ n h R , we can determine whether there exists two rows in X , , * i x and , * j x such that , … n using Matoušek's algorithm.

1.
We define a new, 2 2 × n n matrix ′ X as follows. The first n rows of ′ X are the rows of X followed by zeros in places 1 2 + , , n … n. The next n rows of ′ X are defined as follows. The element , We are interested in the quarter corresponding to C , i.e. in the submatrix [ The runtime remains as the runtime of Matoušek's algorithm.
We will use the above observation in order to solve the two-sensor problem.
we define an × n n matrix X in the following way: After we build the matrix X , we apply an algorithm for observation 1 with (1 1 1

Future work
In this paper, we present an efficient algorithm for covering a given path by two sensors. A challenging vein for future work is to consider approximations for the k -sensor problem, where 2 > k . The k -sensor problem, for general k , is NP-complete [14].


Quantum Computing and Hidden Variables I: Mapping Unitary to Stochastic Matrices

This paper initiates the study of hidden variables from the discrete, abstract perspective of quantum computing. For us, a hidden-variable theory is simply a way to convert a unitary matrix that maps one quantum state to another, into a stochastic matrix that maps the initial probability distribution to the final one in some fixed basis. We list seven axioms that we might want such a theory to satisfy, and then investigate which of the axioms can be satisfied simultaneously. Toward this end, we construct a new hidden-variable theory that is both robust to small perturbations and indifferent to the identity operation, by exploiting an unexpected connection between unitary matrices and network flows. We also analyze previous hidden-variable theories of Dieks and Schrodinger in terms of our axioms. In a companion paper, we will show that actually sampling the history of a hidden variable under reasonable axioms is at least as hard as solving the Graph Isomorphism problem; and indeed is probably intractable even for quantum computers.

Introduction
Quantum mechanics lets us calculate the probability that (say) an electron will be found in an excited state if measured at a particular time. But it is silent about multiple-time or transition probabilities: that is, what is the probability that the electron will be in an excited state at time t 1 , given that it was in its ground state at an earlier time t 0 ? The usual response is that this question is meaningless, unless of course the electron was measured (or otherwise known with probability 1) to be in its ground state at t 0 . A different response-pursued by Schrödinger [22], Bohm [5], Bell [3], Nelson [19], Dieks [10], and others-treats the question as provisionally meaningful, and then investigates how one might answer it mathematically. Specific attempts at answers are called "hidden-variable theories." The appeal of hidden-variable theories is that they provide one possible solution to the measurement problem. For they allow us to apply unitary quantum mechanics to the entire universe (including ourselves), yet still discuss the probability of a future observation conditioned on our current observations. Furthermore, they let us do so without making any assumptions about decoherence or the nature of observers. For example, even if an observer were placed in coherent superposition, that observer would still have a sequence of definite experiences, and the probability of any such sequence could be calculated.
This paper initiates the study of hidden variables from a quantum computing perspective. We restrict our attention to the simplest possible setting: that of discrete time, a finite-dimensional Hilbert space, and a fixed orthogonal basis. Within this setting, we reformulate known hiddenvariable theories due to Dieks [10] and Schrödinger [22], and also introduce a new theory based on network flows. However, our main contribution is the axiomatic approach that we use. We propose seven axioms for hidden-variable theories in our setting, and then compare theories against each other based on which of the axioms they satisfy. A central question in this approach is which subsets of axioms can be satisfied simultaneously.
In a companion paper [1], we will make the connection to quantum computing explicit, by proving that under any hidden-variable theory that satisfies three reasonable axioms (called symmetry, indifference, and robustness), the ability to examine one's entire "history" through a quantum system would entail the ability to solve the Graph Isomorphism problem in polynomial time. What makes this result surprising is that, in the so-called oracle or black-box model, sampling histories would not entail the ability to solve NP-complete problems in polynomial time. We thus obtain the first good example of a computational model that appears "slightly" more powerful than the usual quantum computing model. This paper lays the groundwork for the computational results of [1], in particular by showing that there exists a hidden-variable theory satisfying the symmetry, indifference, and robustness axioms.
The paper is organized as follows. Section 1.1 formally defines hidden-variable theories in our sense; then Section 1.2 contrasts these theories with related ideas such as Bohmian mechanics and modal interpretations. Section 1.3 addresses the most common objections to our approach: for example, that the implicit dependence on a fixed basis is unacceptable.
In Section 2, we introduce seven possible axioms for hidden-variable theories. These are symmetry under permutation of basis states; indifference to the identity operation; robustness to small perturbations; "block robustness," a weaker version of robustness; commutativity with respect to spacelike-separated unitaries; commutativity for the special case of product states; and invariance under decomposition of mixed states into pure states. Ideally, a theory would satisfy all of these axioms. However, we show in Section 3 that no theory satisfies both indifference and commutativity; no theory satisfies both indifference and a stronger version of robustness; no theory satisfies indifference, robustness, and decomposition invariance; and no theory satisfies a stronger version of decomposition invariance. The proofs of two of these results use the same geometric facts that underlie the Bell inequalities.
In Section 4 we shift from negative to positive results. Section 4.1 presents a hidden-variable theory called the flow theory or FT , which is based on the Max-Flow-Min-Cut theorem from combinatorial optimization. The idea is to define a network of "pipes" from basis states at an initial time to basis states at a final time, and then route as much probability mass as possible through these pipes. The capacity of each pipe depends on the corresponding entry of the unitary acting from the initial to final time. To find the probability of transitioning from basis state |i to basis state |j , we then determine how much of the flow originating at |i is routed along the pipe to |j . Our main results are that FT is well-defined and that it is robust to small perturbations. Since FT trivially satisfies the indifference axiom, this implies that the indifference and robustness axioms can be satisfied simultaneously, which was not at all obvious a priori. The flow theory also satisfies symmetry, but not product commutativity, scalar invariance, or decomposition invariance. Section 4.2 presents a second theory that we call the Schrödinger theory or ST , since it is based on a pair of integral equations introduced in a 1931 paper of Schrödinger [22]. Schrödinger conjectured, but was unable to prove, the existence and uniqueness of a solution to these equations; the problem was not settled until the work of Nagasawa [18] in the 1980's. In our discrete setting the problem is simpler, and we give a self-contained proof of existence using a matrix scaling technique due to Sinkhorn [23]. The idea is as follows: we want to convert a unitary matrix that maps one quantum state to another, into a nonnegative matrix whose i th column sums to the initial probability of basis state |i , and whose j th row sums to the final probability of basis state |j . To do so, we first replace each entry of the unitary matrix by its absolute value, then normalize each column to sum to the desired initial probability, then normalize each row to sum to the desired final probability. But then the columns are no longer normalized correctly, so we normalize them again, then normalize the rows again, and so on. We show that this iterative process converges, from which it follows that ST is well-defined. We also show that ST satisfies the symmetry, indifference, and product commutativity axioms; and violates the decomposition invariance axiom. We conjecture that ST satisfies the robustness axiom; proving that conjecture is the main open problem of the paper. We conclude in Section 5.

Hidden-Variable Theories
Suppose we have an N × N unitary matrix U , acting on a state where |1 , . . . , |N is a standard orthogonal basis. Let Then can we construct a stochastic matrix S, which maps the vector of probabilities induced by measuring |ψ , to the vector induced by measuring U |ψ ? Trivially yes. The following matrix maps any vector of probabilities to − → q , ignoring the input vector − → p entirely: Here PT stands for product theory. The product theory corresponds to a strange picture of physical reality, in which memories and records are completely unreliable, there being no causal connection between states of affairs at earlier and later times. So we would like S to depend on U itself somehow, not just on |ψ and U |ψ . Indeed, ideally S would be a function only of U , and not of |ψ . But this is impossible, as the following example shows. Let U be a π/4 rotation, and let |+ = (|0 + |1 ) / On the other hand, it is easy to see that, if S can depend on |ψ as well as U , then there are infinitely many choices for the function S (|ψ , U ). Every choice reproduces the predictions of quantum mechanics perfectly when restricted to single-time probabilities. So how can we possibly choose among them? Our approach in Sections 2 and 4 will be to write down axioms that we would like S to satisfy, and then investigate which of the axioms can be satisfied simultaneously.
Formally, a hidden-variable theory is a family of functions {S N } N ≥1 , where each S N maps an N -dimensional mixed state ρ and an N × N unitary matrix U onto a singly stochastic matrix S N (ρ, U ). We will often suppress the dependence on N , and use subscripts such as PT or FT to indicate the theory in question. Also, if ρ = |ψ ψ| is a pure state we may write S (|ψ , U ) instead of S (|ψ ψ| , U ).
Let (M ) ij denote the entry in the i th column and j th row of matrix M . Then (S) ij is the probability that the hidden variable takes value |j after U is applied, conditioned on it taking value |i before U is applied. At a minimum, any theory must satisfy the following marginalization axiom: for all j ∈ {1, . . . , N }, This says that after U is applied, the hidden variable takes value |j with probability U ρU −1 jj , which is the usual Born probability.
Often it will be convenient to refer, not to S itself, but to the matrix P (ρ, U ) of joint probabilities whose (i, j) entry is (P ) ij = (S) ij (ρ) ii . The i th column of P must sum to (ρ) ii , and the j th row must sum to U ρU −1 jj . Indeed, we will define the theories FT and ST by first specifying the matrix P , and then setting (S) ij := (P ) ij / (ρ) ii . This approach has the drawback that if (ρ) ii = 0, then the i th column of S is undefined. To get around this, we adopt the convention that where ρ ε = (1 − ε) ρ + εI and I is the N × N maximally mixed state. Technically, the limits lim ε→0 + (P (ρ ε , U )) ij (ρ ε ) ii might not exist, but in the cases of interest to us it will be obvious that they do.

Comparison with Previous Work
Before going further, we should contrast our approach with previous approaches to hidden variables, the most famous of which is Bohmian mechanics [5]. Our main criticism of Bohmian mechanics is that it commits itself to a Hilbert space of particle positions and momenta. Furthermore, it is crucial that the positions and momenta be continuous, in order for particles to evolve deterministically. To see this, let |L and |R be discrete positions, and suppose a particle is in state |L at time t 1 , and state (|L + |R ) / √ 2 at a later time t 2 . Then a hidden variable representing the position would have entropy 0 at t 1 , since it is always |L then; but entropy 1 at t 2 , since it is |L or |R both with 1/2 probability. Therefore the earlier value cannot determine the later one. 1 It follows that Bohmian mechanics is incompatible with the belief that all physical observables are discrete. But in our view, there are strong reasons to hold that belief, which include black hole entropy bounds; the existence of a natural minimum length scale (10 −33 cm); results on area quantization in quantum gravity [21]; the fact that many physical quantities once thought to be continuous have turned out to be discrete; the infinities of quantum field theory; the implausibility of analog "hypercomputers"; and conceptual problems raised by the independence of the continuum hypothesis.
Of course there exist stochastic analogues of Bohmian mechanics, among them Nelsonian mechanics [19] and Bohm and Hiley's "stochastic interpretation" [6]. But it is not obvious why we should prefer these to other stochastic hidden-variable theories. From a quantum-information perspective, it is much more natural to take an abstract approach-one that allows arbitrary finitedimensional Hilbert spaces, and that does not rule out any transition rule a priori.
Stochastic hidden variables have also been considered in the context of modal interpretations; see Dickson [8], Bacciagaluppi and Dickson [2], and Dieks [10] for example. However, the central assumptions in that work are extremely different from ours. In modal interpretations, a pure state evolving unitarily poses no problems at all: one simply rotates the hidden-variable basis along with the state, so that the state always represents a "possessed property" of the system in the current basis. Difficulties arise only for mixed states; and there, the goal is to track a whole set of possessed properties. By contrast, our approach is to fix an orthogonal basis, then track a single hidden variable that is an element of that basis. The issues raised by pure states and mixed states are essentially the same.
Finally we should mention the consistent-histories interpretation of Griffiths [16] and Gell-Mann and Hartle [14]. This interpretation assigns probabilities to various histories through a quantum system, so long as the "interference" between those histories is negligible. Loosely speaking, then, the situations where consistent histories make sense are precisely the ones where the question of transition probabilities can be avoided.

Objections
Hidden-variable theories, as we define them, are open to several technical objections. For example, we required transition probabilities for only one orthogonal observable. What about other observables? The problem is that, according to the Kochen-Specker theorem, we cannot assign consistent values to all observables at any single time, let alone give transition probabilities for those values. This is an issue in any setting, not just ours. The solution we prefer is to postulate a fixed orthogonal basis of "distinguishable experiences," and to interpret a measurement in any other basis as a unitary followed by a measurement in the fixed basis. As mentioned in Section 1.2, modal interpretations opt for a different solution, which involves sets of bases that change over time with the state itself. It might be interesting to combine the approaches.
Another objection is that the probability of transitioning from basis state |i at time t 1 to basis state |j at time t 2 might depend on how finely we divide the time interval between t 1 and t 2 . In other words, for some state |ψ and unitaries V, W , we might have (a similar point was made by Gillespie [15]). Indeed, this is true for any hidden-variable theory other than the product theory PT . To see this, observe that for all unitaries U and states |ψ , there exist unitaries V, W such that U = W V and V |ψ = |1 . Then applying V destroys all information in the hidden variable (that is, decreases its entropy to 0); so if we then apply W , then the variable's final value must be uncorrelated with the initial value. In other words, S (V |ψ , W ) S (|ψ , V ) must equal S PT (|ψ , U ). It follows that to any hidden-variable theory we must associate a time scale, or some other rule for deciding when the transitions take place.
In our defense, let us point out that exactly the same problem arises in continuous-time stochastic hidden-variable theories. For if a state |ψ is governed by the Schrödinger equation d |ψ /dt = iH t |ψ , and a hidden variable's probability distribution − → p is governed by the stochastic Finally, it will be objected that we have ignored special relativity. In Section 2 we will define a commutativity axiom, which informally requires that the stochastic matrix S not depend on the temporal order of spacelike separated events. Unfortunately, we will see that when entangled states are involved, commutativity is irreconcilable with another axiom that seems even more basic. The resulting nonlocality has the same character as the nonlocality of Bohmian mechanics-that is, one cannot use it to send superluminal signals in the usual sense, but it is unsettling nonetheless.

Axioms for Hidden-Variable Theories
We now state seven axioms that we would like hidden-variable theories to satisfy.
Symmetry. A theory is symmetric if it is invariant under relabeling of basis states: that is, if for all ρ, U and all permutation matrices Q, All theories discussed in this paper are symmetric.
Indifference. Suppose we partition the basis states into 'blocks,' between which U can never produce interference. Call an ordered pair I, J of subsets of {1, . . . , N } a block if (U ) ij = 0 for all i ∈ I and j / ∈ J, as well as all i / ∈ I and j ∈ J. Also, call I, J a minimal block if |I| = |J| and no I * , J * with I * ⊂ I and J * ⊂ J is a block. Note that if I 1 , J 1 , . . . , I m , J m are the minimal blocks, then both {I 1 , . . . , I m } and {J 1 , . . . , J m } are partitions of {1, . . . , N }. We say a theory is indifferent if it never produces interference between minimal blocks-that is, if (S) ij = 0 for all i, j in different minimal blocks. In particular, indifference implies that given any state ρ in a tensor product space H A ⊗ H B , and any unitary U that acts only on H A (that is, is the identity on H B ), the stochastic matrix S (ρ, U ) acts only on H A as well.
Robustness. A theory is robust if it is insensitive to small errors in a state or unitary (which, in particular, implies continuity). Suppose we obtain ρ and U by making small changes to ρ and U respectively. Then for all polynomials p, there should exist a polynomial q such that for all N , where M = max ij (M ) ij , whenever ρ − ρ ≤ 1/q (N ) and U − U ≤ 1/q (N ). Robustness has an important advantage for quantum computing: if a hidden-variable theory is robust then the set of gates used to define the unitaries U 1 , . . . , U T is irrelevant, since by the Solovay-Kitaev Theorem (see [20]), any universal quantum gate set can simulate any other to a precision ε with O (log c 1/ε) overhead.
Block Robustness. Unfortunately, one of the theories that we wish to study does not satisfy robustness. We therefore define a weaker notion of robustness that this theory satisfies. We say a hidden-variable theory is block robust if robustness holds for all modifications ρ, U → ρ, U such that U and U have the same set I 1 , J 1 , . . . , I m , J m of minimal blocks.
Commutativity. Let ρ AB be a bipartite state, and let U A and U B act only on subsystems A and B respectively. Then commutativity means that the order in which U A and U B are applied is irrelevant: of ρ into pure states. Theorem 2, part (ii) will show that the analogous axiom for P (ρ, U ) is unsatisfiable.

Comparing Hidden-Variable Theories
To fix ideas, let us compare some hidden-variable theories with respect to the above axioms. We have already seen the product theory PT in Section 1.1. It is easy to show that PT satisfies symmetry, robustness, commutativity, and decomposition invariance. However, we consider PT unsatisfactory because it violates indifference: even if a unitary U acts only on the first of two qubits, S PT (ρ, U ) will readily produce transitions between (say) |00 and |01 , or between |01 and |10 .
Recognizing this problem, Dieks [10] proposed an alternative theory that in our terminology corresponds to the following. 2 First find the minimal blocks I 1 , J 1 , . . . , I m , J m of U . Then apply the product theory separately to each minimal block; that is, if i and j belong to the same block I, J then set and otherwise set (S) ij = 0. The resulting Dieks theory, DT , clearly satisfies indifference. However, it does not satisfy robustness (or even continuity), since the set of minimal blocks can change if we replace '0' entries in U by arbitrarily small nonzero entries. In Section 4 we will introduce two other hidden-variable theories, the flow theory FT and the Schrödinger theory ST . The following table lists which axioms the four theories satisfy.

Impossibility Results
This section shows that certain sets of axioms cannot be satisfied by any hidden-variable theory. We first show that the failure of DT , FT , and ST to satisfy commutativity is inherent, and not a fixable technical problem.

Theorem 1 No hidden-variable theory satisfies both indifference and commutativity.
Proof. Assume indifference holds, and let our initial state be |ψ = (|00 + |11 ) / √ 2. Suppose U A applies a π/8 rotation to the first qubit, and U B applies a −π/8 rotation to the second qubit. Then Let v t be the value of the hidden variable after t unitaries have been applied. Let E be the event that v 0 = |00 initially, and v 2 = |10 at the end. If U A is applied before U B , then the unique 'path' from v 0 to v 2 consistent with indifference sets v 1 = |10 . So But if U B is applied before U A , then the probability that v 0 = |11 and v 2 = |10 is at most 1 2 sin 2 π 8 , by the same reasoning. Thus, since v 2 must equal |10 with probability 1/4, and since the only possibilities for v 0 are |00 and |11 , We conclude that commutativity is violated. Let us remark on the relationship between Theorem 1 and Bell's Theorem. Any hiddenvariable theory that is "local" in Bell's sense would immediately satisfy both indifference and commutativity. However, the converse is not obvious, since there might be nonlocal information in the states U A |ψ or U B |ψ , which an indifferent commutative theory could exploit but a local one could not. Theorem 1 rules out this possibility, and in that sense is a strengthening of Bell's Theorem.
The next result places limits on decomposition invariance.
(ii) No theory has the property that Proof.
Our last impossibility result says that no hidden-variable theory satisfies both indifference and "strong continuity," in the sense that for all ε > 0 there exists This is the reason why we defined robustness in terms of the joint probabilities matrix P rather than the stochastic matrix S. On the other hand, note that by giving up indifference, we can satisfy strong continuity, as is shown by FT .

Specific Theories
This section presents the main results of the paper, which concern two nontrivial examples of hidden-variable theories: the flow theory in Section 4.1, and the Schrödinger theory in Section 4.2.

Flow Theory
The idea of the flow theory is to convert a unitary matrix into a weighted directed graph, and then route probability mass through that graph like oil through pipes. Given a unitary U , let    are pure states. Then consider the network G shown in Figure 1. We have a source vertex s, a sink vertex t, and N input and N output vertices labeled by basis states |1 , . . . , |N . Each edge of the form (s, |i ) has capacity |α i | 2 , each edge (|i , |j ) has capacity (U ) ij , and each edge (|j , t) has capacity |β j | 2 . A natural question is how much probability mass can flow from s to t without violating the capacity constraints. Rather surprisingly, we show that one unit of mass (that is, all of it) can. Interestingly, this result would be false if edge (|i , |j ) had capacity (U ) ij 2 (or even (U ) ij 1+ε ) instead of (U ) ij . We also show that there exists a mapping from networks to maximum flows in those networks, that is robust in the sense that a small change in edge capacities produces only a small change in the amount of flow through any edge.
The proofs of these theorems use classical results from the theory of network flows (see [7] for an introduction). In particular, let a cut be a set of edges that separates s from t; the value of a cut is the sum of the capacities of its edges. Then a fundamental result called the Max-Flow-Min-Cut Theorem [11] says that the maximum possible amount of flow from s to t equals the minimum value of any cut.
Theorem 3 One unit of flow can be routed from s to t in G.
Proof. By the above, it suffices to show that any cut C in G has value at least 1. Let A be the set of i ∈ {1, . . . , N } such that (s, |i ) / ∈ C, and let B be the set of j such that (|j , t) / ∈ C. Then C must contain every edge (|i , |j ) such that i ∈ A and j ∈ B, and we can assume without loss of generality that C contains no other edges. So the value of C is Therefore we need to prove the matrix inequality Let U be fixed, and consider the maximum of the right-hand side over all |ψ . Since So letting θ be the angle between H A and H B , λ = 2 cos 2 θ 2 = 1 + cos θ which completes the theorem. Observe that Theorem 3 still holds if U acts on a mixed state ρ, since we can write ρ as a convex combination of pure states |ψ ψ|, construct a flow for each |ψ separately, and then take a convex combination of the flows.
Using Theorem 3, we now define the flow theory FT . Let F (ρ, U ) be the set of maximum flows for ρ, U -representable by N × N arrays of real numbers f ij such that 0 ≤ f ij ≤ (U ) ij for all i, j, and also Clearly F (ρ, U ) is a convex polytope, which Theorem 3 asserts is nonempty. Form a maximum flow f * (ρ, U ) ∈ F (ρ, U ) as follows: first let f * 11 be the maximum of f 11 over all f ∈ F (ρ, U ). Then let f * 12 be the maximum of f 12 over all f ∈ F (ρ, U ) such that f 11 = f * 11 . Continue to loop through all i, j pairs in lexicographic order, setting each f * ij to its maximum possible value consistent with the (i − 1) N + j − 1 previous values.
We define the joint probabilities matrix P by "symmetrizing" f * (ρ, U ) over permutations of basis states-that is, where Q ranges over all N × N permutation matrices. As discussed in Section 1.1, given P we can easily obtain the stochastic matrix S by dividing the i th column by (ρ) ii , or taking a limit in case (ρ) ii = 0. It is easy to check that FT so defined satisfies the symmetry and indifference axioms. Showing that FT satisfies robustness is harder. Our proof is based on the Ford-Fulkerson algorithm [11], a classic algorithm for computing maximum flows that works by finding a sequence of "augmenting paths," each of which increases the flow from s to t by some positive amount.

Theorem 4 FT satisfies robustness.
Proof. Let G be an arbitrary flow network with source s, sink t, and directed edges e 1 , . . . , e m , where each e i has capacity c i and leads from v i to w i . It will be convenient to introduce a fictitious edge e 0 from t to s with unlimited capacity; then maximizing the flow through G is equivalent to maximizing the flow through e 0 . Suppose we produce a new network G by increasing a single capacity c i * by some ε > 0. Let f * be the optimal flow for G, obtained by first maximizing the flow f 0 through e 0 , then maximizing the flow f 1 through e 1 holding f 0 fixed, and so on up to f m . Let f * be the maximal flow for G produced in the same way. We claim that for all i ∈ {0, . . . , m}, To see that the theorem follows from this claim: first, if f * is robust under adding ε to c i * , then it must also be robust under subtracting ε from c i * . Second, if we change ρ, U to ρ, U such that ρ − ρ ≤ 1/q (N ) and U − U ≤ 1/q (N ), then we can imagine the N 2 + 2N edge capacities are changed one by one, so that (Here we have made no attempt to optimize the bound.) Third, symmetrizing over all row and column permutations can only decrease P − P , not increase it.
We now prove to the claim. To do so we describe an iterative algorithm for computing f * . First maximize the flow f 0 through e 0 , by using the Ford-Fulkerson algorithm [11] to find a maximum flow from s to t. Let f (0) be the resulting flow, and let G (1) be the residual network that corresponds to f (0) . For each i, that is, G (1) has an edge e i = (v i , w i ) of capacity c i , and an edge i . Next maximize f 1 subject to f 0 by using the Ford-Fulkerson algorithm to find "augmenting cycles" from w 1 to v 1 and back to w 1 in G (1) \ {e 0 , e 0 }. Continue in this manner until each of f 1 , . . . , f m has been maximized subject to the previous f i 's. Finally set f * = f (m) . Now, one way to compute f * is to start with f * , then repeatedly "correct" it by applying the same iterative algorithm to maximize f 0 , then f 1 , and so on. Let ε i = f * i − f * i ; then we need to show that ε i ≤ ε for all i ∈ {0, . . . , m}. The proof is by induction on i. Clearly ε 0 ≤ ε, since increasing c i * by ε can increase the value of the minimum cut from s to t by at most ε. Likewise, after we maximize f 0 , the value of the minimum cut from w 1 to v 1 can increase by at most ε − ε 0 + ε 0 = ε. For of the at most ε new units of flow from w 1 to v 1 that increasing c i * made available, ε 0 of them were "taken up" in maximizing f 0 , but the process of maximizing f 0 could have again increased the minimum cut from w 1 to v 1 by up to ε 0 . Continuing in this way, and so on up to ε m . This completes the proof.

Schrödinger Theory
Our final hidden-variable theory, which we call the Schrödinger theory or ST , is the most interesting one mathematically. The idea-to make a matrix into a stochastic matrix via an iterative process of row and column rescaling-is natural enough that we came upon it independently, only later learning that it originated in a 1931 paper of Schrödinger [22]. Schrödinger gave a pair of functional integral equations that such an iterative process would solve, but was unable to prove that those equations always have a solution. The existence and uniqueness of a solution were shown under broad conditions by Nagasawa [18], building on earlier work of Fortet [12] and Beurling [4]. Our goal is to give what (to our knowledge) is the first self-contained, reasonably accessible presentation of the main result in this area; and to interpret that result in what we think is the correct way: as providing one example of a hidden-variable theory, whose strengths and weaknesses should be directly compared to those of other theories.
Most of the technical difficulties in [4,12,18,22] arise because the stochastic process being constructed involves continuous time and particle positions. Here we eliminate those difficulties by restricting attention to discrete time and to finite-dimensional Hilbert spaces. We thereby obtain a generalized version 3 of a problem that computer scientists know as (r, c)-scaling of matrices. Sinkhorn [23] gave an algorithm for the (r, c)-scaling problem, which was shown to run in polynomial time by Franklin and Lorenz [13] (see also Linial, Samorodnitsky, and Wigderson [17]).
As in the case of the flow theory, given a unitary U acting on a state ρ, the first step is to replace each entry of U by its absolute value, obtaining the nonnegative matrix U (0) defined by U (0) ij := (U ) ij . We then repeatedly tweak U (0) to bring it closer to a joint probabilities matrix P (ρ, U ). We want to make the i th column of the matrix sum to (ρ) ii , and the j th row sum to U ρU −1 jj for all i, j ∈ {1, . . . , N }. The stochastic matrix S (ρ, U ) is then readily obtained by normalizing each column to sum to 1.
The algorithm is iterative. For each t ≥ 0 we obtain U (2t+1) by normalizing each column i of U (2t) to sum to (ρ) ii ; likewise we obtain U (2t+2) by normalizing each row j of U (2t+1) to sum to U ρU −1 jj . More formally, The crucial fact is that the above iteration converges. Our proof will reuse a result about network flows from Section 4.1, in order to define a nondecreasing "progress measure" based on Kullback-Leibler distance.
Given any such array, define a progress measure where we adopt the convention 0 0 = 1. We claim that Z (t+1) ≥ Z (t) for all t ≥ 1. To see this, assume without loss of generality that we are on an odd step 2t + 1, and let C ij be the i th column sum before we normalize it. Then As a result of the 2t th normalization step, we had i C (2t) i = 1. Subject to that constraint, the maximum of ii for all i-a simple calculus fact that follows from the nonnegativity of Kullback-Leibler distance. This implies that Z (2t+1) ≥ Z (2t) . Similarly, normalizing rows leads to Z (2t+2) ≥ Z (2t+1) .
It follows that the limit U (∞) = lim t→∞ U (t) exists. For suppose not; then some C (t) i is bounded away from (ρ) ii , so there exists an ε > 0 such that Z (t+1) ≥ (1 + ε) Z (t) for all even t. But this is a contradiction, since Z (0) > 0 and Z (t) ≤ 1 for all t.
It is immediate that ST satisfies symmetry and indifference. Let us show that it satisfies product commutativity as well.
Proof. Given a state |ψ = |ψ A ⊗ |ψ B , let U A ⊗ I act only on |ψ A and let I ⊗ U B act only on |ψ B . Then we claim that S (|ψ , U A ⊗ I) = S (|ψ A , U A ) ⊗ I.
The reason is simply that multiplying all amplitudes in |ψ A and U A |ψ A by a constant factor α x , as we do for each basis state |x of |ψ B , has no effect on the scaling procedure that produces S (|ψ A , U A ). Similarly S (|ψ , I ⊗ U B ) = I ⊗ S (|ψ B , U B ) . On the other hand, let us show that ST violates decomposition invariance. Using the same notation as in Section 4.1, we have R π/8 IR −1 π/8 = I, R π/8 ϕ π/8 = ϕ π/4 , and R π/8 ϕ 5π/8 = ϕ 3π/4 , from which it can be calculated that

Discussion
The idea that certain observables in quantum mechanics might have trajectories governed by dynamical laws has reappeared many times: in Schrödinger's 1931 stochastic approach [22], Bohmian mechanics [5], modal interpretations [2,8,10], and elsewhere. Yet because all of these proposals yield the same predictions for single-time probabilities, if we are to decide between them it must be on the basis of internal mathematical considerations. A main message of this paper has been that such considerations can actually get us quite far. To focus attention on the core issues, we restricted attention to the simplest possible setting: discrete time, a finite-dimensional Hilbert space, and a single orthogonal basis. Within this setting, we proposed what seem like reasonable axioms that any hidden-variable theory should satisfy: for example, symmetry under permutation of basis states, robustness to small perturbations, and independence of the temporal order of spacelike-separated events. We then showed that not all of these axioms can be satisfied simultaneously. But perhaps more surprisingly, we also showed that certain subsets of axioms can be satisfied for highly nontrivial reasons. In showing that the indifference and robustness axioms can be simultaneously satisfied, Section 4 revealed an unexpected connection between unitary matrices and the classical theory of network flows.
As mentioned previously, the most important open problem is to show that the Schrödinger theory satisfies robustness. Currently, we can only show that the matrix P ST (ρ, U ) is robust to exponentially small perturbations, not polynomially small ones. The problem is that if any row or column sum in the U (t) matrix is extremely small, then the (r, c)-scaling process will magnify tiny errors in the entries. Intuitively, though, this effect should be washed out by later scaling steps.
A second open problem is whether there exists a theory that satisfies indifference, as well as commutativity for all separable mixed states (not just separable pure states). A third problem is to investigate other notions of robustness-for example, robustness to small multiplicative rather than additive errors.

Acknowledgments
I thank Umesh Vazirani, Ronald de Wolf, and an anonymous reviewer for comments on an earlier version of this paper; Dorit Aharonov, Guido Bacciagaluppi, John Preskill, and Avi Wigderson for helpful discussions; and Dennis Dieks for correspondence.