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

Volume

59

Issue

8

fYear

2014

fDate

Aug. 2014

Firstpage

2176

Lastpage

2181

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;

fLanguage

English

Journal_Title

Automatic Control, IEEE Transactions on

Publisher

ieee

ISSN

0018-9286

Type

jour

DOI

10.1109/TAC.2014.2298985

Filename

6705633