Verification of the Observer Property in Discrete Event Systems
Verification of the Observer Property in Discrete Event Systems
复制标题
离散事件系统中观察者性质的验证
DOI：
--
复制
发表时间：
2014
影响因子：
6.8
通讯作者：
J. Cury
中科院分区：
文献类型：
--
作者：
P. Pena;Hugo J. Bravo;A. E. C. D. Cunha;R. Malik;S. Lafortune;J. Cury
观测器性质是离散事件系统（DES）模型抽象必须满足的一个重要条件。本技术说明提出了一种新的算法，该算法测试通过自然投影获得的DES抽象是否具有观察者属性。该程序，称为OP-验证器，可以应用于（潜在的非确定性）自动机，没有限制的存在周期的“不相关”的事件。这个过程在状态的数量上具有二次复杂性。通过一组实验说明了该算法的性能。
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.