Towards Efficient Verification of Systems with Dynamic Process Creation

International audienceModelling and analysis of dynamic multi-threaded state systems often encounters obstacles when one wants to use automated verification methods, such as model checking. Our aim in this paper is to develop a technical device for coping with one such obstacle, namely that caused by dynamic process creation. We first introduce a general class of coloured Petri nets-not tied to any particular syntax or approach-allowing one to capture systems with dynamic (and concurrent) process creation as well as capable of manipulating data. Following this, we introduce the central notion of our method which is a marking equivalence that can be efficiently computed and then used, for instance, to aggregate markings in a reachability graph. In some situations, such an aggregation may produce a finite representation of an infinite state system which still allows one to establish the relevant be-havioural properties. We show feasibility of the method on an example and provide initial experimental results