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.
展开▼
