Synthesis of Safe Message-Passing Systems

We show that any regular set of basic MSCs can be implemented by a deadlock-free communicating finite-state machine with local termination: Processes stop in local dead-states independently from the contents of channels and the local states of other processes. We present a self-contained, direct, and relatively simple construction based on a new notion called context MSC.

• Type: Conference
• Year: 2007
• Where: FSTTCS
• Authors: Nicolas Baudru, Rémi Morin
• Keywords: Communicating finite-state Machine, FSTTCS 2007, Local Termination, Notion Called Context