This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Temporal Petri Nets and Their Application to Modeling and Analysis of a Handshake Daisy Chain Arbiter
May 1989 (vol. 38 no. 5)
pp. 696-704
A class of Petri nets called temporal Petri nets is introduced, in which timing constraints are represented by the operators of temporal logic. Due to the versatility of the temporal logic operations to express temporal assertions, temporal Petri nets can describe clearly and compactly causal and temporal relationships between the events of a system, including eventuality and fairness. The use

[1] T. Agerwala, "Putting Petri nets to work,"IEEE Computer, pp. 85- 94, Dec. 1979.
[2] B. Alpern and F. B. Schneider, "Defining liveness,"Inform. Processing Lett., vol. 21, pp. 181-185, 1985.
[3] K. A. Bartlett, R. A. Scantlebury, and P.T. Wilkinson, "A note on reliable full-duplex transmission over half-duplex link,"Commun. ACM, vol. 12, no. 5, May 1969.
[4] E. A. Emerson and E. Clarke, "Design and synthesis of synchronization skeletons using branching-time temporal logic," inProc. Workshop Logic of Programs, Lecture Notes in Computer Science 131, Springer-Verlag, 1981.
[5] E. Coolhan, Jr. and N. Roussopoulos, "Timing requirements for time-driven systems using augmented Petri nets,"IEEE Trans. Software Eng., vol. SE-9, pp. 603-616, Sept. 1983.
[6] D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, "On the temporal analysis of fairness," inProc. 7th ACM Symp. Principles of Programming Languages, Las Vegas, NV, Jan. 1980, pp. 163-173.
[7] B. T. Hailpern and S. Owicki, "Verifying network protocols using temporal logic," inTrends and Applications 1980: Computer Network Protocols, IEEE Computer Society, 1980, pp. 18-28.
[8] L. Lamport, "Sometimes is sometimes not never," inProc. Ass. Comput. Mach. Symp. Principles of Programming Languages, Las Vegas, NV, Jan. 1980, pp. 174-185.
[9] K. Lautenbach and H. Schmid, "Use of Petri nets for proving correctness of concurrent process systems,"Inform. Processing 74, pp. 187-191, 1974.
[10] H. Lu, "Modeling and analysis of concurrent processing systems by temporal Petri nets," M.S. thesis, Dept. Comput. Sci., Texas Tech Univ., Dec. 1986.
[11] Z. Manna and A. Pnueli, "Verification of concurrent programs: The temporal framework," inThe Correctness Problem in Computer Science, International Lecture Series in Computer Science, R. S. Boyer and J. S. Moore, Eds.New York: Academic, 1981, pp. 215- 273.
[12] Z. Manna and P. Wolper, "Synthesis of communicating processes from temporal logic specifications,"ACM Trans. Programm. Languag. Syst., vol. 6, no. 1, pp. 68-93, Jan. 1984.
[13] M. Ajmone Marsan, G. Balbo, and G. Conte, "A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems,"ACM Trans. Comput. Syst., vol. 2, pp. 93-122, May 1984.
[14] P. Merlin and D.J. Faber, "Recoverability of communication protocols,"IEEE Trans. Commun, vol. COM-24, no. 9, Sept. 1976.
[15] M. K. Molloy, "On the integration of delay and throughput measures in distributed processing models," Ph.D. dissertation, Dep. Comput. Sci., Univ. of California, Los Angles, 1981.
[16] Owicki, S., and L. Lamport, "Proving Liveness Properties of Concurrent Programs,"ACM Trans. Programming Languages and Systems, Vol. 4, No. 3, July 1982, pp. 455-495.
[17] J. L. Peterson, "Petri nets,"ACM Comput. Surveys, vol. 9, no. 3, pp. 223-252, Sept. 1977.
[18] W. W. Plummer, "Asynchronous arbiters,"IEEE Trans. Comput., vol. C-21, pp. 37-42, Jan. 1972.
[19] A. Pnueli, "The temporal logic of programs," inProc. 18th Symp. Foundations Computer Sci., Province, Nov. 1977, pp. 46-57.
[20] C. V. Ramamoorthy and G. S. Ho, "Performance evaluation of asynchronous concurrent systems using Petri nets,"IEEE Trans. Software Eng., vol. SE-6, pp. 440-449, Sept. 1980.
[21] C. Ramchandani, "Analysis of asynchronous concurrent systems by timed Petri nets," Massachusetts Inst. Technol., Project MAC, Tech. Rep. 120, Feb. 1974.
[22] N. Rescher and A. Urquart,Temporal Logic. New York: Springer-Verlag, 1971.
[23] R. L. Schwarts and P. M. Melliar-Smith, "Temporal logic specification of distributed systems," inProc. Conf. Distribut. Syst., Apr. 1981, pp. 446-454.
[24] I. Suzuki, "Fundemental properties and application of temporal Petri nets," inProc. 9th Annu. Conf. Inform. Sci. Syst., Johns Hopkins Univ., Baltimore, MD, Mar. 1985, pp. 641-646.
[25] I. Suzuki, Y. Motohashi, K. Taniguchi, T. Kasami, and T. Okamoto, "Specification and verification of decentralized daisy chain arbiters withω-extended regular expressions,"Theoret. Comput. Sci., vol. 43, pp. 277-291, 1986.
[26] R. Valk, "Infinite behavior of Petri nets,"Theoret. Comput. Sci., vol. 25, pp. 311-341, 1983.
[27] W. M. Zuberek, "Timed Petri nets and preliminary performance evaluation," inProc. 7th Annu. Symp. Computer Architecture, May 6-8, 1980, pp. 88-96.

Index Terms:
causal relationships; Temporal Petri nets; modeling; analysis; handshake daisy chain arbiter; timing constraints; temporal logic operations; temporal assertions; temporal relationships; eventuality; fairness; formal logic; Petri nets.
Citation:
I. Suzuki, H. Lu, "Temporal Petri Nets and Their Application to Modeling and Analysis of a Handshake Daisy Chain Arbiter," IEEE Transactions on Computers, vol. 38, no. 5, pp. 696-704, May 1989, doi:10.1109/12.24271
Usage of this product signifies your acceptance of the Terms of Use.