Show simple item record

dc.contributor.authorGermanos, Vasileiosen
dc.contributor.authorHaar, Stefanen
dc.contributor.authorKhomenko, Victoren
dc.contributor.authorSchwoon, Stefanen
dc.date.accessioned2019-01-03T10:17:36Z
dc.date.available2019-01-03T10:17:36Z
dc.date.issued2015-12-08
dc.identifier.citationGermanos, V., Haar, S., Khomenko, V. and Schwoon, S. (2015) Diagnosability under Weak Fairness. In special issue on best papers from IEEE International Conference on Application of Concurrency to System Design, ACM Journal of Transactions on Embedded Computing Systems, 14 (4), Article 69en
dc.identifier.issn1539-9087
dc.identifier.urihttp://hdl.handle.net/2086/17389
dc.description.abstractIn 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.en
dc.language.isoenen
dc.publisherACMen
dc.subjectDiagnosabilityen
dc.subjectweak fairnessen
dc.subjectmodel checkingen
dc.subjectLTL-Xen
dc.subjectformal verificationen
dc.subjectPetri netsen
dc.titleDiagnosability Under Weak Fairnessen
dc.typeArticleen
dc.identifier.doihttps://dx.doi.org/10.1145/2832910
dc.peerreviewedYesen
dc.funderN/Aen
dc.projectidN/Aen
dc.cclicenceN/Aen
dc.date.acceptance2015-05-10en
dc.researchinstituteCyber Technology Institute (CTI)en


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record