Business process compliance verification: an annotation based approach with commitments

In this paper we present a framework to support business process compliance verification. A process model, provided in a Business Process Modeling tool, is annotated with information relevant for compliance verification. In particular, if a condition is mentioned in a regulation, an activity that makes that condition true, or that requires it as a precondition, should be annotated accordingly. In our approach, annotations are defined by specifying the effects of atomic tasks, including the obligations they generate, using Artificial Intelligence techniques for reasoning about actions and the notion of commitment developed in the context of a social approach to agent communication. Verifying the compliance of a business process to a regulation includes checking that, in all executions of the business process, all the obligations triggered by the norms are fulfilled. Such a verification is performed using model checking techniques for Temporal Logics. Two approaches are explored, one based on Colored Petri Nets, and one based on Answer Set Programming.