
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Jianan Li, I. Suzuki, M. Yamashita, "A New Structural Induction Theorem for Rings of Temporal Petri Nets," IEEE Transactions on Software Engineering, vol. 20, no. 2, pp. 115126, February, 1994.  
BibTex  x  
@article{ 10.1109/32.265633, author = {Jianan Li and I. Suzuki and M. Yamashita}, title = {A New Structural Induction Theorem for Rings of Temporal Petri Nets}, journal ={IEEE Transactions on Software Engineering}, volume = {20}, number = {2}, issn = {00985589}, year = {1994}, pages = {115126}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.265633}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  A New Structural Induction Theorem for Rings of Temporal Petri Nets IS  2 SN  00985589 SP115 EP126 EPD  115126 A1  Jianan Li, A1  I. Suzuki, A1  M. Yamashita, PY  1994 KW  Petri nets; temporal logic; temporal reasoning; formal verification; structural induction theorem; rings; temporal Petri nets; identical components; temporal logic formula; similar behavior; demanddriven token circulation; correctness; formal verification VL  20 JA  IEEE Transactions on Software Engineering ER   
Presents a new structural induction theorem for rings consisting of identical components that are modeled using a Petri net and a temporal logic formula. The theorem gives a condition in terms of the behavior of the rings of sizes k/spl minus/1 and k, k/spl ges/5, under which all rings of size k/spl minus/1 or greater exhibit "similar" behavior. Using the example of demanddriven token circulation, we show how the theorem can be applied to formally infer the correctness of a ring of any large size from that of a ring having fewer components.
[1] K. R. Apt and D. C. Kozen, "Limits for automatic verification of finitestate concurrent systems,"Information Processing Lett., vol. 15, pp. 307309, May 1986.
[2] L. A. Cherkasova and V. E. Kotov, "The undecidability of propositional temporal logic for Petri nets,"Comput. Artificial Intell., vol. 6, no. 2, 1987.
[3] E. Clarke, O. Grümberg, and M. C. Browne, "Reasoning about networks with many identical finitestate processes," inProc. Fifth Annu. ACM Symp. Principles of Distributed Computing, Aug. 1986, pp. 240248.
[4] K. Wilken, "Optimal signature placement for processorerror detection using signature monitoring," inProc. 21st FTCS, 1991, pp. 326333.
[5] S. Graf and B. Steffen, "Compositional minimization of finite state systems," Proc. 2nd Int. Conf. ComputerAided Verification, E. M. Clarke and R. P. Kurshan, Eds.,Lecture Notes in Computer Science 531. New York: SpringerVerlag, 1991, pp. 186196.
[6] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[7] R. R. Howell and L. E. Rosier, "Problems concerning fairness and temporal logic for conflictfree Petri nets,"Theoretical Comput. Sci., vol. 64, pp. 305329, 1989.
[8] R. R. Howell, L. E. Rosier, and H. C. Yen, "A taxonomy of fairness and temporal logic problem for Petri nets,"Theoretical Comput. Sci., vol. 82, pp. 341372, 1991.
[9] R. P. Kurshan and K. McMillan, "A structural induction theorem for processes,"Proc. 8th ACM Symp. Principles of Distrib. Computing, Edmonton, AB, Canada, 1989, pp. 239247.
[10] J. Li, I. Suzuki, and M. Yamashita, "Temporal Petri nets and structural induction for rings of processes," inProc. 35th Midwest Symp. Circuits Syst., Washington, DC, 1992, pp. 377380. The final version of this paper will appear inTheoretical Comput. Sci..
[11] H. Lu and I. Suzuki, "Application of temporal Petri nets to verification of handshake daisy chain arbiters," inProc. 29th Midwest Symp. Circuits Syst., Lincoln, NE, 1987, pp. 823826.
[12] E. Madelaine and D. Vergamini, "AUTO: A verification tool for distributed systems using reduction of finite automata networks," inFormal Description Techniques II, S. T. Vuong, Ed. NorthHolland, 1990, pp. 6166.
[13] Z. Manna and A. Pnueli, "Verification of concurrent programs: the temporal framework," inThe Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds., International Lecture Series in Computer Science. New York: Academic Press, 1981, pp. 215273.
[14] Z. Manna and P. Wolper, "Synthesis of communicating processes from temporal logic specifications,"ACM Trans. Programm. Languag. Syst., vol. 6, no. 1, pp. 6893, Jan. 1984.
[15] A. Martin, "Distributed Mutual Exclusion on a Ring of Processes,"Science of Computer Programming, Vol. 5, 1985, pp. 265276.
[16] R. Milner,Communication and Concurrency. Englewood Cliffs, NJ: PrenticeHall International, 1989.
[17] T. Murata, "Petri nets: Properties, analysis, and applications,"Proc. IEEE, vol. 77, no. 4, pp. 541580, Apr. 1989.
[18] D. Park, "Concurrency and automata on infinite sequences," inProc. 5th GIConf. Theoretical Comput. Sci., Lecture Notes in Computer Science 104. New York: SpringerVerlag, 1981, pp. 167183.
[19] W. W. Plummer, "Asynchronous arbiters,"IEEE Trans. Comput., vol. C21, pp. 3742, Jan. 1972.
[20] A. Pnueli, "The temporal logic of programs,"Proc. 18th Symp. on Foundations of Computer Science, Province, Nov. 1977, pp. 4657.
[21] I. Suzuki, "Fundamental properties and applications of temporal Petri nets," inProc. 9th Ann. Conf. Information Sci. Syst., Johns Hopkins University, Baltimore, MD, 1985, pp. 641646.
[22] I. Suzuki, "Proving properties of a ring of finite state machines,"Information Processing Lett., vol. 28, pp. 213214, 1988.
[23] I. Suzuki, "Formal analysis of the alternating bit protocol by temporal Petri nets,"IEEE Trans. Software Eng., vol. 16, pp. 12731281, Nov. 1990.
[24] I. Suzuki and H. Lu, "Temporal Petri nets and their application to modeling and analysis of a handshake daisy chain arbiter,"IEEE Trans. Comput., vol. 38, pp. 696704, 1989.
[25] N. Uchihira and S. Honiden, "Verification and synthesis of concurrent programs using Petri nets and temporal logic,"Trans. IEICE, vol. E73, pp. 20012010, 1990.
[26] A. Valmari and M. Tienari, "An improved failure equivalence for finitestate systems with a reduction algorithm," inProtocol Specification, Testing, and Verification XI, B. Jonson, J. Parrow, and B. Pehrson, Eds. Amsterdam: NorthHolland, 1991, pp. 318.
[27] P. Wolper and V. Lovinfosse, "Verifying properties of large sets of processes with network invariants," inAutomatic Verification Methods for Finite State Systems, J. Sifakis, Ed., Lecture Notes in Computer Science 407. New York: SpringerVerlag, 1990, pp. 6880.