...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>IEEE Transactions on Automatic Control >Control of nondeterministic discrete-event systems for bisimulation equivalence
【24h】

Control of nondeterministic discrete-event systems for bisimulation equivalence

机译：非确定性离散事件系统的双仿真对等控制

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Most prior work on supervisory control of discrete event systems is for achieving deterministic specifications, expressed as formal languages. In this paper we study supervisory control for achieving nondeterministic specifications. Such specifications are useful when designing a system at a higher level of abstraction so that lower level details of system and its specification are omitted to obtain higher level models that may be nondeterministic. Nondeterministic specifications are also meaningful when the system to be controlled has a nondeterministic model due to the lack of information (caused for example by partial observation or unmodeled dynamics). Language equivalence is not an adequate notion of behavioral equivalence for nondeterministic systems, and instead we use the finest known notion of equivalence, namely the bisimulation equivalence. Choice of bisimulation equivalence is also supported by the fact that bisimulation equivalence specification is equivalent to a specification in the temporal logic of μ-calculus that subsumes the complete branching-time logic CTL*. Given nondeterministic models of system and its specification, we study the design of a supervisor (possibly nondeterministic) such that the controlled system is bisimilar to the specification. We obtain a small model theorem showing that a supervisor exists if and only if it exists over a certain finite state space, namely the power set of Cartesian product of system and specification state spaces. Also, the notion of state-controllability is introduced as part of a necessary and sufficient condition for the existence of a supervisor. In the special case of deterministic systems, we provide an existence condition that can be verified polynomially in both system and specification states, when the existence condition holds.
机译：在离散事件系统的监督控制方面，大多数先前的工作是实现确定性规范，以形式语言表示。在本文中，我们研究了用于实现不确定性规范的监督控制。当在较高抽象级别设计系统时，此类规范很有用，因此可以省略较低级别的系统详细信息及其规范，以获得可能不确定的较高级别的模型。当要控制的系统由于缺乏信息（例如，由于部分观察或未建模的动力学导致）而具有不确定性模型时，不确定性规范也很有意义。对于非确定性系统，语言对等不是行为对等的充分概念，而是我们使用已知的对等最精细的概念，即双仿真对等。双模拟等效项的选择也受以下事实的支持：双模拟等效项规范等同于μ演算的时态逻辑中包含完整分支时间逻辑CTL *的规范。给定系统及其规范的不确定性模型，我们研究监督者的设计（可能不确定），以使受控系统与规范双相似。我们得到一个小模型定理，表明当且仅当监督者存在于某个有限状态空间（即系统和规范状态空间的笛卡尔积的幂集）上时，监督者才存在。同样，引入状态可控性的概念作为存在监督者的必要和充分条件的一部分。在确定性系统的特殊情况下，当存在条件成立时，我们提供可以在系统状态和规范状态下进行多项式验证的存在条件。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号