In: Trans. Inst. Electron. Inf. Commun. Eng. A (Japan), Vol. J71A, No. 8, pages 1563-1568. 1988. In Japanese.
Abstract: The paper discusses a method for stepwise refinement of Petri nets, which is a very useful method for design of large scale Petri nets. By introducing three conditions, that is, well-behaved, transformable, and matching conditions, this paper proves sufficient conditions for preserving properties such as boundedness and liveness when nets are refined.