CONCUR 2004 START ConferenceManager    

Verification by Network Decomposition

Edmund Clarke, Muralidhar Talupur, Tayssir Touili, Helmut Veith

Presented at Fifteenth International Conference on Concurrency Theory (CONCUR 2004), London, England, 31 August - 3 September, 2004


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 cut-offs for CTL-X on general networks.

START Conference Manager (V2.47.4)