of agent  if the number expressed in binary by set of boolean variables A used to
represent the actions of , is equal to p Propositional state variables are represented by a
single boolean variable, while numerical state variables are represented in binary by a set

The boolean variables are ordered with the input variables rst, followed by an interleaving

of boolean variables.

Let Ae1

$$A_{e_{1}},\ldots,A_{e|_{E}|}\qquad A_{s_{1}},\ldots,A_{s|_{E}|}$$
; : : : ; AsjSj denote sets of boolean variables used to represent vj and x0k vj denote the kth
the joint action of environment and system agents. Further, let xk
boolean variable used to represent state variable vj 2 SV in the current and next state.
of the boolean variables of current state and next state variables: Ae1      AejEj  As1      AsjSj  x1 v1  x01 v1      xm1 v1  x0m1 v1     x1 vn  x01 vn      xmn vn  x0mn vn ; where mi is the number of boolean variables used to represent state variable vi and n is equal to jSV j The construction of T is quite similar to the construction of T in Section 4.2. An obdd representing logical expression is built in the standard way (Bryant, 1986). To build an obdd A dening the constraints of the joint actions, we need to refer to Arithmetic expressions are represented as lists of obdds dening the corresponding binary number. They collapse to single obdds when related by arithmetic relations.

To build an obdd A dening the constraints of the joint actions, we need to refer to Arithmetic expressions are represented as lists of obdds dening the corresponding binary number. They collapse to single obdds when related by arithmetic relations. the values of the boolean variables representing the actions. Let i ) be the function that maps an agent  to the value of the boolean variables representing its action and let b a be the identier value of action a Further let P a) and E a) denote obdd representations of the precondition and eect formula of an action a A is then given by: a 2 d   i ) = b a P a E a  : A  2 Agt Note that logical operators now denote the corresponding obdd operators. An obdd representing the frame relation F changes in a similar way: v2SV  a 2 d  i ) = b a v 2 c a))) s 0 v sv  ; F  2 Agt where c a is the set of constrained variables of action a and sv s 0 v expresses that all current and next state boolean variables representing v are pairwise equal. The expression v 2 c a) evaluates to True or False and is represented by the obdd for True or False The action interference constraint I is given by: I 1; 2 2 S2 a1; a2 2 c 1; 2  i 1) = b a1 i 2 6 b a2  202

