Message Sequence Charts (MSCs) visually represent interactions in distributed systems communicating through FIFO channels. High-Level MSCs (HMSCs) extend MSCs with choice, concatenation, and iteration, allowing for the specification of complex behaviors. In this talk, I will present a class of HMSCs that allows for unbounded channels and maintains effective implementations, and review existing results for channel-bounded systems in light of our new definition. I will also discuss the connection to logic.

This is based on joint work with Benedikt Bollig and Paul Gastin.