A structural operational semantics for interactions with a look at loops
Abstract
Message Sequence Charts & Sequence Diagrams are graphical models that represent the behavior of distributed and concurrent systems via the scheduling of discrete and local emission and reception events. We propose an Interaction Language (IL) to formalize such models, defined as a term algebra which includes strict and weak sequencing, alternative and parallel composition and four kinds of loops. This IL is equipped with a denotational-style semantics associating a set of traces (sequences of observed events) to each interaction. We then define a structural operational semantics in the style of process algebras and formally prove the equivalence of both semantics.
Cite
@article{arxiv.2105.00208,
title = {A structural operational semantics for interactions with a look at loops},
author = {Erwan Mahe and Christophe Gaston and Pascale Le Gall},
journal= {arXiv preprint arXiv:2105.00208},
year = {2021}
}
Comments
14 pages of contents, 9 additional pages with 1 for references and 8 for appendices, 5 figures