期刊
ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS
卷 14, 期 4, 页码 -出版社
ASSOC COMPUTING MACHINERY
DOI: 10.1145/2832910
关键词
Reliability; Verification; Diagnosability; weak fairness; model checking; LTL-X; formal verification; Petri nets
资金
- EPSRC [EP/K001698/1, EP/L025507/1]
- project IMPRO [ANR-2010-BLAN-0317]
- EPSRC [EP/K001698/1, EP/L025507/1] Funding Source: UKRI
- Engineering and Physical Sciences Research Council [1104595, EP/L025507/1, EP/K001698/1] Funding Source: researchfish
In partially observed Petri nets, diagnosis is the task of detecting whether the given sequence of observed labels indicates that some unobservable fault has occurred. Diagnosability is an associated property of the Petri net, stating that in any possible execution, an occurrence of a fault can eventually be diagnosed. In this article, we consider diagnosability under the weak fairness (WF) assumption, which intuitively states that no transition from a given set can stay enabled forever it must eventually either fire or be disabled. We show that a previous approach to WF-diagnosability in the literature has a major flaw and present a corrected notion. Moreover, we present an efficient method for verifying WF-diagnosability based on a reduction to LTL-X model checking. An important advantage of this method is that the LTL-X formula is fixed-in particular, the WF assumption does not have to be expressed as a part of it (which would make the formula length proportional to the size of the specification), but rather the ability of existing model checkers to handle weak fairness directly is exploited.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据