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 speciﬁcation and veriﬁcation 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 speciﬁcations. Finally, we show that, despite GL is undecidable, there is a signiﬁcant decidable fragment which we provide with a sound and complete proof system for checking validity of formulae.
This page is printed from https://en.itu.dk/research/portalplaceholder?layoutfraction=top&langRef=https://pure.itu.dk/portal/da/journals/journal-of-global-information-technology-management(7012c5f4-e87b-4242-b3e6-de0c234de17a)/publications.html