Pena, Patricia N.Bravo, H. J.da Cunha, A. E. C.Malik, RobiLafortune, S.Cury, José E. R.2015-06-0920142015-06-092014Pena, P. N., Bravo, H. J., da Cunha, A. E. C., Malik, R., Lafortune, S., & Cury, J. E. R. (2014). Verification of the observer property in discrete event systems. IEEE Transactions on Automatic Control, 59(8), 2176–2181. http://doi.org/10.1109/TAC.2014.22989850018-9286https://hdl.handle.net/10289/9360The 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.application/pdfenThis is an author’s accepted version of an article published in the journal: IEEE Transactions on Automatic Control. © 2014 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to severs or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.discrete event systemsnatural projectionsobserver propertyJournal Article10.1109/TAC.2014.2298985