Toward Proving the Extension of Johnson’s Rule to a Three-Machine Flow Shop Scheduling Problem

Manufacturing companies can achieve their goals of reducing production costs and improving productivity by using an efficient production schedule. In this paper, a formal verification procedure, supported by relevant arguments, has been used to verify the accuracy of flow-shop scheduling behaviour and to reduce total production time. We focus on the algorithm of sequence generation (Johnson’s algorithm), as well as model a three-machine scheduling procedure as a finite-state machine (FSM). The correctness requirements are expressed in Computational Tree Logic (CTL) and Linear-Time Logic (LTL) and are proved by the NuSMV model checker. The associated technique enables automated scheduling of property proofs during the design phase. In our verification, a counterexample demonstrates that Johnson’s rule can yield a suboptimal makespan in a three-machine setting, thereby revealing a limitation of its generalisation. The current findings indicate that using a model checker in CTL/LTL can be an effective method for establishing the logical validity of flow-shop scheduling and failure scenarios, thereby informing future heuristic development.