Modelling 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 behavioural properties. We show feasibility of
the method on an example and provide initial experimental results.
Keywords Petri nets - multi-threaded systems - marking symmetries - state-space generation