A new technique for the logic synthesis of asynchronous circuits is presented. It is based on the structural theory of Petri nets and integer linear programming. The technique is capable of checking implementability conditions, such as, complete state coding, and deriving a gate netlist to implement the specified behavior. This technique can synthesize specifications with few thousands of transitions in the Petri net, providing a speed-up of several orders of magnitude with regard to other existing techniques.