Polynomial-time verification for bisimilarity control of partially observed nondeterministic discrete event systems with deterministic specifications

Polynomial-time verification for bisimilarity control of partially observed nondeterministic discrete event systems with deterministic specifications
复制标题

具有确定性规范的部分观测的非确定性离散事件系统的双相似性控制的多项式时间验证

DOI:
10.1016/j.automatica.2023.110940
复制
发表时间:
2023
期刊:
影响因子:
6.4
通讯作者:
Shigemasa Takai
Shigemasa Takai
中科院分区:
计算机科学2区
文献类型:
--
作者:
吉岡 璃皇;浦川 禎之;Shigemasa Takai

文献摘要

相似文献

研究了部分可观测非确定离散事件系统的双相似控制问题。它要求我们合成一个在部分观测下工作的监督器,使得监督系统与规范是双相似的。验证已知的必要和充分条件存在这样一个监督的计算复杂度是指数的系统和规范的状态数。我们表明,在一个特殊的情况下,规格是确定性的,存在的监督,解决了双相似性控制问题的多项式验证。
We consider a bisimilarity control problem for partially observed nondeterministic discrete event systems. It requires us to synthesize a supervisor that works under partial observation so that the supervised system is bisimilar to the specification. The computational complexity of verifying the known necessary and sufficient condition for the existence of such a supervisor is exponential in the numbers of states of the system and the specification. We show that, in a special case where the specification is deterministic, the existence of a supervisor that solves the bisimilarity control problem is polynomially verified.