Title :
Verification of the Observer Property in Discrete Event Systems
Author :
Pena, Patricia N. ; Bravo, Hugo J. ; da Cunha, Antonio E. C. ; Malik, Rohit ; Lafortune, Stephane ; Cury, Jose E. R.
Author_Institution :
Dept. de Eng. Eletron., Univ. Fed. de Minas Gerais, Belo Horizonte, Brazil
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.
Keywords :
discrete event systems; observers; DES models; OP-verifier; abstractions; discrete event system; natural projection; nondeterministic automata; nonrelevant events; observer property; quadratic complexity; Automata; Complexity theory; Context; Discrete-event systems; Observers; Supervisory control; Testing; Discrete event systems; natural projections; observer property;
Journal_Title :
Automatic Control, IEEE Transactions on
DOI :
10.1109/TAC.2014.2298985
