Abstract:
To represent a model that includes both data and resource perspectives, Data Petri nets could be used. In this formalism, each transition has a constraint that includes input and output conditions on variables. To stay within decidability, the conditions should not contain arithmetic operations, so the resources are usually represented as separate places. Existing correctness criteria such as easy, relaxed and lazy soundness could be adapted to resource-oriented Data Petri nets but deciding them requires solving a reachability problem that is known to have very high complexity even for classical Petri nets. In this paper, we propose a new correctness notion called relaxed lazy soundness that incorporates the main features of the aforementioned properties and that could be decided as a coverability problem, which is known to be less computationally complex than the reachability one. We provide an algorithm to verify this property, prove its correctness, and implement it in the existing soundness verification toolkit. The performance evaluation results confirm the applicability of the algorithm to process models of a moderate size. The algorithm could be used both for verification of resource-oriented models and for preliminary validation of arbitrary process models represented as Data Petri nets.
Keywords:data Petri net, verification of distributed processes with data, soundness verification, transition systems
Fulltext:
PDF file (1443 kB)