Declarative Choreographies and Liveness

Thomas T. Hildebrandt, Tijs Slaats, Hugo A. López, Søren Debois, Marco Carbone

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


We provide the first formal model for declarative choreographies, which is able to express general omega-regular liveness properties. We use the Dynamic Condition Response (DCR) graphs notation for both choreographies and end-points. We define end-point projection as a restriction of DCR graphs and derive the condition for end-point projectability from the causal relationships of the graph. We illustrate the results with a running example of a Buyer-Seller-Shipper protocol. All the examples are available for simulation in the online DCR workbench at
Original languageEnglish
Title of host publicationInternational Conference on Formal Techniques for Distributed Objects, Components, and Systems : FORTE 2019: Formal Techniques for Distributed Objects, Components, and Systems
Number of pages19
Publication dateJun 2019
ISBN (Electronic)978-3-030-21759-4
Publication statusPublished - Jun 2019
SeriesLecture Notes in Computer Science


  • Liveness
  • Choreographies
  • Declarative models


Dive into the research topics of 'Declarative Choreographies and Liveness'. Together they form a unique fingerprint.

Cite this