High-Level Message Sequence Charts: Satisfiability and Realizability Revisited
Abstract
Message sequence charts (MSCs) visually represent interactions in distributed systems that communicate through FIFO channels. High-level MSCs (HMSCs) extend MSCs with choice, concatenation, and iteration, allowing for the specification of complex behaviors. This paper revisits two classical problems for HMSCs: satisfiability and realizability. Satisfiability (also known as reachability or nonemptiness) asks whether there exists a path in the HMSC that gives rise to a valid behavior. Realizability concerns translating HMSCs into communicating finite-state machines to ensure correct system implementations. While most positive results assume bounded channels, we introduce a class of HMSCs that allows for unbounded channels while maintaining effective implementations. On the other hand, we show that the corresponding satisfiability problem is still undecidable.
Keywords
Cite
@article{arxiv.2504.19814,
title = {High-Level Message Sequence Charts: Satisfiability and Realizability Revisited},
author = {Benedikt Bollig and Marie Fortin and Paul Gastin},
journal= {arXiv preprint arXiv:2504.19814},
year = {2025}
}