Translations between models expressed in textual transition systems and those expressed in structured Petri net notation are
presented, in both directions. The translations are
structure-preserving, meaning that the hierarchical structure of the systems is preserved. Furthermore, assuming non-finite data has been abstracted
out of the textual transition system, then translating one model to another and then back results in a model which is identical
to the original one, up to renaming and the form of Boolean expressions. Due to inherent differences between the two notations,
however, some additional information is required in order to obtain this identity. The information is collected during the
translation in one direction and is used in the translation back.
Our translation is also semantics-preserving. That is, the original model and the translated model are bisimulation equivalent, assuming non-finite data is abstracted.
Thus, the translation preserves all temporal properties expressible in the logic CTL*.
The translations are both more generally applicable and more detailed than previously considered. They are shown both for
individual modules, with a collection of transitions, and for a structured system, where modules are combined in different
ways.
Keywords model translations - Petri nets - textual transition systems - structure and semantics preservation