Efficient Computation of Observer Projections using OP-Verifiers1

This paper proposes a procedure to compute abstractions of Discrete Event System (DES) models with the observer property (OP). The procedure, named OP-Search, is based on the OP-Verifier algorithm which verifies if a given natural projection has the observer property. In case OP fails for a projection in σr of an automaton M, OP-Search modifies M by relabelling transitions and incorporating the new events in σr, in a way that the modified natural projection generates OP-abstractions. Although OP-Search does not guarantee minimal abstracted models, it leads in general to very reasonable solutions and is shown to be of lower time complexity compared to previous work in the literature.