关于带标签 Petri 网与有限自动机的可检测性

我们研究带标签 Petri 网与有限自动机的可检测性性质。我们首先研究弱近似可检测性（WAD），其含义为系统存在一条无限观测输出序列，使得该输出序列每个长度大于给定值的前缀都允许观测者确定当前状态是否属于给定集合。我们还考虑两个新概念：瞬时强可检测性（ISD）与最终强可检测性（ESD）。前者含义为对每条可能的无限观测输出序列，其每个前缀都允许重构当前状态。后者含义为对每条可能的无限观测输出序列，存在某个值使得长度大于该值的每个前缀都允许重构当前状态。结果：WAD：对带标签 Petri 网不可判定，对有限自动机为 PSPACE-完全；ISD：对带标签 Petri 网可判定且 EXPSPACE-困难，对有限自动机属于 P；ESD：在及时性假设下对带标签 Petri 网可判定且 EXPSPACE-困难，对有限自动机属于 P；SD：对有限自动机属于 P，在死锁自由与及时性两个假设下强化了 Shu 与 Lin 2011 年的结果；对带标签 Petri 网与有限自动机均有 ISD<SD<ESD<WD<WAD。