In: Journal Inform. Process. Cybern., EIK (formerly: Elektron. Inform. verarb. Kybern.), Vol. 27, No. 4, pages 227-244. 1991.
Abstract: This paper shows how to study boundedness and liveness of a finte Time Petri net in a discrete way by using its reachability graph. The computation of the reachability graph defined here is a recursive-enumerable process. The decidability of the reachability for an arbitrary state in a finite and bounded Time Petri net is shown.
Keywords: finite time net; boundedness; liveness; reachability graph computation; reachability decidability.