@inproceedings{486fbcd385c742d19a66809e6ade54d9,
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 = "Liveness, Choreographies, Declarative models, Liveness, Choreographies, Declarative models",
author = "Hildebrandt, {Thomas T.} and Tijs Slaats and L{\'o}pez, {Hugo A.} and S{\o}ren Debois and Marco Carbone",
year = "2019",
month = jun,
doi = "10.1007/978-3-030-21759-4_8",
language = "English",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "129--147",
booktitle = "International Conference on Formal Techniques for Distributed Objects, Components, and Systems",
address = "Germany",
}