Decomposition in asynchronous circuit design

Signal Transition Graphs (STGs) are a version of Petri nets for the specification of asynchronous circuit behaviour. It has been suggested to decompose such a specification as a first step; this leads to a modular implementation, which is often more efficient, and it can support circuit synthesis by possibly avoiding state explosion or allowing the use of library elements. We present a decomposition algorithm and formally prove it correct, where an interesting aspect is the use of a bisimulation with angelic nondeterminism. In contrast to similar approaches in the literature, our algorithm is very generally applicable. We show that transition contraction -- the main operation in the algorithm -- can be applied with fewer restrictions than known so far. We also prove that deletion of redundant places can be used in the algorithm, which turns out to be very useful in examples