Symbolic analysis of bounded Petri nets

This work presents a symbolic approach for the analysis of bounded Petri ne ts. The structure and behavior of the Petri net is symbolically modeled by using Boolean functions, thus reducing reasoning about Petri nets to Boolea n calculation. The set of reachable markings is calculated by symbolically firing the transitions in the Petri net. Highly concurrent systems suffer f rom the state explosion problem produced by an exponential increase of the number of reachable states. This state explosion is handled by using Binary Decision Diagrams (BDDs) which are capable of representing large sets of m arkings with small data structures. Petri nets have the ability to model a large variety of systems and the flexibility to describe causality, concurr ency, and conditional relations. The manipulation of vast state spaces gene rated by Petri nets enables the efficient analysis of a wide range of probl ems, e.g., deadlock freeness, liveness, and concurrency. A number of exampl es are presented in order to show how large reachability sets can be genera ted, represented, and analyzed with moderate BDD sizes. By using this symbo lic framework, properties requiring an exhaustive analysis of the reachabil ity graph can be efficiently verified.