This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Deriving Petri Nets from Finite Transition Systems
August 1998 (vol. 47 no. 8)
pp. 859-882

Abstract—This paper presents a novel method to derive a Petri Net from any specification model that can be mapped into a state-based representation with arcs labeled with symbols from an alphabet of events (a Transition System, TS). The method is based on the theory of regions for Elementary Transition Systems (ETS). Previous work has shown that, for any ETS, there exists a Petri Net with minimum transition count (one transition for each label) with a reachability graph isomorphic to the original Transition System. Our method extends and implements that theory by using the following three mechanisms that provide a framework for synthesis of safe Petri Nets from arbitrary TSs. First, the requirement of isomorphism is relaxed to bisimulation of TSs, thus extending the class of synthesizable TSs to a new class called Excitation-Closed Transition Systems (ECTS). Second, for the first time, we propose a method of PN synthesis for an arbitrary TS based on mapping a TS event into a set of transition labels in a PN. Third, the notion of irredundant region set is exploited, to minimize the number of places in the net without affecting its behavior. The synthesis method can derive different classes of place-irredundant Petri Nets (e.g., pure, free choice, unique choice) from the same TS, depending on the constraints imposed on the synthesis algorithm. This method has been implemented and applied in different frameworks. The results obtained from the experiments have demonstrated the wide applicability of the method.

[1] R. Alur and D. Dill, "Automata for Modeling Real-Time Systems," Proc. 17th Int'l Colloq. Aut. Lang. Prog., 1990.
[2] A. Arnold, Finite Transition Systems. Prentice Hall, 1994.
[3] E. Badouel, L. Bernardinello, and P. Darondeau, "Polynomial Algorithms for the Synthesis of Bounded Nets," Lecture Notes in Computer Science, vol. 915, pp. 364-383, 1995.
[4] E. Badouel and P. Darondeau, "Theory of Regions," Third Advance Course on Petri Nets. Springer-Verlag, 1998.
[5] L. Bernardinello, "Synthesis of Net Systems," Application and Theory of Petri Nets, Lecture Notes in Computer Science, vol. 691, pp. 89-105. Springer-Verlag, 1993
[6] L. Bernardinello, G. De Michelis, K. Petruni, and S. Bigna, "On Synchronic Structure of Transition Systems," Proc. Int'l Workshop Structures in Concurrency Theory (STRICT), pp. 69-84, May 1995.
[7] G. Berthelot, "Transformations and Decompositions of nets," Advances in Petri Nets '86, W. Reisig, W. Brauer, and G. Rozenberg, eds., Lecture Notes in Computer Science, vol. 254, pp. 359-376. Springer-Verlag, Feb. 1987.
[8] K. Bilinski and E. Dagless, "High Level Synthesis of Synchronous Parallel Controllers," Proc. 17th Int'l Conf. Applications and Theory of Petri Nets, Lecture Notes in Computer Science, vol. 1,091, pp. 346-365,Osaka, Japan, June 1996.
[9] R.K. Brayton, G.D. Hachtel, C.T. McMullen, and A.L. Sangiovanni-Vincintelli, Logic Minimization Algorithms for VLSI Synthesis.Boston: Kluwer Academic, 1984.
[10] R.E. Bryant, "Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams," ACM Computing Surveys, vol., 24 no. 3, pp. 293-318, 1992.
[11] F. Di Cesare, G. Harhalakis, J.M. Proth, M. Silva, and F.B. Vernadat, Practice of Petri Nets in Manufacturing. Chapman&Hall, 1993.
[12] T.-A. Chu, "Synthesis of Self-Timed VLSI Circuits from Graph-Theoretic Specifications," PhD thesis, Massachusetts Inst. of Tech nology, June 1987.
[13] E.M. Clarke, D.E. Long, and K.L. McMillan, "A Language for Compositional Specification and Verification of Finite State Hardware Controllers," Proc. IEEE, vol. 79, no. 9, Sept. 1991.
[14] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev, "Complete State Encoding Based on the Theory of Regions," Proc. Int'l Symp. Advanced Research in Asynchronous Circuits and Systems, pp. 36-47, Mar. 1996.
[15] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev, "Methodology and Tools for State Encoding in Asynchronous Circuit Synthesis," Proc. Design Automation Conf., pp. 63-66, June 1996.
[16] J. Cortadella, M. Kishinevsky, A. Kondratyev, L. Lavagno, and A. Yakovlev, "Petrify: A Tool for Manipulating Concurrent Specifications and Synthesis of Asynchronous Controllers," IEICE Trans. Information and Systems, vol. E80-D, no. 3, pp. 315-325, Mar. 1997.
[17] J. Cortadella, M. Kishinevsky, L. Lavagno, and A. Yakovlev, "Deriving Petri Nets from Finite Transition Systems," Technical Report UPC-DAC-1996-19, Dept. of Computer Architecture, Universitat Politècnica de Catalunya, June 1996. ftp://ftp.ac.upc.es/pub/reports/DAC/1996 UPC-DAC-1996-19.ps.Z.
[18] O. Coudert, C. Berthet, and J.C. Madre, "Verification of Sequential Machines Using Boolean Functional Vectors," Proc. IFIP Int'l Workshop Applied Formal Methods for Correct VSLI Design, L. Claesen, ed., pp. 111-128,Leuven, Belgium, Nov. 1989.
[19] G. de Jong and B. Lin, "A Communicating Petri Net Model for the Design of Concurrent Asynchronous Modules," Proc. Design Automation Conf., pp. 49-55, Apr. 1994.
[20] J. Desel and J. Esparza, Free-Choice Petri Nets, Cambridge Tracts in Theoretical Computer Science, vol. 40. Cambridge Univ. Press, 1995.
[21] J. Desel and W. Reisig, "The Synthesis Problem of Petri Nets," Acta Informatica, vol. 33, no. 4, pp. 297-315, 1996.
[22] D.L. Dill, Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits.Cambridge, Mass.: MIT Press, 1988.
[23] D. Drusinsky, "Extended State Diagrams and Reactive Systems," Dr. Dobb's J., pp. 72-80, 106-107, Oct. 1994.
[24] A. Ehrenfeucht and G. Rozenberg, "Partial (Set) 2-Structures, Parts I II," Acta Informatica, vol. 27, pp. 315-368, 1990.
[25] J. Esparza and M. Nielsen, "Decidability Issues for Petri Nets," Petri Nets Newsletter, vol. 94, pp. 5-23, 1994.
[26] G. Hachtel and F. Somenzi, Logic Synthesis and Verification Algorithms. Kluwer Academic, 1996.
[27] M. Hack, "Analysis of Production Schemata by Petri Nets," TR 94, Project MAC, Massachusetts Inst. of Tech nology, 1972.
[28] C.A.R. Hoare,“Communicating sequential processes,” Comm. of the ACM, vol. 21, no. 8, pp. 666-677, Aug. 1978.
[29] H. Hulgaard and S.M. Burns,“Bounded delay timing analysis of a class of CSP programs with choice,” Int’l Symp. Advanced Research in Asynchronous Circuits and Systems, Nov. 1994.
[30] R.M. Keller, "A Fundamental Theorem of Asynchronous Parallel Computation," Lecture Notes in Computer Science, vol. 24, pp. 103-112, 1975.
[31] M. Kishinevsky, J. Cortadella, A. Kondratyev, L. Lavagno, and A. Yakovlev, "Synthesis of General Petri Nets," Technical Report 57, IEICE, Japan, May 1996.
[32] M. Kishinevsky, A. Kondratyev, A. Taubin, and V. Varshavsky, Concurrent Hardware: The Theory and Practice of Self-Timed Design.London: John Wiley and Sons, 1993.
[33] R.P. Kurshan, "Analysis of Discrete Event Coordination," Lecture Notes in Computer Science. Springer-Verlag, 1990.
[34] L. Lavagno and A. Sangiovanni-Vincentelli, Algorithms for Synthesis and Testing of Asynchronous Circuits, Kluwer Academic Publishers, Boston, 1993.
[35] C.Y. Lee, "Representation of Switching Functions by Vinary Decision Programs," Bell System Technical J., vol. 38, pp. 985-999, 1959.
[36] B. Lin and F. Somenzi, "Minimization of Symbolic Relations," Proc. IEEE Int'l Conf. Computer-Aided Design, pp. 88-91,Santa Clara, Calif., Nov. 1990.
[37] R. Milner, A Calculus of Communicating Systems. Berlin: Springer Verlag, vol. 92, 1980.
[38] R. Milner, Communication and Concurrency, Prentice-Hall, Englewood Cliffs, N.J., 1989.
[39] D. Misunas, "Petri Nets and Speed-Independent Design," Comm. ACM, pp. 474-481, Aug. 1973.
[40] M. Mukund, "Petri Nets and Step Transition Systems," Int'l J. Foundations of Computer Science, vol. 3, no. 4, pp. 443-478, 1992.
[41] T. Murata, “Petri Nets: Properties, Analysis and Application,” Proc. IEEE, vol. 77, no. 4, 1989.
[42] M. Nielsen, G. Rozenberg, and P.S. Thiagarajan, "Elementary Transition Systems," Theoretical Computer Science, vol. 96, pp. 3-33, 1992.
[43] S.M. Nowick and D.L. Dill, "Automatic Synthesis of Locally-Clocked Asynchronous State Machines," Proc. ICCAD, 1991.
[44] J. Oldfield and R. Dorf, Field-Programmable Gate Arrays: Reconfigurable Logic for Rapid Prototyping and Implementation of Digital Systems. John Wiley and Sons, 1995.
[45] E. Paster and J. Cortadella, "Polynomial Algorithm for the Synthesis of Hazard-Free Circuits from STGs," Proc. Int'l Cconf. Computer Aided Design, pp. 250-254, 1993.
[46] E. Pastor et al., "Petri Net Analysis Using Boolean Manipulation," Proc. Int'l Conf. Applications and Theory of Petri Nets, LNCS 815, Springer-Verlag, Berlin, 1994, pp. 416-435.
[47] M. Peña and J. Cortadella, "Combining Process Algebras and Petri Nets for the Specification and Synthesis of Asynchronous Circuits," Proc. Int'l Symp. Advanced Research in Asynchronous Circuits and Systems, pp. 222-232, Mar. 1996.
[48] C.A. Petri, "Kommunidation mit Automaten," PhD thesis, Technical Report Schriften des IIM Nr. 3, Institut für Instrumentalle Mathematik, Bonn, Germany, 1962.
[49] S.R. Petrick, "A Direct Determination of the Irredundant Forms of a Boolean Function from the Set of Prime Implicants," Technical Report AFCRC-TR-56-110, Air Force Cambridge Research Center, Cambridge, Mass., Apr. 1956.
[50] M. Pezzè, R.N. Taylor, and M. Young, "Graph Models for Reachability Analysis of Concurrent Programs," ACM Trans. Software Eng. and Methodology, vol. 4, no. 2, pp. 171-213, Apr. 1995.
[51] I. Reicher and M. Yoeli, "Net-Based Modeling of Communicating Parallel Processes with Applications to VLSI Design," Technical Report 532, Technion, Haifa, Israel, 1988.
[52] T.G. Rokicki,“Representing and modeling digital circuits,” PhD thesis, Stanford Univ., 1993.
[53] L.Y. Rosenblum and A.V. Yakovlev, “Signal Graphs: From Self-Timed to Timed Ones,” Proc. Int’l Workshop Timed Petri Nets, IEEE CS Press, 1985, pp. 199-207.
[54] M. Silva, Las Redes de Petri en la Automática y la Informática.Madrid, Spain: AC, 1985. (in Spanish)
[55] D.C. Tsichritzis and P.A. Bernstein, Operating Systems.London: Academic Press, 1974.
[56] K. van Berkel, Handshake Circuits: An Asynchronous Architecture for VLSI Programming, Int'l series parallel computation. Cambridge Univ. Press, 1993.
[57] G. Winskel, "Petri Nets, Algebras, Morphisms, and Compositionality," Information and Computation, pp. 197-238, vol. 72, 1987.
[58] M. Zhou, F. DiCesare, and A. Desrochers, "A Hybrid Methodology for Synthesis of Petri Net Models for Manufacturing Systems," IEEE Trans. Robotics and Automation, vol. 8, no. 3, pp. 350-361, June 1992.

Index Terms:
Petri Nets, transition systems, concurrent systems, asynchronous systems, synthesis.
Citation:
Jordi Cortadella, Michael Kishinevsky, Luciano Lavagno, Alexandre Yakovlev, "Deriving Petri Nets from Finite Transition Systems," IEEE Transactions on Computers, vol. 47, no. 8, pp. 859-882, Aug. 1998, doi:10.1109/12.707587
Usage of this product signifies your acceptance of the Terms of Use.