Modelling of discrete manufacturing systems having multiple jobs for verification by Model-Checking

A formal model for describing the behaviour of a discrete manufacturing system, where multiple jobs are carried out simultaneously and even overtaking of subtasks of different jobs may occur, and besides, that contains both External-Events and Internal-Events having no difference in the rate of incidence among them, was proposed. And besides, taking the difficulty of combinatorial explosion of the states into consideration, a procedural method for generating so called Possible-World based on the proposed model was also developed in order to apply Model-Checking-method to the verification of the system.