This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Mapping Petri Nets with Inhibitor Arcs onto Basic LOTOS Behavior Expressions
December 1995 (vol. 44 no. 12)
pp. 1361-1370

Abstract—The integration of different formal description techniques is an important feature in the design of communication protocols and concurrent systems. In this paper we address the problem of translating Petri nets with inhibitor arcs into basic LOTOS specifications, which is an important step in the direction of integrating these two commonly used formalisms. A mapping which preserves strong bisimulation equivalence is formally defined and illustrated by means of an example. The definition of the mapping enables us also to state a new result about the expressive power of the basic LOTOS subset which constitutes the mapping range.

[1] S.C. Murphy,P. Gunningberg,, and J.P. J. Kelly,“Implementing protocols with multiple specifications: Experienceswith Estelle, LOTOS and SDL,” Protocol Specification, Testing and Verification IX, E. Brinksma, G. Scollo, and C.A. Vissers, eds. Elsevier Science, 1990.
[2] H. Saria,H. Nirschl,, and C. Binding,“Mixing LOTOS and SDL specifications,” Proc. FORTE’91: Fourth Int’l Conf. Formal Description Techniques, K. Parker, and G. Rose, eds. Elsevier Science, 1992.
[3] J.L. Peterson, Petri Net Theory and the Modeling of Systems.Englewood Cliffs, N.J.: Prentice Hall, 1981.
[4] IS 8807: Information Processing Systems, Open Systems Interconnection,LOTOS—A Formal Description Technique Based on the Temporal Ordering ofObservational Behavior, ISO, 1989.
[5] E. Brinksma and T. Bolognesi, "Introduction to the ISO Specification Language LOTOS," Computer Networks and ISDN Systems, vol. 14, pp. 25-59, 1987.
[6] M. Diaz,“Modeling and analysis of communication and cooperation protocolsusing Petri net based models,” Computer Networks, vol. 6, pp. 419-441, 1982.
[7] G. Boudol,G. Roucairol,, and R. de Simone,“Petri nets and algebraic calculi of processes,” Advances in Petri Nets 1985, pp. 41-58.
[8] U. Goltz, and W. Reisig,“CSP-programs as nets with individual tokens,” Advances in Petri Nets 1984, G. Rozenberg, ed., pp.169-196, LNCS 188, Springer-Verlag, 1985.
[9] U. Goltz, and A. Mycroft,“On the relationship of CCS and Petri nets,” Proc. ICALP’84, LNCS 172, pp. 196-208, Springer-Verlag, 1984.
[10] U. Goltz,“On representing CCS programs by finite Petri nets,” Mathematical Foundations of Computer Science 1988, pp. 339-350, LNCS 324, Springer-Verlag, 1988.
[11] M. Nielsen,“CCS and its relationship to Net theory,” Advances in Petri Nets 1986, W. Brauer, ed., pp. 393-415, LNCS 255, Springer-Verlag, 1986.
[12] S. Marchena, and G. Leon,“Transformation from LOTOS specs to Galileo nets,” Proc. of FORTE’88: First Int’l Conf. Formal Description Techniques, K. J. Turner, ed. Elsevier Science, 1989.
[13] R. Van Glabbeek, and F. Vaandrager,“Petri net models for algebraic theories of concurrency,” Proc. PARLE, LNCS 259, Springer-Verlag, 1987.
[14] H. Garavel, and J. Sifakis,“Compilation and verification of LOTOS specifications,” Protocol Specification, Testing and Verification X, L. Logrippo, R.L. Probert, and H. Ural, eds. Elsevier Science, 1990.
[15] D. Taubner,Finite Representations of CCS and TCSP Programs by Automata andPetri Nets, LNCS 369. Springer-Verlag, 1989.
[16] R. Milner, A Calculus of Communicating Systems. Berlin: Springer Verlag, vol. 92, 1980.
[17] K. Jensen,“Coloured Petri nets and the invariant-method,” Theoretical Computer Science, vol. 14, pp. 317-336, 1981.
[18] H.J. Genrich, and K. Lautenbach,“System modelling with high-level Petri nets,” Theoretical Computer Science, vol. 13, pp. 109-136, 1981.
[19] A. Fantechi,S. Gnesi,, and G. Mazzarini,“How much expressive are LOTOS behavior expressions?,” Proc. FORTE’90: Third Int’l Conf. Formal Dscription Techniques, J. Quemada, J. Manas, and E. Vasquez, eds. Elsevier Science, 1991.

Index Terms:
Concurrent systems design, formal description techniques, LOTOS, Petri nets, protocol engineering.
Citation:
Adriano Valenzano, Riccardo Sisto, "Mapping Petri Nets with Inhibitor Arcs onto Basic LOTOS Behavior Expressions," IEEE Transactions on Computers, vol. 44, no. 12, pp. 1361-1370, Dec. 1995, doi:10.1109/12.477242
Usage of this product signifies your acceptance of the Terms of Use.