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.
Author supplied keywords
Cite
CITATION STYLE
Hildebrandt, T. T., Slaats, T., López, H. A., Debois, S., & Carbone, M. (2019). Declarative Choreographies and Liveness. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11535 LNCS, pp. 129–147). Springer Verlag. https://doi.org/10.1007/978-3-030-21759-4_8
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
