Conference paper

Exploiting Symmetry for Efficient Verification of Infinite-State Component-Based Systems

In this paper we present an efficient verification algorithm for infinite-state component-based systems modeled in the behavior-interaction- priority (BIP) framework. Our algorithm extends the persistent set partial order reduction by taking into account system symmetries, and further combines it with lazy predicate abstraction. We have implemented the new verification algorithm in our model checker for BIP. The experimental evaluation shows that for systems exhibiting certain symmetries, our new algorithm outperforms the existing algorithms significantly.


Related material