Soundness analytics of composed logical workflow nets

Cooperative systems with passing value indeterminacy and batch processing can be well modeled by composed logical workflow nets. Soundness guarantees no deadlock and livelock and each activity has potential to be executed. The soundness of composed logical workflow nets can be judged by reachability graphs. But reachability graphs can cause state space explosion. Path nets, single line nets, composed path nets and composed single line nets are proposed in the paper. They are used to determine soundness of logical workflow nets and composed logical workflow nets based on net structures and logical expressions avoiding reachability graphs. The presented concepts and techniques are applied to judge soundness of e-commerce transaction processes modeled by composed logical workflow nets, and they are illustrated by an example.