a variable v **with** pred(v) = {**u, w**}, v 0 = bv**, and** v
∗ = wv**. Recall that every operator in**
Λ
⊲⊳ **is presented as a three-tuple** hpre, post, prvi **of pre-, post-, and prevail conditions of the**
operator respectively. Suppose that:

σ(u) = b 1u · w 1u σ(w) = b 1w · w 1w · b 2w · w 2w  A1 v = {pre : {bv}, post : {wv}, prv : {bu,ww}} A2 v = {pre : {wv}, post : {bv}, prv : {bu, bw}} A3 v = {pre : {wv}, post : {bv}, prv : {wu,ww}} Λ ⊲⊳ v = 
For this case, the graph G(v**) is presented by Figure 2.**

![0_image_0.png](0_image_0.png)

$\mathrm{\text{\hspace{0.17em}}}\mathrm{\text{true}}\text{\hspace{0.17em}}$ 2. 
The constructed graph G(v) captures information about all potentially possible **executions of the operators in Λ**⊲⊳
v**that can provide us** MaxReq(v**) or less value changes of** v.

Each path, started at the source node of G(v**), uniquely corresponds to such an execution.**
Although the number of these alternative executions may be exponential in n, this graphical representation is compact: the number of edges in G(v) is O(n · |Λ
⊲⊳ v |**). Note that the**
information about the number of times that each operator in Λ⊲⊳
v**can be executed is not**
captured by G(v**). The following two steps add this information indirectly and exploit it to**
find a maximal sequence σ(v).

At the second step of construction, we expand G(v) with respect to the maximal sequences σ(w1), . . . , σ(wk) as follows: Each edge e ∈ G(v**) (which by definition corresponds**
to some operator A ∈ Λ
⊲⊳
v**), is replaced by a set of edges such that their labels correspond to**
all possible assignments of the elements of σ(w1), . . . , σ(wk) to l(e**) (i.e.,** prv(A**)). Likewise,**
we add a dummy source node sv, with an edge from sv **to the original source node of** G(v)
labeled by a tuple of the first elements of σ(w1), . . . , σ(wk) (= initial values of w1**, . . . , w**k).

Similarly, we add a dummy target node tv**, with an edge from the original target node of**
G(v) to tv labeled by a tuple of the last elements of σ(w1), . . . , σ(wk**) (= goal values of**
w1, . . . , wk). We denote this extended graph by G′(v), and Figure 3 illustrates G′(v**) for the**
example above.

The extended graph G′(v**) can be viewed as a projection of the maximal sequences** σ(wi),
1 ≤ i ≤ k, on the graph G(v). Each edge in G(v**) may be replaced by** O(n k**) edges in** G′(v),
and thus the number of edges in G′(v**) is** O(n k+1 · |Λ
⊲⊳
v|).

It is easy to see that not all paths in G′(v) starting at sv **are relevant. For example, in**
G′(v**) above, an operator instance prevailed by** b 1ub 2w **can not be performed after an operator**
instance prevailed by b 1uw 2w**. Thus, now we are faced with the problem of finding a longest**
feasible path from sv to a node in G′(v**), the label of which is consistent with** v
∗**. The**
following (last) step provides a reduction of the problem of **finding a longest feasible path**
from sv **to a** v
∗-colored node in G′(v**) to a known problem of finding a longest path in a**