Loading...
Verification of the observer property in discrete event systems
Verification of the observer property in discrete event systems
Abstract
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.
Type
Journal Article
Type of thesis
Series
Citation
Pena, 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.2298985
Date
2014
Publisher
Institute of Electrical and Electronics Engineers Inc.
Degree
Supervisors
Rights
This 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.