A novel method to solve the state encoding problem in Signal Transition Graphs is presented. It is based on the structural theory of Petri nets and can be applied to large specifications with hundreds of signals. This new method opens the door to incorporate logic synthesis in the design flow of large control circuits obtained from high-level specifications. The experimental results validate the quality of the encoded circuits and show the significant improvements that can be obtained by the synthesis of large controllers. Categories and Subject Descriptors: B.6.3 [Hardware]: Logic Design - Design Aids; J.6 [Computer Applications]: Computer-aided engineering. General Terms: Algorithms, Design.