Safe Distribution of Declarative Processes

Thomas Hildebrandt, Raghava Rao Mukkamala, Tijs Slaats

Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review


We give a general technique for safe distribution of a declarative (global) process as a network of (local) synchronously communicating declarative processes. Both the global and local processes are given as Dynamic Condition Response (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 transition semantics between markings of the graph allows DCR Graphs to be conveniently used as both specification and execution model. The technique for distribution 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 communicated 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 projections is bisimilar to the original global process graph. We exemplify the distribution technique on a process identified in a case study of an cross-organizational case management system carried out jointly with Exformatics A/S.
Original languageEnglish
Title of host publicationSEFM'11 Proceedings of the 9th international conference on Software engineering and formal methods
Number of pages16
Publication date2011
ISBN (Print)237-252
Publication statusPublished - 2011
Event9th International Conference on Software Engineering and Formal Methods - Montevideo, Uruguay
Duration: 14 Nov 201118 Nov 2011
Conference number: 9th


Conference9th International Conference on Software Engineering and Formal Methods
Internet address


Dive into the research topics of 'Safe Distribution of Declarative Processes'. Together they form a unique fingerprint.

Cite this