A Logic for Choreographies

Hugo Andres Lopez; Marco Carbone; Thomas Hildebrandt; Davide Grohmann

A Logic for Choreographies

Hugo Andres Lopez, Marco Carbone, Thomas Hildebrandt, Davide Grohmann

Computer Science

Research output: Journal Article or Conference Article in Journal › Journal article › Research › peer-review

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 speciﬁcation and veriﬁcation 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 speciﬁcations. Finally, we show that, despite GL is undecidable, there is a signiﬁcant decidable fragment which we provide with a sound and complete proof system for checking validity of formulae.

Original language	English
Journal	Places
Volume	69
Pages (from-to)	29-43
ISSN	0731-0455
Publication status	Published - 2010

Access to Document

CGHL10Submitted manuscript, 246 KB

Cite this

@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 speciﬁcation and veriﬁcation 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 speciﬁcations. Finally, we show that, despite GL is undecidable, there is a signiﬁcant 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",

}

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 speciﬁcation and veriﬁcation 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 speciﬁcations. Finally, we show that, despite GL is undecidable, there is a signiﬁcant 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 speciﬁcation and veriﬁcation 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 speciﬁcations. Finally, we show that, despite GL is undecidable, there is a signiﬁcant 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 -

A Logic for Choreographies

Abstract

Access to Document

Fingerprint

Cite this