In: Concurrency and Hardware Design, pages 152-190. Advances in Petri Nets, Volume 2549 of Lecture Notes in Computer Science / J. Cortadella, A. Yakovlev, G. Rozenberg (Eds.) --- Springer Verlag, November 2002.
Also in: FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science, Proceedings of the 22nd Conference, Kanpur, India, December 12-14, 2002, pages 336-347. Volume 2556 of Lecture Notes in Computer Science / M. Agrawal, A. Seth (Eds.) --- Springer Verlag, December 2002.
Abstract: 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 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.