对标记Petri网的可检测性进行判定
Deciding Detectability for Labeled Petri Nets
AI总结：
本文研究了由标记Petri网建模的离散事件系统中强可检测性和弱可检测性的验证问题，证明强可检测性是可判定的而弱可检测性是不可判定的，扩展了现有研究从有限状态自动机到标记Petri网的可检测性验证。
摘要：
离散事件系统（DESs）的可检测性是一种属性，用于确定基于观察是否可以提前确定当前及后续状态。本文研究了由标记Petri网建模的DESs的两种可检测性属性——强可检测性和弱可检测性的验证。强可检测性要求在有限次观察后能够确定系统的当前及后续标记，而弱可检测性要求在有限次观察后能够确定某些轨迹的当前及后续标记。我们证明对于由标记Petri网建模的DESs，检查强可检测性是可判定的，而检查弱可检测性是不可判定的。我们的结果将现有研究从有限状态自动机扩展到标记Petri网。作为结果，我们加强了对标记Petri网当前状态隐蔽性的检查结果。
英文摘要：
Detectability of discrete event systems (DESs) is a property to determine a priori whether the current and subsequent states can be determined based on observations. In this paper, we investigate the verification of two detectability properties -- strong detectability and weak detectability -- for DESs modeled by labeled Petri nets. Strong detectability requires that we can always determine, after a finite number of observations, the current and subsequent markings of the system, while weak detectability requires that we can determine, after a finite number of observations, the current and subsequent markings for some trajectories of the system. We show that for DESs modeled by labeled Petri nets, checking strong detectability is decidable whereas checking weak detectability is undecidable. Our results extend the existing studies on the verification of detectability from finite-state automata to labeled Petri nets. As a consequence, we strengthen a result on checking current-state opacity for labeled Petri nets.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
