Exploration of Large State Spaces

The goal of this seminar is to bring together researchers working on state-exploration methods in artificial intelligence (AI) and in automated verification (AV).

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. Over the last few years, automated

verification tools, such as model checkers, have shown their ability to provide thorough analysis of reasonably complex designs. 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 artificial intelligence , the state-explosion problem arises also in the sub-fields of Markov decision processes and action planning. In both areas, it is necessary to explore large state-spaces and a number of techniques have been used to deal with problem of exploring these state spaces, e.g., using heuristic search with heuristics derived from the problem description, by using propositional satisfiability techniques, by making use of binary decision programs or generalizations of them etc.

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.