A Logic for Choreographies

Research output: Contribution to journal › Journal article › Research › peer-review

Standard

A Logic for Choreographies. / Carbone, Marco; Grohmann, Davide; Hildebrandt, Thomas T.; López, Hugo A.

In: Electronic Proceedings in Theoretical Computer Science, 01.10.2011.

Research output: Contribution to journal › Journal article › Research › peer-review

Harvard

Carbone, M, Grohmann, D, Hildebrandt, TT & López, HA 2011, 'A Logic for Choreographies', Electronic Proceedings in Theoretical Computer Science. <http://arxiv.org/pdf/1110.4159>

APA

Carbone, M., Grohmann, D., Hildebrandt, T. T., & López, H. A. (2011). A Logic for Choreographies. Electronic Proceedings in Theoretical Computer Science. http://arxiv.org/pdf/1110.4159

Vancouver

Carbone M, Grohmann D, Hildebrandt TT, López HA. A Logic for Choreographies. Electronic Proceedings in Theoretical Computer Science. 2011 Oct 1.

Author

Carbone, Marco ; Grohmann, Davide ; Hildebrandt, Thomas T. ; López, Hugo A. / A Logic for Choreographies. In: Electronic Proceedings in Theoretical Computer Science. 2011.

Bibtex

@article{41e4787381964327a98517cb9b72b8e8,
title = "A Logic for Choreographies",
abstract = "We explore logical reasoning for the global calculus, a coordination model based on the notion of choreography, with the aim to provide a methodology for specification and verification of structured communications. Starting with an extension of Hennessy-Milner logic, we present the global logic (GL), a modal logic describing possible interactions among participants in a choreography. We illustrate its use by giving examples of properties on service specifications. Finally, we show that, despite GL is undecidable, there is a significant decidable fragment which we provide with a sound and complete proof system for checking validity of formulae.",
keywords = "Computer Science - Programming Languages, Computer Science - Distributed, Parallel, and Cluster Computing, Computer Science - Logic in Computer Science, F.3.1, F.3.2, C.2.4",
author = "Marco Carbone and Davide Grohmann and Hildebrandt, {Thomas T.} and L{\'o}pez, {Hugo A.}",
year = "2011",
month = oct,
day = "1",
language = "English",
journal = "Electronic Proceedings in Theoretical Computer Science",
issn = "2075-2180",
publisher = "Open Publishing Association",

}

RIS

TY - JOUR

T1 - A Logic for Choreographies

AU - Carbone, Marco

AU - Grohmann, Davide

AU - Hildebrandt, Thomas T.

AU - López, Hugo A.

PY - 2011/10/1

Y1 - 2011/10/1

N2 - We explore logical reasoning for the global calculus, a coordination model based on the notion of choreography, with the aim to provide a methodology for specification and verification of structured communications. Starting with an extension of Hennessy-Milner logic, we present the global logic (GL), a modal logic describing possible interactions among participants in a choreography. We illustrate its use by giving examples of properties on service specifications. Finally, we show that, despite GL is undecidable, there is a significant decidable fragment which we provide with a sound and complete proof system for checking validity of formulae.

AB - We explore logical reasoning for the global calculus, a coordination model based on the notion of choreography, with the aim to provide a methodology for specification and verification of structured communications. Starting with an extension of Hennessy-Milner logic, we present the global logic (GL), a modal logic describing possible interactions among participants in a choreography. We illustrate its use by giving examples of properties on service specifications. Finally, we show that, despite GL is undecidable, there is a significant decidable fragment which we provide with a sound and complete proof system for checking validity of formulae.

KW - Computer Science - Programming Languages

KW - Computer Science - Distributed

KW - Parallel

KW - and Cluster Computing

KW - Computer Science - Logic in Computer Science

KW - F.3.1

KW - F.3.2

KW - C.2.4

M3 - Journal article

JO - Electronic Proceedings in Theoretical Computer Science

JF - Electronic Proceedings in Theoretical Computer Science

SN - 2075-2180

ER -

ID: 247462863