Making Workflow Models Sound Using Petri Net Controller Synthesis

More and more companies use ”process aware” information systems to make their business processes more efficient. To do this, workflow definitions must be formulated in a formal specification language, as they represent executable derivates of business process descriptions. Both for the less formal descriptions of business processes as well as the workflow definitions, Petri-net based approaches are used successfully. In the literature the business process descriptions are required to be well-structured, leading to a sound workflow definition. We argue that in many cases well-structuredness is too restrictive for practitioners. Relaxed soundness has been introduced previously as a more suitable requirement. The paper presents how methods from controller synthesis for Petri nets can be used to automatically make this type of models sound. For this reason we adopt the idea of controllability for Petri net workflow models.