Computational Logic for the verIfication and Modeling of Business constraints

Many emerging settings, such as Business Process Management systems, Clinical Guidelines, Services Composition/Choreographies and Multi-Agent Systems, are characterized by a distribution of activities and resources and by exhibiting complex dynamics. This is due to their intrinsic openness, to the autonomy of their stakeholders, and to the unpredictability of the environment in which they are situated. To understand such dynamics and to develop methods and tools apt to accommodate modeling and reasoning about them is a very challenging goal.

All these systems center around the interaction of the involved parties. Interaction, in turn, must be disciplined so as to ensure that the interacting entities comply with external regulations, norms, business rules and internal policies. Such forces have the effect of constraining the courses of interaction, and can be thus grouped under the umbrella term of business constraint.

Business constraints constitute a form of declarative knowledge: they restrict the set of compliant courses of interaction, without explicitly stating how the interacting entities must behave. Unfortunately, traditional modeling approaches have a closed and procedural nature, and thus require to write down explicitly all the compliant behaviors, producing “spaghetti-like” models which tend to sacrifice flexibility and readability.

In this respect, a shift towards open and declarative modeling abstractions is needed. However, the adoption of declarative open interaction models poses two challenging questions:

  • how can we specify them, and what is their semantics?
  • How is it possible to support their design, execution, verification and analysis?

CLIMB is a Computational Logic-based framework that provides an answer to both questions: it addresses the specification, verification, execution, monitoring and analysis of interaction models.