A Logic for Choreographies

TL;DR

This paper introduces a logical framework, called global logic (GL), for specifying and verifying structured communications in choreographies, including a decidable fragment with a proof system.

Contribution

It extends Hennessy-Milner logic to model interactions in choreographies and provides a sound, complete proof system for a decidable fragment.

Findings

Global logic (GL) describes interactions among choreography participants.

A decidable fragment of GL has been identified and formalized.

The proof system for the fragment is sound and complete.

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.