Model Checking Unbounded Artifact-Centric Systems

ABSTRACT. Artifact-centric systems are a recent paradigm used to represent and implement business processes. We present further results on the verification problem of artifact-centric systems specified by means of FO-CTL specifications. While the general problem is known to be undecidable, results in the literature prove decidability for artifact systems with infinite domains under boundedness and conditions such as uniformity. We here follow a different approach and investigate the general case under the infinite domains assumption. We show the decidability for the class of artifact-centric systems whose database schemas consist of a single unary relation, and we show that that the problem is undecidable if artifact systems are defined by using one binary relation or two unary relations.