@inproceedings{6184f63303544f87958c828245aa7345,
title = "Declarative Choreographies and Liveness",
abstract = "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.",
keywords = "Choreographies, Declarative models, Liveness",
author = "Hildebrandt, {Thomas T.} and Tijs Slaats and L{\'o}pez, {Hugo A.} and S{\o}ren Debois and Marco Carbone",
year = "2019",
doi = "10.1007/978-3-030-21759-4_8",
language = "English",
isbn = "9783030217587",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "129--147",
editor = "P{\'e}rez, {Jorge A.} and Nobuko Yoshida",
booktitle = "Formal 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",
note = "39th 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 ; Conference date: 17-06-2019 Through 21-06-2019",
}