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 channelswhile 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

  • Benedikt Bollig,
  • Marie Fortin,
  • Paul Gastin

摘要

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 channelswhile maintaining effective implementations. On the other hand, we show that the corresponding satisfiability problem is still undecidable.