ITU
ITU

Declarative Choreographies and Liveness

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

View graph of relations

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 http://dcr.tools/forte19.
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
PublisherSpringer
Publication dateJun 2019
Pages129-147
ISBN (Electronic)978-3-030-21759-4
DOIs
Publication statusPublished - Jun 2019
SeriesLecture Notes in Computer Science
Volume11535
ISSN0302-9743
Close

    Research areas

  • Liveness, Choreographies, Declarative models

ID: 84259679