IEEE Transactions on Automatic Control, Vol.59, No.8, 2176-2181, 2014
Verification of the Observer Property in Discrete Event Systems
The observer property is an important condition to be satisfied by abstractions of Discrete Event System (DES) models. This technical note presents a new algorithm that tests if an abstraction of a DES obtained through natural projection has the observer property. The procedure, called OP-Verifier, can be applied to (potentially nondeterministic) automata, with no restriction on the existence of cycles of "non-relevant" events. This procedure has quadratic complexity in the number of states. The performance of the algorithm is illustrated by a set of experiments.