A technique of state space search based on unfolding. (English) Zbl 0829.68085

McMillan, K. L.

Form. Methods Syst. Des. 6, No. 1, 45-65 (1995).

Summary: Unfolding of Petri nets provide a method of searching the state space of concurrent systems without considering all possible interleavings of concurrent events. A procedure is given for constructing the unfolding of a Petri net, terminating the construction when it is sufficient to represent all reachable markings. This procedure is applied to hazard and deadlock detection in asynchronous circuits. Examples are given of scalable systems with exponential size state spaces, but polynomial size unfoldings, including a distributed mutual exclusion ring circuit.

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68Q85	Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Keywords:

unfolding; Petri nets; searching; concurrent systems

References:

[1]	J.R. Burch, E.M. Clarke, and D.E. Long, Symbolic model checking with partitioned transition relations. In the Proceedings of VLSI’91.
[2]	J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and J. Hwang, Symbolic model checking: 1020 states and beyond. InProceedings of the Fifth Annual Symposium on Logic in Computer Science, June 1990.
[3]	E.M. Clarke and E.A. Emerson, Synthesis of synchronization skeletons for branching time temporal logic. In Dexter Kozen, editor,Logic of Programs: Workshop, volume 131 ofLecture Notes in Computer Science, Yorktown Heights, New York, May 1981. Springer-Verlag. · Zbl 0546.68014
[4]	D. Dill, Trace theory for automatic hierarchical verification of speed-independent circuits. Technical Report 88-119, Carnegie Mellon University, Computer Science Dept., 1988.
[5]	P, Godefroid, Using partial orders to improve automatic verification methods. InWorkshop on Computer Aided Verification, 1990. · Zbl 0786.68061
[6]	P. Godefroid and P. Wolper, A partial approach to model checking. InLICS, 1991. · Zbl 0806.68079
[7]	R.P. Kurshan, Testing containment of ?-regular languages. Technical Report 1121-861010-33-TM, Bell Laboratories, 1986.
[8]	A.J. Martin, The design of a self-timed circuit for distributed mutual exclusion. In Henry Fuchs, editor,1985 Chapel Hill Conference on VLSI, pp. 245-260. Computer Science Press, 1985.
[9]	M. Nielsen, G. Plotkin, and G. Winskel, Petri nets, event structures and domains, part I.Theoretical Computer Science, 13:85-108, 1981. · Zbl 0452.68067
[10]	D.K. Probst and H.F. Li, Abstract specification, composition, and proof of correctness of delay-insensitive circuits and systems. Technical Report, Concordia University, Dept. of Computer Science, 1989.
[11]	D.K. Probst and H.F. Li, Using partial order semantics to avoid the state explosion problem in asynchronous systems. InSecond Workshop on Computer Aided Verification, June 1990. Also LNCS 531, pp. 15-24. · Zbl 0800.94302
[12]	D.K. Probst and H.F. Li, Uartial order model checking: A guide for the perplexed. InThird Workshop on Computer Aided Verification, pp. 405-416, July 1991. Also LNCS 575, pp. 322-331.
[13]	C.L. Seitz, System timing. In Carver Mead and Lynn Conway, editors,Introduction to VLSI Systems, pp. 218-262. Addison-Wesley, 1980.
[14]	A. Valmari, Stubborn sets for reduced state space generation. In10th Int. Conf. on Application and Theory of Petri Nets, 1989.
[15]	A. Valmari, A stubborn attack on the state explosion problem. InWorkshop on Computer Aided Verification, 1990. · Zbl 0786.68069
[16]	Tomohiro Yoneda, Yoshihiro Tohma, and Yutaka Kondo, Acceleration of timing verification method based on time Petri Nets.Systems and Computers in Japan, 22(12):37-52, 1991.