soundness check PM4Py

[s-j-v-zelst]

I do not understand the soundness check in PM4Py. WF net is a graph theoretical property, so that check is easy and seems fine. However, soundness is a behavioral property (which can to some extent be extended to arbitrary Petri nets).

When I browse the code that check whether a given WF-net is sound, I do not observe where the marking is used (i.e. putting 1 token in the initial place). There are ways to check whether a WF net is sound on the basis of its structure, however, one needs to first compute whether the WF net is well-structured, which, as far as I can see is not performed in the code.

Please explain the code and provide a link to the publication of the underlying algorithm

[fit-alessandro-berti]

The article is the following:

https://www.degruyter.com/downloadpdf/j/amcs.2014.24.issue-4/amcs-2014-0068/amcs-2014-0068.pdf

Look at page 5 second column

[fit-alessandro-berti]

The soundness checker has been perfectioned. Now, aside from checking on the Lyapunov stability of the eigenvalues, that is a needed but not enough solution, the following checks are done:

• (albeit not strictly needed) Check on the relaxed soundness of the Petri net, through the "check_relaxed_soundness_net_in_fin_marking" method (basically, a path is searched from the initial marking to the final marking using the explore_path.__search method (adapted from alignments)

• Check on loops generating tokens, through the "check_loops_generating_tokens" function (heuristics are used to visit the state space and evaluate the loops)

• Check on the non-blocking condition, through the "check_non_blocking" function (heuristics are used to visit the state space)

The functioning of the methods has been tested on the models extracted by Alpha Miner, the Inductive Miner on the 10 logs contained in the "input_data" folder. The behavior is the one expected:

• The Petri nets converted from Heuristics Nets pass the workflow net, the relaxed soundness and the stability test, but fail the non-blocking test.
• The Petri nets extracted by Inductive Miner pass the soundness test.
• The Petri nets extracted by Alpha Miner generally do not pass the test, except for "01_running-example" and "04_reviewing".
• Always with the Alpha Miner, the "05_bpic2017" and the "03-repairExample" almost pass the test, but fail on the loop condition.

Worryngly, the 03-repairExample Alpha model fails only the loop conditions, albeit having several edges from transitions to the sink place. I think I may also need to revise the check on workflow nets, to check if transitions connected to the source place have a single input arc, and transitions connected to the sink place have a single output arc.

UPDATE: fix for workflow checking is also up now.