Verification of the observer property in discrete event systems

Pena, Patricia N.; Bravo, H. J.; da Cunha, A. E. C.; Malik, Robi; Lafortune, S.; Cury, José E. R.

doi:10.1109/TAC.2014.2298985

Files

OP_Verif_TN_2c.pdf

Accepted version, 118.9Kb

DOI

10.1109/TAC.2014.2298985

Citation

Export 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

Permanent Research Commons link: https://hdl.handle.net/10289/9360

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.

Date

2014

Type

Journal Article

Publisher

Institute of Electrical and Electronics Engineers Inc.

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.

Collections

Computing and Mathematical Sciences Papers [1455]