A Logic for Choreographies
Programming Languages
2011-10-20 v1 Distributed, Parallel, and Cluster Computing
Logic in Computer Science
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.
Keywords
Cite
@article{arxiv.1110.4159,
title = {A Logic for Choreographies},
author = {Marco Carbone and Davide Grohmann and Thomas T. Hildebrandt and Hugo A. López},
journal= {arXiv preprint arXiv:1110.4159},
year = {2011}
}
Comments
In Proceedings PLACES 2010, arXiv:1110.3853