High-Level Message Sequence Charts: Satisfiability and Realizability Revisited
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910920688533504 |
|---|---|
| author | Bollig, Benedikt Fortin, Marie Gastin, Paul |
| author_facet | Bollig, Benedikt Fortin, Marie Gastin, Paul |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_19814 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | High-Level Message Sequence Charts: Satisfiability and Realizability Revisited Bollig, Benedikt Fortin, Marie Gastin, Paul Logic in Computer Science Formal Languages and Automata Theory 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. |
| title | High-Level Message Sequence Charts: Satisfiability and Realizability Revisited |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2504.19814 |