Declarative Choreographies and Liveness

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

Standard

Declarative Choreographies and Liveness. / Hildebrandt, Thomas T.; Slaats, Tijs; López, Hugo A.; Debois, Søren; Carbone, Marco.

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. red. / Jorge A. Pérez; Nobuko Yoshida. Springer, 2019. s. 129-147 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 11535 LNCS).

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

Harvard

Hildebrandt, TT, Slaats, T, López, HA, Debois, S & Carbone, M 2019, Declarative Choreographies and Liveness. i JA Pérez & N Yoshida (red), 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. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), bind 11535 LNCS, s. 129-147, 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, Kongens Lyngby, Danmark, 17/06/2019. https://doi.org/10.1007/978-3-030-21759-4_8

APA

Hildebrandt, T. T., Slaats, T., López, H. A., Debois, S., & Carbone, M. (2019). Declarative Choreographies and Liveness. I J. A. Pérez, & N. Yoshida (red.), 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 (s. 129-147). Springer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind. 11535 LNCS https://doi.org/10.1007/978-3-030-21759-4_8

Vancouver

Hildebrandt TT, Slaats T, López HA, Debois S, Carbone M. Declarative Choreographies and Liveness. I Pérez JA, Yoshida N, red., 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. Springer. 2019. s. 129-147. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 11535 LNCS). https://doi.org/10.1007/978-3-030-21759-4_8

Author

Hildebrandt, Thomas T. ; Slaats, Tijs ; López, Hugo A. ; Debois, Søren ; Carbone, Marco. / Declarative Choreographies and Liveness. 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. red. / Jorge A. Pérez ; Nobuko Yoshida. Springer, 2019. s. 129-147 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Bind 11535 LNCS).

Bibtex

@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",

}

RIS

TY - GEN

T1 - Declarative Choreographies and Liveness

AU - Hildebrandt, Thomas T.

AU - Slaats, Tijs

AU - López, Hugo A.

AU - Debois, Søren

AU - Carbone, Marco

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

KW - Choreographies

KW - Declarative models

KW - Liveness

U2 - 10.1007/978-3-030-21759-4_8

DO - 10.1007/978-3-030-21759-4_8

M3 - Article in proceedings

AN - SCOPUS:85067365596

SN - 9783030217587

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 129

EP - 147

BT - 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

A2 - Pérez, Jorge A.

A2 - Yoshida, Nobuko

PB - Springer

T2 - 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

Y2 - 17 June 2019 through 21 June 2019

ER -

ID: 227336580