# High-Level Message Sequence Charts: Satisfiability and Realizability Revisited

arXiv: https://arxiv.org/abs/2504.19814 · HTML: https://mlsanity.com/paper/2504.19814/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Apr 2025.

## Built on by (most cited first, 1 of 1)

- [Provable Coordination for LLM Agents via Message Sequence Charts](https://mlsanity.com/paper/2604.17612/) (2026)

## Abstract (arXiv)

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.