Germanos, Vasileios and Haar, Stefan and Khomenko, Victor and Schwoon, Stefan (2014) Diagnosability under Weak Fairness. In: 2014 14th International Conference on Application of Concurrency to System Design, 23-27 June 2014, Tunis La Marsa.
Preview |
Text
paper.pdf Download (749kB) | Preview |
Abstract
In partially observed Petri nets, diagnosis is the
task of detecting whether or not 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 paper 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.
| Item Type: | Conference or Workshop Item (Paper) |
|---|---|
| Additional Information and Comments: | "(c) 2014 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other users, including reprinting/ republishing this material for advertising or promotional purposes, creating new collective works for resale or redistribution to servers or lists, or reuse of any copyrighted components of this work in other works." DOI: 10.1109/ACSD.2014.9 |
| Faculty / Department: | Faculty of Human and Digital Sciences > Mathematics and Computer Science |
| Depositing User: | Vasileios Germanos |
| Date Deposited: | 19 May 2016 11:39 |
| Last Modified: | 12 Sep 2016 10:27 |
| URI: | https://hira.hope.ac.uk/id/eprint/1337 |
Actions (login required)
 |
View Item |
Altmetric
Altmetric
