多智能体离散事件系统中重标记观测一致性的判定
Deciding Relabeling Observation Consistency in Multi-Agent Discrete-Event Systems
浏览论文内容
中文总结 AI 辅助
本文证明多智能体离散事件系统的重标记观测一致性（ROC）是PSPACE完全问题，给出易处理情形的多项式时间算法与充分条件，修正了文献中相关错误结论并证明ROC的组合性。
中文摘要 AI 辅助
多智能体离散事件系统的可伸缩监控器通过通用模板控制一组同构智能体。在部分观测下，若将智能体映射到其模板的重标记是重标记观测一致（ROC）的，且满足局部伴随条件，则此类监控器具有最大允许性。ROC是否可判定是一个未解决的问题。本文证明ROC是PSPACE完全的：对于具有两个可观测事件和一个不可观测事件的非确定性植物，以及具有两个可观测事件和两个不可观测事件的确定性植物。在易处理方面，本文刻画了对任意植物都能保证ROC的重标记，给出了不可观测事件上重标记为单射的确定性植物的多项式时间算法，还基于饱和和模拟给出了充分条件，两者均有多项式时间测试。本文进一步证明，对于具有两两不相交模板的组件，ROC是可组合的；若字母表也两两不相交，则等价，且这两个假设均不可省略。最后，本文证明文献中提出的保证ROC的结构条件不正确，并修复了同一命题所断言的伴随包含关系。
英文摘要
Scalable supervisors for multi-agent discrete-event systems control groups of isomorphic agents through a common template. Under partial observation, such a supervisor is maximally permissive if the relabeling that maps the agents onto their template is relabeling observation consistent (ROC) and a local companion condition holds. Whether ROC is decidable was open. We show that it is PSPACE-complete: for nondeterministic plants with two observable and one unobservable event, and for deterministic plants with two observable and two unobservable events. On the tractable side, we characterize the relabelings that guarantee ROC for every plant, we give a polynomial-time algorithm for deterministic plants whose relabeling is injective on unobservable events, and we give sufficient conditions based on saturation and on simulation, with polynomial-time tests for both. We further show that ROC is compositional for components with pairwise disjoint templates, with equivalence if the alphabets are moreover pairwise disjoint, and that neither hypothesis can be dropped. Finally, we show that the structural condition proposed in the literature to guarantee ROC is incorrect, and repair the companion inclusion that the same proposition asserts.
