In: Proceedings of CONCUR 2004 - Concurrency Theory: 15th International Conference, London, UK, August 31 - September 3, 2004, pages 99-114. Volume 3170 of Lecture Notes in Computer Science / Philippa Gardner, Nobuko Yoshida (Eds.) --- Springer-Verlag, September 2004.
Abstract: Netcharts have been introduced recently by Mukund et al. This new appealing approach to the specification of collections of message sequence charts (MSCs) benefits from a graphical description, a formal semantics based on Petri nets, and an appropriate expressive power. As opposed to high-level MSCs, any regular MSC language is the language of some netchart. Motivated by two open problems raised by Mukund et al., we establish in this paper that the questions (i) whether a given high-level MSC describes some netchart language (ii) whether a given netchart is equivalent to some high-level MSC (iii) whether a given netchart describes a regular MSC language are undecidable. These facts are closely related to our first positive result: We prove that netchart languages are exactly the MSC languages that are implementable by message passing automata up to refinement of message contents. Next we focus on FIFO netcharts: The latter are defined as the netcharts whose executions correspond to all firing sequences of their low-level Petri net. We show that the questions (i) whether a netchart is a FIFO netchart (ii) whether a FIFO netchart describes a regular MSC language (iii) whether a regular netchart is equivalent to some high-level MSC are decidable.