MODEL CHECKING WITH LAYERED LOCALIZATION REDUCTION

A method for verifying a property of a complete model of a system under study includes abstracting at least some of the variables from the model so as to produce an abstract model of the system. Beginning with an initial state in a state space of the abstract model, an abstract path is found through the state space of the abstract model in accordance with the transition relation to a target state defined by the property. A subset of the abstracted variables is restored to the abstract model so as to produce an intermediate model of the system, and the property on the complete model is verified based on the intermediate model.