Automatic Abstraction for Promela Behavioral Model

This paper proposes an automatic abstraction algorithm for constructing a trace equivalent abstract model from the detailed Promela model. The abstract model has a minimum of state variables and the smallest state space. It can be used in place of the detailed model when building environmental model or checking global property to improve the efficiency of model checking .