Abstract: The design method of specifications of the control description for sequential manufacturing systems is presented. The Petri net semantics of the specifications is discussed. The design algorithm has been developed for the initial markings such that the Petri net controlleer has the properties such as liverness, boundedness or safeness, and reversibility. Using the Petri net controller with the desired properties, the real-time control for a practical manufacturing system can be brought into force.