effect of DunkP1 and (arm ∧ clog ∧ ¬inP1 ∧ inP2) from the conditional effect of DunkP2, which reduces to BSP . Construction could stop here because BSP entails the label of the goal ℓ
∗ k
(¬arm∧¬clog)= ℓk(¬arm) ∧ ℓk(¬clog) = BSP ∧ BSP = BSP . However, level off occurs at the next level because there is no change in the labels of the literals.

When level off occurs at level three in our example, we can say that for any BS, where BS |=
BSP , that a formula f is reachable in k steps if BS |= ℓ
∗ k
(f). If no such level k exists, then f is not reachable from BS. If there is some level k, where f is reachable from BS, then the first such k is a lower bound on the number of parallel plan steps needed to reach f from BS. This lower bound is similar to the classical planning max heuristic (Nguyen et al., 2002). We can provide a more informed heuristic by extracting a relaxed plan to support f with respect to BS, described shortly.

## 4.4.2 Same-World Labelled Mutexes

There are several types of mutexes that can be added to the LUG. To start with, we only concentrate on those that can evolve in a single possible world because same-world mutexes are more effective as well as relatively easy to understand. We extend the mutex propagation that was used in the multiple graphs so that the mutexes are on one planning graph. The savings of computing mutexes on the LUG instead of multiple graphs is that we can reduce computation when a mutex exits in several worlds. In Appendix B we describe how to handle cross-world mutexes, despite their lack of effectiveness in the experiments we conducted. Cross-world mutexes extend the LUG to compute the same set of mutexes found by CGP (Smith & Weld, 1998).

Same-world mutexes can be represented with a single label, ˆℓk(x1, x2), between two elements
(actions, effect, or literals). The mutex holds between elements x1 and x2 in all worlds S where S |= ˆℓk(x1, x2). If the elements are not mutex in any world, we can assume the label of a mutex between them is false ⊥. We discuss how the labelled mutexes are discovered and propagated for actions, effect relations, and literals.

By using mutexes, we can refine what it means for a formula f to be reachable from a set of worlds BSP . We must ensure that for every state in BSP , there exists a state of f that is reachable.

A state S
′ of f is reachable from a state S of BSP when there are no two literals in S
′that are mutex in world S and BSP |= ℓ
∗ k
(S).

In each of the action, effect, and literal layers there are multiple ways for the same pair of elements to become mutex (e.g. interference or competing needs). Thus, the mutex label for a pair is the disjunction of all labelled mutexes found for the pair by some means.

Action Mutexes: The same-world action mutexes at a level k are a set of labelled pairs of actions.

Each pair is labelled with a formula that indicates the set of possible worlds where the actions are mutex. The possible reasons for mutex actions are interference and competing needs.

- **Interference** Two actions **a, a**′interfere if (1) the unconditional effect consequent ε 0(a) of one is inconsistent with the execution precondition ρ e(a
′) of the other, or (2) vice versa.

They additionally interfere if (3) both unconditional effect consequents ε 0(a) and ε 0(a
′) are inconsistent, or (4) both execution preconditions ρ e(a) and ρ e(a
′) are inconsistent. The mutex will exist in all possible world projections ˆℓk(a, a′) = BSP . Formally, a and a
′interfere if