A modular verification methodology for D-NRI Petri nets

Summary form only given. Verification techniques concerning temporal properties are known to be based on the detection of infinite runs. However, their practical interests are limited due to a combinatorial explosion problem in space and time. Therefore, we introduce a new class of Petri net, named D-NRI, which can be decomposed through an interface of transitions. Conditions are specified in such a way that the checking is realized on the components separately. With this divide and conquer technique, we address the problem of model checking of action based temporal properties as for client-server protocols.