In: Concurrency, Specification and Programming CS&P'2006, Vol. 1: Concurrency. Informatik-Bericht Nr. 206 der Humbold-Universität zu Berlin, Eds.: G. Lindemann, H. Schlingloff., pages 68-79. September 06.
Abstract: We present in this paper the algorithm which performs the translation of MSC'2000 diagrams into Petri net modulo strong bisimulation. The correctness of this algorithm is justified. Here we supplement MCS'2000 standard supplying it with formal definition of MSC element <condition> by means of process algebra. We would mention here that this translation algorithm is the part of the automated verification system which specifies formally and verify designed software or hardware system specified in MSC language, and is presented in (1), and (2).