the formulae that describe the preconditions and postconditions of operators as discussed in ection . . ll other formulae remain una ected.

onsider an operator with preconditions i n, and  2 =  12 n',' one of which is chosen nondeterministically.  The non determinism in the e ecution of this operator at time point is represented by a variable that is one of the universally  uantified variables.  f the operator is e ecuted at   and is true, then the operator has the ect 1, and if   is false, then the ect is  2. The generali ation to the case with more than two alternative e ects is obvious.

The frame a ioms and the formulae describing postconditions of operators have to be rewritten to re ect the nondeterminism. The changes make the e ects conditional on the variable 0 prec    =   1 n and postc   =   i n

i t →  n t it n' t +1 i t  n' 2

rame a  ioms in general are of the form the possible causes for the change of from false to true at . n ection . the only possible causes were the applications of operators that make true. hen adopting nondeterministic operators and spontaneous change in the environment, the causes for changes become more complicated.   onsider the frame a iom for a literal  that occurs in  1. Now one of the dis uncts i in the frame a iom is i.t where is the inde of the operator. f occurs in  2, then   i,t Nondeterministic change can be modeled by rules 1 2 that work like nondeter ministic operators e cept that one of the alternative e ects 1 or 2 becomes true always when the precondition is true. The formulae describing the ects of this kind of rules are obvious  the truth of   implies the truth of   at the ne t point of time when a variable representing the nondeterminism is true, and the truth of  2 when   is false. The construc tion of frame a  ioms for literals in   and     is modified like in the case of nondeterministic operators. or a literal in 1, the frame a iom contains a dis unct that is the con unction of and , and for literal in 2 the respective frame a ioms has a dis unct that is the con unction of   and

## 5. An Example

The complete uantified oolean formula for the block e ample developed in the preced ing sections is given ne t . This formula consists of a formali ation of plan e ecutions from ection . , formulae formali ing the plans from  ection . . , and formulae for  uantifi cation from ection . . . The preconditions and the postconditions of the operators are described by the following formulae for 0 o t → onAB t clearA t contableA t+1 ı¸¢ → onBA† clearB† ontableB†††
2 t → ontableA t clearB t onAB t +1 3 t → ontableB t clearA t onBAt+1 onABE+1   clearBE+1 onBAt+1  clearAt+1 clearBt+1 clear At +1

$$\operatorname{erf}2$$ $$o\,m4$$ $$o\,m4$$
$\large1t+2$  2. 
onta ble At +1 ontableBe+1