Petri net analysis using boolean manipulation
Document typePart of book or chapter of book
Rights accessOpen Access
All rights reserved. This work is protected by the corresponding intellectual and industrial property rights. Without prejudice to any existing legal exemptions, reproduction, distribution, public communication or transformation of this work are prohibited without permission of the copyright holder
This paper presents a novel analysis approach for bounded Petri nets. The net behavior is modeled by boolean functions, thus reducing reasoning about Petri nets to boolean calculation. The state explosion problem is managed by using Binary Decision Diagrams (BDDs), which are capable to represent large sets of markings in small data structures. The ability of Petri nets to model systems, the flexibility and generality of boolean algebras, and the efficient implementation of BDDs, provide a general environment to handle a large variety of problems. Examples are presented that show how all the reachable states (1018) of a Petri net can be efficiently calculated and represented with a small BDD (103 nodes). Properties requiring an exhaustive analysis of the state space can be verified in polynomial time in the size of the BDD.
CitationPastor, E. [et al.]. Petri net analysis using boolean manipulation. A: "Application and Theory of Petri Nets 1994, 15th International Conference: Zaragoza, Spain, June 20–24, 1994: proceedings". Berlín: Springer, 1994, p. 416-435.