An Abstract Semantics of the Global View of Choreographies

TL;DR

This paper presents an abstract semantics framework for global choreographies using pre-orders, demonstrating greater expressiveness and its relation to communicating machines for formalizing local views.

Contribution

It introduces a novel abstract semantics for choreographies that is more expressive and adaptable to various lower-level semantics, linking global and local views.

Findings

Framework is more expressive than existing models.

Semantics accommodates different lower-level semantics.

Illustrated with interesting examples.

Abstract

We introduce an abstract semantics of the global view of choreographies. Our semantics is given in terms of pre-orders and can accommodate different lower level semantics. We discuss the adequacy of our model by considering its relation with communicating machines, that we use to formalise the local view. Interestingly, our framework seems to be more expressive than others where semantics of global views have been considered. This will be illustrated by discussing some interesting examples.