In: Fifth International Conference on Application of Concurrency to System Design (ACSD'05), pages 244-253. 2005. http://doi.ieeecomputersociety.org/10.1109/ACSD.2005.21.
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. In a previous paper, the original method was extended and shown to be much more generally applicable than known before. But further extensions are necessary, and some are presented here, e.g.: to avoid dynamic autoconflicts, the previous paper insisted on avoiding structural auto-conflicts, which is too restrictive; we show how to work with the latter type of auto-conflicts. This and another simple extension makes it necessary to restructure presentation and correctness proof of the decomposition algorithm.