A generalized state assignment theory for transformations on signal transition graphs

A constraint satisfaction framework is proposed that can guarantee necessary and sufficient conditions for a state graph assignment to result in a transformed state graph that is race-free. Performing transformations at the state graph level has the advantage that the requirements imposed on the initial signal transition graph (STG) are very weak. Unlike previous methods, the initial STG need not be a live, safe, free choice net. The only requirement is that the corresponding initial state graph should be finite and connected, and have a consistent state assignment. Hence, a very broad range of STGs can be synthesized. The transformation achievable using the proposed framework correspond to very complex transformations on STGs. Even transformations that convert a free choice net into a correct non-free choice net, and a 1-safe net into a correct 2-safe net are feasible. Addition of transitions that do not follow the Petri net firing rule is also possible.<>