Soundness for S- and A-Timed Workflow Nets Is Undecidable

The main purpose of workflow management systems is to support the definition, execution, and control of workflow processes. With or without time constraints, workflow management systems should satisfy certain correctness properties. The most important and widely used is the soundness property. In this paper, we focus on the soundness property for two classes of Petri-net-based workflow management systems with time constraints, S- and A-timed workflow nets (WNs), and we show that this property is undecidable for them. The proof technique, based on the undecidability of the halting problem for deterministic counter machines, shows first that the reachability, coverability, boundedness, and quasi-liveness problems are undecidable for these two classes of timed WNs, and then, as a consequence, the undecidability of the soundness problem is derived.