
## Domain Btuc

ACTIONS Dunk_1, Dunk_2, Flush; FLUENTS In_1, In_2, Defused, Clogged : boolean; INERTIAL Clogged, Defused, In_1, In_2; ALWAYS In_1 <-> !In_2; Flush CAUSES !Clogged; for i in [1, 2] {
Dunk_<i> HAS PRECONDITIONS !Clogged; Dunk_<i> CAUSES Defused IF In_<i>;
Dunk_<i> POSSIBLY CHANGES Clogged; INITIALLY !Defused; CONFORMANT Defused & !Clogged; Figure 8: An AR description for the BTUC problem time.  The automaton corresponding to an AR description is obtained by means of the minimization procedure by Giunchiglia (1996). This procedure solves the frame problem and the ramification problem, and is efficiently implemented in MBP (Cimatti et al., 1997).

Because of the separation between the domain construction and the planning phases, MBP
is not bound to AR . Standard deterministic domains specified in P DDL (Ghallab et al., 1998) can also be given to MBP by means of a (prototype) compiler. We are also starting to investigate the potential use of the C action language (Giunchiglia & Lifschitz, 1998),
which allows to represent domains with parallel actions.

Different planning algorithms can be applied to the specified planning problems. They operate solely on the automaton representation, and are completely independent of the particular language used to specify the domain. MBP allows for automatic construction of conditional plans under total observability, by implementing the algorithms for strong planng (Cimatti et al., 1998b), and for strong cyclic plannig (Cimatti et al., 1998a; Daniele, Traverso, & Vardi, 1999). In CMBP, we implemented the ideas described in the previous sections. The primitives to construct and prune BsP tables required a lot of tuning, in particular with the ordering of BDD variables. We found a general ordering strategy which works reasonably well: action variables are positioned at the top of the ordering, followed by plan variables, followed by state variables, with current state and next state variables interleaved. The specific ordering within action variables, plan variables, and state variables is determined by the standard mechanism implemented in NUSMV . CMBP implements several algorithms for conformant planning. In addition to the backward algorithm presented in