An analytical method for well-formed workflow/Petri net verification of classical soundness - Clempner, Julio (Zielona Góra: Uniwersytet Zielonogórski)
In this paper we consider workflow nets as dynamical systems governed by ordinary difference equations described by a particular class of Petri nets. Workflow nets are a formal model of business processes. Well-formed business processes correspond to sound workflow nets. Even if it seems necessary to require the soundness of workflow nets, there exist business processes with conditional behavior that will not necessarily satisfy the soundness property. In this sense, we propose an analytical method for showing that a workflow net satisfies the classical soundness property using a Petri net. To present our statement, we use Lyapunov stability theory to tackle the classical soundness verification problem for a class of dynamical systems described by Petri nets.
Keywords: Petri nets; decidability; workflow nets; Lyapunov stability; soundness; verification