A structural operational semantics for interactions with a look at loops

TL;DR

This paper introduces a formal Interaction Language (IL) with a structural operational semantics to model and analyze behaviors of distributed systems, including loops, ensuring semantic consistency between different formalizations.

Contribution

It presents a novel formal language for interactions with loops and proves the equivalence of its denotational and operational semantics.

Findings

The IL effectively models distributed system interactions.

Semantic equivalence between denotational and operational semantics is established.

The language includes various composition operators and loop constructs.

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.