A Logic for Choreographies

Marco Carbone, Davide Grohmann, Thomas T. Hildebrandt, Hugo A. López

Research output: Contribution to journalJournal articleResearchpeer-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 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.
Original languageEnglish
JournalElectronic Proceedings in Theoretical Computer Science
ISSN2075-2180
Publication statusPublished - 1 Oct 2011

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

Cite this