Abstract
Artifacts are entities characterized by data of interest (constituting the state of the artifact) in a given business application, and a lifecycle, which constrains the artifact's possible evolutions. In this paper we study relational artifacts, where data are represented by a full fledged relational database, and the lifecycle is described by a tempo-ral/dynamic formula expressed in µ-calculus. We then consider business processes, modeled as a set of condition/action rules, in which the execution of actions (aka tasks, or atomic services) results in new artifact states. We study conformance of such processes wrt the artifact lifecy-cle as well as verification of temporal/dynamic properties expressed in µ-calculus. Notice that such systems are infinite-state in general, hence undecidable. However, inspired by recent literature on database dependencies developed for data exchange, we present a natural restriction that makes such systems finite-state, and the above problems decidable.