Generating Exact Approximations to Model Check Concurrent Systems

In this paper, we present a method to generate abstractions for model checking concurrent systems. A program using a defined syntax and semantics, first describes the concurrent system that can be infinite. This program is abstracted using the framework of abstract interpretation where an abstract function will be given. This abstract program is demonstrated to be an accurate approximation of the original program that may contain spurious behaviours. These spurious behaviours will be identified and removed using a new defined abstraction framework based on the restrictions. The new produced abstract program is an exact approximation of the original program