This Article 
 Bibliographic References 
 Add to: 
A New Structural Induction Theorem for Rings of Temporal Petri Nets
February 1994 (vol. 20 no. 2)
pp. 115-126

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 demand-driven 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 finite-state concurrent systems,"Information Processing Lett., vol. 15, pp. 307-309, 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 finite-state processes," inProc. Fifth Annu. ACM Symp. Principles of Distributed Computing, Aug. 1986, pp. 240-248.
[4] K. Wilken, "Optimal signature placement for processor-error detection using signature monitoring," inProc. 21st FTCS, 1991, pp. 326-333.
[5] S. Graf and B. Steffen, "Compositional minimization of finite state systems," Proc. 2nd Int. Conf. Computer-Aided Verification, E. M. Clarke and R. P. Kurshan, Eds.,Lecture Notes in Computer Science 531. New York: Springer-Verlag, 1991, pp. 186-196.
[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 conflict-free Petri nets,"Theoretical Comput. Sci., vol. 64, pp. 305-329, 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. 341-372, 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. 239-247.
[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. 377-380. 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. 823-826.
[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. North-Holland, 1990, pp. 61-66.
[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. 215-273.
[14] 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.
[15] A. Martin, "Distributed Mutual Exclusion on a Ring of Processes,"Science of Computer Programming, Vol. 5, 1985, pp. 265-276.
[16] R. Milner,Communication and Concurrency. Englewood Cliffs, NJ: Prentice-Hall International, 1989.
[17] T. Murata, "Petri nets: Properties, analysis, and applications,"Proc. IEEE, vol. 77, no. 4, pp. 541-580, Apr. 1989.
[18] D. Park, "Concurrency and automata on infinite sequences," inProc. 5th GI-Conf. Theoretical Comput. Sci., Lecture Notes in Computer Science 104. New York: Springer-Verlag, 1981, pp. 167-183.
[19] W. W. Plummer, "Asynchronous arbiters,"IEEE Trans. Comput., vol. C-21, pp. 37-42, Jan. 1972.
[20] A. Pnueli, "The temporal logic of programs,"Proc. 18th Symp. on Foundations of Computer Science, Province, Nov. 1977, pp. 46-57.
[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. 641-646.
[22] I. Suzuki, "Proving properties of a ring of finite state machines,"Information Processing Lett., vol. 28, pp. 213-214, 1988.
[23] I. Suzuki, "Formal analysis of the alternating bit protocol by temporal Petri nets,"IEEE Trans. Software Eng., vol. 16, pp. 1273-1281, 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. 696-704, 1989.
[25] N. Uchihira and S. Honiden, "Verification and synthesis of concurrent programs using Petri nets and temporal logic,"Trans. IEICE, vol. E73, pp. 2001-2010, 1990.
[26] A. Valmari and M. Tienari, "An improved failure equivalence for finite-state systems with a reduction algorithm," inProtocol Specification, Testing, and Verification XI, B. Jonson, J. Parrow, and B. Pehrson, Eds. Amsterdam: North-Holland, 1991, pp. 3-18.
[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: Springer-Verlag, 1990, pp. 68-80.

Index Terms:
Petri nets; temporal logic; temporal reasoning; formal verification; structural induction theorem; rings; temporal Petri nets; identical components; temporal logic formula; similar behavior; demand-driven token circulation; correctness; formal verification
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. 115-126, Feb. 1994, doi:10.1109/32.265633
Usage of this product signifies your acceptance of the Terms of Use.