\documentclass[twoside,11pt]{article}
\usepackage{jair}
\usepackage{theapa}
\input epsf %% at top of file
\usepackage{xspace}
\usepackage{epsfig}
\usepackage{amssymb}
\usepackage{amsbsy}
\usepackage{amsmath}
\usepackage{path}
\usepackage{subfigure}
\usepackage[dvips]{rotating}


\jairheading{13}{2000}{305-338}{6/00}{12/00}
\ShortHeadings{Conformant Planning via Symbolic Model Checking}
{Cimatti \& Roveri}
\firstpageno{305}

\title{Conformant Planning via Symbolic Model Checking}

\author{\name Alessandro Cimatti \email cimatti@irst.itc.it \\
       \addr \textsc{ITC-irst}, Via Sommarive 18, 38055 Povo, Trento, Italy \\
       \AND
       \name Marco Roveri \email roveri@irst.itc.it \\
       \addr \textsc{ITC-irst}, Via Sommarive 18, 38055 Povo, Trento, Italy \\
       \addr DSI, University of Milano, Via Comelico 39, 20135 Milano, Italy
}


%%% Figure and tables positioning
\def\topfraction{0.75}
\def\bottomfraction{0.65}
\def\totalnumber{1}

% PAPER CONTROL MACROS

\hyphenation{Giun-chi-glia So-men-zi}

% MACROS
\newtheorem{definition}{Definition}
\newtheorem{lemma}{Lemma}
\newtheorem{theorem}{Theorem}
\newtheorem{proof}{Proof}

\newcommand{\tlim}{{---}\xspace}
\newcommand{\mlim}{{$=\!\!\!=\!\!\!=$}\xspace}
\newcommand{\sizeof}[1]{\ensuremath{|#1|}}
\newcommand{\trans}[3]{\ensuremath{#1{\stackrel{\rightarrow}{#2}}{#3}}}
\newcommand{\substwith}[2]{\ensuremath{[#1/#2]}}
\newcommand{\imbox}[1]{\mbox{\itshape #1}}
\newcommand{\eqbydef}{\ensuremath{{{\ \dot{=}\ }}}}
\newcommand{\truth}{\ensuremath{{True}}}
\newcommand{\falsity}{\ensuremath{{False}}}
\newcommand{\liff}{\ensuremath{\leftrightarrow}}
\newcommand{\imp}{\ensuremath{\rightarrow}}
\newcommand{\con}{\ensuremath{\wedge}}
\newcommand{\bigcon}{\ensuremath{\bigwedge}}
\newcommand{\dis}{\ensuremath{\vee}}
%
\newcommand{\ConformantPlanName}{{\textsc{ConformantPlan}}}
\newcommand{\ConformantPlan}[2]{\ensuremath{\ConformantPlanName}(#1,#2)}
%
\newcommand{\ConformantPreimageName}{{\textsc{ExpandBsPTable}}}
\newcommand{\ConformantPreimage}[1]{\ensuremath{\ConformantPreimageName}(#1)}
\newcommand{\ConformantPreimageSPName}{{\textsc{ExpandBsPPair}}}
\newcommand{\ConformantPreimageSP}[1]{\ensuremath{\ConformantPreimageSPName}(#1)}
%
\newcommand{\ConformantPruneName}{{\textsc{PruneBsPTable}}}
\newcommand{\ConformantPrune}[3]{\ensuremath{{\ConformantPruneName}(#1,#2,#3)}}
\newcommand{\ConformantSameLevelPruneName}{{\textsc{PruneBsPTableSameLevel}}}
\newcommand{\ConformantSameLevelPrune}[1]{\ensuremath{{\ConformantSameLevelPruneName}(#1)}}
\newcommand{\ConformantPrevLevelsPruneName}{{\textsc{PruneBsPTablePrevLevels}}}
\newcommand{\ConformantPrevLevelsPrune}[3]{\ensuremath{{\ConformantPrevLevelsPruneName}(#1,#2,#3)}}
%
\newcommand{\GetPlansName}{{\textsc{ExtractSolution}}}
\newcommand{\GetPlanName}{{\GetPlansName}}
\newcommand{\GetPlan}[2]{\ensuremath{{\GetPlansName}(#1,#2)}}
%
\newcommand{\DiffPlansName}{{\textsc{DiffPlans}}}
\newcommand{\DiffPlans}[2]{\ensuremath{{\DiffPlansName}(#1,#2)}}
%
\newcommand{\tuple}[1]{\ensuremath{<\!\!#1\!\!>}}
\newcommand{\bdds}{\textsc{Bdd}s\xspace}
\newcommand{\bdd}{\textsc{Bdd}\xspace}
\newcommand{\obdd}{\textsc{obdd}\xspace}
\newcommand{\LL}{$\!\!\!|$L$|\!\!\!$}
\newcommand{\IS}{$\!\!\!|$IS$|\!\!\!$}
\newcommand{\PL}{$\!\!\!|$P$|\!\!\!$}
\newcommand{\CTI}{\multicolumn{1}{c|}{Time}}
\newcommand{\CTII}{\multicolumn{1}{c|}{Time I}}
\newcommand{\CTINI}{\multicolumn{1}{c|}{Time NI}}
\newcommand{\CTD}{\multicolumn{1}{c||}{Time}}
\newcommand{\CPN}{\multicolumn{1}{c|}{\#P.}}


\newcommand{\vect}[1]{\ensuremath{{\mathbf{#1}}}}
\newcommand{\balpha}{\ensuremath{{{\pmb{\alpha}}}}}
\newcommand{\bpi}{{{{\pmb{\pi}}}}}
\newcommand{\vectx}{{{\ensuremath{\pmb{x}}}}}
\newcommand{\vectnx}{{{\ensuremath{\pmb{x}'}}}}
\newcommand{\bbeta}{{{\ensuremath{\pmb{\rho}}}}}
\newcommand{\planvar}[1]{\ensuremath{\vect{{\bpi}_{[{#1}]}}}}


\newcommand{\SPT}{\ensuremath{\textit{BsPT}}}
\newcommand{\PSPT}{\ensuremath{\textit{PSPT}}}
\newcommand{\SPTarr}{\ensuremath{\textit{BsPTables}}}
\newcommand{\conformance}{conformance}
\newcommand\mbp{\textsc{Mbp}\xspace}
\newcommand\cmbp{\textsc{Cmbp}\xspace}
\newcommand\cgp{\textsc{Cgp}\xspace}
\newcommand\gpt{\textsc{Gpt}\xspace}
\newcommand\astar{A{\ensuremath{^*}}\xspace}
\newcommand\qbfplan{\textsc{Qbfplan}\xspace}
\newcommand\blackbox{\textsc{Blackbox}\xspace}
\newcommand\graphplan{{\textsc{Graphplan}}}
\newcommand\smv{{\textsc{Smv}}}
\newcommand\nusmv{{\textsc{NuSMV}}}
\newcommand\satplan{{\textsc{Satplan}}}
\newcommand{\ar}{\mbox{$\cal AR$}}
\newcommand{\adl}{{\textsc{Adl}}}
\newcommand{\pddl}{{\textsc{Pddl}}}
\newcommand\state{\mbox{\i{State}$_F$}}
\newcommand\resp{\mbox{\i{Res}$_F$}}
\newcommand\resop{\mbox{\i{Res}$^0_F$}}

\newenvironment{pf}{\noindent{\bf Proof }}{\mbox{\hspace{0cm}}\hfill $\Box$}
\newcommand{\T}{{\sf T}}
\newcommand{\F}{{\sf F}}
\newcommand{\New}[3]{\i{New}_{#1}(#2,#3)}
\newcommand{\Id}[3]{\i{C}_{#1}^{#3}(#2)}
\newcommand{\Res}[2]{\i{Res}(#1,#2)}
\newcommand{\Reso}[2]{\i{Res}^0(#1,#2)}
\def\o{\overline}
\def\i#1{\hbox{\it #1\/}}
\def\be{\begin{equation}}
\def\ee{\end{equation}}
\def\beq{\begin{equation}}
\def\eeq#1{\label{#1}\end{equation}}
\def\after{\hbox{\bf after}}
\def\initially{\hbox{\bf initially}}
\def\causes{\hbox{\bf causes}}
\def\always{\hbox{\bf always}}
\def\pchanges{\hbox{\bf possibly changes}}
\def\iif{\hbox{\bf if}}
\def\rng{\hbox{\it Rng}}
\def\is{\hbox{\bf is}}

\def\init{\cali}
\def\Init{\init}
\def\goal{\calg}
\def\Goal{\goal}
\def\cala{{\ensuremath{\cal A}}}
\def\calc{{\ensuremath{\cal C}}}
\def\cald{{\ensuremath{\cal D}}}
\def\calf{{\ensuremath{\cal F}}}
\def\calg{{\ensuremath{\cal G}}}
\def\call{{\ensuremath{\cal L}}}
\def\cali{{\ensuremath{\cal I}}}
\def\calr{{\ensuremath{\cal R}}}
\def\cals{{\ensuremath{\cal S}}}
\def\calp{{\ensuremath{\cal P}}}

\newcommand{\pdomaino}{\ensuremath{(\mathcal{P},\mathcal{S},\mathcal{A},\mathcal{R})}}
\newcommand{\pdomainn}{\ensuremath{(\mathcal{S},\mathcal{A},\mathcal{R},\mathcal{L})}}
\newcommand{\pdomain}{\pdomaino}

\newcommand{\execname}{\i{Image}}
\newcommand{\exec}[2]{\execname[{\ensuremath{#1}}](\ensuremath{#2})}
\newcommand{\weakpreimage}[2]{\i{WPreImage}[#1](#2)}
\newcommand{\strongpreimagename}{\i{SPreImage}}
\newcommand{\strongpreimage}[2]{\ensuremath{\strongpreimagename[#1](#2)}}
\newcommand{\appl}[1]{\i{Appl}[#1]}
\newcommand{\applicabilityname}{\ensuremath{\textsc{Applicable}}\xspace}
\newcommand{\applicability}[2]{\ensuremath{\applicabilityname(#1,#2)}}
\def\AXalpha{\bf AX_{\alpha}}

% MACROS FOR IL FWD E FWD-BWD
%
\newcommand{\ita}[1]{\hbox{\textit{ #1\/}}}
\newcommand{\ConformantBwdPlan}[2]{\ensuremath{\textsc{ConformantBwdPlan}(#1,#2)}\xspace}
\newcommand{\ConformantFwdPlan}[2]{\ensuremath{\textsc{ConformantFwdPlan}(#1,#2)}\xspace}
\newcommand{\ConformantFBPlan}[2]{\ensuremath{\textsc{ConformantFBPlan}(#1,#2)}\xspace}
\newcommand{\FSParr}{\ensuremath{\mathit{FSPTarr}}}
\newcommand{\GetFwdPlansName}{{\textsc{ExtractSolutionFwd}}}
\newcommand{\GetFwdPlan}[2]{\ensuremath{{\GetFwdPlansName}(#1,#2)}\xspace}
\newcommand{\GetBwdPlansName}{{\textsc{ExtractSolutionBwd}}}
\newcommand{\GetBwdPlan}[2]{\ensuremath{{\GetBwdPlansName}(#1,#2)}\xspace}
\newcommand{\GetFBPlansName}{{\textsc{ExtractSolutionFB}}}
\newcommand{\GetFBPlan}[2]{\ensuremath{{\GetFBPlansName}(#1,#2)}\xspace}
\newcommand{\ConformantFwdImageName}{\ensuremath{\textsc{ConformantFwdImage}}}
\newcommand{\ConformantFwdImage}[1]{\ensuremath{\textsc{\ConformantFwdImageName}(#1)}\xspace}
\newcommand{\ConformantBwdImage}[1]{\ensuremath{\textsc{ConformantBwdImage}(#1)}\xspace}
\newcommand{\ConformantBwdPruneName}{\ensuremath{\textsc{ConformantBwdPrune}}\xspace}
\newcommand{\ConformantBwdPrune}[2]{\ensuremath{\textsc{\ConformantBwdPruneName}(#1,#2)}\xspace}
\newcommand{\ConformantFwdPruneName}{\ensuremath{\textsc{ConformantFwdPrune}}\xspace}
\newcommand{\ConformantFwdPrune}[2]{\ensuremath{\textsc{\ConformantFwdPruneName}(#1,#2)}\xspace}
\newcommand{\ConformantFBPrune}[2]{\ensuremath{\textsc{ConformantFBPrune}(#1,#2)}\xspace}
\newcommand{\Plans}{\mbox{\textit{Plans}}\xspace}
\newcommand{\Fail}{\mbox{\textit{Fail}}\xspace}
\newcommand{\SParr}{\ensuremath{\mathit{SPTarr}}}

% MATH STUFF
\newcommand{\openset}{\ensuremath{{\{}\xspace}}
\newcommand{\closeset}{\ensuremath{{\}}\xspace}}
\newcommand{\mkset}[1]{\ensuremath{{\{#1\}}\xspace}}
\newcommand{\mkpair}[2]{\ensuremath{\langle{#1}\ .\ {#2}\rangle\xspace}}
\newcommand{\mktuple}[1]{\ensuremath{\langle{#1}\rangle\xspace}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                   %
%%% This environment writes a boxed verbatim text;                    %
%%%                                                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newlength{\verbboxwidth}% 
\newenvironment{boxverbatim}%
   {\setlength{\verbboxwidth}{\textwidth}
    \addtolength{\verbboxwidth}{-2\arrayrulewidth}%
    \addtolength{\verbboxwidth}{-2\tabcolsep}%
    \begin{flushleft}%
    \begin{tabular}{|l|}\hline%
    \\%
    \begin{minipage}{\verbboxwidth}}%
   {\vspace*{.5\baselineskip}%
    \end{minipage}%
    \\\hline%
    \end{tabular}%
    \end{flushleft}}


\begin{document}
\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{abstract} 
  We tackle the problem of planning in nondeterministic domains, by
  presenting a new approach to conformant planning.
%
  Conformant planning is the problem of finding a sequence of actions
  that is guaranteed to achieve the goal despite the nondeterminism
  of the domain.
%
  Our approach is based on the representation of the planning domain
  as a finite state automaton. We use Symbolic Model Checking
  techniques, in particular Binary Decision Diagrams, to compactly
  represent and efficiently search the automaton.
%
  In this paper we make the following contributions.
%
  First, we present a general planning algorithm for conformant
  planning, which applies to fully nondeterministic domains, with
  uncertainty in the initial condition and in action effects.
%
  The algorithm is based on a breadth-first, backward search, and
  returns conformant plans of minimal length, if a solution to the
  planning problem exists, otherwise it terminates concluding that the
  problem admits no conformant solution.
%
  Second, we provide a symbolic representation of the search space
  based on Binary Decision Diagrams (\bdds), which is the basis for
  search techniques derived from symbolic model checking. The symbolic
  representation makes it possible to analyze potentially large sets
  of states and transitions in a single computation step, thus
  providing for an efficient implementation.
% 
  Third, we present {\cmbp} (Conformant Model Based Planner), an
  efficient implementation of the data structures and algorithm
  described above, directly based on \bdd manipulations, which allows
  for a compact representation of the search layers and an efficient
  implementation of the search steps.
%
  Finally, we present an experimental comparison of our approach with
  the state-of-the-art conformant planners {\cgp}, {\qbfplan} and
  {\gpt}. Our analysis includes all the planning problems from the
  distribution packages of these systems, plus other problems defined
  to stress a number of specific factors.
%
  Our approach appears to be the most effective: {\cmbp} is strictly
  more expressive than {\qbfplan} and {\cgp} and, in all the problems
  where a comparison is possible, {\cmbp} outperforms its
  competitors, sometimes by orders of magnitude. 
\end{abstract}

\section{Introduction}
\label{sec-intro}

%
In recent years, there has been a growing interest in planning in
nondeterministic domains. 
%
Rejecting some fundamental (and often unrealistic) assumptions of
classical planning, domains are considered where actions can have
uncertain effects, exogenous events are possible, and the initial
state can be only partly specified.
%
The challenge is to find a {\em strong} plan, that is guaranteed to
achieve the goal despite the nondeterminism of the domain, regardless
of the uncertainty on the initial condition and on the effect of actions.
%
Conditional planning~\cite{cassandra,sgp,cimatti28} tackles this
problem by searching for a conditional course of actions, that
depends on information that can be gathered at run-time.
%
In certain domains, however, run-time information gathering may
be too expensive or simply impossible. 
%
{\em Conformant planning}~\cite{goldman1} is the problem of finding
an unconditioned course of actions, i.e.\ a classical plan, that does
not depend on run-time information gathering to guarantee the
achievement of the goal.
%
Conformant planning has been recognized as a significant problem in
Artificial Intelligence since the work by Michie~\citeyear{michie1}: the Blind Robot problem
requires to program the activity for a sensorless agent, which can be
positioned in any location of a given room, so that it will be
guaranteed to achieve a given goal.
%
Conformant planning can be also seen as a problem of control for a
system with an unobservable and unknown state, such as a microprocessor
at power-up, or a software system under black-box testing.
%

%
Because of uncertainty,
a plan is associated to potentially many different executions, which
must be all taken into account in order to guarantee goal
achievement.
%
This makes conformant planning significantly harder than classical
planning~\cite{rintanen1,degiacomo1}.
%
Despite this increased complexity, several approaches to conformant
planning have been recently proposed, based on (extensions of) the
main planning techniques for classical planning. The most interesting
are \cgp \cite{cgp} based on {\graphplan}, \qbfplan 
\cite{rintanen1} which extends the SAT-plan approach to QBF,
and \gpt \cite{bonet1} which encodes conformant planning as heuristic search.
%
In this paper, we propose a new approach to conformant planning, based
on Symbolic Model Checking~\cite{mcmillan1}. Symbolic Model Checking
is a formal verification technique, which allows one to analyze finite
state automata of high complexity, relying on symbolic techniques,
Binary Decision Diagrams (\bdds)~\cite{bryant2} in particular, for the
compact representation and efficient search of the automaton.
%
Our approach builds on the planning via model checking
paradigm presented by Cimatti and his colleagues~\citeyear{cimatti27,cimatti28,cimatti29}, where finite state
automata are used to represent complex, nondeterministic planning
domains, and planning is based on (extensions of) the basic model
checking steps.
%
We make the following contributions.
%
\begin{itemize}
\item First, we present a general algorithm for conformant planning,
  which applies to any nondeterministic domain with uncertain action
  effects and initial condition, expressed as a nondeterministic
  finite-state automaton.
%
  The algorithm performs a breadth-first search, exploring plans of
  increasing length, until a plan is found or no more candidate plans
  are available.
%
  The algorithm is complete, i.e.\ it returns with failure if and only
  if the problem admits no conformant solution. If the problem admits
  a solution, the algorithm returns a conformant plan of minimal
  length.

\item Second, we provide a symbolic representation of the search space
  based on Binary Decision Diagrams, which allows for the application
  of search techniques derived from symbolic model checking. The
  symbolic representation makes it possible to analyze {\em sets} of
  transitions in a single computation step. These sets can be
  compactly represented and efficiently manipulated despite their
  potentially large cardinality. This way it is possible to
  overcome the enumerative nature of the other approaches to
  conformant planning, for which the degree of nondeterminism tends to
  be a limiting factor.

\item Third, we developed {\cmbp} (Conformant Model Based Planner),
  which is an efficient implementation of the data structures and
  algorithm described above.  {\cmbp} is developed on top of {\mbp},
  the planner based on symbolic model checking techniques developed by
  Cimatti, Roveri and Traveso~\citeyear{cimatti28,cimatti29}.  {\cmbp} implements several new
  techniques, directly based on \bdd manipulations, to compact the
  search layers and optimize termination checking.

\item Finally, we provide an experimental evaluation of the
  state-of-the-art conformant planners, comparing {\cmbp} with {\cgp}, 
  {\qbfplan} and {\gpt}.
%
  Because of the difference in expressivity, not all the problems
  which can be tackled by {\cmbp} can also be represented in the other
  planners.
%
  However, for the problems where a direct comparison was possible,
  {\cmbp} outperforms its competitors. In particular, it features a
  better qualitative behavior, not directly related to the {\em
    number} of initial states and uncertain action effects, and more
  stable with respect to the use of heuristics.
\end{itemize}


The paper is structured as follows.
%
In Section~\ref{sec-background} we review the representation of
(nondeterministic) planning domains as finite state automata.
%
In Section~\ref{sec-conformant-planning} we provide the intuitions and
a formal definition of conformant planning in this setting.
%
In Section~\ref{sec-algo-definition} we present the planning
algorithm, and in Section~\ref{sec-symbolic-representation} we discuss
the symbolic representation of the search space, which allows for an
efficient implementation.
%
In Section~\ref{sec-cmbp} we present the {\cmbp} planner, and in
Section~\ref{sec-experiments} we present the experimental results.
%
In Section~\ref{sec-relwork} we discuss some further related work.
%
In Section~\ref{sec-concl} we draw the conclusions and discuss future
research directions.

\section{Planning Domains as Finite State Automata}
% 
\label{sec-background}

We are interested in complex, nondeterministic planning domains, where
actions can have preconditions, conditional effects, and uncertain
effects, and the initial state can be only partly specified.
%
In the rest of this paper, we use a very simple though paradigmatic
domain for explanatory purposes, a variation of Moore's {\em bomb in
the toilet} domain~\cite{McDermott:1987} (from now on called BTUC~---
BT with Uncertain Clogging).
%
There are two packages, and one of them contains an armed bomb. It is
possible to dunk either package in the toilet (actions $Dunk_1$ and
$Dunk_2$), provided that the toilet is not clogged. Dunking either
package has the uncertain effect of clogging the toilet. Furthermore,
dunking the package containing the bomb has the effect of disarming
the bomb. The action $Flush$ has the effect of unclogging the toilet.
%

\begin{figure}[tb]
\begin{center}
{{\psfig{figure=fig/btautomaton.eps,height=0.3\textheight}}}
\end{center}

\caption{The automaton for the BTUC domain}
\label{fig-bt-automa}
\end{figure}

We represent such domains as finite state automata.
%
Figure~\ref{fig-bt-automa} depicts the automaton for the BTUC domain.
%
Each state is given a number, and contains all the propositions holding
in that state. 
%
For instance, state 1 represents the state where the bomb is in
package 1, is not defused, and the toilet is not clogged. Given that
there is only one bomb, we write ${In_2}$ as an abbreviation for
the negation of ${In_1}$.
%
Arrows between states depict the transitions of the automaton,
representing the possible behavior of actions. 
%
The transition from state 2 to state 1 labeled by $Flush$ represents
the fact that the action $Flush$, if executed in state 2, only has the
effect of removing the clogging.
%
The execution of $Dunk_1$ in state 1, which has the uncertain effect
of clogging the toilet, is represented by the multiple
transitions to states 5 and 6.
%
Since there is no transition outgoing from state 2 and labelled by
$Dunk_1$, state 2 does not satisfy the preconditions of action
$Dunk_1$, i.e.\ $Dunk_1$ is not applicable in state 2.

We formally define nondeterministic planning domains as follows.
%
\begin{definition}[Planning Domain]
%
A Planning Domain is a 4-tuple ${\cald}=\pdomain$,
%
where {\calp} is the (finite) set of atomic propositions,
%
${\cals}\ {\subseteq}\ 2^{\calp}$ is the set of states,
%
{\cala} is the (finite) set of actions, 
%
and $\calr\ \subseteq\ \cals\times\cala\times\cals$ is the transition
relation.
\end{definition}

Intuitively, a proposition is in a state if and only if it holds in
that state.
%
In the following we assume that a planning domain $\cald$ is given. We use
$s$, $s'$ and $s''$ to denote states of $\cald$, and $\alpha$ to
denote actions.
%
$\calr(s,\alpha,s')$ holds iff when executing the action $\alpha$ in
the state $s$ the state $s'$ is a possible outcome.
%
We say that an action $\alpha$ is applicable in $s$ iff there is at
least one state $s'$ such that $\calr(s,\alpha,s')$ holds.
%
We say that an action $\alpha$ is deterministic in $s$ iff there is a
unique state $s'$ such that $\calr(s,\alpha,s')$ holds.
%
An action $\alpha$ has an uncertain outcome in $s$ if there are at
least two distinct states $s'$ and $s''$ such that
$\calr(s,\alpha,s')$ and $\calr(s,\alpha,s'')$ hold.
%
As described by Cimatti and his colleagues~\citeyear{cimatti27}, the automaton for a given domain can
be efficiently built starting from a compact description given in an
expressive high level action language, for instance {\ar}~\cite{giunchiglia100}. 


\section{Conformant Planning}
\label{sec-conformant-planning}

\begin{figure}[tb]
\begin{center}
\epsfig{figure=fig/bt-conf-exec.eps,width=0.9\textwidth}
\end{center}

\caption{A conformant solution for the BTUC problem}
\label{fig-bt-conf-exec}
\end{figure}

%
Conformant planning~\cite{goldman1} can be described as the problem of
finding a sequence of actions that is guaranteed to achieve the goal
regardless of the nondeterminism of the domain.
That is, for {\em all} possible initial states, and for {\em all}
uncertain action effects, the execution of
the plan results in a goal state.

%
Consider the following problem for the BTUC domain. Initially, the
bomb is armed but its position and the status of the toilet are
uncertain, i.e.\ the initial state can be any of the states in
\mkset{1,2,3,4}.
%
The goal is to reach a state where the bomb is defused, and the toilet is
not clogged, i.e.\ the set of goal states is \mkset{5,7}.
% 
A conformant plan solving this problem is 
%
\begin{equation}
Flush ;\ Dunk_1\ ;\ Flush\ ;\ Dunk_2 ;\ Flush
\label{eq-conf-solution}
\end{equation}
%
Figure~\ref{fig-bt-conf-exec} outlines the possible executions of the
plan, for all possible initial states and uncertain action effects.
%
The initial uncertainty lies in the fact that the domain might be in any of the
states in \mkset{1,2,3,4}. The possible initial states of the planning
domain are collected into a set by a dashed line. We call such a set a
{\em belief state}. Intuitively, a belief state expresses a condition
of uncertainty about the domain, by collecting together all the states
which are indistinguishable from the point of view of an agent
reasoning about the domain. 
%
The first action, $Flush$, is used to remove the possible clogging.
This reduces the uncertainty to the belief state~\mkset{1,3}.  Despite
the remaining uncertainty (i.e.\ it is still not known in which package
the bomb is), action $Dunk_1$ is now guaranteed to be applicable
because its precondition is met in both states.
%
$Dunk_1$ has the effect of defusing the bomb if it is contained in
package 1, and has the uncertain effect of clogging the toilet. The
resulting belief state is~\mkset{3,4,5,6}.
%
The following action, $Flush$, removes the clogging, reducing the
uncertainty to the belief state~\mkset{3,5}, and guarantees the
applicability of $Dunk_2$.
%
After $Dunk_2$, the bomb is guaranteed to be defused, but the toilet
might be clogged again (states 6 and 8 in the belief
state~\mkset{5,6,7,8}).
%
The final $Flush$ reduces the uncertainty to the belief state
$\mkset{5,7}$, and guarantees the achievement of the goal.

% 
In general, in order for a plan to be a conformant solution, no action
must be executed in states which do not satisfy the preconditions, and
any state that can result from the execution of the plan (for all the
initial states and for all the uncertain action effects) is a goal
state.
%
The main difficulty in achieving these conditions is that no
information is (assumed to be) available at run-time. Therefore, at
planning time we face the problem of reasoning about action execution
in a belief state, i.e.\ under a condition of uncertainty.
%
\begin{definition}[Action Applicability]
Let ${Bs}\subseteq\cals$ be a Belief State.
%
The action $\alpha$ is applicable in $Bs$ iff $Bs\neq\emptyset$ and
$\alpha$ is applicable in every state $s\in{Bs}$.
\end{definition}
%
In order for an action to be applicable in a belief state, we require
that its preconditions must be guaranteed notwithstanding the
uncertainty.
%
In other words, we reject ``reckless'' plans,
which take the chance of applying an action without the guarantee of
its applicability. 
%
This choice is strongly motivated in practical domains, where possibly
fatal consequences can follow from the attempt to apply an action when
its preconditions might not be satisfied (e.g.\  starting to fix an
electrical device without being sure that it is not powered).
%
The effect of action execution from an uncertain condition is defined
as follows.
%
\begin{definition}[Action Image]
Let ${Bs}\subseteq\cals$ be a belief state, and let $\alpha$ be an
action applicable in $Bs$.
%
The image (also called execution) of $\alpha$ in $Bs$,
written $\exec{\alpha}{Bs}$, is defined as follows.
$$
\exec{\alpha}{Bs}\ \ \eqbydef\ \ 
\{ s'\ |\ there\ exists\ s\in Bs\ such\ that\ \calr(s,\alpha,s') \}
$$
\end{definition}
%
Notice that the image of an action combines the uncertainty in the
belief state with the uncertainty on the action effects. (Consider for
instance that \exec{Dunk_1}{\mkset{1,3}}=\mkset{3,4,5,6}.)
%
In the following, we write $\exec{\alpha}{s}$ instead of
$\exec{\alpha}{\{s\}}$.


% 
Plans are elements of $\cala^*$, i.e.\ finite sequences of actions.
%
We use $\epsilon$ for the 0-length plan, $\pi$ and $\rho$ to denote
generic plans, and $\pi;\rho$ for plan concatenation.
%
The notions of applicability and image generalize to
plans as follows. 
%
\begin{definition}[Plan Applicability and Image]
\label{def-plan-appl}
%
Let $\pi\in\cala^*$, and let ${Bs}\subseteq\cals$.
%
$\pi$ is applicable in $Bs$ iff one of the following holds:
\begin{enumerate}
\item $\pi={\epsilon}$ and ${Bs}\neq\emptyset$;
\item $\pi={\alpha;\rho}$,
%
  $\alpha$ is applicable in $Bs$, and
  $\rho$ is applicable in $\exec{\alpha}{Bs}$.
\end{enumerate}

\noindent The image (also called execution) of $\pi$ in $Bs$, written
$\exec{\pi}{Bs}$, is defined as:
\begin{enumerate}
\item {$\exec{\epsilon}{Bs} \eqbydef Bs$};

\item
{$\exec{\alpha;\pi}{Bs} \eqbydef \exec{\pi}{\exec{\alpha}{Bs}}$};
\end{enumerate}
\end{definition}

%
A planning problem is formally characterized by the set of initial and
goal states. The following definition captures the intuitive meaning
of conformant plan given above.
%
\begin{definition}[Conformant Planning]
\label{def-conformant-plan}
\label{def-planning-problem}
  Let ${\cald} = \pdomain$ be a planning domain.
  A Planning Problem for ${\cald}$ is a triple
  $({\cald},\init,\goal)$, where $\emptyset \not = \init \subseteq \cals$ and
  $\emptyset \not = \goal \subseteq \cals$.

  The plan $\pi$ is a conformant plan for (that is, a conformant solution to)
  the planning problem $(\cald,\init,\goal)$ iff the following
  conditions hold:
\begin{itemize}
\item[{$(i)$}] $\pi$ is applicable in $\init$;
\item[{$(ii)$}] $\exec{\pi}{\init}\subseteq\Goal$.
\end{itemize}
\end{definition}
%
In the following, when clear from the context, we omit the domain from
the planning problem, and we simply write $(\init,\goal)$.


\section{The Conformant Planning Algorithm}
\label{sec-algo-definition}
\label{sec-algo}
\label{sec-algo-intuitions}

% 
Our conformant planning algorithm is based on the exploration of the
space of plans, limiting the exploration to plans which are conformant
by construction. 
%
The algorithm builds Belief state-Plan (BsP) pairs of the form
\mkpair{Bs}{\pi}, where $Bs$ is a non-empty belief state and $\pi$ is
a plan.
%
The idea is to use a BsP pair to associate each explored plan with the
maximal belief state where it is applicable, and from which it is
guaranteed to result in goal states.
%
The exploration is based on the basic function
{\strongpreimage{\alpha}{Bs}}, that, given a belief state $Bs$ and an
action $\alpha$, returns the belief state containing all the states
where $\alpha$ is applicable, and whose image under $\alpha$ is
contained in $Bs$.
%
\begin{definition}[Strong Pre-Image]
Let $\emptyset \not = Bs \subseteq \cals$ be a belief state and let $\alpha$ be an action.
The strong pre-image of $Bs$ under $\alpha$, written
$\strongpreimage{\alpha}{Bs}$, is defined as follows. 
$$
\strongpreimage{\alpha}{Bs}\ \eqbydef\ 
\{ s\ |\ \alpha \ is\ applicable\ in\ s, and\ \exec{\alpha}{s}\
\subseteq\ Bs \}
$$
\end{definition}
%
If \strongpreimage{\alpha}{Bs} is not empty, then $\alpha$ is
applicable in it, and it is a conformant solution to the
problem $(\strongpreimage{\alpha}{Bs},Bs)$.
%
Therefore, if the plan $\pi$ is a conformant solution for the problem
$(Bs,\goal)$, then the plan $\alpha;\pi$ is a conformant solution to
the problem $(\strongpreimage{\alpha}{Bs},\goal)$.

\begin{figure}[hbt]
  \begin{center}
    \epsfig{figure=fig/bt-sptables.eps,width=0.8\textwidth}
  \end{center}
  \caption{The BsP tables for the BTUC problem}
  \label{fig-bt-solution}
\end{figure}

% 
Figure~\ref{fig-bt-solution} depicts the space of BsP pairs built by
the algorithm while solving the BTUC problem. The levels are built
from the goal, on the right, towards the initial states, on the left.
%
At level 0, the only BsP pair is \mkpair{\mkset{5,7}}{\epsilon},
composed by the set of goal states indexed by the 0-length plan
$\epsilon$. (Notice that $\epsilon$ is a conformant solution to every
problem with goal set $\mkset{5,7}$ and initial states
contained in $\mkset{5,7}$.)
%
The dashed arrows represent the application of {\strongpreimagename}.
At level 1, only the BsP pair \mkpair{\mkset{5,6,7,8}}{Flush} is
built, since the strong pre-image of the belief state 0 for the actions
$Dunk_1$ and $Dunk_2$ is empty.
%
At level 2, there are three BsP pairs, with (overlapping) belief
states Bs$_{2}$, Bs$_{3}$ and Bs$_{4}$, indexed, respectively, by the length 2 plans
$Dunk_1;Flush$, $Flush;Flush$ and $Dunk_2;Flush$. (A plan associated
with a belief state Bs$_{i}$ is a sequence of actions labeling the path
from Bs$_{i}$ to Bs$_{0}$.) Notice that Bs$_{3}$ is equal to Bs$_{1}$, and therefore
deserves no further expansion.
%
The expansion of belief states 2 and 4 gives the belief states 5 and
6, both obtained by the strong pre-image under $Flush$, while the
strong pre-image under actions $Dunk_1$ and $Dunk_2$ returns empty
belief states.
%
The further expansion of Bs$_{5}$ results in three belief states. The one
resulting from the strong pre-image under $Flush$ is not reported,
since it is equal to Bs$_{5}$. Belief state 7 is also equal to Bs$_{2}$, and
deserves no further expansion. Belief state 8 can be obtained by
expanding both Bs$_{5}$ and Bs$_{6}$.
%
At level 5, the expansion produces Bs$_{10}$, which contains all the
initial states. Therefore, both of the corresponding plans are
conformant solutions to the problem. 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% PLANNING ALGORITHM
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{figure}[thb]
\begin{tabbing}
x\=xxxi\=xx\=xxxx\=xxxx\=xxxx\=xxxx\kill
\>\>\itshape \textbf{function} \ConformantPlan{\init}{\goal}\\
\>0\>\itshape \textbf{begin}\\
\>1\>\>\itshape i = 0;\\
\>2\>\>\itshape \SPTarr[0] := \{ \mkpair{\goal}{\epsilon} \};\\
\>3\>\>\itshape Plans := \GetPlan{\init}{\SPTarr[0]};\\
\>4\>\>\itshape \textbf{while} (($\SPTarr[i] \neq \emptyset) \con (Plans = \emptyset))$ \textbf{do}\\
\>5\>\>\>\itshape i := i + 1;\\
\>6\>\>\>\itshape \SPTarr[i] := \ConformantPreimage{\SPTarr[i-1]};\\
\>7\>\>\>\itshape \SPTarr[i] := \ConformantPrune{\SPTarr[i]}{\SPTarr}{i};\\
\>8\>\>\>\itshape Plans := \GetPlan{\init}{\SPTarr[i]};\\
\>9\>\>\itshape\textbf{done}\\
\>10\>\>\itshape \textbf{if} ($\SPTarr[i] = \emptyset$) \textbf{then}\\
\>11\>\>\>\itshape \textbf{return} \Fail;\\
\>12\>\>\>\itshape \textbf{else return} Plans;\\
\>13\>\itshape \textbf{end}
\\
\end{tabbing}

\caption{The conformant planning algorithm.}
\label{fig-cpalgorithm}
\end{figure}

\begin{figure}[t]

  \begin{displaymath}
    \begin{array}{c}\displaystyle
      {\ConformantPreimage{{\SPT}} \eqbydef} {\bigcup_{\mkpair{Bs}{\pi} \in {\SPT}} \ConformantPreimageSP{\mkpair{Bs}{\pi}}}

    \end{array}
  \end{displaymath}

  \begin{displaymath}
    \begin{array}{c}
      {\ConformantPreimageSP{\mkpair{Bs}{\pi}}\eqbydef}
      {\{\mkpair{Bs'}{\alpha;\pi}|\mbox{ such that}\ Bs'=\strongpreimage{\alpha}{Bs}\neq\emptyset\}}
    \end{array}
  \end{displaymath}

\begin{displaymath}
\begin{array}{l}
\ConformantPrune{\SPT}{\SPTarr}{i}
\eqbydef
\\
\mkset{{\mkpair{Bs}{\pi}\in\SPT}
\ |
\ \mbox{for all}\ j<i,
\ \mbox{there is no}\ \mkpair{Bs}{\pi'}\in \SPTarr[j]
\ \mbox{such that }
(Bs'=Bs)}
%
\end{array}
\end{displaymath}


  \begin{displaymath}
    \begin{array}{c}
      {\GetPlan{\init}{{\SPT}} \eqbydef}
      {\{ \pi\ |\ \mbox{there exists}\  \mkpair{Bs}{\pi}\in {\SPT}\ \mbox{such that}\ \init\subseteq Bs \}}
    \end{array}
  \end{displaymath}

\caption{The primitives used by the conformant planning algorithm.}
\label{fig-cpalgorithm-primitives}
\end{figure}



The conformant planning algorithm {\ConformantPlanName} is presented
in Figure~\ref{fig-cpalgorithm}. It takes as input the planning
problem in the form of the set of states $\init$ and $\goal$ (the domain
{\cald} is assumed to be globally available).
%
The algorithm performs a backwards breadth-first search, exploring BsP
pairs corresponding to plans of increasing length at each step.
%
The status of the search (each level in Figure~\ref{fig-bt-solution})
is represented by a BsP table, i.e.\ a set of BsP pairs
%
$$
{\SPT} = \mkset{\mkpair{Bs_1}{\pi_1},\ldots,\mkpair{Bs_n}{\pi_n}}
$$
%
where the $\pi_i$ are plans of the same length, such that
$\pi_i\neq\pi_j$ for all $1\leq j{\neq}i\leq n$.
%
We call $Bs_i$ the belief set indexed by $\pi_i$. When no ambiguity
arises, we write $\SPT(\pi_i)$ for $Bs_i$.
%
The array $\SPTarr$ is used to store the BsP tables representing the
levels of the search.
%
The algorithm first checks (line 4) if there are plans of length 0,
i.e.\  if $\epsilon$ is a solution. If no conformant plan of such length
exists ($(Plans = \emptyset)$ in line~4), then the while loop is
entered. At each iteration, conformant plans of increasing length
are explored (lines 5 to 8).
%
The step at line~6 expands the BsP table in $\SPTarr[i-1]$ and stores the
resulting BsP table in $\SPTarr[i]$.
%
BsP pairs which are redundant with respect to the current search
are eliminated from $\SPTarr[i]$ (line~7).
%
The possible solutions contained in $\SPTarr[i]$ are extracted and
stored in $Plans$ (line~8).
%
The loop terminates if either a plan is found $(Plans \neq
\emptyset)$, or the space of conformant plans has been completely
explored $(\SPTarr[i]=\emptyset)$.


The definitions of the basic functions used in the algorithm are
reported in Figure~\ref{fig-cpalgorithm-primitives}.
%
The function {\ConformantPreimageName} expands the BsP table provided
as argument, containing conformant plans of length $i-1$, and returns
a BsP table with conformant plans of length $i$. Each BsP in the input
BsP table is expanded by {\ConformantPreimageSPName}. For each
possible action $\alpha$, the strong pre-image of $Bs$ is computed, and
if the resulting belief state $Bs'$ is not empty, i.e.\ there is a
belief state from which $\alpha$ guarantees the achievement of $Bs$,
then the plan $\pi$ is extended with $\alpha$ and
$\mkpair{Bs'}{\alpha;\pi}$ is returned.
%
The expansion of a BsP table is the union of the expansions of each
BsP pair.
%
The function {\GetPlanName} takes as input a BsP table and returns the
(possibly empty) set of plans which index a belief states containing
{\init}.
%
{\ConformantPruneName} takes as input the BsP table to be pruned, an
array of previously constructed BsP tables $\SPTarr$, and an index of
the current step. It removes from the BsP table in the input the plans
which are not worth being explored because the corresponding belief
states have already been visited.

The algorithm has the following properties. First, it always
terminates. This follows from the fact that the set of explored belief
sets (stored in {\SPTarr}) is monotonically increasing~--- at each
step we proceed only if at least one new belief state is generated.
Because of its finiteness (the set of accumulated belief states is
contained in $2^{\cals}$ which is finite), a fix point is eventually
reached.
%
Second, it is correct, i.e.\ when a plan is returned it is a conformant
solution to the given problem. The correctness of the algorithm
follows from the properties of {\strongpreimagename}: each plan is
associated with a belief state for which it is conformant, i.e.\ where
it is guaranteed to be applicable and from which it results in a
belief state contained in the goal.
%
Third, the algorithm is optimal, i.e.\ it returns plans of minimal
length. This property follows from the breadth-first style of the
search.
%
Finally, the algorithm is able to decide whether a problem admits no
solution, returning $\Fail$ in such cases.
%
Indeed, a conformant solution is always associated with a belief state
containing the initial states. {\strongpreimagename} generates the
{\em maximal} belief state associated with a conformant plan, each new
belief state generated in the exploration is compared with the initial
states to check if it is a solution, and a plan is pruned only if an
equivalent plan has already been explored.


\section{Conformant Planning via Symbolic Model Checking}
\label{sec-symbolic-representation}

Model checking is a formal verification technique based on the
exploration of finite state automata~\cite{clarke3}.
%
Symbolic model checking~\cite{mcmillan1} is a particular form of
model checking using Binary Decision Diagrams to compactly
represent and efficiently analyze finite state automata.
%
The introduction of symbolic techniques into model checking led to a
breakthrough in the size of model which could be
analyzed~\shortcite{burch1}, and made it possible for model checking to be
routinely applied in industry, especially in logic circuits design
\cite<for a survey see>{clarke96a}.

In the rest of this section, we will provide an overview of Binary
Decision Diagrams, and we will describe the representation of 
planning domains, based on the \bdd-based representation of finite
state automata used in model checking. 
%
Then, we will discuss the extension which allows to symbolically
represent BsP tables and their transformations, thus allowing for an
efficient implementation of the algorithm described in the previous
section.

\subsection{Binary Decision Diagrams}
%
\begin{figure}[ht]
  \begin{center}
    \begin{tabular}{c@{\hspace{1cm}}c}
      \subfigure[\ ]{\psfig{file=fig/obdd1.eps,width=3.6cm}} &
      \subfigure[\ ]{\psfig{file=fig/obdd2.eps,height=7.8cm}}
    \end{tabular}
  \end{center}

   \caption{Two \bdds for the formula $(a_1 \leftrightarrow b_1)
   \wedge (a_2 \leftrightarrow b_2) \wedge (a_3 \leftrightarrow b_3)$.}

 \label{fig-bdd}
\end{figure}
%

A Reduced Ordered Binary Decision Diagram~\cite{bryant1,bryant2}
(improperly called {\bdd}) is a directed acyclic graph (DAG).  The
terminal nodes are either {\truth} or {\falsity}. Each non-terminal
node is associated with a boolean variable, and two \bdds,
called left and right branches.
%
Figure~\ref{fig-bdd}~(a) depicts a {\bdd} for $(a_1 \leftrightarrow
b_1) \wedge (a_2 \leftrightarrow b_2) \wedge (a_3 \leftrightarrow b_3)$.
%
At each non-terminal node, the right [left, respectively] branch is
depicted as a solid [dashed, resp.] line, and represents the
assignment of the value {\truth} [{\falsity}, resp.] to the
corresponding variable.
%
A {\bdd} represents a boolean function.
%
For a given truth assignment to the variables in the \bdd, the value
of the function is determined by traversing the graph from the root to
the leaves, following each branch indicated by the value assigned to
the variables\footnote{A path from the root to a leaf can visit nodes
  associated with a subset of all the variables of the \bdd. See for
  instance the path associated with $a_1, \neg b_1$ in
  Figure~\ref{fig-bdd}(a).}.
%
The reached leaf node is labeled with the resulting truth value.
%
If $v$ is a \bdd, its size \sizeof{v} is the number of its nodes. If
$n$ is a node, $var(n)$ indicates the variable indexing node $n$.

\bdds are a canonical representation of Boolean functions. The
canonicity follows by imposing a total order $<$ over the set of
variables used to label nodes, such that for any node $n$ and
respective non-terminal child $m$, their variables must be ordered,
i.e.\ $var(n) < var(m)$, and requiring that the \bdd contains no
isomorphic subgraphs.

\bdds can be combined with the usual boolean transformations
(e.g.\ negation, conjunction, disjunction). Given two \bdds, for instance,
the conjunction operator builds and returns the \bdd corresponding to
the conjunction of its arguments.
%
Substitution can also be represented as \bdd transformations.
%
In the following, if $v$ is a variable, and $\Phi$ and $\psi$ are
\bdds, we indicate with $\Phi\substwith{v}{\psi}$ the \bdd resulting
from the substitution of $v$ with $\psi$ in $\Phi$.
%
If \vect{v_1} and \vect{v_2} are vectors of (the same number of)
distinct variables, we indicate with
$\Phi\substwith{\vect{v_1}}{\vect{v_2}}$ the parallel substitution in
$\Phi$ of the variables in vector $\vect{v_1}$ with
the (corresponding) variables in $\vect{v_2}$.

\bdds also allow for transformations described as quantifications, in
the style of Quantified Boolean Formulae (QBF). QBF is a definitional
extension to propositional logic, where propositional variables can be
universally and existentially quantified.
%
In terms of \bdd computations, a quantification corresponds to a
tranformation mapping the \bdd of $\Phi$ and the variable $v_i$ being
quantified into the \bdd of the resulting (propositional) formula.
%
If $\Phi$ is a formula, and $v_i$ is one of its variables, the
existential quantification of $v_i$ in $\Phi$, written
$\exists{v_i}.\Phi(v_1,\ldots{},v_n)$, is equivalent to
$\Phi(v_1,\ldots{},v_n)\substwith{v_i}{\falsity}\dis\Phi(v_1,\ldots{},v_n)\substwith{v_i}{\truth}$.
%
Analogously, the universal quantification
$\forall{v_i}.\Phi(v_1,\ldots{},v_n)$ is equivalent to
$\Phi(v_1,\ldots{},v_n)\substwith{v_i}{\falsity}\con\Phi(v_1,\ldots{},v_n)\substwith{v_i}{\truth}$.
%
In QBF, quantifiers can be arbitrarily applied and nested. In general,
a QBF formula has an equivalent propositional formula, but the
conversion is subject to an exponential blow-up.

The time complexity of the algorithm for computing a truth-functional
boolean transformation $f_1 \tuple{op} f_2$ is
$O(\sizeof{f_1}\cdot\sizeof{f_2})$.
%
As far as quantifications are concerned, the time complexity is
quadratic in the size of the \bdd being quantified, and linear in the
number of variables being quantified,
i.e.\ $O(\sizeof{\vect{v}}\cdot\sizeof{f}^2)$~\cite{bryant1,bryant2}.

{\bdd} {\em packages} are efficient implementations of such data
structures and algorithms~\shortcite{BrRB90,somenzi1,yang:fmcad98,TiGeR}.
%
Basically, a \bdd package deals with a single multi-rooted DAG, where
each node represents a boolean function.
%
Memory efficiency is obtained by using a ``unique table'', and by
sharing common subgraphs between \bdds.
%
The unique table is used to guarantee that at each time there are no
isomorphic subgraphs and no redundant nodes in the multi-rooted DAG.
Before creating a new node, the unique table is checked to see if the
node is already present, and only if this is not the case a new node
is created and stored in the unique table.
%
The unique table allows to perform the equivalence check between two
\bdds in constant time (since two equivalent functions always share
the same subgraph)~\cite{BrRB90,somenzi1}.
%
Time efficiency is obtained by maintaining a ``computed table'', which
keeps track of the results of recently computed transformations, thus
avoiding the recomputation.

A critical computational factor with {\bdd}s is the order of the
variables used. (Figure~\ref{fig-bdd} shows an example of the impact
of a change in the variable ordering on the size of a \bdd.)
%
For a certain class of boolean functions, the size of the
corresponding \bdd is exponential in the number of variables for any
possible variable ordering~\cite{Bry91}. In many practical cases,
however, finding a good variable ordering is rather easy.
%
Beside affecting the memory used to represent a Boolean function,
finding a good variable ordering can have a big impact on computation
times, since the complexity of the transformation algorithms depends
on the size of the operands.
%
Most \bdd packages provide heuristic algorithms for finding good
variable orderings, which can be called to try to reduce the overall
size of the stored \bdds.
%
The reordering algorithms can also be activated dynamically by the
package, during a {\bdd} computation, when the total number of nodes
in the package reaches a predefined threshold (dynamic reoredering).

\subsection{Symbolic Representation of Planning Domains}

A planning domain $\pdomain$ can be represented symbolically using
{\bdds}, as follows.
%
A set of (distinct) \bdd variables, called {\em state} variables, is
devoted to the representation of the states $\cals$ of the domain.
Each of these variables has a direct association with a proposition of
the domain in $\calp$ used in the description of the domain. For
instance, for the BTUC domain, each of $In_1$, $Defused$ and $Clogged$
is associated with a unique \bdd variable. In the following we write
{\vectx} for the vector of state variables. Because the particular
order is irrelevant but for performance issues, in the rest of this
section we will not distinguish a proposition and the corresponding \bdd
variable.

A state is a set of propositions of {\calp} (specifically, the
propositions which are intended to hold in it). For each state $s$,
there is a corresponding assignment to the state variables {\vectx},
i.e.\ the assignment where each variable corresponding to a proposition
$p\in{s}$ is assigned to $\truth$, and each other variable is assigned
to $\falsity$. We represent $s$ with the \bdd $\xi(s)$, having such an
assignment as its unique satisfying assignment.
% 
For instance, $\xi(6)\eqbydef(In_1\con Defused\con Clogged)$ is the
\bdd representing state 6, while $\xi(4)\eqbydef\neg In_1\con \neg
Defused\con Clogged$ represents state 4, and so on.  (Without loss of
generality, in the following we do not distinguish a propositional
formula from the corresponding \bdd.)
%
This representation naturally extends to any {\em set of states}
$Q\subseteq{{\cals}}$ as follows:
%
$$
\xi(Q)\eqbydef\bigvee_{s\in{Q}}\xi(s)
$$
%
In other words, we associate a set of states with the generalized
disjunction of the \bdds representing each of the states. Notice that
the satisfying assignments of the $\xi(Q)$ are exactly the assignment
representations of the states in $Q$.
%
This representation mechanism is very natural. For instance, the \bdd
$\xi(\cali)$ representing the the set of initial states of the BTUC
$\cali\eqbydef\mkset{1,2,3,4}$ is $\neg{Defused}$, while for the set of
goal states $\calg\eqbydef\mkset{5,7}$ the corresponding \bdd is
$Defused\con\neg{Clogged}$. A \bdd is also used to represent the set
$\cals$ of all the states of the domain automaton. In the BTUC,
$\xi(\cals)={\truth}$ because $\cals=2^{\calp}$. In a different
formulation, where two {\em independent} propositions $In_1$ and
$In_2$ are used to represent the position of a bomb, $\xi(\cals)$
would be the \bdd $In_1\liff\neg{In_2}$.

In general, a \bdd represents the set of (states which correspond to)
its models. As a consequence, set theoretic transformations are
naturally represented by propositional operations, as follows.

$$
\begin{array}{lcr}
\xi(\cals\backslash Q) & \eqbydef & \xi(\cals) \con \neg \xi(Q)\\
\xi(Q_1\cup Q_2) & \eqbydef & \xi(Q_1) \dis \xi(Q_2)\\
\xi(Q_1\cap Q_2) & \eqbydef & \xi(Q_1) \con \xi(Q_2)\\
\end{array}
$$

The main efficiency of this symbolic representation lies in the fact that the
cardinality of the represented set is not directly related to the size
of the \bdd.
%
For instance, $\xi(\calg)$ uses two (non-terminal) nodes to represent
two states, while $\xi(\cali)$ uses one node to represent four states.
As limit cases, $\xi(\cals)$ and $\xi(\mkset{})$ are (the leaf
\bdds) $\truth$ and $\falsity$, respectively.
%
As a further advantage, symbolic representation is extremely
efficient in dealing with irrelevant information. Notice, for
instance, that only the variable $Defused$ occurs in
$\xi(\mkset{5,6,7,8})$.
%
For this reason, a symbolic representation can have a dramatic
improvement over an explicit, enumerative representation. This is what
allows symbolic, {\bdd}-based model checkers to handle finite state
automata with a very large number of states~\cite<see for instance>{burch1}.
%
In the following, we will collapse a set of states and the \bdd
representing it.

%
Another set of {\bdd} variables, called {\em action} variables,
written \vect{\balpha}, is used to represent actions. We use one
action variable for each possible action in {\cala}. Intuitively, a
\bdd action variable is true if and only if the corresponding action
is being executed. If we assume that a sequential encoding is used,
i.e.\ no concurrent actions are allowed, we also use a \bdd,
\textsc{Seq(\balpha)}, to express that exactly one of the action
variables must be true at each time\footnote{In the specific case of
  sequential encoding, an alternative approach using only
  $\lceil\log{\sizeof{\cala}}\rceil$ is possible: an assignment to the
  action variables denotes a specific action to be executed. Two
  assignments being mutually exclusive, the constraint {\sc
    Seq(\balpha)} needs not to be represented. When the cardinality of
  the set of actions is not a power of two, the standard solution is
  to associate more than one assignment to certain values. This
  optimized solution, which is actually used in the implementation, is
  not described here for the sake of simplicity.}.
%
For the BTUC problem, where $\cala$ contains three actions, we use the
three \bdd variables $Dunk_1$, $Dunk_2$ and $Flush$, while we express
the serial encoding constraint with the following \bdd:
{\small
$$
\mbox{{\sc Seq(\balpha)}} \eqbydef
(Dunk_1\dis Dunk_2 \dis Flush)
\con\neg(Dunk_1\con Dunk_2)
\con\neg(Dunk_1\con Flush)
\con\neg(Dunk_2\con Flush)
$$
}
As for state variables, we are referring to \bdd action variables with
symbolic names for the sake of simplicity. In practice, they will be
internally represented as integers, but their position in the ordering
of the \bdd package is totally irrelevant in logical terms.

%
A \bdd in the variables {\vectx} and \vect{\balpha} represents a set
of state-action pairs, i.e.\ a relation between states and actions.
%
For instance, the applicability relation in the BTUC (i.e., all
actions are possible in all states, except for dunking actions which
require the toilet not to be clogged) is represented by the \bdd
$\neg(Clogged \con (Dunk_1 \dis Dunk_2))$.
%
Notice that it represents a set of 16 state-action pairs, each
associating a state with an applicable action.
%

A transition is a 3-tuple composed of a state (the initial state of
the transition), an action (the action being executed), and a state
(the resulting state of the transition).
%
To represent transitions, another vector {\vectnx} of \bdd variables,
called {\em next state} variables, is allocated in the \bdd package.
We write $\xi'(s)$ for the representation of the state $s$ in the next
state variables. With $\xi'(Q)$ we denote the construction of the \bdd
corresponding to the set of states Q, using each variable in the next
state vector $\vectx'$ instead of each current state variables
$\vectx$.
%
We require that $\sizeof{\vectx}=\sizeof{\vectx'}$, and assume that
the $i$-th variable in {\vectx} and the $i$-th variable in ${\vectx'}$
correspond. We define the representation of a set of states in the
next variables as follows.
$$
\xi'(s) \eqbydef \xi(s)\substwith{\vectx}{\vectnx}
$$
%
We call the operation $\Phi\substwith{\vectx}{\vectx'}$ ``forward
shifting'', because it transforms the representation of a set of
``current'' states in the representation of a set of ``next'' states.
The dual operation $\Phi\substwith{\vectx'}{\vectx}$ is called
backward shifting.
%
In the following, we call $\vectx$ {\em current} state variables to
distinguish them from next state variables. 
%
A transition is represented as an assignment to {\vectx}, {\balpha}
and ${\vectnx}$. For the BTUC, the transition corresponding to the
application of action $Dunk_1$ in state $1$ resulting in state $5$ is
represented by the following \bdd
$$
\xi(\mktuple{1,Dunk_1,5})
\eqbydef
\xi(1)\con Dunk_1\con\xi'({5})
$$

The transition relation $\calr$ of the automaton corresponding to a
planning domain is simply a set of transitions, and is thus
represented by a \bdd in the \bdd variables {\vectx}, \vect{\balpha}
and ${\vectx'}$, where each satisfying assignment represents a
possible transition.
$$
\xi(\calr)\eqbydef \textsc{Seq(\balpha)} \wedge \bigvee_{t\in{\calr}}\xi(t)
$$

% 
In the rest of this paper, we assume that the \bdd representation of a
planning domain is given. In particular, we assume as given the
vectors of variables ${\vectx},{\vectx}',\balpha$, the encoding
functions $\xi$ and $\xi'$, and we simply call $\cals$, $\calr$,
$\init$ and $\goal$ the \bdd representing the states of the domain,
the transition relation, the initial states and the goal states,
respectively. 
%
We write $\Phi(\vect{v})$ to stress that the \bdd $\Phi$ depends on
the variables in $\vect{v}$.
%
With this representation, it is possible to reason about plans,
simulating symbolically the execution of sets of actions in sets of
states, by means of QBF transformations.
%
The \bdd representing the applicability relation can be directly
obtained with the following computation.
$$
\applicability{\vectx}{\balpha}
\eqbydef
\exists {\vectx'}.\calr({\vectx},\vect{\balpha},{\vectx'})
$$
%
The resulting \bdd, \applicability{\vectx}{\balpha}, represents the set
of state-action pairs such that the action is applicable in the state.
%
The \bdd representing the states reachable from $Q$ in one step is
obtained with the following computation.
$$
\exists{\vectx}.\exists{\balpha}.
(\calr({\vectx},{\balpha},{\vectx}'){\con}Q({\vectx}))
\substwith{\vectx'}{\vectx} 
$$
%
Notice that, with this single operation, we symbolically simulate the
effect of the application of any applicable action in {\cala} to any
of the states in $Q$.
%
Similarly, the following transformation allows to symbolically compute
the {\strongpreimagename} of a set of states $Q$ under all possible
actions in one single computation:
$$
\forall {\vectx'}.
(\calr({\vectx},\vect{\balpha},{\vectx'})
\imp
Q({\vectx})
\substwith{\vectx}{\vectx'})
\ \con \ 
\applicability{\vectx}{\vect{\balpha}}
$$
%
The resulting \bdd represents all the state-action pairs
\mkpair{\vectx}{\balpha} such that {\balpha} is applicable in {\vectx}
and the execution of {\balpha} in {\vectx} results in states in $Q$.

\subsection{Symbolic Search in the Space of Belief States}

The main strength of the symbolic approach is that it allows to
perform a symbolic breadth-first search, and it provides a way for
compactly representing and efficiently expanding the frontier.
%
For instance, plans can be constructed by symbolic
breadth-first search in the space of states, repeatedly
applying the strong pre-image to the goal states~\cite{cimatti28}.
%
However, the machinery presented in the previous section cannot be
directly applied to tackle conformant planning. The basic difference
is that with conformant planning we are searching in the space of
belief states\footnote{In principle, the machinery for symbolic search
  could be used to do conformant planning if applied to the
  determinization of the domain automaton, i.e.\ an automaton having
  $2^{\cals}$ as its state space. However, this would require the
  introduction of an exponential number of state variables, which is
  impractical even for very small domains.}, and therefore the
frontier of the search is basically a {\em set of sets of states}.
%
We introduce a way to symbolically represent BsP tables. Basically,
this can be seen as a construction on demand, based on the algorithm
steps, of increasingly large portions of the space of belief states.
%
The key intuition is that a BsP table
$$
\mkset{
\mkpair{\mkset{s^1_1,\ldots,s^1_{n_1}}}{\pi_1},
\ldots,
\mkpair{\mkset{s^k_1,\ldots,s^k_{n_k}}}{\pi_k}
}
$$
%
is represented as a relation between plans (of the same length) and
states, by associating the plan directly with each state in the
belief state indexed by the plan, as follows:
% 
\begin{eqnarray}
\mkset{
\mkpair{s^1_1}{\pi_1},\ldots,\mkpair{s^1_{n_1}}{\pi_1},
\ldots,
\mkpair{s^k_1}{\pi_k},\ldots,\mkpair{s^k_{n_k}}{\pi_k}
}
\label{eqn-unfold-bsptable}
\end{eqnarray}
%
We use additional variables to represent the plans in the BsP tables.
In order to represent plans of increasing length, at each step of the
algorithm, a vector of new \bdd variables, called \emph{plan
variables}, is introduced. The vector of plan variables introduced at
the $i$-th step of the algorithm is written {\planvar{i}}, with
$\sizeof{\planvar{i}} = \sizeof{\vect{\balpha}}$, and is used to encode the $i$-th
to last action in the plan\footnote{The search being performed
backwards, plans need to be reversed once found.}. 
%
At step one of the algorithm, we introduce the vector of plan
variables {\planvar{1}} to represent the action corresponding to each
1-length possible conformant plan.
%
The BsP table ${\SPT}_{1}$ at level 1 is built by
{\ConformantPreimageName} by performing the following \bdd computation
starting from the BsP table at level 0, i.e.\ {\goal}({\vectx}):
%
$$
(\forall {\vectx'}.
(\calr({\vectx},\vect{\balpha},{\vectx'})
\imp
{\goal}({\vectx})
\substwith{\vectx}{\vectx'})
\ \con \ 
\applicability{\vectx}{\vect{\balpha}}
)\substwith{\vect{\balpha}}{\planvar{1}}
$$
%
The computation collects those state-action pairs
$\mkpair{\vectx}{\vect{\balpha}}$ such that (the action represented
by) ${\balpha}$ is applicable in (the state represented by)
${\vectx}$, and such that all the resulting (states represented by)
${\vectx'}$ are goal states. Then we replace the vector of action
variables ${\balpha}$ with the first vector of plan variables
{\planvar{1}}. The resulting \bdd, $\SPT(\vectx,\planvar{1})$,
represents a BsP table containing plans of length one in the form of a
relation between states and plans as in~(\ref{eqn-unfold-bsptable}).
%
In the general case, after step $i-1$, the BsP table $\SPT_{i-1}$,
associating belief states to plans of length $i-1$, is represented by
a \bdd in the state variables {\vectx} and in the plan variables
$\planvar{i-1},\ldots{},\planvar{1}$.
%
The computation performed by {\ConformantPreimageName} at step $i$ is
implemented as the following \bdd transformation on $\SPT_{i-1}$
%
\begin{eqnarray}
(
\forall {\vectx'}.
(\calr({\vectx},\vect{\balpha},{\vectx'})
\imp
{\SPT_{i-1}}({\vectx},\planvar{{i-1}},\ldots{},\planvar{1})
\substwith{\vectx}{\vectx'})
&
\con 
&
\applicability{\vectx}{\balpha}
)\substwith{\vect{\balpha}}{\planvar{i}}
\label{eqn-conformant-preimage}
\end{eqnarray}
%
The next state variables in $\calr$ and in $\SPT_{i-1}$ (resulting
from the forward shifting) disappear because of the universal
quantification.
%
The action variables $\balpha$ are renamed to the newly
introduced plan variables $\planvar{i}$, so that in the next step of
the algorithm the construction can be repeated.
%

{\GetPlanName} extracts the assignments to plan variables such that 
the corresponding set contains the initial states.
In terms of \bdd transformations, {\GetPlanName} is implemented as follows:
%
\begin{eqnarray}
\forall {\vectx}.
(\init({\vectx})\imp {\SPT_{i}}({\vectx},\planvar{{i}},\ldots,\planvar{{1}}))
\end{eqnarray}
%
The result is a \bdd in the plan variables
$\planvar{{i}},\ldots,\planvar{{1}}$. If the \bdd is \falsity, then
there are no solutions of length $i$. Otherwise, each of the
satisfying assignments to the resulting \bdd represents a conformant
solution to the problem.

\begin{figure}[tb]
\begin{center}
{{\psfig{figure=fig/redundant.eps,width=0.7\textwidth}}}
\end{center}
\caption{An example of pruning of a BsP table}
\label{fig-pruning-plans}
\end{figure}

To guarantee the termination of the algorithm, at each step the BsP
table returned by {\ConformantPreimageName} is simplified by
{{\ConformantPruneName}} by removing all the belief states which do
not deserve further expansion.
%
This requires the comparison of the belief states contained in the BsP
table with the belief states contained in each of the BsP tables built
at previous levels.
%
This is one of the crucial steps in terms of efficiency.
An earlier implementation of this step with logical \bdd
transformations, following directly from the set-theoretical
definition of~\ConformantPruneName, was extremely inefficient~\cite{cimatti33}.
%
Furthermore, we noticed that the serial encoding could yield BsP
tables containing a large number of equivalent plans, all indexing
exactly the same belief state. Often these equivalent plans only
differ in the order of some independent actions, and this is a
potential source of combinatorial explosion. This occurs even in the
simple version of the BTUC (in Figure~\ref{fig-bt-solution}, two
equivalent conformant plans are associated with Bs$_{8}$).
%
Therefore, we developed a new implementation which could tackle these
two problems by operating directly on the BsP table. The idea is
depicted in Figure~\ref{fig-pruning-plans}. Initially, the cache
contains Bs$_{1}$, Bs$_{2}$ and Bs$_{3}$. The simplification
performs a traversal of the {\bdd}, by accumulating the subtrees
representing belief states, comparing them with the ones built at
previous levels, and inserting the new ones in the cache (in
Figure~\ref{fig-pruning-plans}, Bs$_{4}$, Bs$_{5}$ and Bs$_{6}$). Each
time a path is identified which represents a plan indexing an already cached belief
state, the plan is redundant and the corresponding path is
pruned\footnote{This pruning mechanism is actually weaker than the
  earlier one~\cite{cimatti33}. Here we require that the same belief state must
  not be expanded twice during the search, while in the earlier version
  we prune belief states {\em contained} in previously explored ones.
  This may increase the {\em number} of explored belief states.
  However, it allows for a much more efficient implementation, without
  impacting on the properties of the
algorithm.}.
%
The cost of the simplification is linear in the size of the BsP being
simplified and is highly effective in pruning.
%

\begin{figure}[tb]
\begin{boxverbatim}
\begin{verbatim}
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;
\end{verbatim}
\end{boxverbatim}

\caption{An {\ar} description for the BTUC problem}
\label{fig-ar-btuc}
\end{figure}


\section{CMBP: a BDD-based Conformant Planner}
\label{sec-cmbp}

{\cmbp} (Conformant Model Based Planner) is a conformant planner
implementing the data structures and algorithms for conformant
planning described in the previous sections. 
%
{\cmbp} inherits the features of
{\mbp}~\cite{cimatti27,cimatti28,cimatti29}, a planner based on
symbolic model checking techniques.
%
{\mbp} is built on top of {\nusmv}, a symbolic model checker jointly
developed by ITC-IRST and CMU~\shortcite{NUSMVSTTT}, and uses the
CUDD~\cite{somenzi1} state-of-the-art {\bdd} package.
%
{\mbp} is a two-stage system. In the first stage, an internal
\bdd-based representation of the domain is built, while in the second
stage planning problems can be solved.
%
Currently, planning domains are described by means of the high-level
action language {\ar}~\cite{giunchiglia100}. {\ar} allows to specify
(conditional and uncertain) effects of actions by means of high level
assertions.
%
For instance, Figure~\ref{fig-ar-btuc} shows the {\ar} description of
the BTUC problem\footnote{{\tt !}~and {\tt \&} stand for negation and
  conjunction, respectively. The description is slightly edited for
  the sake of readability. In particular, {\mbp} currently does not
  accept parameterized {\ar} descriptions. In practice we use a script
  language to generate ground instances of different complexity
  from a parameterized problem description.}.
%
The semantics of {\ar} yields a serial encoding, i.e.\ exactly one
action is assumed to be executed at each time.
%
The automaton corresponding to an {\ar} description is obtained by
means of the minimization procedure by Giunchiglia~\citeyear{giunchiglia91}. This procedure solves the frame problem and
the ramification problem, and is efficiently implemented in {\mbp}~\cite{cimatti27}.
%
Because of the separation between the domain construction and the
planning phases, {\mbp} is not bound to {\ar}. Standard deterministic
domains specified in {\pddl}~\shortcite{pddlreference} can also be given to
{\mbp} by means of a (prototype) compiler.
%
We are also starting to investigate the potential use of the {\calc}
action language~\cite{AAAI98_IAAI98*623}, 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
planning~\cite{cimatti28}, and for strong cyclic plannig~\cite{cimatti29,danieletraversovardi}.
%
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
Section~\ref{sec-algo}, {\cmbp} implements an algorithm based on
forward search, which allows to exploit the initial knowledge of the
problem, sometimes resulting in significant speed
ups~\cite{cimatti-roveri-wshop-aips2000}. Backward and forward search
can also be combined, to tackle the exponential growth of the search
time with the depth of search.
%
For all these algorithms, different options enable and
disable different versions of the termination check.
%

\section{Experimental Evaluation}
\label{sec-experiments}

In this section we present an experimental evaluation of our approach,
which was carried out by comparing \cmbp with state-of-the-art
conformant planners.
%
We first describe the other conformant planners considered in the
analysis, and then we present the experimental comparison that was
carried out.

\subsection{Other Conformant Planners}

%
{\cgp}~\cite{cgp} extends the ideas of
{\graphplan}~\cite{BlumFurst95,BlumFurst97} to deal with uncertainty.
Basically, a planning graph is built of every possible sequence of
possible worlds, and constraints among planning graphs are propagated
to ensure conformance.
%
The {\cgp} system takes as input domains described in an extension of
{\pddl}~\cite{pddlreference}, where it is possible to specify
uncertainty in the initial state.
%
{\cgp} inherits from {\graphplan} the ability to deal with parallel
actions.
%
{\cgp} was the first efficient conformant planner: it was shown to
outperform several other planners such as Buridan~\cite{peot2} and
UDTPOP~\cite{kushm.hanks-1995:algorfor:journal:239}. The detailed
comparison reported by Smith and Weld~\citeyear{cgp} leaves no doubt on the superiority
of {\cgp} with respect to these systems. Therefore, we compared
{\cmbp} with {\cgp} and did not consider the other systems analyzed
by Smith and Weld~\citeyear{cgp}.
%
{\cmbp} is more expressive than {\cgp} in two respects. First, {\cgp}
can only handle uncertainty in the initial state. For instance, {\cgp}
cannot analyze the BTUC domain presented in
Section~\ref{sec-conformant-planning}. Smith and Weld \citeyear{cgp}
describe how the approach can be extended to actions with uncertain
effects.  Second, {\cgp} cannot conclude that a planning problem has
no conformant solutions.

%
{\qbfplan} is (our name for) the planning system by
Rintanen~\citeyear{rintanen1}. {\qbfplan} generalizes the idea of
SAT-based planning~\cite{KautzEtal96,KautzSelman96,kautzselman} to
nondeterministic domains, by encoding problems in QBF.
%
The {\qbfplan} approach is not limited to conformant planning, but can
be used to do conditional planning under uncertainty, also under
partial observability: different encodings, corresponding to different
structures in the resulting plan, can be synthesized. 
%
In this paper, we are only considering encodings which enforce the
resulting plan to be a sequence.
%
Given a bound on the length of the plan, first a QBF encoding of the
problem is generated, and then a QBF solver~\cite{rintanen2} is
called. If no solution is found, a new encoding for a longer plan must
be generated and solved.
%
{\qbfplan} is able to handle actions with uncertain effects. This is
done by introducing auxiliary (choice) variables, the assignments to
which the different possible outcomes of actions correspond. These
variables are universally quantified to ensure conformance of
the solution.
%
Differently from e.g.\ {\blackbox}~\cite{kautzselman}, {\qbfplan} does
not have a heuristic to guess the ``right'' length of the plan. Given
a limit in the length of the plan, it generates all the encodings up
to the specified length, and repeatedly calls the QBF solver on
encodings of increasing length until a plan is found. 
%
As {\cgp}, {\qbfplan} cannot conclude that a planning problem has no
conformant solutions.
%
Similarly to {\cmbp}, {\qbfplan} relies on a symbolic representation
of the problem, although QBF transformations are performed by a theorem
prover rather than with \bdds.

%
\gpt~\cite{bonet1} is a general planning framework, where the
conformant planning problem is seen as deterministic search problem in
the space of belief states. \gpt uses an explicit representation of
the search space, where each belief state is represented as a separate
data structure. The search is based on the \astar
algorithm~\cite{NIL80}, driven by domain dependent heuristics which
are automatically generated from the problem description.
%
\gpt accepts problem descriptions in a syntax based on \pddl, extended
to deal with probabilities and uncertainty.
%
It is possible to represent domains with uncertain action effects
(although the representation of actions resulting in a large number of
different states is rather awkward). As for the planning algorithm,
{\gpt} is able to conclude that a given planning problem has no
conformant solution by exhaustively exploring the space of belief
states.

\subsection{Experiments and Results}

The evaluation was performed by running the systems on a number of
parameterized problem domains.
% 
We considered all the problems from the \cgp and \gpt distributions,
plus other problems which were defined to test specific features of
the planners.
%
We considered domains with uncertainty limited to the initial state,
and domains with uncertain action effects. Besides problems admitting
a solution, we also considered problems not admitting a solution, in
which case we measured the effectiveness of the plannner in returning
with failure.

Given their different expressivity, it was not possible to run all the
systems on all the examples.
%
{\cmbp} was run on all the classes of examples, while {\gpt} was run
on all but one.
%
\cgp was run only on the problems which admit a solution, and with
uncertainty limited to the initial condition.
%
{\qbfplan} was run on all the examples for which an encoding was
already available from the {\qbfplan} distribution. This is only a
subset of the problems expressible in {\cgp}. The main limiting factor
was the low level of the input format of {\qbfplan}: problem
descriptions must be specified as ML code which generates the QBF
encodings.  Writing new encodings turned out to be a very
difficult task, especially due to the lack of documentation.
% 

We ran \cgp, \qbfplan and \cmbp on an Intel 300MHz Pentium-II, 512MB
RAM, running Linux.
%
The comparison between \cmbp and \gpt was run on a Sun
Ultra Sparc 270MHz, 128Mb RAM running Solaris (\gpt was available as a
binary). However, the performance of the two machines is comparable ---
the run times for \cmbp were almost identical.
%
CPU time was limited to 7200 sec (two hours) for each test. To avoid
swapping, the memory limit was fixed to the physical memory of the
machine. In the following, we write ``\tlim'' or ``\mlim'' for a test
that did not complete within the above time and memory limits,
respectively.
%
The performance of the systems are reported in tables listing only the
search time. 
%
This excludes the time needed by {\qbfplan} to generate the encodings,
the time spent by {\cmbp} to construct the automaton representation
into \bdd, and the time needed by {\gpt} to generate the source code
of its internal representation, and to compile it. Overall, the most
significant time ignored is the automaton construction of {\cmbp}.
Currently, the automaton construction is not fully optimized. 
% 
Even in the most complex examples, however, the construction never
required more than a couple of minutes\footnote{More precisely, the
  maximum time in building the automaton was required for the
  BMTC(10,6) examples (88~secs.), the RING(10) example (77~secs.), the
  BMTC(9,6) examples (40~secs.), and the BMTC(10,5) examples
  (41~secs.). For most of the other examples, the time required for
  the automaton construction was less than 10 seconds.}.


\subsubsection{Bomb in the Toilet}

\paragraph{Bomb in the Toilet.}
The first domain we tackled is the classical bomb in the toilet, where
there is no notion of clogging. We call the problem BT($p$), where the
parameter $p$ is the number of packages. The only uncertainty is in
the initial condition, where it is not known which package contains
the bomb. The goal is to defuse the bomb.
%
The results for the BT problem are shown in Table~\ref{tab-bt}. 
%
The columns relative to {\cmbp} are the length of the plan ($|$P$|$),
the number of cached belief states
and the number of hits in the cache (\#BS and \#NBS respectively), the
time (expressed in seconds) needed for searching the automaton under
Pentium/Linux (Time(L)) and under Sparc/Solaris (Time(S)). In the
following, when clear from the context, the execution platform is
omitted.
%
The columns relative to {\cgp} are the number of levels in the
planning graphs (\sizeof{L}) and the search time.
%
The column relative to \gpt is the search time.

\begin{table}[htb]
\scriptsize
\begin{center}
\begin{tabular}{|l||r|r|r|r||r|r||r|}\cline{2-8}
\multicolumn{1}{c|}{\ }       &\multicolumn{4}{c||}{\cmbp}           &\multicolumn{2}{c||}{\cgp} & \gpt \\\hline
       & \PL      & \#BS/\#BSH & Time(L) & Time(S) & \LL & \CTD  &  \CTI \\\hline
BT(2)  & 2        & 2    / 2    &  0.000  &  0.000  & 1   & 0.000 & 0.074 \\\hline
BT(3)  & 3        & 6    / 11   &  0.000  &  0.000  & 1   & 0.000 & 0.077 \\\hline
BT(4)  & 4        & 14   / 36   &  0.000  &  0.000  & 1   & 0.000 & 0.080 \\\hline
BT(5)  & 5        & 30   / 103  &  0.000  &  0.000  & 1   & 0.000 & 0.087 \\\hline
BT(6)  & 6        & 62   / 266  &  0.010  &  0.010  & 1   & 0.010 & 0.102 \\\hline
BT(7)  & 7        & 126  / 641  &  0.010  &  0.030  & 1   & 0.010 & 0.139 \\\hline
BT(8)  & 8        & 254  / 1496 &  0.030  &  0.030  & 1   & 0.020 & 0.230 \\\hline
BT(9)  & 9        & 510  / 3463 &  0.070  &  0.070  & 1   & 0.020 & 0.481 \\\hline
BT(10) & 10       & 1022 / 7862 &  0.150  &  0.140  & 1   & 0.020 & 1.018 \\\hline
\end{tabular}
\end{center}

\caption{Results for the BT problems.}
\label{tab-bt}
\end{table}

The BT problem is intrinsically parallel, i.e.\ the depth of the
planning graph is always one, because all the packages can be dunked
at the same time.
%
{\cgp} inherits from {\graphplan} the ability to deal with parallel
actions efficiently, and therefore it is almost insensitive to the
problem size. For this problem {\cgp} outperforms both {\cmbp} and
\gpt. Notice that the number of levels explored by {\cgp} is always 1,
while the length of the plan produced by {\cmbp} and {\cgp} grows
linearly. \cmbp performs slightly better than \gpt.

\paragraph{Bomb in the Toilet with Clogging.}
We call BTC($p$) the extension of the BT($p$) where dunking a package
(always) clogs the toilet, flushing can remove the clogging, and no
clogging is a precondition for dunking a package. Again, $p$ is the
number of packages. The toilet is initially not clogged. With this
modification, the problem no longer allows for a parallel solution.
%
The results for this problem are listed in Table~\ref{tab-btc}. 
%
\begin{table}[htb]
\scriptsize
\begin{center}
\begin{tabular}{cc}\renewcommand{\tabcolsep}{1mm}
\begin{tabular}{|l||r|r|r|r||r|r||r|}\cline{2-8}
\multicolumn{1}{c|}{\ } &\multicolumn{4}{c||}{\cmbp}       &\multicolumn{2}{c||}{\cgp}  & \gpt \\\hline
       & \PL        & \#BS/\#BSH     & Time(L)& Time(S)& \LL    & \CTD    &  \CTI \\\hline
BTC(2) & 3          & 6     / 8      & 0.000  & 0.010  & 3      &   0.000 &   0.074 \\ \hline
BTC(3) & 5          & 14    / 23     & 0.000  & 0.000  & 5      &   0.010 &   0.077 \\ \hline
BTC(4) & 7          & 30    / 61     & 0.010  & 0.010  & 7      &   0.030 &   0.082 \\ \hline
BTC(5) & 9          & 62    / 150    & 0.020  & 0.020  & 9      &   0.130 &   0.094 \\ \hline
BTC(6) & 11         & 126   / 347    & 0.020  & 0.020  & 11     &   0.860 &   0.113 \\ \hline
BTC(7) & 13         & 254   / 796    & 0.070  & 0.080  & 13     &   2.980 &   0.166 \\ \hline
BTC(8) & 15         & 510   / 1844   & 0.150  & 0.160  & 15     &  13.690 &   0.288 \\ \hline
BTC(9) & 17         & 1022  / 4149   & 0.320  & 0.330  & 17     &  41.010 &   0.607 \\ \hline
BTC(10)& 19         & 2046  / 9190   & 0.710  & 0.700  & 19     & 157.590 &   1.309 \\ \hline
\multicolumn{8}{c}{\ } \\[-4pt]\hline
BTC(16)& 31         &131070 / 921355 & 99.200 & 99.800 &        &         & 351.457 \\ \hline

\end{tabular}
%
&\renewcommand{\tabcolsep}{1mm}
\begin{tabular}{|r|r||r|r|}\hline
\multicolumn{4}{|c|}{\qbfplan} \\\hline
\multicolumn{2}{|c||}{BTC(6)} &\multicolumn{2}{c|}{BTC(10)}
\\\hline
\PL    & \CTD   &\PL    & \CTI   \\\hline
1      & 0.00   &1      &0.02      \\\hline
2      & 0.01   &2      &0.03      \\\hline
3      & 0.26   &3      &0.78      \\\hline
4      & 0.63   &4      &2.30      \\\hline
5      & 1.53   &5      &4.87      \\\hline
6      & 2.82   &6      &8.90      \\\hline
7      & 6.80   &7      &22.61     \\\hline
8      &14.06   &8      &52.72     \\\hline
9      &35.59   &9      &156.12    \\\hline
10     &93.34   &10     &410.86    \\\hline
11     &(+) 2.48&11     &1280.88   \\\hline 
       &        &13     &3924.96   \\\hline 
       &        &14     &    \tlim \\\hline 
       &        &$\ldots$&$\ldots$ \\\hline 
       &        &18     &    \tlim \\\hline 
       &        &19     &(+) 16.84 \\\hline 
\end{tabular}
\end{tabular}
\end{center}

\caption{Results for the BTC problems.}
\label{tab-btc}
\end{table}
%
The impact of the depth of the plan length becomes significant for all
systems. Both {\cmbp} and \gpt outperform {\cgp}. In this case \cmbp
performs better than \gpt, especially on large instances (see BTC(16)).
% 
The comparison with {\qbfplan} is limited to the 6 and 10 package
instances (the ones available from the distribution package). The
performance of {\qbfplan} is reported in the left table in
Table~\ref{tab-btc}. Each line reports the time needed to decide
whether there is a plan of length $i$. The performance of {\qbfplan}
is rather good when tackling an encoding admitting a solution (in
Table~\ref{tab-btc} these entries are labeled by (+)). For
instance, in the BTC(10) {\qbfplan} finds the solution solving the
encodings at depth 19 reasonably fast. However, when a solution
cannot be found, i.e.\  the QBF formula admits no model, the
performance of {\qbfplan} degrades significantly (for the depth 18
encoding, we let the solver run for 10 CPU hours and it did not
complete the search). 
%
Because of the difference in performance, and the difficulty in
writing new domains, in the rest of the comparison we will not
consider {\qbfplan}.


\paragraph{Bomb in Multiple Toilets.} 

\begin{table}
{
\tiny
\begin{center}
\begin{sideways}
\hspace*{-0.5cm}\renewcommand{\tabcolsep}{1.7mm}
\begin{tabular}{|r||c|r|r|r|c|r||c|r|r|c|r||c|r|r|c|r|}
\cline{2-17}
\multicolumn{1}{c|}{\ }
              &\multicolumn{6}{c||}{Low Uncertainty}
              &\multicolumn{5}{c||}{Mid Uncertainty}
              &\multicolumn{5}{c|}{High Uncertainty}
\\\cline{1-17}
\multicolumn{1}{|c||}{{\sc bmtc}} & \multicolumn{1}{c|}{\ }
              &\multicolumn{3}{c|}{\cmbp} &\multicolumn{2}{c||}{\cgp}
              &\multicolumn{1}{c|}{\ } &\multicolumn{2}{c|}{\cmbp} &\multicolumn{2}{c||}{\cgp}
              &\multicolumn{1}{c|}{\ } &\multicolumn{2}{c|}{\cmbp} &\multicolumn{2}{c|}{\cgp}
 \\\cline{2-17}\cline{2-17}
    (p,t) &IS&\PL    & \#BS/\#BSH   & \CTI  &\LL &  \CTD  &IS& \#BS/\#BSH   & \CTI  &\LL& \CTD &IS & \#BS/\#BSH & \CTI  &\LL& \CTI   \\\hline\hline
    (2,2) &2 &2      & 10   / 18    & 0.000 &1  &   0.000&4 & 12   / 34    & 0.000 & 2 & 0.010&8  & 12   / 40   &  0.000 & 2 &   0.030\\\hline
    (3,2) &3 &4      & 26   / 84    & 0.000 &3  &   0.020&6 & 28   / 106   & 0.000 & 3 & 0.040&12 & 28   / 112  &  0.010 & 4 &  13.560\\\hline
    (4,2) &4 &6      & 58   / 250   & 0.020 &3  &   0.030&8 & 60   / 286   & 0.020 & 4 & 0.460&16 & 60   / 294  &  0.010 & 4 & 145.830\\\hline
    (5,2) &5 &8      & 122  / 652   & 0.030 &5  &   1.390&10& 124  / 702   & 0.030 & 5 &13,180&20 & 124  / 710  &  0.040 & 4 & \tlim  \\\hline
    (6,2) &6 &10     & 250  / 1552  & 0.070 &5  &   3.490&12& 252  / 1614  & 0.080 & 5 & \tlim&24 & 252  / 1622 &  0.080 &   &        \\\hline
    (7,2) &7 &12     & 506  / 3586  & 0.180 &7  & 508.510&14& 508  / 3662  & 0.190 &   &      &28 & 508  / 3670 &  0.190 &   &        \\\hline
    (8,2) &8 &14     & 1018 / 8262  & 0.400 &7  & 918.960&16& 1020 / 8362  & 0.430 &   &      &32 & 1020 / 8372 &  0.450 &   &        \\\hline
    (9,2) &9 &16     & 2042 / 18484 & 0.940 &7  &  \tlim &18& 2044 / 18602 & 0.960 &   &      &36 & 2044 / 18612&  0.950 &   &        \\\hline
    (10,2)&10&18     & 4090 / 40676 & 1.820 &   &        &20& 4092 / 40810 & 1.990 &   &      &40 & 4092 / 40820&  2.030 &   &        \\\hline\hline
%                                                                                       
    (2,3) &2 &2      & 18   / 42    & 0.000 &1  &   0.010&8 & 24  / 99     & 0.000 & 2 & 0.090&16 & 24   / 126   & 0.010 & 2 &   0.170\\\hline
    (3,3) &3 &3      & 47   / 202   & 0.010 &1  &   0.010&12& 56  / 349    & 0.020 & 2 & 0.200&24 & 56   / 373   & 0.020 & 2 &   0.690\\\hline
    (4,3) &4 &5      & 110  / 736   & 0.030 &3  &   0.110&16& 120 / 942    & 0.040 & 3 & 0.990&32 & 120  / 972   & 0.040 & 3 & \tlim  \\\hline
    (5,3) &5 &7      & 237  / 2034  & 0.080 &3  &   0.170&20& 248 / 2335   & 0.110 & 3 & \tlim&40 & 248  / 2371  & 0.120 &   &        \\\hline
    (6,3) &6 &9      & 492  / 5106  & 0.230 &3  &   0.340&24& 504 / 5520   & 0.250 &   &      &48 & 504  / 5562  & 0.240 &   &        \\\hline
    (7,3) &7 &11     & 1003 / 12128 & 0.560 &5  &6248.010&28& 101 / 12673  & 0.590 &   &      &56 & 1016 / 12721 & 0.640 &   &        \\\hline
    (8,3) &8 &13     & 2026 / 27836 & 1.300 &4  &  \tlim &32& 204 / 28530  & 1.350 &   &      &64 & 2040 / 28584 & 1.330 &   &        \\\hline
    (9,3) &9 &15     & 4073 / 62470 & 3.330 &   &        &36& 408 / 63331  & 3.370 &   &      &72 & 4088 / 63391 & 3.390 &   &        \\\hline
    (10,3)&10&17     & 8168 / 138046& 7.280 &   &        &40& 818 / 139092 & 7.460 &   &      &80 & 8184 / 139158& 7.430 &   &        \\\hline\hline
%                                                                                      
    (2,4) &2 &2      & 29    / 75     & 0.010  &1  &   0.000&8 & 29    / 75    &  0.000 & 1 & 0.020&32 & 48    / 332   & 0.020  & 2 &   1.610\\\hline
    (3,4) &3 &3      & 92    / 492    & 0.020  &1  &   0.010&12& 108   / 808   &  0.030 & 2 & 0.290&48 & 112   / 960   & 0.040  & 2 &   8.690\\\hline
    (4,4) &4 &4      & 206   / 1686   & 0.060  &1  &   0.010&16& 236   / 2356  &  0.080 & 2 & 0.730&64 & 240   / 2532  & 0.090  & 2 &  32.190\\\hline
    (5,4) &5 &6      & 457   / 4987   & 0.190  &3  &   0.500&20& 492   / 5888  &  0.230 & 2 &\tlim &80 & 496   / 6092  & 0.240  & 3 &  \tlim \\\hline
    (6,4) &6 &8      & 964   / 12456  & 0.410  &3  &   1.160&24& 1004  / 13648 &  0.470 &   &      &96 & 1008  / 13876 & 0.470  &   &        \\\hline
    (7,4) &7 &10     & 1983  / 29453  & 1.040  &3  &   2.410&28& 2028  / 31004 &  1.120 &   &      &112& 2032  / 31260 & 1.160  &   &        \\\hline
    (8,4) &8 &12     & 4026  / 68466  & 2.740  &3  &   8.540&32& 4076  / 70584 &  2.870 &   &      &128& 4080  / 70912 & 2.910  &   &        \\\hline
    (9,4) &9 &14     & 8117  / 153895 & 6.690  &4  & \tlim  &36& 8172  / 15654 &  6.900 &   &      &144& 8176  / 156904& 6.970  &   &        \\\hline
    (10,4)&10&16     & 16304 / 339160 & 14.420 &   &        &40& 16364 / 34234 & 14.630 &   &      &160& 16368 / 342736& 14.770 &   &        \\\hline\hline
%                                                                                    
    (2,5) &2 &2      & 43    / 117    & 0.010  &1  &   0.010&16& 43    / 117   & 0.010  & 1 & 0.130&64 & 93    / 751   & 0.030 & 2 &  21.120\\\hline
    (3,5) &3 &3      & 164   / 1031   & 0.040  &1  &   0.020&24& 212   / 2008  & 0.080  & 2 & 3.540&96 & 224   / 2591  & 0.120 & 2 & 138.430\\\hline
    (4,5) &4 &4      & 416   / 4304   & 0.150  &1  &   0.020&32& 475   / 6375  & 0.260  & 2 & 6.320&128& 480   / 6740  & 0.260 & 2 & 551.210\\\hline
    (5,5) &5 &5      & 872   / 11763  & 0.490  &1  &   0.050&40& 987   / 15928 & 0.700  & 2 &37,959&160& 992   / 16393 & 0.730 & 2 &1523.840\\\hline
    (6,5) &6 &7      & 1875  / 31695  & 1.300  &3  &   5.920&48& 2011  / 37759 & 1.890  & 2 &\tlim &192& 2016  / 38334 & 1.980 & 2 &  \tlim \\\hline
    (7,5) &7 &9      & 3901  / 78009  & 3.990  &3  &  18.410&56& 4059  / 86716 & 4.480  &   &      &224& 4064  / 87411 & 4.540 &   &        \\\hline
    (8,5) &8 &11     & 7974  / 183036 & 9.670  &3  &  62.040&64& 8155  / 195055& 10.590 &   &      &256& 8160  / 195880& 10.640&   &        \\\hline
    (9,5) &9 &13     & 16142 / 416333 & 24.250 &3  & 194.640&72& 16347 / 432408& 25.600 &   &      &288& 16352 / 433373& 25.370&   &        \\\hline
    (10,5)&10&15     & 32501 / 927329 & 54.910 &3  & 289,680&80& 32731 / 948279& 56.420 &   &      &320& 32736 / 949394& 56.290&   &        \\\hline\hline
%                                                                                
    (2,6) &2 &2      & 60    / 168        & 0.010   &1  &   0.010&16&  60    / 168        & 0.010  & 1 & 0.200&128& 171   / 1533       & 0.040  & 2 & 337.604\\\hline
    (3,6) &3 &3      & 270   / 1848       & 0.070   &1  &   0.010&24&  270   / 1848       & 0.070  & 1 & 0.830&192& 448   / 6248       & 0.310  & 2 &1459.110\\\hline
    (4,6) &4 &4      & 786   / 9294       & 0.300   &1  &   0.040&32&  920   / 13810      & 0.500  & 2 &30.630&256& 960   / 16344      & 0.690  & 2 &5643.450\\\hline
    (5,6) &5 &5      & 1777  / 29075      & 1.160   &1  &   0.060&40&  1958  / 37636      & 1.940  & 2 &30.140&320& 1984  / 39710      & 2.120  & 2 &  \tlim \\\hline
    (6,6) &6 &6      & 3613  / 71123      & 3.290   &1  &   0.100&48&  4005  / 90111      & 4.080  & 2 &57.300&384& 4032  / 92772      & 4.600  &   &        \\\hline
    (7,6) &7 &8      & 7625  / 180127     & 9.060   &3  & 211.720&56&  8100  / 208050     & 10.130 & 2 &\tlim &448& 8128  / 211370     & 10.400 &   &        \\\hline
    (8,6) &8 &10     & 15726 / 429198     & 20.710  &3  &1015.160&64&  16291 / 469277     & 22.620 &   &      &512& 16320 / 473328     & 23.000 &   &        \\\hline
    (9,6) &9 &12     & 32012 / 986188     & 50.610  &3  &3051.990&72&  32674 / 1.04173e+06& 53.510 &   &      &576& 32704 / 1.04658e+06& 54.010 &   &        \\\hline
    (10,6)&10&14     & 64675 / 2.21106e+06& 111.830 &2  &  \tlim &80&  65441 / 2.28585e+06& 116.440&   &      &640& 65472 / 2.29158e+06& 116.240&   &        \\\hline
\multicolumn{17}{p{0.92\textheight}}{\caption{Results for the BMTC problems.\label{tab-bmtc-cgp}}}
\end{tabular}
\end{sideways}
\end{center}
}

\end{table}

\begin{table}[htb]
{\scriptsize
\begin{center}
\begin{tabular}{|c||r|r||r|r|}
\cline{2-5}
\multicolumn{1}{c|}{\ }
              &\multicolumn{2}{c||}{Low Unc.}
              &\multicolumn{2}{c|}{High Unc.}
\\\cline{1-5}
\multicolumn{1}{|c||}{{\sc bmtc}} 
              &\multicolumn{1}{c|}{\cmbp} &\multicolumn{1}{c||}{\gpt}
              &\multicolumn{1}{c|}{\cmbp} &\multicolumn{1}{c|}{\gpt}
 \\\cline{2-5}\cline{2-5}
    (p,t) & \CTI  & \CTD     & \CTI  & \CTI   \\\hline\hline
    (2,2) & 0.000 &    0.079 & 0.010 &  0.079 \\\hline                 
    (3,2) & 0.010 &    0.087 & 0.010 &  0.091 \\\hline           
    (4,2) & 0.000 &    0.105 & 0.020 &  0.121 \\\hline           
    (5,2) & 0.040 &    0.146 & 0.040 &  0.198 \\\hline          
    (6,2) & 0.080 &    0.227 & 0.070 &  0.376 \\\hline         
    (7,2) & 0.190 &    0.441 & 0.200 &  0.850 \\\hline          
    (8,2) & 0.390 &    0.922 & 0.400 &  1.966 \\\hline          
    (9,2) & 0.910 &    2.211 & 0.950 &  4.743 \\\hline         
   (10,2) & 1.850 &    5.169 & 1.900 & 10.620 \\\hline\hline         

    (2,4) &  0.000  &    0.109 &   0.010 &   0.121 \\\hline
    (3,4) &  0.010  &    0.156 &   0.040 &   0.284 \\\hline
    (4,4) &  0.050  &    0.270 &   0.100 &   1.016 \\\hline
    (5,4) &  0.180  &    0.616 &   0.240 &   3.282 \\\hline
    (6,4) &  0.370  &    1.435 &   0.460 &   9.374 \\\hline
    (7,4) &  1.080  &    3.484 &   1.190 &  27.348 \\\hline
    (8,4) &  2.700  &    8.767 &   2.830 &  72.344 \\\hline
    (9,4) &  8.970  &   23.858 &   6.920 & 180.039 \\\hline
   (10,4) & 14.210  &   59.966 & 114.690 & 440.308 \\\hline\hline

    (2,6) & 0.010   &    0.303 &   0.060 &   0.482 \\\hline
    (3,6) & 0.050   &    0.562 &   0.260 &   2.471 \\\hline
    (4,6) & 0.310   &    1.354 &   0.620 &  17.406 \\\hline
    (5,6) & 1.110   &    3.257 &   2.060 &  74.623 \\\hline
    (6,6) & 3.400   &    8.691 &   4.660 & 243.113 \\\hline
    (7,6) & 8.910   &   25.677 &  10.430 & 701.431 \\\hline
    (8,6) & 21.240  &   68.427 &  23.860 & \mlim   \\\hline
    (9,6) & 49.880  &  289.000 &  54.190 &         \\\hline
   (10,6) & 113.680 &  486.969 & 118.590 &         \\\hline
\end{tabular}
\end{center}
}
\caption{Results for the BMTC problems.}
\label{tab-bmtc-gpt}
\end{table}

The next domain, called BMTC($p$,$t$), is the generalization of the
BTC problem to the case of multiple toilets ($p$ is the number of
packages, while $t$ is the number of toilets).
%
The problem becomes more parallelizable when the number of toilets
increases.
%
Furthermore, we considered three versions of the problem
with increasing uncertainty in the initial states.
%
In the first class of tests (``Low Uncertainty'' columns), the only
uncertainty is the position of the bomb which is unknown, while
toilets are known to be not clogged.
%
The ``Mid Uncertainty'' and ``High Uncertainty'' columns show the
results in presence of more uncertainty in the initial state. In the
second [third, respectively] class of tests, the status of every odd
[every, resp.] toilet can be either clogged or not clogged. This
increases the number of possible initial states.


The results are reported in Table~\ref{tab-bmtc-cgp} (for the
comparison with \cgp) and in Table~\ref{tab-bmtc-gpt} (for the
comparison with \gpt). The IS column represents the number of initial
states of the corresponding problem.
%
{\cgp} is able to fully exploit the parallelism of the problem.
However, {\cgp} is never able to explore more than 9 levels in the
planning graph, with depth decreasing with the number of initial states.
%
The results also show that {\cmbp} and {\gpt} are much less sensitive
to the number of initial states than {\cgp}. With increasing initial
uncertainty, {\cgp} is almost unable to solve what were trivial
problems. \gpt performs better than \cgp, but it suffers from the
explicit representation of the search space. 

\paragraph{Bomb in the Toilet with Uncertain Clogging.}
% 
The BTUC($p$) domain is the domain described in
Section~\ref{sec-background}, where clogging is an uncertain outcome 
of dunking a package.
%
This kind of problem cannot be expressed in~{\cgp}. 
%
The results for \cmbp and \gpt are reported in Table~\ref{tab-btuc}.
Although \cmbp performs better than \gpt (by a factor of two to
three), there is no significant difference in the behavior.
%
It is interesting to compare the results of \cmbp for the BTC and BTUC
problems.
%
For \gpt a slight difference is noticeable, resulting from the
increased branching factor in the search space due to the
uncertainties in the effects of action executions.
%
In the performance of {\cmbp}, the number of uncertainties is not a
direct factor --- for example, in the BTC(16) and BTUC(16), the
performance is almost the same.
%
\begin{table}[th]
\scriptsize
\begin{center}
\begin{tabular}{|l||r|r|r||r|}\cline{2-5}
\multicolumn{1}{c|}{\ } &\multicolumn{3}{c||}{\cmbp} & \gpt \\\hline
        & \PL     & \#BS/\#BSH      & \CTD   & \CTI   \\\hline
BTUC(2) & 3       & 6      / 8      & 0.000  & 0.076  \\\hline
BTUC(3) & 5       & 14     / 23     & 0.000  & 0.078  \\\hline
BTUC(4) & 7       & 30     / 61     & 0.010  & 0.085  \\\hline
BTUC(5) & 9       & 62     / 150    & 0.010  & 0.098  \\\hline
BTUC(6) & 11      & 126    / 347    & 0.030  & 0.128  \\\hline
BTUC(7) & 13      & 254    / 796    & 0.050  & 0.205  \\\hline
BTUC(8) & 15      & 510    / 1844   & 0.170  & 0.380  \\\hline
BTUC(9) & 17      & 1022   / 4149   & 0.310  & 0.812  \\\hline
BTUC(10)& 19      & 2046   / 9190   & 0.720  & 1.828  \\\hline
\multicolumn{5}{c}{ \ }\\[-6pt]\hline
BTUC(16)& 31      & 131070 / 921355 & 98.270 & 486.252\\\hline
\end{tabular}
%
\end{center}
\caption{Results for the BTUC problems.}
\label{tab-btuc}
\end{table}

\subsubsection{Ring of Rooms}

\paragraph{Simple Ring of Room.}
We considered another domain, where a robot can move in a ring of
rooms. Each room has a window, which can be either open, closed or
locked. The robot can move (either clockwise or counterclockwise),
close the window of the room where it is, and lock it if closed. The
goal is to have all windows locked.
%
\begin{center}
  \epsfig{figure=fig/ring.eps,width=.35\textwidth}
\end{center}
%
In the problem RING($r$), where $r$ is the number of rooms, the
uncertainty is only in the initial condition: both the position of the
robot and the status of the windows can be uncertain.
%
These problems do not have a parallel solution, and have a large
number of initial states ($r * 3^r$), corresponding to full
uncertainty on the position of the robot and on the status of
each window.
%
\begin{table}[tbh]
\scriptsize
\begin{center}
\begin{tabular}{c@{\hspace{0.6cm}}c}
\begin{tabular}{|l||r|r|r||r|r||r|}\cline{2-7}
\multicolumn{1}{c|}{\ } & \multicolumn{3}{c||}{\cmbp}    &\multicolumn{2}{c||}{\cgp} & \multicolumn{1}{c|}{\gpt} \\\hline
        & \PL     & \#BS/\#BSH     &  \CTD   &  \LL     & \CTD   & \CTI   \\\hline
RING(2) & 5       & 8     / 24     & 0.000   &     3    & 0.070  &   0.085 \\\hline
RING(3) & 8       & 26    / 78     & 0.020   &     4    & \tlim  &   0.087 \\\hline
RING(4) & 11      & 80    / 240    & 0.040   &          &        &   0.392 \\\hline
RING(5) & 14      & 242   / 726    & 0.120   &          &        &   1.150 \\\hline
RING(6) & 17      & 728   / 2184   & 0.370   &          &        &   6.620 \\\hline
RING(7) & 20      & 2186  / 6558   & 1.420   &          &        &  23.636 \\\hline
RING(8) & 23      & 6560  / 19680  & 4.950   &          &        & 105.158 \\\hline
RING(9) & 26      & 19682 / 59046  & 27.330  &          &        & \mlim   \\\hline
RING(10)& 29      & 59048 / 177144 & 106.870 &          &        &         \\\hline
\end{tabular}
&
\begin{tabular}{|r|r|r|r|r|}\hline
\multicolumn{5}{|c|}{{\cgp} on RING(5)}         \\\hline
  IS    & \LL      & \CTI   & \LL & \CTI     \\\hline
   1    &  5       &   0.010&  9  &   0.020  \\\hline
   2    &  5       &   0.060&  9  &   0.140  \\\hline
   4    &  5       &   0.420&  9  &   1.950  \\\hline
   8    &  5       &   6.150&  9  & 359.680  \\\hline
  16    &  5       &  \tlim &  9  & \tlim    \\\hline
% 16    &  5       &8703.800&  9  &  ---     \\\hline
% 32    &  5       &        &  9  &          \\\hline
\end{tabular}
\end{tabular}
\end{center}

\caption{The results for the RING problems.}
\label{tab-ring}
\end{table}
%
The results\footnote{The times reported for {\cgp} refer to a
  scaled-down version of the problem, where locking is not taken into
  account, and thus the maximum number of initial states is $r*2^r$.}
are reported on the left in Table~\ref{tab-ring}.
%
\cmbp outperforms both \cgp and \gpt, although \gpt performs much
better than \cgp. Both \cgp and \gpt suffer from the increasing
complexity of the problem.
%
On the right in Table~\ref{tab-ring}, we plot (for the RING(5)
problem) the dependency of {\cgp} on the number of initial states
combined with the number of levels to be explored (different goals
were provided which require the exploration of different levels). It
is clear that the number of initial states and the depth of the search
are both critical factors for {\cgp}.

\paragraph{Ring of Rooms with Uncertain Action Effects.} 
%
We considered a variation of the RING domain, called URING, first
introduced by Cimatti and Roveri~\citeyear{cimatti33}, which is
not expressible in {\cgp}. If a window is not locked and the robot is
not performing an action which will determine its status (e.g.\ closing
it), then the window can open or close nondeterministically. For
instance, while the robot is moving from room 1 to room 2, the windows
in room 3 and 4 could be open or closed by the wind.
%
This domain is clearly designed to stress the ability of a planner to
deal with actions having a large number of resulting states. In the
worst case (e.g.\ a move action performed when no window is locked),
there are $2^r$ possible resulting states. Although seemingly
artificial, this captures the fact that environments can be in
practice highly nondeterministic. 
%
We tried to compare {\cmbp} and {\gpt} on the URING problem.
%
In principle {\gpt} is able to deal with uncertainty in the action
effects. However, we failed to codify the URING in the \gpt language,
because it requires a conditional description of uncertain effects.
%
Therefore, we experimented with a variation of the RING domain
featuring a higher degree of nondeterminism, called NDRING in the
following. The NDRING domain contains an increasing number of
additional propositions, called in the following {\em noninertial}
propositions, which are initially unknown and are
nondeterministically altered by each action. 
%
\newcommand{\CTA}[1]{\multicolumn{1}{c|}{Time #1}}
\newcommand{\CTE}[1]{\multicolumn{1}{c||}{Time #1}}
\begin{table}[tbh]
\scriptsize
\begin{center}
\begin{tabular}{|l||r|r|r||r|r|r|r|}\cline{2-8}
\multicolumn{1}{c|}{\ } & \multicolumn{3}{c||}{\cmbp} & \multicolumn{4}{c|}{\gpt} \\\hline
          & \PL     & \#BS/\#BSH     &\CTE{(5)}&\CTA{(2)}&\CTA{(3)}&\CTA{(4)}&\CTA{(5)}\\\hline
NDRING(2) & 5       & 8     / 24     & 0.000   &   0.140 &  0.384  &  0.948  &  4.544  \\\hline
NDRING(3) & 8       & 26    / 78     & 0.020   &   0.256 &  0.679  &  2.574  & 13.960  \\\hline
NDRING(4) & 11      & 80    / 240    & 0.040   &   1.046 &  3.025  & 12.548  & 67.714  \\\hline
NDRING(5) & 14      & 242   / 726    & 0.110   &   4.550 & 12.960  & 48.426  & \mlim   \\\hline
NDRING(6) & 17      & 728   / 2184   & 0.350   &  18.758 & 57.300  & \mlim   &         \\\hline
NDRING(7) & 20      & 2186  / 6558   & 1.350   & 108.854 & \mlim   &         &         \\\hline
NDRING(8) & 23      & 6560  / 19680  & 4.990   & \mlim   &         &         &         \\\hline
NDRING(9) & 26      & 19682 / 59046  & 27.060  &         &         &         &         \\\hline
NDRING(10)& 29      & 59048 / 177144 & 103.760 &         &         &         &         \\\hline
\end{tabular}
\end{center}

\caption{The results for the NDRING problems.}
\label{tab-ring-unc}
\end{table}
%
If $i$ is the number of noninertial propositions, each action has $2^i$
possible outcomes.
%
The results are listed in Table~\ref{tab-ring-unc}, with columns
labeled with Time{($i$)}.
%
The growing branching factor during the search has a major impact on
the performance of \gpt, while \cmbp is insensitive to this kind of
uncertainty. (The performance of \cmbp for a lower number of
noninertial propositions are not reported because they are basically
the same.)

\begin{table}[htb]
\scriptsize
\begin{center}
\begin{tabular}{|l||c|r|r|}\cline{2-4}
\multicolumn{1}{c|}{\ } & \multicolumn{3}{c|}{\cmbp}  \\\hline
           & $|$P$|$ & \#BS/\#BSH  & \CTI  \\\hline
URING(2)   & 5       & 5    / 16   & 0.000 \\\hline
URING(3)   & 8       & 11   / 34   & 0.010 \\\hline
URING(4)   & 11      & 23   / 70   & 0.020 \\\hline
URING(5)   & 14      & 47   / 142  & 0.040 \\\hline
URING(6)   & 17      & 95   / 286  & 0.080 \\\hline
URING(7)   & 20      & 191  / 574  & 0.190 \\\hline
URING(8)   & 23      & 383  / 1150 & 0.410 \\\hline
URING(9)   & 26      & 767  / 2302 & 0.980 \\\hline
URING(10)  & 29      & 1535 / 4606 & 2.2300\\\hline
\end{tabular}
\end{center}

\caption{Results for the URING problems.}
\label{tab-uring}
\end{table}
%
The URING problem was run only on \cmbp. The results are listed in 
Table~\ref{tab-uring}. 
%
It can be noticed that the performances of \cmbp improve significantly
with respect to the RING problem. This can be explained considering
that, despite the larger number of transitions, the number of explored
belief states is significantly smaller (see the Bs cache statistics in
Tables~\ref{tab-ring} and~\ref{tab-uring}).
% 

\subsubsection{Square and Cube}
%
The following domains are the SQUARE($n$) and CUBE($n$) from the
{\gpt} distribution~\cite{bonet1}. These problems consist of a robot
navigating in a square or cube of side $n$. In both domains there are
actions for moving the robot in all the possible directions. Moving
the robot against a boundary leaves the robot in the same position.
%
The original problems, called CORNER in the following, require the
robot to reach a corner, starting from a completely unspecified position.
%
We introduced two variations. In the first, called FACE, the initial
position is any position of a given side [face] of the square [cube],
while the goal is to reach the central position of the opposite side
[face].
%
In the second, called CENTER, the initial position is completely
unspecified, and the goal is the center of the square [cube].
%
For the corner problem, a simple heuristic is to perform only steps
towards the corner, thus pruning half of the actions. The variations
are designed not to allow for a simple heuristic --- for instance, in
the CENTER problem, no action can be eliminated.

\begin{table}[thb]
{\tiny
\begin{center}
\vspace*{5mm}
\begin{tabular}{@{\hspace{-0.2mm}}c}\renewcommand{\tabcolsep}{1.4mm}
\begin{tabular}{|c|c|r|r||r||c|r|r||r||c|r|r||r|}
\cline{2-13}
\multicolumn{1}{c|}{\ } & \multicolumn{4}{c||}{CORNER} &
\multicolumn{4}{c||}{FACE}  & \multicolumn{4}{c|}{CENTER} \\ \hline
SQUARE($i$) & \multicolumn{3}{c||}{\cmbp} & \multicolumn{1}{c||}{\gpt} &
              \multicolumn{3}{c||}{\cmbp} & \multicolumn{1}{c||}{\gpt} &
              \multicolumn{3}{c||}{\cmbp} & \multicolumn{1}{c|}{\gpt} \\ \cline{2-13}
           &\PL & \#BS/\#BSH  & \CTD  & \CTD  &\PL & \#BS/\#BSH  &\CTD   & \CTD  &\PL &\#BS/\#BSH   &\CTD   & \CTI   \\\hline
SQUARE(2)  & 2  &  2   / 4    & 0.000 & 0.074 & 2  & 2    / 4    & 0.000 & 0.058 & 2  & 2    / 4    & 0.000 &  0.060 \\\hline
SQUARE(4)  & 6  &  15  / 37   & 0.000 & 0.080 & 7  & 33   / 83   & 0.000 & 0.065 & 8  & 76   / 190  & 0.010 &  0.083 \\\hline
SQUARE(6)  & 10 &  35  / 93   & 0.000 & 0.092 & 12 & 86   / 232  & 0.020 & 0.089 & 14 & 218  / 592  & 0.040 &  0.216 \\\hline
SQUARE(8)  & 14 &  63  / 173  & 0.020 & 0.115 & 17 & 163  / 453  & 0.040 & 0.139 & 20 & 432  / 1210 & 0.090 &  0.695 \\\hline
SQUARE(10) & 18 &  99  / 277  & 0.030 & 0.149 & 22 & 264  / 746  & 0.090 & 0.228 & 26 & 718  / 2044 & 0.190 &  2.135 \\\hline
SQUARE(12) & 22 &  143 / 405  & 0.050 & 0.196 & 27 & 389  / 1111 & 0.150 & 0.371 & 32 & 1076 / 3094 & 0.360 &  5.340 \\\hline
SQUARE(14) & 26 &  195 / 557  & 0.070 & 0.261 & 32 & 538  / 1548 & 0.230 & 0.582 & 38 & 1506 / 4360 & 0.560 & 12.284 \\\hline
SQUARE(16) & 30 &  255 / 733  & 0.080 & 0.357 & 37 & 711  / 2057 & 0.320 & 0.908 & 44 & 2008 / 5842 & 0.820 & 26.241 \\\hline
SQUARE(18) & 34 &  323 / 933  & 0.120 & 0.503 & 42 & 908  / 2638 & 0.540 & 1.343 & 50 & 2582 / 7540 & 1.330 & 52.091 \\\hline
SQUARE(20) & 38 &  399 / 1157 & 0.160 & 0.638 & 47 & 1129 / 3291 & 0.650 & 1.883 & 56 & 3228 / 9454 & 1.790 & 94.204 \\\hline

\end{tabular}
%
\\
\vspace*{5mm} \\
\\\renewcommand{\tabcolsep}{1.4mm}
%
\begin{tabular}{|c|c|r|r||r||c|r|r||r||c|r|r||r|}
\cline{2-13}
\multicolumn{1}{c|}{\ } & \multicolumn{4}{c||}{CORNER} &
\multicolumn{4}{c||}{FACE}  & \multicolumn{4}{c|}{CENTER} \\ \hline
  CUBE($i$) & \multicolumn{3}{c||}{\cmbp} & \multicolumn{1}{c||}{\gpt} &
              \multicolumn{3}{c||}{\cmbp} & \multicolumn{1}{c||}{\gpt} &
              \multicolumn{3}{c||}{\cmbp} & \multicolumn{1}{c|}{\gpt} \\ \cline{2-13}
           &\PL & \#BS/\#BSH  & \CTD  & \CTD  &\PL & \#BS/\#BSH     &\CTD    & \CTD   &\PL &\#BS/\#BSH      & \CTD   & \CTI    \\\hline
  CUBE(2)  & 3  & 6    / 19   & 0.000 & 0.332 & 3  & 6     / 19     &  0.000 &  0.061 & 3  & 6     / 19     &  0.010 &   0.061 \\\hline
  CUBE(3)  & 6  & 26   / 99   & 0.010 & 0.168 & 6  & 26    / 99     &  0.000 &  0.069 & 6  & 26    / 99     &  0.010 &   0.144 \\\hline
  CUBE(4)  & 9  & 63   / 261  & 0.020 & 0.430 & 11 & 319   / 1360   &  0.050 &  0.193 & 12 & 722   / 3091   &  0.130 &   0.569 \\\hline
  CUBE(5)  & 12 & 124  / 537  & 0.040 & 0.276 & 14 & 709   / 3095   &  0.220 &  0.412 & 15 & 1696  / 7402   &  0.430 &   2.010 \\\hline
  CUBE(6)  & 15 & 215  / 957  & 0.050 & 0.500 & 19 & 1343  / 6116   &  0.430 &  1.479 & 21 & 3365  / 15432  &  0.910 &  10.717 \\\hline
  CUBE(7)  & 18 & 342  / 1551 & 0.100 & 0.567 & 22 & 2255  / 10377  &  0.840 &  3.323 & 24 & 5797  / 26814  &  1.860 &  34.074 \\\hline
  CUBE(8)  & 21 & 511  / 2349 & 0.160 & 1.082 & 27 & 3519  / 16464  &  1.400 &  8.161 & 30 & 9248  / 43541  &  3.520 & 109.852 \\\hline
  CUBE(9)  & 24 & 728  / 3381 & 0.330 & 1.765 & 30 & 5169  / 24331  &  2.810 & 16.272 & 33 & 13786 / 65237  &  7.260 & 701.910 \\\hline
  CUBE(10) & 27 & 999  / 4677 & 0.440 & 2.068 & 35 & 7279  / 34564  &  4.550 & 32.226 & 39 & 19667 / 93898  &  9.990 & \mlim  \\\hline
  \multicolumn{13}{c}{\ }\\[-4pt]\hline                                                    
  CUBE(15) & 42 & 3374 / 16167& 1.940 & 9.207 & 54 & 26439 / 127825 & 28.560 & \mlim  & 60 & 74041 / 359354 & 58.930 &        \\\hline

\end{tabular}
\\
\ \\
\\
\end{tabular}
\end{center}
}
\caption{Results for the SQUARE and CUBE problems.\label{tab-navigation}}
\end{table}
%
The results for these problems are reported in
Table~\ref{tab-navigation}. The tests were run only with \cmbp and \gpt.
%
The experiments highlight that the efficiency of \gpt strongly depends
on the quality of the heuristic function. If, as in the first set of
experiments, the heuristics are effective, then \gpt is almost as good
as \cmbp. Otherwise, \gpt degrades significantly. In general,
finding heuristics which are effective in the belief space appears to
be a nontrivial problem.
%
\cmbp appears to be more stable\footnote{Consider also that the
  problems are increasingly more difficult (see for instance the plan
  length).}, as it performs a blind, breadth-first search, and relies
on the cleverness of the symbolic representation to achieve
efficiency.

\subsubsection{Omelette}

Finally, we considered the OMELETTE($i$) problem \cite{levesque1996}.
The goal is to have $i$ good eggs and no bad ones in one of two bowls
of capacity $i$. There is an unlimited number of eggs, each of which
can be unpredictably good or bad. The eggs can be grabbed and broken
into a bowl. The content of a bowl can be discarded, or poured to the
other bowl. Breaking a rotten egg in a bowl has the effect of spoiling
the bowl. A bowl can always be cleaned by discarding its content. The
problem is originally presented as a partial observability problem,
with a sensing action allowing to test if a bowl is spoiled or not.
%
We considered the variation of the problem without sensing action: in
this case no conformant solution exists.  We used the OMELETTE
problems to test the ability of \cmbp and \gpt to discover that the
problem admits no conformant solution. The results are reported in
Table~\ref{tab:omelette}. The table shows that \cmbp is very effective
in checking the absence of a conformant solution, and outperforms \gpt
by several orders of magnitude.

\begin{table}[bht]
{\scriptsize
\begin{center}
  \begin{tabular}{|l|c|r|c||c|}\cline{2-5}
\multicolumn{1}{c|}{\ } & \multicolumn{3}{c||}{CMBP} & GPT \\\hline
                & \# steps & \#BS/\#BSH & \CTD    & \CTI\\\hline
   OMELETTE(3)  & 9        & 15  / 34       & 0.020  &   0.237    \\\hline 
   OMELETTE(4)  & 11       & 19  / 42       & 0.030  &   0.582    \\\hline 
   OMELETTE(5)  & 13       & 23  / 50       & 0.040  &   1.418    \\\hline 
   OMELETTE(6)  & 15       & 27  / 58       & 0.050  &   2.904    \\\hline 
   OMELETTE(7)  & 17       & 31  / 66       & 0.060  &   5.189    \\\hline 
   OMELETTE(8)  & 19       & 35  / 74       & 0.090  &  10.307    \\\hline 
   OMELETTE(9)  & 21       & 39  / 82       & 0.110  &  18.744    \\\hline 
   OMELETTE(10) & 23       & 43  / 90       & 0.120  &  32.623    \\\hline 
   \multicolumn{5}{c}{\ }\\[-6pt]\hline
   OMELETTE(15) & 33       & 63  / 130      & 0.210  & 225.530   \\\hline 
   \multicolumn{5}{c}{\ }\\[-6pt]\hline                                  
   OMELETTE(20) & 43       & 83  / 170      & 0.440  & \mlim     \\\hline 
   \multicolumn{5}{c}{\ }\\[-6pt]\hline                                  
   OMELETTE(30) & 63       & 123 / 250      & 0.890  &           \\\hline 
  \end{tabular}
\end{center}
}
\caption{Results for the OMELETTE problems.}
\label{tab:omelette}
\end{table}

\subsection{Summarizing Remarks}

Overall, {\cmbp} appears to implement the most effective approach to
conformant planning, both in terms of expressivity and performance.
%
{\cgp} is only able to deal with uncertainties in the initial states,
and cannot conclude that the problem does not admit a conformant
solution.
%
The main problem in {\cgp} seems to be its enumerative approach to
uncertainties, and the increased number of initial states severely
affects the performance (see Table~\ref{tab-bmtc-cgp} and
Table~\ref{tab-ring}).

{\qbfplan} is in principle able to deal with uncertain action effects,
but cannot conclude that the problem does not admit a conformant
solution. From the small number of experiments that we could perform,
the approach implemented by {\qbfplan} is limited by  the
{\satplan} style of search: the intermediate results obtained while
solving an encoding at depth $k$ are not reused while solving
encodings of increasing depth. Furthermore, the solver appears to be
specialized in finding a model, rather than in proving
unsatisfiability. However, the latter ability is needed in all
encodings but the final one.

{\gpt} is a very expressive system, which allows efficiently dealing
with a wide class of planning problems. As far as conformant planning
is concerned, it is as expressive as {\cmbp}. It allows dealing with
uncertain action effects, and can conclude that a problem does not
have a conformant solution. However, {\cmbp} appears to outperform
{\gpt} in several respects. First, the behaviour of {\gpt} appears to
be directly related to the number of possible outcomes in an action.
Furthermore, the efficiency of {\gpt} depends on the effectiveness of
the heuristic functions, which can be sometimes difficult to devise,
and cannot help when the problem does not admit a solution.

The main strength of {\cmbp} is its independence on the {\em number}
of uncertainties, which is achieved with the use of symbolic
techniques. Being fully symbolic, {\cmbp} does not exhibit the
enumerative behaviour of its competitors. Compared to the original approach
described by Cimatti and Roveri~\citeyear{cimatti33}, a substantial improvement of the
performance has been obtained by the new implementation of the pruning
step.
%
A disclaimer is in order. It is well known that \bdd based
computations are subject to a blow-up in memory requirements when
computing certain classes of boolean functions,
e.g.\ multipliers~\cite{bryant2}. It would be trivial to make up an example
where the performance of \cmbp degrades exponentially. However, in none
of the examples we considered, which included all the examples in the
distribution of {\cgp} and {\gpt}, this phenomenon occurred.

\section{Other Related Work}
\label{sec-relwork}

The term \emph{conformant planning} was first introduced
by Goldman~\citeyear{goldman1}, while presenting a formalism for constructing
conformant plans based on an extension of dynamic logic.
%
Recently, Ferraris and Giunchiglia~\citeyear{giunchigliaAAAI00} presented another conformant
planner based on SAT techniques. The system is not available for a
direct comparison with {\cmbp}.
%
The effectiveness of the approach is difficult to evaluate, as only a
limited testing is described~\cite{giunchigliaAAAI00}. The performance
is claimed to be comparable with {\cgp}. However, the results are
reported only for the enconding corresponding to the solution, and the
behaviour of {\qbfplan} reported in Table~\ref{tab-btc} suggests that
this kind of analysis might be limited.

Several works share the idea of planning based on automata theory.
%
The most closely related are the works in the lines of planning via
model checking~\cite{cimatti27}, upon which our work is based. This
approach allows, for instance, to automatically construct universal
plans which are guaranteed to achieve the goal in a finite number of
steps~\cite{cimatti28}, or which implement trial-and-error
strategies~\cite{cimatti29,danieletraversovardi}.
%
These results are obtained under the hypothesis of total
observability, while here run-time observation is not available. The
main difference is that a substantial extension is required to lift
symbolic techniques to search in the space of belief states.
%
De Giacomo and Vardi~\citeyear{degiacomo1} analyze several forms of
planning in the automata theoretic framework.
%
Goldman, Musliner and Pelican~\citeyear{goldman-aips2000} present a method where model
checking in timed automata is interleaved with the plan formation
activity, to make sure that the timing constraints are met.
%
Finally, Hoey and his colleagues~\citeyear{hoey99spudd} use algebraic decision diagrams to
tackle the problem of stochastic planning.


\section{Conclusions and Future Work} 
\label{sec-concl}

In this paper we presented a new approach to conformant planning,
based on the use of Symbolic Model Checking techniques.
%
The algorithm is very general, and applies to complex planning
domains, with uncertainty in the initial condition and in action
effects, which can be described as finite state automata. 
%
The algorithm is based on a breadth-first, backward search, and
returns conformant plans of minimal length, if a solution to the
planning problem exists. Otherwise, it terminates with
failure.
%
The algorithm is designed to take full advantage of the symbolic
representation based on \bdds. The implementation of the approach in
the {\cmbp} system has been highly optimized, in particular in
the crucial step of termination checking.
%
We performed an experimental comparison of our approach with the state
of the art conformant planners {\cgp}, {\qbfplan} and {\gpt}.
%
{\cmbp} is strictly more expressive than {\qbfplan} and {\cgp}. On all
the problems for which a comparison was possible, {\cmbp} outperformed
its competitors in terms of run times, sometimes by orders of
magnitude.
%
Thanks to the use of symbolic data structures, \cmbp is able to deal
efficiently with problems with large numbers of initial states and
action outcomes. On the other hand, the qualitative behavior of \cgp
and \gpt seems to depend heavily on the enumerative nature of their
algorithms.
%
Differently from \gpt, \cmbp is independent of the effectiveness of
the heuristic used to drive the search.

%
The research presented in this paper will be extended in the following
directions. First, we are investigating an alternative approach
to conformant planning, where the breadth-first style of the search is
given up. These techniques appear to be extremely promising ---
preliminary experiments have led to speed ups of up to two orders
of magnitude over the results presented in this paper for problems
which admit a solution.
%
Second, we will tackle the problem of conditional planning under
partial observability, under the hypothesis that a limited amount of
information can be acquired at run time. As conformant planning, this
problem can be seen as search in the belief space. However, it appears
to be significantly complicated by the need for dealing with
run-time observation and conditional plans. 
%
Finally, we are considering the extension of the domain construction
of the planner with more expressive input language, such as {\calc},
and invariant detection techniques.

\section*{Acknowledgements}

Fausto Giunchiglia provided continuous encouragement and feedback on
this work. We thank Piergiorgio Bertoli, Blai Bonet, Marco Daniele,
Hector Geffner, Enrico Giunchiglia, Jussi Rintanen, David Smith, Paolo
Traverso, Dan Weld for valuable discussions on conformant planning and
various comments on this paper.
%
David Smith provided the code of {\cgp}, a large number of examples,
and the time-out mechanism used in the experimental evaluation.
%
Jussi Rintanen made {\qbfplan} available under Linux.
%

\bibliography{ref,a-l,m-z}
\bibliographystyle{latex/theapa}

\end{document}

