Date Added: Jun 2010
The authors present an effective algorithm for the automatic construction of finite modal transition systems as abstractions of potentially infinite concurrent processes. Modal transition systems are recognised as valuable abstractions for model checking because they allow for the validation as well as refutation of safety and liveness properties. However, the algorithmic construction of finite abstractions from potentially infinite concurrent processes is a missing link that prevents their more widespread usage for model checking of concurrent systems. Their algorithm is a work-list algorithm using concepts from abstract interpretation and operating upon mappings from sets to intervals in order to express simultaneous over- and under-approximations of the multi-sets of process actions available in a particular state.