In: Valette, R.: Lecture Notes in Computer Science, Vol. 815; Application and Theory of Petri Nets 1994, Proceedings 15th International Conference, Zaragoza, Spain, pages 531-547. Springer-Verlag, 1994.
Abstract: A compositional verfication method for Petri nets composed of place-bordered subnets is presented. The method assumes that the Petri net can be divided into an interesting and an environment component, and it facilitates the verification of all properties which can be stated in terms of the projections of the execution s of the net onto its interesting component. For instance, one can checkw hat is the lowest upper bound of the markin g of any place in the interesting component, or whether some transition of the interesting component may ever occur. Also deadlocks and a certain class of livelocks can be detected. The method is based on the process-algebraic compositional approach, but is novel in that it can be used to produce state-oriented information, and it works in a framwork with asynchronous communication. In the example used for demonstrating the method, an in finite number of systems of different size is analysed with a small finite amount of effort