A deductive system for proving workflow models from operational procedures

Many modern business environments employ software to automate the delivery of workflows; whereas, workflow design and generation remains a laborious technical task for domain specialists. Several different approaches have been proposed for deriving workflow models. Some approaches rely on process data mining approaches, whereas others have proposed derivations of workflow models from operational structures, domain specific knowledge or workflow model compositions from knowledge-bases. Many approaches draw on principles from automatic planning, but conceptual in context and lack mathematical justification. In this paper we present a mathematical framework for deducing tasks in workflow models from plans in mechanistic or strongly controlled work environments, with a focus around automatic plan generations. In addition, we prove an associative composition operator that permits crisp hierarchical task compositions for workflow models through a set of mathematical deduction rules. The result is a logical framework that can be used to prove tasks in workflow hierarchies from operational information about work processes and machine configurations in controlled or mechanistic work environments.

► A k-dimensional Petri net (called a k-PN) presented in Section  2.2 and Definition 4.
► Functions to map actions involving pre and post conditions to k-PN in Section  4.1.
► In Section 4.2, a functional form of k-PN called a k-PN   template was presented.
► Associative serial combination operator (⊕⊕) for k-PN templates followed by proofs.
► Efficient hierarchical composition and query methods for action k-PN templates.