A BRICS Mini-Course
October 6, 8 and 10, 1997
Lectures by
Antti Valmari
Software Systems Laboratory, Department of Information Technology, Tampere University of Technology, Finland
State space methods are one of the most important approaches to computer-aided analysis and verification of the behaviour of concurrent systems. In their basic form, they consist of enumerating and analysing the set of the states the system can ever reach. Unfortunately, the number of states of even a relatively small system is often far greater than can be handled in a realistic computer. The goal of this mini-course is to analyse this ``state explosion problem'' from several directions. Many advanced state space methods alleviate the problem by using a subset or an abstraction of the set of states. Unfortunately, their use tends to restrict the set of analysis or verification questions that can be answered, making it impossible to discuss the methods without some taxonomy of the questions. Therefore, the course contains a lengthy discussion on alternative ways of stating analysis and verification questions, and algorithms for answering them. After that, many advanced state space methods are briefly described. The state explosion problem is also investigated from the computational complexity point of view.