Diagnosability Under Weak Fairness

Date

2014-06

Advisors

Journal Title

Journal ISSN

ISSN

1550-4808

DOI

Volume Title

Publisher

IEEE

Type

Conference

Peer reviewed

Yes

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.

Description

Keywords

Diagnosability, weak fairness, model checking, LTL-X, formal verification, Petri nets

Citation

Germanos, V., Haar, S., Khomenko, V. and Schwoon S. (2014) Diagnosability under weak fairness. 15th IEEE International Conference on Application of Concurrency to System Design, June 2014

Rights

Research Institute

Cyber Technology Institute (CTI)