ITU

A Logic for Choreographies

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Standard

A Logic for Choreographies. / Lopez, Hugo Andres; Carbone, Marco; Hildebrandt, Thomas; Grohmann, Davide.

In: Places, Vol. 69, 2010, p. 29-43.

Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

Harvard

APA

Vancouver

Author

Bibtex

@article{ccb201ce0d7d4cdc9fbffdf5ac472ac3,
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. Weillustrate 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.",
author = "Lopez, {Hugo Andres} and Marco Carbone and Thomas Hildebrandt and Davide Grohmann",
year = "2010",
language = "English",
volume = "69",
pages = "29--43",
journal = "Places (Brooklyn) (Print)",
issn = "0731-0455",
publisher = "Design History Foundation",

}

RIS

TY - JOUR

T1 - A Logic for Choreographies

AU - Lopez, Hugo Andres

AU - Carbone, Marco

AU - Hildebrandt, Thomas

AU - Grohmann, Davide

PY - 2010

Y1 - 2010

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

M3 - Journal article

VL - 69

SP - 29

EP - 43

JO - Places (Brooklyn) (Print)

JF - Places (Brooklyn) (Print)

SN - 0731-0455

ER -

ID: 34548883