A Logic for Choreographies

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

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review


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.
Sider (fra-til)29-43
StatusUdgivet - 2010


Dyk ned i forskningsemnerne om 'A Logic for Choreographies'. Sammen danner de et unikt fingeraftryk.