Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Saddek Bensalem, Vijay Ganesh, Yassine Lakhnech, César Muñoz, Sam Owre, Harald Rueß, John Rushby, Vlad Rusu, Hassen Saïdi, N. Shankar, Eli Singerman, and Ashish Tiwari. An overview of SAL. In C. Michael Holloway, editor, LFM 2000: Fifth NASA Langley Formal Methods Workshop, pages 187–196, Hampton, VA, June 2000. Available at http://shemesh.larc.nasa.gov/fm/Lfm2000/Proc/.
N. Bjorner, A. Browne, E. Chang, M. Colon, A. Kapur, Z. Manna, H.B. Simpa, and T.E. Uribe. Step: The stanford temporal prover-user’s manual. Technical Report STAN-CS-TR-95-1562, Department of Computer Science, Stanford University, November 1995.
B. Eichenauer and M. Zelm. Transformation of cimosa-models into petrinet-models with pace. Technical report, 1999. http://www.ibepace.com.
R. Esser. An Object Oriented Petri Net Approach to Embedded System Design. Phd dissertation, ETH Zurich, 1996.
R. Esser, J.W. Janneck, and M. Naedele. Using an object-oriented petri net tool for heterogeneous systems design: A case study. In Proceedings of Algorithmen und Werkzeuge fur Petrinetze, 1997.
B. Grahlmann and C. Pohl. Profiting from spin in pep. In Proceedings of the SPIN’98 Workshop, 1998.
S. Katz and O. Grumberg. A framework for translating models and specifications. In Third international conference on Integrated Formal Methods (IFM’02), Turku, Finland, May 2002.
P. Kemper. Logistic process models go petri nets. In S. Philippi, editor, Fachberichte Informatik, No. 7-2000: 7. Workshop Algorithmen und Werkzeuge fur Petrinetze, 2.–3, pages 69–74. Universitatt Koblenz-Landau, Institut fur Informatik, 2000.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
M. Nielsen, G. Rozenberg, and P.S. Thiagarajan. Elementery transition systems. Theoretical Computer Science, 96:3–33, 1992.
M. Pietkiewicz-Koutny. Transition systems of elementary net systems with inhibitor arcs. In P. Azma and G. Balbo, editors, 18th International Conference on Application and Theory of Petri Nets, volume 1248 of LNCS, pages 310–327. Springer-Verlag, 1997.
W. Reisig. Elements of Distributed Algorithms-Modeling and Analysis with Petri Nets. Springer-Verlag, 1998.
L. Shi and P. Nixon. An improved translation of sa/rt specification model to high-level timed petri nets. In FME’96: Industrial Benefit and Advances in Formal Methods, volume 1051 of LNCS, pages 518–537. Springer-Verlag, 1996.
R. Sisto and A. Valenzano. Mapping petri nets with inhibitor arcs onto basic lotos behaviour expressions. IEEE Transactions on Computers, 44(12):1361–1370, 1995.
W. Vogler. Concurrent implementation of asynchronous transition systems. In Application and Theory of Petri Nets 1999, 20th International Conference, ICATPN’99, volume 1630 of LNCS, pages 284–303. Springer-Verlag, 1999.
G. Wimmel. A bdd-based model checker for the pep tool. Technical report. Project Report 1997, http://theoretica.Informatik.Uni-Oldenburg.DE/pep.
G. Winskel and M. Nielsen. Models for concurrency. In S. Abramskky, D. Gabbay, and T.S.E. Maibaum, editors, Handbook of Logic in Computer Science, volume 4, pages 1–148. 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Korenblat, K., Grumberg, O., Katz, S. (2002). Translations between Textual Transition Systems and Petri Nets. In: Butler, M., Petre, L., Sere, K. (eds) Integrated Formal Methods. IFM 2002. Lecture Notes in Computer Science, vol 2335. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47884-1_19
Download citation
DOI: https://doi.org/10.1007/3-540-47884-1_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43703-1
Online ISBN: 978-3-540-47884-3
eBook Packages: Springer Book Archive