On the analysis of safety specifications using LTL for a class of discrete event controllers applied to manufacturing systems

A model checking procedure, based on the recently introduced linear temporal logic LTL^[e] framework, is proposed for the analysis of a class of safety specifications for the synthesis of discrete-event supervisory controllers. A restricted syntax is proposed for capturing specifications which, in our experience, are common in the design of control systems for manufacturing processes. Semantic models for finite trajectories are constructed as labelled finite state machines (LFSM) based on the open-loop behaviour of the particular system under analysis. Logic consistency of the specification set is verified by model checking each LTL^[e] formula against the LFSM semantic models of the rest of the specifications. The approach, although computationally intensive in the use of linear complexity algorithms, guarantees the logic correctness of the monolithic specification before executing the synthesis calculations that are of quadratic complexity. The advantages of the proposed approach are illustrated with the analysis of a specification set employed in the synthesis of a supervisor module for a manufacturing system.