• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>IFAC PapersOnLine >Diagnosability Analysis of Input/Output Discrete-Event Systems Using Model-Checking
【24h】

Diagnosability Analysis of Input/Output Discrete-Event Systems Using Model-Checking

机译：使用模型检查的输入/输出离散事件系统的可诊断性分析

获取原文
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

This paper deals with analysis of diagnosability andK-diagnosability of dynamic systems in a model-checking framework. Dynamic systems are abstracted here as Discrete-Event Systems (DESs) and modeled by Input/Output Transition Systems (IOTSs). We reformulate diagnosability issues using CTL formula while considering extended definitions of diagnosability. Moreover, we introduce a formal definition ofK-diagnosability in model-checking framework and we discuss the problem ofKmin-diagnosability (the minimal value ofKensuring diagnosability). We also show how diagnosability analysis in model-checking framework can be extended in order to deal with repeated/intermittent failures. In this regard, the case of [1-∞]-diagnosability analysis is investigated. Finally, some of these theoretical contributions are illustrated through a benchmark.
机译：本文在模型检查框架中分析动态系统的可诊断性和K可诊断性。动态系统在这里抽象为离散事件系统（DES），并由输入/输出转换系统（IOTS）建模。在考虑扩展的可诊断性定义的同时，我们使用CTL公式重新定义了可诊断性问题。此外，我们在模型检查框架中引入了K可诊断性的正式定义，并讨论了Kmin可诊断性（Kensuring可诊断性的最小值）的问题。我们还展示了如何扩展模型检查框架中的可诊断性分析，以应对重复/间歇性故障。在这方面，研究了[1-∞]可诊断性分析的情况。最后，通过基准说明了其中一些理论贡献。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号