Declarative Choreographies and Liveness

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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

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 publicationFormal Techniques for Distributed Objects, Components, and Systems - 39th IFIP WG 6.1 International Conference, FORTE 2019, held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019, Proceedings
EditorsJorge A. Pérez, Nobuko Yoshida
Number of pages19
PublisherSpringer
Publication date2019
Pages129-147
ISBN (Print)9783030217587
DOIs
Publication statusPublished - 2019
Event39th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2019 held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019 - Kongens Lyngby, Denmark
Duration: 17 Jun 201921 Jun 2019

Conference

Conference39th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects, Components, and Systems, FORTE 2019 held as part of the 14th International Federated Conference on Distributed Computing Techniques, DisCoTec 2019
LandDenmark
ByKongens Lyngby
Periode17/06/201921/06/2019
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11535 LNCS
ISSN0302-9743

    Research areas

  • Choreographies, Declarative models, Liveness

ID: 227336580