A Boolean approach to the state machine decomposition of Petri nets with OBDD´s

Proposes the combination of Boolean reasoning and binary decision diagrams (BDD) algorithms to represent and manipulate, in a symbolic way, structural objects of a P/T net (like P-subnets, traps, siphons, etc.). The authors propose a systematic method to compute the Boolean functions representing some structural objects. This method is based on the classical concept of characteristic functions of sets and k-ary relations. The authors apply the method to the computation of the P-components of a P/T net, but with minor changes can be extended to many other structural objects. An algorithm to compute all minimal coverings corresponding to two statements of the state-machine decomposability problem in P/T nets is presented. Finally, an application example from the field of asynchronous circuit design is shown