Verifying Generalized Soundness of Workflow Nets

We improve the decision procedure from [10] for the problem of generalized soundness of workflow nets. A workflow net is generalized sound iff every marking reachable from an initial marking with k tokens on the initial place terminates properly, i.e. it can reach a marking with k tokens on the final place, for an arbitrary natural number k. Our new decision procedure not only reports whether the net is sound or not, but also returns a counterexample in case the workflow net is not generalized sound. We report on experimental results obtained with the prototype we made and explain how the procedure can be used for the compositional verification of large workflows.

• Type: Conference
• Year: 2006
• Where: ERSHOV
• Authors: Kees M. van Hee, Olivia Oanea, Natalia Sidorova, Marc Voorhoeve
• Keywords: Decision Procedure, ERSHOV 2006, Initial Place Terminates, Theoretical Computer Science, Workflow Net