Petri nets and linear logic for process oriented diagnosis

The first part of the paper shows how linear logic permits a characterization of sequences or sets of sequences which is more accurate than the usual Petri net one. Its backward reasoning ability is used for diagnosis purpose. Considered nets are ordinary ones including cycles and synchronizations: they model the physical device in terms of resources which are produced and consumed. A short example illustrates how a set of hypotheses can be derived from an event observation and a linear logic representation of the Petri net based model