Dagstuhl Seminar 01451:
Exploration of Large State Spaces
November 4 - November 9, 2001.
Schloss Dagstuhl, Germany
The goal of this workshop is to bring together researchers working
on state-exploration methods in artifical intelligence (AI) and in
automated verification (AV). The idea of organizing such a
workshop came during the DIMACS/IRCS Tutorial and Workshop on Logic and
Cognitive Science, which was held in April 1999 at the University of
Philadelphia. We realized there that state-exploration is a major
issue in computer-aided verification and in artificial intelligence.
Automated Verification
Automated verification provides a new approach to validating the
correct behavior of software and hardware designs. In traditional
design validation, ``confidence'' in the design is the result of
running a large number of test cases through the design.
Automated verification, in contrast, uses mathematical techniques
to check the entire state space of the design for conformance to some
specified behavior. Thus, while simulation is open-ended and fraught
with uncertainty, formal verification is definitive and eliminates
uncertainty. Over the last few years, automated verification tools,
such as model checkers, have shown their ability to provide thorough
analysis of reasonably complex designs. Companies such as AT\&T,
Cadence, Fujitsu, HP, IBM, Intel, Motorola, NEC, SGI, Siemens, and Sun
are using model checkers increasingly on their own designs to ensure
outstanding product quality. Unfortunately, model checking suffers
from a fundamental problem known as state-explosion: the
ability to handle only systems with limited-size state spaces. This
explosion arises mainly because the transition system analyzed describes
the global behavior of the system. In a system comprised of multiple
components, the global state space is a cross product of the individual
component state spaces. Even a system containing only small components
can therefore yield a large global state-space. For a modern
hardware and software, the global state space is prohibitively large.
This poses a serious challenge to extant model checkers. Combating
state-explosion is therefore a complex computational problem of
critical importance.
Markov Decision Processes
Work on Markov decision processes (MDPs) dates back to the
1950's and there is a large literature stemming primarily from
the fields of operations research and adaptive control.
In the 1980's there was renewed interest in MDPs coming from
work in automated planning in artificial intelligence and the
work on binary decision diagrams from the verification
community. Dean and Kanazawa [1989] and Tatman and Shachter
[1990] introduced the idea of structured Markov processes and
suggested how they might be used for representing and solving
planning and control problems with very large state and action
spaces. In subsequent years, a great deal of progress was made
exploring structured versions of earlier, unstructured
algorithms from the operations research and adaptive control
communities.
True MDPs, i.e., problems in which the current state of the
system is completely observable to the decision maker, are rare
in practice and hence the partially observable variant (POMDP)
is of great importance. Recently there has been a
resurgence of interest in POMDPs, partially spurred by the
success of Cassandra, Kaelbling and Littman, and a host of new
algorithms have been developed, including variational methods
which open up the possibility of solving a wide range of
problems. Variational statistical methods can in some cases
reduce the need for state exploration using a combination of
sampling techniques and reformulation in terms of a (continuous)
parameterized space of actions.
More recently researchers have begun using the basic technology
for model checking including binary decision diagrams (BDDs),
various algebraic extensions, and quantified variants that make
use of modal logics of time to tackle a wider class of MDPs and
their partially observable counterparts. In all cases, the
need for exploring very large state and action spaces is dealt
with by identifying and then exploiting structure in the
combinatorial space of states and actions.
AI Planning
Planning is a sub-field of AI which is concerned with the generation of
a rational course of action given a declarative specification of the
environment, the goals, and the possible actions. In the case of
``classical planning,'' one usually makes the simplifying assumptions
that everything (that is relevant) is observable, that all actions are
deterministic, and that the only change in the world is caused by
actions of the agent. While this seems like a trivialization of the
MDP problem, the problem is still computationally very hard because
of the large state space one has to explore. The last five years
brought considerable progress on the algorithmic side. In particular,
the planning-graph approach by Blum and Furst [1995], which
outperformed any existing planning system then, led to a flurry of
further developments, such as planners that reduce the planning
problem to a sequence of propositional satisfiability problems
[Kautz and Selman 1996] or nonmonotonic reasoning problems
[Dimopoulos at al 1997]. Type inference algorithms, the derivations
of invariants and other techniques were used to prune the search space
and to speed up planning, and OBDDs were used to code sets of states
in a compact way. All these developments led to an impressive
performance of AI planning systems as demonstrated at the first
international planning competition in 1997 (at AIPS'97). Just to give
an example, Kautz and Selman's BLACKBOX planner produced a 100-action
plan in a world with approx.{} $10^{16}$ states in a few minutes.
This has to be compared with the state of the art in the beginning of
the nineties, when a 10-action plan needed a few hours to be generated.
Currently, the main focus of research is in extending the existing
techniques to handle more expressive planning formalism (e.g.,
including resources), in improving the core search algorithms, and in
exploiting all types of knowledge that can be derived from the problem
specification in order to prune the search space.
Benefits
We expect that the workshop will help to increase the awareness of the
researchers working in one field of the problems and methods in the
others and thus to increase the interaction and collaboration of the
two fields, and the transfer of methodologies from one field to
another.
The list of participants can be found
here.
Last modified: October 30, 2001
Moshe Y. Vardi
(vardi@cs.rice.edu)