A new approach to modular liveness analysis conceived for large logic controllers' design

When dealing with complex automation systems, the development and maintenance of control software often is a delicate task and takes a long time. The paper illustrates a Petri nets-based model to design logic controllers in an incremental mode, in which liveness analysis can be easily carried out, based on the compressed information contained in a compact graph that can be associated to the Petri net. Moreover, the incremental liveness analysis allows the portion of a net specifically involved in a fault to be identified and suggests a number of possible, even complex, remedies according to the nature of the detected faults. A necessary and sufficient condition of liveness is stated and proved.>