two operators in the right subtree of  move fail to satisfy the accessibility condition is due to their having add as their second step The definition of add states that x prior to operator application  and therefore we have no guarantee of  3 s accessibility  given that 1 is accessible from an initial state The following are the definitions of the operators for which the accessibility condition is true Operator Schema 13 (Odelete+gen) Apply  delete to edge   1  2  and then apply  gen to edge   1   3  ·
As an example  in Figure    we can move the condition  a    b" from edge  STATE
STATE to edge STATE STATE to make R STATE STATE
and to make k STATE STATE   c a b This is deletion of edge STATE STATE 
followed by generalization of the transition condition on edge  STATE   STATE
Operator Schema 14 (Ospec+gen) Apply spec to edge   1   2  and then apply  gen to edge 1 3 ·
As an example  in Figure    we can move the disjunct  b" from edge  STATE
STATE
to edge STATE STATE to make K STATE STATE STATE S
a band k STATE
STATE
c   b  This is a specialization of the transition condition on edge  STATE
STATE    followed by a generalization of the transition condition on edge   STATE     STATE
Operator Schema 15 (Ostay) The definition is the same as that of  move, with one exception. Replace vertex 3 with vertex 1 everywhere. In other words, the operator consists of moving a condition from edge   1  2  to edge   1   1  ·
Note that each operator instantiation of the schema for   stay will be a special case of one of the following    delete+add   spec+add   delete+gen  Or   spec+gen  It is considered   stay if and only if on the second step of the operator the transition condition is moved to edge For example  using Figure    when we applied operator  spec+add  in the example above to move the disjunct  b" from edge  STATE   STATE   to edge  STATE  
STATE
to bband make b this could be considered an instantiation of  stay  as well as   spec+add   Likewise when we applied delete+add to delete edge  STATE   STATE   and add edge  STATE   STATE    with   c" as the transition condition this could also be considered an instantiation of a stay Operator stgy is an especially useful operator  It makes the reasonable assumption that when an agent no longer wants to transition to another state  e g  an edge is deleted the agent just stays in its current state In other words the condition for transitioning to another state is transferred to the edge leading back to the current state  For example suppose rover I becomes stuck at the lander and cannot rendezvous with F for an inde terminate period of time  It could generate a temporary plan  see Figure    that keeps I in its DELIVERING state by deleting edge  DELIVERING  RECEIVING  and making r DELIVERING  DELIVERING       and DELIVERING would have to become an initial state Recall that accessibility is a key issue for verification  Now that we have a set of op erator schemas  let us consider how these operators affect accessibility from initial states