Artifact systems are a novel paradigm for specifying and implementing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and life-cycle models, which respectively account for the relational structure of the artifact state and its possible evolutions over time.

We consider the problem of verifying artifact systems against specifications expressed in a first-order extension of branching-time temporal logic. This problem is undecidable in general, as, put simply, each state is a database instance with elements coming from an infinite domain, and there is no regularity one can exploit to decide whether the system satisfies an arbitrary property. The work focuses on a decidable (bounded) variant of the problem, where the states of the system can only accommodate a bounded number of distinct elements. Even under this assumption the system contains an infinite number of states. However, a data abstraction technique can be used to reduce the problem to standard model checking. Interestingly, in some cases solving the bounded version of a generic instance is informative with respect to the original instance, too.

In this talk, I will introduce the problem, give an overview of the abstraction technique, describe the relationship between the bounded and the general formulations, and discuss ongoing and possible future research directions.