Synthesis and reduction of state machine workflow nets
Isaac Corro Ramos, A. Di Bucchianico, Lusine Hakobyan, Kees M. van Hee · 2006
We present two rules for generating State Machine Workflow (SMWf) nets. We prove the soundness of these rules, i.e., we show that applying these rules to an SMWf net results in an SMWf net. We also prove completeness, i.e., we show that any SMWf net can be obtained by applying our rules to the initial SMWf net containing one transition only. We present two proofs for completeness, one based on synthesis and one based on reduction.