In: IEICE Trans. on Fundamentals in Electronics, Communications and Computer Sciences, Vol. E82-A, No. 8, pages 1648-1655. 1999.
Abstract: A Petri net is a graphical and mathematical modeling tool for discrete-event systems. This paper treats analysis problems of time Petri nets. In this model, minimal and maximal firing delays are assigned to each transition. If a transition is enabled, it can fire after minimal delay has passed and must fire before maximal delay has elapsed. Since a time Petri net can simulate register machines, it has an equivalent modeling power to that of the Turing machine. It means, however, that most of the analysis problems for time petri nets with general net structure are undecidable. In this paper, net structures are restricted to a subclass called partially ordered condition (POC) nets and dissynchronous-choice (DC) nets. Firing delays are also restricted to satisfy the `static fair condition' which assures the chance to fire for all transitions enabled simultaneously. First, a sufficient condition of liveness of a time DC net with the static far condition is derived. Then it is shown that liveness of a time DC net with the static fair condition is equivalent to liveness of the underlying nontime net. This means that the liveness problem of this class is decidable. Lastly, the liveness property of the extended free-choice (EFC) net is shown to be decidable.
Keywords: DC nets, POC nets, decidable problems, dissynchronous-choice nets, liveness property, partially ordered condition nets, static fair condition, time Petri nets.