Dagstuhl Seminar 01451:

Exploration of Large State Spaces

November 4 - November 9, 2001.
Schloss Dagstuhl, Germany

[ Organizers ] [ Description ] [ Keynote Speakers ] [ Participants ]
[ Program ]



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.


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.

Keynote Speakers:


The list of participants can be found here.


[ Monday, Nov. 5, 2001 ]
[ Tuesday, Nov. 6, 2001 ]
[ Wednesday, Nov. 7, 2001 ]
[ Thursday, Nov. 8, 2001 ]
[ Friday, Nov. 9, 2001 ]

Last modified: October 30, 2001
Moshe Y. Vardi (vardi@cs.rice.edu)