A Logic for Choreographies

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

    Research output: Journal Article or Conference Article in 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
    JournalPlaces
    Volume69
    Pages (from-to)29-43
    ISSN0731-0455
    Publication statusPublished - 2010

    Keywords

    • Choreography
    • Specifications
    • Modal Logic
    • Undecidable
    • Coordination Models
    • Logical Reasoning
    • Hennessy-Milner Logic
    • Global Calculus
    • Proof Systems

    Fingerprint

    Dive into the research topics of 'A Logic for Choreographies'. Together they form a unique fingerprint.

    Cite this