Foundations of Relational Artifacts Verification

Proc. of the 9th Int. Conference on Business Process Management (BPM 2011). Volume 6896 of Lecture Notes in Computer Science. 2011.

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 temporal/dynamic formula expressed in mu-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 lifecycle as well as verification of temporal/dynamic properties expressed in mu-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.

@inproceedings{BPM-2011,
   title = "Foundations of Relational Artifacts Verification",
   year = "2011",
   author = "Bagheri Hariri, Babak and Diego Calvanese and De Giacomo,
Giuseppe and De Masellis, Riccardo and Paolo Felli",
   booktitle = "Proc. of the 9th Int. Conference on Business Process
Management (BPM 2011)",
   pages = "379--395",
   volume = "6896",
   publisher = "Springer",
   series = "Lecture Notes in Computer Science",
   doi = "10.1007/978-3-642-23059-2_28",
}