Reduction and Abstraction Techniques for BIP

Reduction and abstraction techniques have been proposed to address the state space explosion problem in verification. In this paper, we present reduction and abstraction techniques for component-based systems modeled in BIP (Behavior, Interaction and Priority). Given a BIP system consisting of several atomic components, we compute the product of two selected atomic components. The product operation often exposes opportunities for constant propagation in the product component that were hidden originally. Moreover, the product operation introduces states that are branching bisimilar. Our method detects and merges those states resulting in a behavior that may overapproximate the original one. The presented method is fully implemented. Our results show a drastic improvement in verifying BIP systems.