Infinite-state high-level MSCs: Model-checking and realizability

Message sequence charts (MSC) and High-level MSC (HMSC) is a visual notation for asynchronously communicating processes and a standard of the ITU. They usually represent incomplete specifications of required or forbidden properties of communication protocols. We consider in this paper two basic problems concerning the automated validation of HMSC specifications, namely model-checking and synthesis. We identify natural syntactic restrictions of HMSCs for which we can solve the above questions. We show first that model-checking for globally cooperative (and locally cooperative) HMSCs is decidable within the same complexity as for the restricted class of bounded HMSCs. Furthermore, model-checking local-choice HMSCs turns out to be as efficient as for finite-state (sequential) systems. The study of locally cooperative and local-choice HMSCs is motivated by the synthesis question, i.e., the question of implementing HMSCs through communicating finite-state machines (CFM) with additional message data. We show that locally cooperative and local-choice HMSCs are always implementable. Furthermore, the implementation of a local-choice HMSC is deadlock-free and of linear size.