The foundation of a process model lies in its structural specifications. Us
ing a generic process modeling language for workflows, we show how a struct
ural specification may contain deadlock and lack of synchronization conflic
ts that could compromise the correct execution of workflows. In general, id
entification of such conflicts is a computationally complex problem and req
uires development of effective algorithms specific for the target modeling
language. We present a visual verification approach and algorithm that empl
oys a set of graph reduction rules to identify structural conflicts in proc
ess models for the given workflow modeling language. We also provide insigh
ts into the correctness and complexity of the reduction process. Finally, w
e show how the reduction algorithm may be used to count possible instance s
ubgraphs of a correct process model. The main contribution of the paper is
a new technique for satisfying well-defined correctness criteria in process
models. (C) 2000 Published by Elsevier Science Ltd. All rights reserved.