Parameterized Model Checking
                            E. Allen Emerson
                       University of Texas at Austin

Electronic mail: emerson@cs.utexas.edu


Abstract:
Traditional model checking deals with systems of a fixed, finite size,
e.g. systems composed of 3 or 10 finite state processes running in parallel.
In the Parameterized Model Checking Problem (PMCP) we consider infinite
uniform families of systems each comprised of n homogeneous processes
running in parallel. The problem is to determine whether such a system
is correct for every size n. This provides a solution to the state
explosion and scaling problems in one fell swoop. Unfortunately,
PMCP is in general algorithmically unsolvable.

Because of it importance for applications, PMCP has nonetheless
garnered a great deal of attention yielding various partial or
restricted solutions. We overview some of those and then describe some
of our recent work with Vineet Kahlon, identifying useful frameworks
permitting the reduction of PMCP to model checking over systems composed
of c homogeneous processes, for small constant c. It follows then
that in this framework PMCP is decidable, in some cases efficiently.