Verification by network decomposition

Abstract

We describe a new method to verify networks of homogeneous processes which communicate by token passing. Given an arbitrary network graph and an indexed LTL\X property, we show how to decompose the network graph into multiple constant size networks, thereby reducing one model checking call on a large network to several calls on small networks. We thus obtain cut-offs for arbitrary classes of networks, adding to previous work by Emerson and Namjoshi on the ring topology. Our results on LTL\X are complemented by a negative result which precludes the existence of reductions for CTL\X on general networks. © Springer-Verlag 2004.