Towards Using Structural Abstraction for Model Checking

Abstract

Model checking is a method for formally verifying whether defined properties hold for a behavioral model of a system. With increasing complexity of these models, combinatorial explosion may arise. This problem can be addressed by a well-known approach to behavioral abstraction, employed, e.g., in CEGAR. These abstractions need to be over-approximations in the sense of enriching the behavior of the system, to ensure that correctness at the abstract level implies correctness of the original system. However, structural models, which the behaviors operate on, have not yet been considered when applying abstraction operations for model checking.We propose to use structural models as an essential part for model checking with abstraction operations. In this paper, we present an approach to systematically abstracting structural models, from which behavioral abstractions result, so that the ideas of CEGAR can be adapted for structural abstraction. We model structure using bigraphs, and propose abstraction operations on them.