Abstract
<jats:title>Abstract</jats:title> <jats:p>Workflow nets are a variant of Petri nets used for modelling business processes. Central decision problems are soundness problems, one popular variant called generalised soundness. These problems intuitively ask whether initiated processes can be finalised. We introduce weighted soundness, which strengthens the classical concepts of soundness. In weighted soundness, we bound the weight (typically length) of runs to finalise processes. This allows one to require processes to be finalised within a restricted budget.</jats:p> <jats:p> We provide multiple reasons supporting the relevance of weighted soundness. Our theoretical analysis shows that weighted soundness is provably simpler than classical soundness. Our main result is that weighted generalised soundness is co- <jats:sc>NP</jats:sc> <jats:inline-formula> <jats:alternatives> <jats:tex-math>$$^{\textsc {NP}}$$</jats:tex-math> <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mrow/> <mml:mi>NP</mml:mi> </mml:msup> </mml:math> </jats:alternatives> </jats:inline-formula> -complete, while (unweighted) generalised soundness is known to be PSPACE-complete. Our practical analysis shows that on standard benchmarks classical soundness coincides with weighted soundness, if the weight is set to the number of transitions in the workflow net. Furthermore we analyse the Inductive Miner algorithm, one of the most popular algorithms generating workflow nets from event logs. Inductive Miner is known to guarantee the output workflow nets to be generalised sound. We show that it outputs workflow nets that are weighted generalised sound with a weight linear in the size of the event alphabet. Finally, we generalise reduction techniques from soundness to weighted soundness. Such reductions are crucial in implementations of soundness algorithms. </jats:p>