Safe Distribution of Declarative Processes

Abstract. We give a general technique for safe distribution of a declarative (global) process as a network of (local) synchronously communicating declarative pro-cesses. Both the global and local processes are given as Dynamic Condition Re-sponse (DCR) Graphs. DCR Graphs is a recently introduced declarative process model generalizing labelled prime event structures to a systems model able to finitely represent ω-regular languages. An operational semantics given as a tran-sition semantics between markings of the graph allows DCR Graphs to be conve-niently used as both specification and execution model. The technique for distri-bution is based on a new general notion of projection of DCR Graphs relative to a subset of labels and events identifying the set of external events that must be com-municated from the other processes in the network in order for the distribution to be safe. We prove that for any vector of projections that covers a DCR Graph that the network of synchronously communicating DCR Graphs given by the projec-tions is bisimilar to the original global process graph. We exemplify the distribu-tion technique on a process identified in a case study of an cross-organizational case management system carried out jointly with Exformatics A/S.