Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

High-Level Message Sequence Charts: Satisfiability and Realizability Revisited

Benedikt Bollig, Marie Fortin, Paul Gastin

TL;DR

The paper addresses two core problems for high-level message sequence charts (HMSCs): realizability (synthesis) and satisfiability (nonemptiness). It introduces loop-connected HMSCs, which permit unbounded channels yet admit effective translations toCFMs via existential monadic second-order logic (EMSO), enabling synthesis in this broader setting. The authors prove EMSO-definable MSC languages are closed under union, concatenation, and iteration for connected cases, and provide a state-elimination framework to realize loop-connected HMSCs as CFMs. Despite these constructive results, they show satisfiability is undecidable even under several restrictions, including loop-connectedness with a flat structure, two processes, or a singleton message alphabet, via PCP and halting problem reductions. The work delineates the boundary between realizability and satisfiability in distributed systems with unbounded buffers, informing synthesis and verification approaches for complex MSC-based specifications.

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.

High-Level Message Sequence Charts: Satisfiability and Realizability Revisited

TL;DR

The paper addresses two core problems for high-level message sequence charts (HMSCs): realizability (synthesis) and satisfiability (nonemptiness). It introduces loop-connected HMSCs, which permit unbounded channels yet admit effective translations toCFMs via existential monadic second-order logic (EMSO), enabling synthesis in this broader setting. The authors prove EMSO-definable MSC languages are closed under union, concatenation, and iteration for connected cases, and provide a state-elimination framework to realize loop-connected HMSCs as CFMs. Despite these constructive results, they show satisfiability is undecidable even under several restrictions, including loop-connectedness with a flat structure, two processes, or a singleton message alphabet, via PCP and halting problem reductions. The work delineates the boundary between realizability and satisfiability in distributed systems with unbounded buffers, informing synthesis and verification approaches for complex MSC-based specifications.

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.
Paper Structure (20 sections, 8 theorems, 23 equations, 6 figures)

This paper contains 20 sections, 8 theorems, 23 equations, 6 figures.

Table of Contents

  1. Introduction
  2. Outline.
  3. Preliminary Definitions
  4. Message Sequence Charts
  5. Concatenation.
  6. Infinite product.
  7. High-Level Message Sequence Charts
  8. Communicating Finite-State Machines
  9. (Existential) Monadic Second-Order Logic
  10. Main Results
  11. Realizability of HMSCs
  12. The case of bounded channels.
  13. Satisfiability of HMSCs
  14. Some Closure Properties of EMSO Languages
  15. Realizability of HMSCs
  16. ...and 5 more sections

Key Result

theorem 1

For every EMSO sentence $\varphi$, one can effectively construct a CFM $\mathcal{A}$ such that $L(\varphi) = L(\mathcal{A})$.

Figures (6)

  • Figure 1: Example cMSCs.
  • Figure 2: Example HMSC that is loop-connected but not safe
  • Figure 3: An example CFM
  • Figure 4: Connected and flat HMSC used for the reduction from the PCP problem.
  • Figure 5: Simulation of a run of a Turing machine with an MSC.
  • ...and 1 more figures

Theorems & Definitions (15)

  • definition 1: compositional MSC
  • remark 1
  • definition 2
  • definition 3
  • theorem 1: BolligFG21
  • theorem 2
  • theorem 3: Genest, Kuske, and Muscholl GenestKM06
  • theorem 4
  • theorem 5
  • lemma 1
  • ...and 5 more