Abstract
The paper presents a logic-based framework for the analysis of workflow models, where a rich graphical representation of workflow schemes is combined with simple, i.e., stratified, yet powerful DATLOG rules to express properties and constraints on executions. The graphical representation and the DATALOC rules are mapped into a unique program in DATALOG!ev, which is an extension of DATALOC for handling events. The high expressive power of the language provides the designer with effective mechanisms for reasoning on workflows: (i) modeling a workflow schema with the possibility of expressing many types of constraints on the executions; (ii) defining various execution scenarios, i.e., sequences of workflow executions for the same schema; and (iii) simulating the actual behavior of the modeled scheme by fixing an initial state and an execution scenario and by querying the state after such executions. As a scenario may include a certain amount of non-determinism, the designer can also verify under which conditions a given (desirable or undesirable) goal can be eventually achieved.