Speaker: Olivia Oanea (AIS, TU/e)

Title: Verifying Generalized Soundness for Workflow Nets

 Abstract: We improve the decision procedure for the problem of
 generalized soundness for workflow nets:
 "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".
 Moreover, our new decision procedure returns a counterexample
 in case the workflow net is not generalized sound.
 We also 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.

(Joint work with Kees van Hee, Natalia Sidorova and Marc Voorhoeve)