A workflow net is a sort of directed graphs that simultaneously represent a set of ordinary graphs by means of inserting logical nodes. Such net adequately simulates any business processes configurations. This article deals with a standard workflow model that composes of functional and logical nodes and satisfies several limitations with respect to net organization.
Gist of verifying workflow net soundness is to ascertain a fact of the whole or partial reachability or inaccessibility of activities, which are functional nodes. This issue is of immediate interest for all realms of process-aware information systems engineering. Our technique uses propositional logic and some aspects of graph theory to analyze reachability of every join and split connectors along with activities nodes. We unveil some structural configurations of a net that effect appearance or failure of activity nodes at all net instances. As a consequence a reachability issue result in a task of graph traversal and calculation of vertexes statuses. A status testifies whether a vertex can be reach or not at the whole or separate net instances. To status estimate we use Boolean functions, which meet logical operations that assign to logical nodes, with domains that are calculated on the basis of net structural parameters values. Finally, we resort to the original threading of a workflow net to improve the
traversal and reachability algorithm efficiency. Keywords: business process, workflow, verification, soundness, reachability analysis